Research Projects - Infinite State Systems

Verification of Infinite State Systems

M. C. Escher: Encounter Cooperations Financial Support,

Master's Theses, Term Projects

Publications

Current Members: Former Members: Links
Research on the verification of infinite-state systems was started in 1994. We follow essentially two lines of research: On the one hand, we study the decidability and complexity of verification problems for different classes of infinite automata that can be organized in a Chomsky-like hierarchy. On the other hand, we are interested in the machine-assisted verification of infinite-state and parameterized systems within process classes for which the verification is potentially undecidable. The results find application in the area of program optimization (in particular in the interprocedural dataflow analysis), and in the verification of parameterized systems.

Decidability and Complexity of Verification Problems

We have established several results about the decidability and computational complexity of the model checking problem for a hierarchy of Process Rewrite Systems (PRS) including context-free processes, Basic Parallel Processes, and Petri nets. The PRS hierarchy presents a unified view of all these models. It is strict with respect to bisimulation equivalence. I.e., in every class there exists a process that is not bisimilar to any process from the lower classes. Similar hierarchies have been defined by Stirling, Caucal, and Moller [Cau92, Mol96].
The model checking problem is as follows: Given a formal description of a system (e.g., as a Petri net) and a property in terms of a logical formula, does the systems satisfy the property?
We have studied the problem for different standard modal and temporal logics, comprising computation tree logic (CTL) and fragments of it, linear-time temporal logic (LTL), the modal µ-calculus, and the linear-time µ-calculus [Bra92, Eme94, MB96].
Further we have studied the reachability problem for the PRS hierarchy: Given a formal description of a system and two of its states, can the one state be reached from the other.
The following graphics give an overview of the obtained results:
model-checking branching-time logics model-checking linear-time logics
Branching-time logics
Linear-time logics
reachability
Reachability

For more details see [May98].

We have shown that model checking the modal µ-calculus is equivalent to solving Boolean equation systems, and to some automata-theoretic and game-theoretic problems. The results allow to infer new complexity results for model checking the modal µ-calculus.
Further, we have developed a new model checking algorithm based on solving Boolean equation systems. Its methodology is similar to Gauß elimination for linear equation systems.
For infinite-state systems model checking is equivalent to solving infinite Boolean equation systems. A second algorithm is based on this relationship.
See also our section on partial order model checking.

For more details see [Mad97].

Machine-assisted Verification

Our research on the machine-assisted verification of infinite-state and parameterized systems within process classes for which the verification is potentially undecidable, follows two orthogonal lines: On the one hand, we develop fully automatic techniques for reduced verification problems. This allows to verify simple properties of large systems. On the other hand, we study the mechanization in theorem provers of general proof techniques. This allows us to verify complex properties of systems with a small representation.
The techniques are applicable to infinite-state and parameterized systems. We are particularly interested in applying them to mobile and higher-order systems as well.
Fully automatic verification with type systems
We are developing generic type systems for concurrent systems ensuring, e.g., deadlock freedom, or security properties. So far we have considered a graph-based higher-order calculus with a reduction semantic, called SPIDER. The calculus is general enough to encode the -calculus as well as the -calculus. For the composition of process graphs both process algebraical and category theoretical techniques are available. The processes can then be analyzed using types. We have developed a generic type system for SPIDER, i.e., we have given a general-scale type system that can be instantiated for specific purposes like showing that a process is deadlock-free. If a process is typable in a specific instantiation of the type system, we know that it fulfills the related property. The current type system can, e.g., be instantiated to verify deadlock freedom, or security properties. This is particularly useful, as usually it is simpler to infer the type of a process than to verify a property given in a modal or temporal logic (see above).
Using a generic type system has the following advantages: Important properties like subject reduction have to be proved only once, for the general type systems; they hold automatically for all of the instantiations. Also, the principle of type inference is equal for all instantiations, and need only be provided for the general type system. A type inference algorithm can thus be implemented generically, and instantiated for the single properties by the user.
We have experimented with instantiations for safety properties, such as deadlock freedom, as well as security properties. The latter are vital to ensure a secure flow of messages in mobile systems. We are planning to further generalize the generic type system, and to transfer the developed techniques to mobile calculi such as the -calculus [MPW89], and to prototypical programming languages such as Concurrent Idealized Algol [Bro96].

For more details see [Koe99a, Koe99b].

Mechanization of bisimilation proofs
Observation equivalence (or weak bisimilarity) is a natural notion of equivalence. It has been introduced in the framework of CCS in [Mil89]. Observation equivalence is behaviourally based: two processes are observation equivalent if they are able to mutually simulate one another's behaviours; if one process is capable of performing an output, say, the other process has to perform the same output (possibly preceeded and followed by internal steps), and the resulting processes have to be bisimilar again.
There exist two general ways of showing that two processes are observation equivalent. One, semantically oriented way, is to follow the definition: exhibit a relation containing as a pair the two processes and show that it is a bisimulation, i.e., that for every pair in the relation, the processes can mutually simulate each other's behaviour resulting in process pairs that are again in the relation. Another, syntactically oriented, way is to use algebraic (equational) reasoning, i.e., to transform one process into the other by a continuous application of algebraic laws.
Observation equivalence is decidable for finite-state processes, and for very simple infinite-state process classes like Basic Parallel Processes [KM99]. Once restriction comes into play to hide internal channels from the observer it becomes undecidable, as restrictions can be used to model counters. Yet, more realistic examples usually have to be modelled within fragments of process algebras for which observation equivalence is undecidable.
Algebraic techniques are commonly applied to verify concurrent systems [GS95, GS96, HM98], especially in the framework of µCRL (see the µCRL information page). Following the semantically oriented way, we study the mechanization in theorem provers of bisimilarity proofs be exhibiting a concrete bisimulation relation. To the best of our knowledge, this approach has not been taken so far. In [RE99] we report on our experience in using the Isabelle theorem prover to mechanize bisimulation based proofs in order to verify infinite-state and parameterized communication protocols. We model the protocols and their specifications as CCS-style transition systems, instead of giving a full syntactic formalization of the process algebra. Another case study mechanizes a bisimulation proof for a write invalidate cache coherence protocol. The proof is based on a transition system implementing a broadcast mechanism, and uses up to expansion techniques. In contrast to the above case studies, mechanizations that are rather interested in proving meta-theorems about process algebras implement the whole syntax [Hir97, HMS98].
We are planning to extend our case studies to mobile and higher-order systems, including examples from the -calculus. This allows us to derive mechanized proofs of properties for higher-order programming languages such as Concurrent Idealized ALGOL [Bro96].

Cooperations

Financial Support



Publications

[Postscript] [PDF]

Links to Related Sites


Selected References


Mon Dec 6 10:08:47 MET 1999