Research Projects - Infinite State Systems
Verification of Infinite State Systems
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
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
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
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
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:
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
Further, we have developed a new model checking algorithm based on solving Boolean
equation systems. Its methodology is similar to Gauß elimination for linear
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
For more details see [Mad97].
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
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
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
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
We are planning to further generalize the generic type system, and to
transfer the developed techniques to mobile calculi such as the
to prototypical programming languages such as Concurrent Idealized Algol
For more details see [Koe99a,
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
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
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
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
Links to Related Sites
Mon Dec 6 10:08:47 MET 1999