Task T1.2: Symbolic analysis

Symbolic reachability analysis is based on using data structures which allow to represent and manipulate (infinite) sets of configurations, and powerful configuration-space exploration procedures which allow to construct effectively the set of all reachable configurations. This analysis can be used in several ways, mainly to perform on-the-fly verification of safety properties, and to generate invariants and finite abstract models.

In our project, algorithmic verification techniques for various infinite-state systems have been developed based on symbolic reachability analysis.

1. In [ES01c,EKS01] (D1), efficient symbolic model-checking algorithms are developed for Boolean programs with mutually recursive procedures. In [BHM01] (D1,D2), symbolic analysis techniques are developed for mutually recursive procedures with one integer parameter.
2. In [AJ01b] (D1), a general framework for the verification of infinite-state systems is developed based on backward symbolic reachability analysis. General termination conditions are given from which it is possible to derive the decidability of verification problems for various classes of models.
3. In [AB01] (D1), the power of various computational models is studied under the assumption of perturbation (noise, unreliability, etc). A natural notion of robustness under perturbation is defined, and it is shown that the class of robust systems coincides with the class of decidable ones.
4. In [AN01] (D1), a symbolic algorithm for deciding the coverability problem for (unbounded) Timed Petri Nets is provided. In [AJ01c] (D2) similar techniques are used to solve the verification problem of safety properties (such as mutual exclusion) for a class of parametrized networks of 1-clock timed automata.
5. In [AJ01a,ABB01] (D1), symbolic verification algorithms are provided for automata communicating through unbounded lossy FIFO channels.
6. In [BJW01] (D1), efficient data structures (NDDs and RVAs) based on finite-state automata have been introduced for symbolic representation of infinite sets of integer or real vectors. These representations are shown to have nice algorithmic properties an that they are expressive enough to handle linear arithmetics. These representations have been implemented in the tool LASH [LAS]. In [BL01] (D1), NDDs are used to compute automatically the number of solutions of arithmetical constraints expressed in Presburger arithmetics.
7. In [ABS01] (D1), a new tool called TReX is presented for the verification of extended automata (clock and counter automata) with parametric guards. This tool manipulates data structures based on a matrix-based representation and applies fixpoint acceleration techniques on these representations allowing to generate the reachability sets of protocols with complex parametric constraints [CAS01] (D2).
8. In [KMM+01] (D2), the regular model checking framework is advocated as a uniform framework for the analysis of parametrized networks of finite-state systems arranged in linear, ring-like, or tree-like topologies. In this framework, sets of configurations of arbitrary lengths are represented by means of regular languages (automata on words or trees), systems are modeled as regular relations (transductions), and verification problems are reduced to the problem of computing closure of languages under regular relations (which is not possible in general since the transition relation of any Turing machine is a regular transduction). In [Bou01] (D1), a similar framework based on the use of languages and rewriting systems is presented.
9. In [BMT01] (D2), a subclass of regular languages is considered and shown to be a natural class for the analysis of infinite-state systems. In contrast to regular languages, this class is shown to be closed under permutations (semi-commutations) which correspond to common operations in the description of many parametrized systems.
10. In [Tou01] (D2), widening operations are developed for accelerating fixpoint computations in the framework of regular model checking. These techniques are shown to be exact and complete in many cases.
11. In [DLS01] (D2), techniques for computing transitive closures of regular relations (finite transducers) are defined. These techniques are based collapsing states during the computation of the iterated transducers using notions of backward and forward bisimulations.
12. In [FP01] (D2), the framework of regular model checking is extended in order to deal with classes of parametrized systems generating nonregular languages (such as context-free languages).
13. In [Mai01] (D2), an original symbolic analysis technique is introduced in order to deal with parametrized networks. The paper gives a characterization of a subclass of parameterized systems for which the algorithm is always guaranteed to terminate. The subclass is sufficiently wide to cover existing results for token rings and broadcast protocols.