Research Projects  Infinite State Systems
Verification of Infinite State Systems
Research on the verification of infinitestate 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 Chomskylike
hierarchy. On the other hand, we are interested in the
machineassisted
verification of infinitestate 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 contextfree 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, lineartime temporal
logic (LTL), the modal µcalculus, and the lineartime µ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:


Branchingtime logics 
Lineartime logics 

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 automatatheoretic and gametheoretic
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 infinitestate 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].
Machineassisted Verification
Our research on the machineassisted verification of infinitestate 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 infinitestate and parameterized systems.
We are particularly interested in applying them to
mobile and higherorder 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 graphbased higherorder 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 generalscale
type system that can be instantiated for specific purposes like showing
that a process is deadlockfree. 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 finitestate processes,
and for very simple infinitestate 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
infinitestate and parameterized communication protocols. We model the
protocols and their specifications as CCSstyle 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
metatheorems about process algebras implement the whole syntax
[Hir97,
HMS98].
We are planning to extend our case studies
to mobile and higherorder systems,
including examples from the calculus. This allows us to derive
mechanized proofs of properties for higherorder 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