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

DOI10.1007/978-3-030-76983-3_9zbMATH Open1489.68150arXiv2104.09850OpenAlexW3163218045MaRDI QIDQ2117166FDOQ2117166

Authors: Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio 

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

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

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)

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

• z3
• Cubicle
• GitHub

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)