Skip to Main content Skip to Navigation
Conference papers

Efficient Algorithms for Three Reachability Problems in Safe Petri Nets

Pierre Bouvier 1 Hubert Garavel 1 
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : We investigate three particular instances of the marking coverability problem in ordinary, safe Petri nets: the Dead Places Problem, the Dead Transitions Problem, and the Concurrent Places Problem. To address these three problems, which are of practical interest, although not yet supported by mainstream Petri net tools, we propose a combination of static and dynamic algorithms. We implemented these algorithms and applied them to a large collection of 13,000+ Petri nets obtained from realistic systems-including all the safe benchmarks of the Model Checking Contest. Experimental results show that 95% of the problems can be solved in a few minutes using the proposed approaches.
Document type :
Conference papers
Complete list of metadata
Contributor : Hubert Garavel Connect in order to contact the contributor
Submitted on : Tuesday, July 13, 2021 - 9:10:09 PM
Last modification on : Saturday, June 25, 2022 - 7:36:02 PM
Long-term archiving on: : Thursday, October 14, 2021 - 7:21:30 PM


Files produced by the author(s)




Pierre Bouvier, Hubert Garavel. Efficient Algorithms for Three Reachability Problems in Safe Petri Nets. PETRI NETS 2021 - 42nd International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2021, Paris, France. pp.339-359, ⟨10.1007/978-3-030-76983-3_17⟩. ⟨hal-03286069⟩



Record views


Files downloads