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

DOI10.3233/FI-222134OpenAlexW4287205805MaRDI QIDQ5044397FDOQ5044397

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

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

Mathematics Subject Classification ID

Computer science (68-XX)

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?)
• Understanding IC3
• Reduction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Stubborn versus structural reductions for Petri nets
• Model Checking Software
• Symbolic and Structural Model-Checking
• Title not available (Why is that?)
• Directed reachability for infinite-state systems

Cited In (2)

• On the complexity of proving polyhedral reductions
• Automated polyhedral abstraction proving

Uses Software

• z3
• Cubicle
• GitHub

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)