|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
Efficient Algorithms for Three Reachability Problems in Safe Petri Nets
Pierre Bouvier and Hubert Garavel
Proceedings of the 42nd International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'21), Paris, France, June 2021
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.
| 23 pages |  |
 PostScript |
| Slides of P. Bouvier's lecture at the Petri Net 2021 conference | |