*For the most recent entries see the
Petri Nets Newsletter.*

## Ensuring completeness of symbolic verification methods for infinite-state systems.

Abdulla, Parosh Aziz;
Jonsson, Bengt
In:
*Theoretical Computer Science 256 (1-2)*, pages 145-167.
April 2001.

Abstract:
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.

Keywords:
Infinite-state systems; Model checking; Reachability analysis; Symbolic
verification.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*