Generic Techniques for the Verification of Infinite-State Systems
-----------------------------------------------------------------

Within the context of the verification of infinite-state systems,
``Regular model checking'' is the name of a family of techniques in
which states are represented by words or trees, sets of states by
finite automata on these objects, and transitions by finite automata
operating on pairs of state encodings, i.e. finite-state
transducers. In this context, the problem of computing the set of
reachable states of a system can be reduced to the one of computing
the iterative closure of the finite-state transducer representing its
transition relation. This thesis provides several techniques to
computing the transitive closure of a finite-state transducer. One of
the motivations of the thesis is to show the feasibility and
usefulness of this approach through a combination of the necessary
theoretical developments, implementation, and experimentation. For
systems whose states are encoded by words, the iteration technique
proceeds by comparing a finite sequence of successive powers of the
transducer, detecting an ``increment'' that is added to move from one
power to the next, and extrapolating the sequence by allowing
arbitrary repetitions of this increment. For systems whose states are
represented by trees, the iteration technique proceeds by computing
the powers of the transducer and progressively collapsing their states
according to an equivalence relation until a fixed point is reached.

The proposed iteration techniques can just as well be exploited to
compute the closure of a given set of states by repeated applications
of the transducer, which has proven to be a very effective way of
using the technique. Various examples have been handled completely
within the automata-theoretic setting.

Another applications of the techniques are the verification of linear
temporal properties as well as the computation of the convex hull of a
finite set of integer vectors.