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 wellstructured 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 symbolic backward analysis or expand-enlarge-and-check algorithms both in time taken and space usage.
Inspired by the success of IC3 algorithm in finite state model checking, Kloos et al. REF proposed an incremental, inductive procedure to check coverability of downward-finite WSTS, which contains Petri nets, broadcast protocols, and lossy channel systems.
Incremental, Inductive Coverability
ArXiv
ArXiv
Computer Science Mathematics