Incremental, Inductive Coverability

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 symbolic backward analysis or expand-enlarge-and-check algorithms both in time taken and space usage.