Abstraction-based incremental inductive coverability for Petri nets

DOI10.1007/978-3-030-76983-3_19MaRDI QIDQ2117187zbMATH OpenOpenAlexFDO

Authors Jiawen Kang, Y. J. Bai, Li Jiao

Publication date 21 March 2022

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

zbMATH Keywords

coverabilityIC3inductive invariantsPetri netsplace-merge abstraction

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) Nonnumerical algorithms (68W05)

Recommendations

• Approaching the coverability problem continuously
• An SMT-based approach to coverability analysis
• From Many Places to Few: Automatic Abstraction Refinement for Petri Nets
• From many places to few: automatic abstraction refinement for Petri nets

Cites work

• \textsf{PrIC3}: property directed reachability for MDPs
• An SMT-based approach to coverability analysis
• Complexity of some problems in Petri nets
• Counterexample-guided abstraction refinement for symbolic model checking
• Efficient coverability analysis by proof minimization
• From Many Places to Few: Automatic Abstraction Refinement for Petri Nets
• scientific article; zbMATH DE number 3885321 (Why is no real title available?)
• Infinite-state invariant checking with IC3 and predicate abstraction
• SAT-Based Model Checking without Unrolling
• SMT-based induction methods for timed systems
• SMT-based scenario verification for hybrid systems
• Well-structured transition systems everywhere!

Cited in

(4)

• An SMT-based approach to coverability analysis
• From many places to few: automatic abstraction refinement for Petri nets
• From Many Places to Few: Automatic Abstraction Refinement for Petri Nets
• Property directed reachability for generalized Petri nets

Describes a project that uses

Uses Software

• CTIGAR

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

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