Fundamenta Informaticae - Volume 192, issue 3-4

Authors: Lorenz, Robert | Lasota, Sławomir

Article Type: Editorial

DOI: 10.3233/FI-242193

Citation: Fundamenta Informaticae, vol. 192, no. 3-4, pp. i-ii, 2024

Authors: Fahrenberg, Uli | Ziemiański, Krzysztof

Article Type: Research Article

Abstract: We establish a Myhill-Nerode type theorem for higher-dimensional automata (HDAs), stating that a language is regular if and only if it has finite prefix quotient. HDAs extend standard automata with additional structure, making it possible to distinguish between interleavings and concurrency. We also introduce deterministic HDAs and show that not all HDAs are determinizable, that is, there exist regular languages that cannot be recognised by a deterministic HDA. Using our theorem, we develop an internal characterisation of deterministic languages. Lastly, we develop analogues of the Myhill-Nerode construction and of determinacy for HDAs with interfaces.

Keywords: higher-dimensional automaton, Myhill-Nerode theorem, concurrency theory, determinism

DOI: 10.3233/FI-242194

Citation: Fundamenta Informaticae, vol. 192, no. 3-4, pp. 219-259, 2024

Authors: Arias, Jaime | Bae, Kyungmin | Olarte, Carlos | Ölveczky, Peter Csaba | Petrucci, Laure

Article Type: Research Article

Abstract: This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the “standard” semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work …opens up the possibility of using the many formal analysis capabilities of Maude—including full LTL model checking, analysis with user-defined execution strategies, and even statistical model checking—for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Roméo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Roméo in many cases. Show more

Keywords: parametric timed Petri nets, rewriting logic, Maude, SMT, parameter synthesis, symbolic reachability analysis

DOI: 10.3233/FI-242195

Citation: Fundamenta Informaticae, vol. 192, no. 3-4, pp. 261-312, 2024

Authors: Würdemann, Nick | Chatain, Thomas | Haar, Stefan | Panneke, Lukas

Article Type: Research Article

Abstract: Unfoldings are a well known partial-order semantics of P/T Petri nets that can be applied to various model checking or verification problems. For high-level Petri nets, the so-called symbolic unfolding generalizes this notion. A complete finite prefix of a P/T Petri net’s unfolding contains all information to verify, e.g., reachability of markings. We unite these two concepts and define complete finite prefixes of the symbolic unfolding of high-level Petri nets. For a class of safe high-level Petri nets, we generalize the well-known algorithm by Esparza et al. for constructing small such prefixes. We evaluate this extended algorithm through …a prototype implementation on four novel benchmark families. Additionally, we identify a more general class of nets with infinitely many reachable markings, for which an approach with an adapted cut-off criterion extends the complete prefix methodology, in the sense that the original algorithm cannot be applied to the P/T net represented by a high-level net. Show more

Keywords: Petri Nets, High-level Petri Nets, Unfoldings, Concurrency Theory

DOI: 10.3233/FI-242196

Citation: Fundamenta Informaticae, vol. 192, no. 3-4, pp. 313-361, 2024

Authors: Amat, Nicolas | Dal Zilio, Silvano | Le Botlan, Didier

Article Type: Research Article

Abstract: We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems. Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the …fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples. Show more

Keywords: Automated reasoning, Abstraction techniques, Reachability problems, Petri nets

DOI: 10.3233/FI-242197

Citation: Fundamenta Informaticae, vol. 192, no. 3-4, pp. 363-394, 2024