Property Directed Reachability for Generalized Petri Nets
Logic in Computer Science
2022-08-08 v1
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.
Keywords
Cite
@article{arxiv.2208.03043,
title = {Property Directed Reachability for Generalized Petri Nets},
author = {Nicolas Amat and Silvano Dal Zilio and Thomas Hujsa},
journal= {arXiv preprint arXiv:2208.03043},
year = {2022}
}
Comments
This is a long version of a paper published in the proceedings of TACAS 2022 under the same title