↓Skip to main content

Property Directed Reachability for Generalized Petri Nets

Verification Tools SMPT Petri Reductions
Table of Contents

Nicolas Amat, Silvano Dal Zilio, Thomas Hujsa
In TACAS 2022 — International Conference on Tools and Algorithms for the Construction and Analysis of Systems, mar 2022.

conference paper

 PDF  DOI〈10.1007/978-3-030-99524-9_28〉  HAL-03545594

Abstract
#

We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on the method used for abstracting possible witnesses, and that are able to handle problems of increasing difficulty. We have implemented our methods in a model-checker called SMPT and give empirical evidences that our approach can handle problems that are difficult or impossible to check with current state of the art tools.

Citation
#


@InProceedings{DalzilioS:tacas2022pdr,
   author    = {Amat, Nicolas and {Dal Zilio}, Silvano and Hujsa, Thomas},
   title     = {{Property Directed Reachability for Generalized Petri Nets}},
   booktitle = {TACAS 2022 -- International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
   series    = {Lecture Notes in Computer Science},
   volume    = {13243},
   publisher = {Springer-Verlag},
   doi = {10.1007/978-3-030-99524-9_28},
   pages     = {505--523},
   month     = mar, 
   year      = 2022
}