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 inwhich states are represented by words or trees, sets of states byfinite automata on these objects, and transitions by finite automataoperating on pairs of state encodings, i.e. finite-statetransducers. In this context, the problem of computing the set ofreachable states of a system can be reduced to the one of computingthe iterative closure of the finite-state transducer representing itstransition relation. This thesis provides several techniques tocomputing the transitive closure of a finite-state transducer. One ofthe motivations of the thesis is to show the feasibility andusefulness of this approach through a combination of the necessarytheoretical developments, implementation, and experimentation. Forsystems whose states are encoded by words, the iteration techniqueproceeds by comparing a finite sequence of successive powers of thetransducer, detecting an 'increment' that is added to move from onepower to the next, and extrapolating the sequence by allowingarbitrary repetitions of this increment. For systems whose states arerepresented by trees, the iteration technique proceeds by computingthe powers of the transducer and progressively collapsing their statesaccording to an equivalence relation until a fixed point is reached.The proposed iteration techniques can just as well be exploited tocompute the closure of a given set of states by repeated applicationsof the transducer, which has proven to be a very effective way ofusing the technique. Various examples have been handled completelywithin the automata-theoretic setting.Another applications of the techniques are the verification of lineartemporal properties as well as the computation of the convex hull of afinite set of integer vectors.