A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking

DOI10.3233/FI-222134MaRDI QIDQ5044397zbMATH OpenOpenAlexFDO

Authors Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio

Publication date 31 October 2022

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-222134

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
• A CTL* Model Checker for Petri Nets
• scientific article; zbMATH DE number 7438162
• scientific article; zbMATH DE number 408787
• A satisfiability-based approach to abstraction refinement in model checking
• Model checking Petri nets with MSVL
• SMT-based reachability checking for bounded time Petri nets

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 1956602 (Why is no real title available?)
• scientific article; zbMATH DE number 1863166 (Why is no real title available?)
• Bounded model checking using satisfiability solving
• Directed reachability for infinite-state systems
• Infinite-state invariant checking with IC3 and predicate abstraction
• Model Checking Software
• Reduction
• SAT-Based Model Checking without Unrolling
• Stubborn versus structural reductions for Petri nets
• Symbolic and structural model-checking
• Understanding IC3

Cited in

(3)

• On the complexity of proving polyhedral reductions
• 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: A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5044397)