Petri Net Reductions for Counting Markings

Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio
In SPIN 2018 — International Symposium on Model Checking Software, jun 2018.

 PDF  DOI〈10.1007/978-3-319-94111-0_4〉  HAL-01822078

Abstract

#

We propose a method to count the number of reachable markings of a Petri net without having to enumerate these first. The method relies on a structural reduction system that reduces the number of places and transitions of the net in such a way that we can faithfully compute the number of reachable markings of the original net from the reduced net and the reduction history. The method has been implemented and computing experiments show that reductions are effective on a large benchmark of models.

References

#

• A longer version appears in the International Journal on Software Tools for Technology Transfer (STTT), April 2019.  Link

Citation

#

@InProceedings{DalzilioS:spin2018counting,
   author    = {Berthomieu, Bernard and {Le Botlan}, Didier and {Dal Zilio}, Silvano},
   title     = {{Petri Net Reductions for Counting Markings}},
   booktitle = {SPIN 2018 -- International Symposium on Model Checking Software},
   series    = {Lecture Notes in Computer Science},
   volume    = {10869},
   publisher = {Springer-Verlag},
   doi = {10.1007/978-3-319-94111-0_4},
   pages     = {65--84},
   month     = jun, 
   year      = 2018
}