On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
From MaRDI portal
Publication:2117166
DOI10.1007/978-3-030-76983-3_9zbMATH Open1489.68150arXiv2104.09850OpenAlexW3163218045MaRDI QIDQ2117166FDOQ2117166
Nicolas Amat, Silvano Dal Zilio, Bernard Berthomieu
Publication date: 21 March 2022
Abstract: 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.
Full work available at URL: https://arxiv.org/abs/2104.09850
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- SAT-Based Model Checking without Unrolling
- Infinite-state invariant checking with IC3 and predicate abstraction
- Bounded model checking using satisfiability solving
- Title not available (Why is that?)
- Title not available (Why is that?)
- Understanding IC3
- Reduction
- Title not available (Why is that?)
- Stubborn versus structural reductions for Petri nets
- Automatic Decomposition of Petri Nets into Automata Networks – A Synthetic Account
- Structural Reductions Revisited
- Petri Net Reductions for Counting Markings
- Model Checking Software
- An SMT-Based Approach to Coverability Analysis
- Hierarchical Set Decision Diagrams and Regular Models
- Title not available (Why is that?)
Cited In (5)
- Accelerating the computation of dead and concurrent places using reductions
- On the complexity of proving polyhedral reductions
- A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking
- Automated polyhedral abstraction proving
- Property directed reachability for generalized Petri nets
Uses Software
This page was built for publication: On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117166)
