On the combination of polyhedral abstraction and SMT-based model checking for Petri nets

DOI10.1007/978-3-030-76983-3_9MaRDI QIDQ2117166zbMATH OpenOpenAlexFDO

Authors Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio

Publication date 21 March 2022

Full work available at URL https://arxiv.org/abs/2104.09850

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Symbolic and structural model-checking
• scientific article; zbMATH DE number 1852166
• SMT-based reachability checking for bounded time Petri nets
• Decompositional Petri Net Reductions
• Automated Technology for Verification and Analysis

Cites work

• scientific article; zbMATH DE number 4033100 (Why is no real title available?)
• scientific article; zbMATH DE number 177506 (Why is no real title available?)
• scientific article; zbMATH DE number 1302046 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• An SMT-based approach to coverability analysis
• Automatic decomposition of Petri nets into automata networks -- a synthetic account
• Bounded model checking using satisfiability solving
• Hierarchical Set Decision Diagrams and Regular Models
• Infinite-state invariant checking with IC3 and predicate abstraction
• Model Checking Software
• Petri Net Reductions for Counting Markings
• Reduction
• SAT-Based Model Checking without Unrolling
• Structural reductions revisited
• Stubborn versus structural reductions for Petri nets
• Understanding IC3

Cited in

(6)

• Accelerating the computation of dead and concurrent places using reductions
• Symbolic and structural model-checking
• 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

Describes a project that uses

Uses Software

• GitHub
• Cubicle
• z3

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)