Ensuring completeness of symbolic verification methods for infinite-state systems

Over the last few years there has been an increasing research effort directed towards the automatic verification of infinite state systems. For different classes of such systems, e.g., hybrid automata, data-independent systems, relational automata, Petri nets, and lossy channel systems, this research has resulted in numerous highly nontrivial algorithms. As the interest in this area increases, it will be important to extract common principles that underly these and related results. In this paper, we will present a general model of infinite-state systems, and describe a standard algorithm for reachability analysis of such systems. Our contribution consists in finding conditions under which the algorithm can be fully automated. We perform backward reachability analysis. Using an iterative procedure, we generate successively larger approximations of the set of all states from which a given final state is reachable. We consider classes of systems where these approximations are well quasi-ordered, implying that the iterative procedure always terminates. Starting from these general termination conditions, we derive several computations models for which reachability is decidable. Many of these models are extensions of those existing in the literature. Using a well-known reduction from safety properties to reachability properties, we can use our algorithm to decide large classes of safety properties for infinite-state systems. A motivation for our approach is the long-term desire to build general tools for verification of infinite-state systems, which implies that we should employ principles applicable across a rather wide range of such systems. (C) 2001 Elsevier Science B.V. All rights reserved.