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.