Incremental, Inductive Coverability
Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac

TL;DR
This paper introduces an incremental, inductive procedure for verifying coverability in well-structured transition systems, extending IC3 from hardware to infinite-state systems, with practical implementation and competitive performance on Petri nets.
Contribution
It generalizes the IC3 safety verification method to infinite-state systems, providing a sound, complete, and terminating algorithm for downward-finite well-structured transition systems.
Findings
Algorithm is sound, complete, and terminating for downward-finite systems.
Implementation for Petri nets shows competitive performance.
Efficient implementation without SMT solvers demonstrated.
Abstract
We give an incremental, inductive (IC3) procedure to check coverability of well-structured transition systems. Our procedure generalizes the IC3 procedure for safety verification that has been successfully applied in finite-state hardware verification to infinite-state well-structured transition systems. We show that our procedure is sound, complete, and terminating for downward-finite well-structured transition systems---where each state has a finite number of states below it---a class that contains extensions of Petri nets, broadcast protocols, and lossy channel systems. We have implemented our algorithm for checking coverability of Petri nets. We describe how the algorithm can be efficiently implemented without the use of SMT solvers. Our experiments on standard Petri net benchmarks show that IC3 is competitive with state-of-the-art implementations for coverability based on…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Safety Systems Engineering in Autonomy · Physical Unclonable Functions (PUFs) and Hardware Security
