General results on methodology of verification

In [AJ01b], the authors present a general model of infinite-state systems, and describe a standard algorithm for reachability analysis of such systems. The contribution of this paper consists in finding conditions under which the algorithm can be fully automated. The idea consists of performing backward reachability analysis. Using an iterative procedure, one generates successively larger approximations of the set of all states from which a given final state is reachable. The classes of systems that are considered are such that these approximations are well quasi-ordered, implying that the iterative procedure always terminates. Starting from these general termination conditions, one derives 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, the algorithm introduced in the paper can be used to decide large classes of safety properties for infinite-state systems. A motivation for this approach is the long-term desire to build general tools for verification of infinite-state systems, which implies that one should employ principles applicable across a rather wide range of such systems.

In [Bou01], a general approach is introduced for verifying algorithmically infinite-state systems. This approach is based on the use of languages (not necessarily regular) as symbolic representations of infinite sets of configurations, and the use of rewriting systems as models for these systems. The verification problem is then reduced to the problem of computing closures of languages under rewriting systems. The paper presents in a uniform manner several applications of this approach to different kinds of infinite-state systems: Pushdown systems, FIFO-channel systems, and parametrized networks of identical processes.

In [AB01], the computational power of several models of dynamical systems is investigated under infinitesimal perturbations of their dynamics. This study considers models for discrete and continuous time dynamical systems: Turing machines, Piecewise affine maps, Linear hybrid automata and Piecewise constant derivative systems (a simple model of hybrid systems). One associates with each of these models a notion of perturbed dynamics by a small $\varepsilon$ (w.r.t. to a suitable metrics), and define the perturbed reachability relation as the intersection of all reachability relations obtained by $\varepsilon$-perturbations, for all possible values of $\varepsilon$. It is shown that for the four kinds of models we consider, the perturbed reachability relation is co-recursively enumerable, and that any co-r.e. relation can be defined as the perturbed reachability relation of such models. A corollary of this result is that systems that are robust, i.e., their reachability relation is stable under infinitesimal perturbation, are decidable.