Abstraction-based incremental inductive coverability for Petri nets

DOI10.1007/978-3-030-76983-3_19zbMath1489.68162OpenAlexW3168898146MaRDI QIDQ2117187

Li Jiao, Yunjun Bai, Jiawen Kang

Publication date: 21 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-76983-3_19

zbMATH Keywords

Petri netsIC3coverabilityinductive invariantsplace-merge abstraction

Mathematics Subject Classification ID

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

Uses Software

• CTIGAR

Cites Work

• Unnamed Item
• Complexity of some problems in Petri nets
• \textsf{PrIC3}: property directed reachability for MDPs
• Infinite-state invariant checking with IC3 and predicate abstraction
• SMT-based scenario verification for hybrid systems
• Efficient Coverability Analysis by Proof Minimization
• An SMT-Based Approach to Coverability Analysis
• SAT-Based Model Checking without Unrolling
• Counterexample-guided abstraction refinement for symbolic model checking
• From Many Places to Few: Automatic Abstraction Refinement for Petri Nets
• SMT-Based Induction Methods for Timed Systems
• Well-structured transition systems everywhere!

This page was built for publication: Abstraction-based incremental inductive coverability for Petri nets