A Toolchain to Compute Concurrent Places of Petri Nets - Réseaux, Informatique, Systèmes de Confiance
Journal Articles LNCS Transactions on Petri Nets and Other Models of Concurrency Year : 2023

A Toolchain to Compute Concurrent Places of Petri Nets

Abstract

The concurrent places of a Petri net are all pairs of places that may simultaneously have a token in some reachable marking. Concurrent places generalize the usual notion of dead places and are particularly useful for decomposing a Petri net into synchronized automata executing in parallel. We present a state-of-the-art toolchain to compute the concurrent places of a Petri net. This is achieved by a rich combination of various techniques, including: state-space exploration using BDDs, structural rules for concurrent places, quadratic over- and under-approximation of reachable markings, and polyhedral abstraction of the state space based on structural reductions and linear arithmetic constraints on markings. We assess the performance of our toolchain on a large collection of 850 nets originating from the 2022 edition of the Model Checking Contest.
Fichier principal
Vignette du fichier
Amat-Bouvier-Garavel-23.pdf (749.65 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04392784 , version 1 (26-07-2024)

Licence

Identifiers

Cite

Nicolas Amat, Pierre Bouvier, Hubert Garavel. A Toolchain to Compute Concurrent Places of Petri Nets. LNCS Transactions on Petri Nets and Other Models of Concurrency, 2023, Lecture Notes in Computer Science, 14150, pp.1-26. ⟨10.1007/978-3-662-68191-6_1⟩. ⟨hal-04392784⟩
267 View
32 Download

Altmetric

Share

More