Skip to Main content Skip to Navigation
New interface
Conference papers

Property Directed Reachability for Generalized Petri Nets

Nicolas Amat 1 Silvano Dal Zilio 1 Thomas Hujsa 1 
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
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.
Document type :
Conference papers
Complete list of metadata

https://hal.laas.fr/hal-03545594
Contributor : Silvano Dal Zilio Connect in order to contact the contributor
Submitted on : Thursday, January 27, 2022 - 12:33:19 PM
Last modification on : Tuesday, October 25, 2022 - 11:58:11 AM

File

paper.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Nicolas Amat, Silvano Dal Zilio, Thomas Hujsa. Property Directed Reachability for Generalized Petri Nets. Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022, Apr 2022, Munich, Germany. ⟨10.1007/978-3-030-99524-9_28⟩. ⟨hal-03545594⟩

Share

Metrics

Record views

48

Files downloads

1