Coverability Analysis for Infinite-State Systems

We propose a novel algorithm for coverability analysis in a broad class of infinite-state systems named well-structured transition systems by using finite-state model checking techniques. Firstly, the well-structured transition system is divided into a series of finite-state machines with different weights. Then, the state-of-the-art model checking algorithm is used to compute the over-approximation of the reachability for the finite state machines, incrementally. Finally, the algorithm produces a coverable counterexample path or proves the system is uncoverable. The results show that the algorithm can solve more instances under the same time limit. 97.2% instances are solved within 1 GB memory, which is more than two times of the compared algorithms.