| Autor: |
Amat, Nicolas, Berthomieu, Bernard, Zilio, Silvano Dal |
| Rok vydání: |
2021 |
| Předmět: |
|
| Zdroj: |
Fundamenta Informaticae, Volume 187, Issues 2-4: Petri Nets 2021 (October 21, 2022) fi:8831 |
| Druh dokumentu: |
Working Paper |
| DOI: |
10.3233/FI-222134 |
| Popis: |
We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some Petri net, into the verification of an updated reachability property on a reduced version of this net. This method relies on a new state space abstraction based on systems of constraints, called polyhedral abstraction. We prove the correctness of this method using a new notion of equivalence between nets. We provide a complete framework to define and check the correctness of equivalence judgements; prove that this relation is a congruence; and give examples of basic equivalence relations that derive from structural reductions. Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used in the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
