Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
Institute of Formal Methods in Computer Science

Software Reliability and Security Group

 

Verification of Infinite State Systems

M. C. Escher: Encounter Cooperations

Publications

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


Publications

BCK01
P. Baldan, A. Corradini, and B. König.
A static analysis technique for graph transformation systems.
In Proc. of CONCUR '01, number 2154 in Lecture Notes in Computer Science, pages 381-395. Springer-Verlag, 2001. [gzipped Postscript ]

BEM97
A. Bouajjani, J. Esparza, and O. Maler.
Reachability analysis of pushdown automata: Application to model-checking.
In Proc. of CONCUR'97, 1997. [gzipped Postscript ]

BM99
A. Bouajjani and R. Mayr.
Model checking lossy vector addition systems.
In C. Meinel and S. Tison, editors, Proc. of STACS'99, number 1563 in Lecture Notes in Computer Science. Springer-Verlag, 1999.

BE96
O. Burkart and J. Esparza.
More infinite results.
Electronic Notes in Theoretical Computer Science, 6, 1996. [gzipped Postscript ]P>

BE97
O. Burkart and J. Esparza.
More infinite results.
Bulletin of the EATCS 62 (Concurrency Column), 1997.

DEP99
G. Delzanno, J. Esparza, and A. Podelski.
Constraint-based analysis of broadcast protocols.
In Proceedings of CSL '99, number 1683 in Lecture Notes in Computer Science, pages 50-66. [gzipped Postscript ]

Esp94
J. Esparza.
On the decidabilty of model checking for several mu-calculi and petri nets.
In S. Tison, editor, Proceedings of Trees in Algebra and Programming - CAAP '94, 19th International Colloquium 1994, number 787 in Lecture Notes in Computer Science, pages 115-129, 1994.

Esp96
J. Esparza.
More infinite results.
In Proc. of INFINITY'96, Research Report MIP-9614, University of Passau, 1996. [gzipped Postscript ]

Esp97b
J. Esparza.
Decidability of model-checking for infinite-state concurrent systems.
Acta Informatica, 34:85-107, 1997. [gzipped Postscript ]

Esp97a
J. Esparza.
Petri nets, commutative context-free grammars, and basic parallel processes.
Fundamenta Informaticae, 31:13-26, 1997. [gzipped Postscript ]

EHRS00a
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon.
Efficient algorithms for model checking pushdown systems.
Technical Report TUM-I0002, SFB-Bericht 342/1/00 A, Technische Universität München, Institut für Informatik, February 2000. [gzipped Postscript ]

EHRS00b
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon.
Efficient algorithms for model checking pushdown systems.
In Proc. of CAV'2000, number 1855 in Lecture Notes in Computer Science, pages 232-247. Springer-Verlag, 2000. [gzipped Postscript ]

EK95
J. Esparza and A. Kiehn.
On the model checking problem for branching time logics and basic parallel processes.
In Proc. of CAV'95, number 939 in Lecture Notes in Computer Science, pages 353-366. Springer-Verlag, 1995. [gzipped Postscript ]

EK99
J. Esparza and J. Knoop.
An automata-theoretic approach to interprocedural dataflow analysis.
In W. Thomas, editor, Proceedings von FOSSACS'99, number 1578 in Lecture Notes in Computer Science, pages 14-30, 1999. [gzipped Postscript ]

EN94
J. Esparza and M. Nielsen.
Decibility issues for Petri nets - a survey.
Journal of Informatik Processing and Cybernetics, 30(3):143-160, 1994. [gzipped Postscript ]

ES01
J. Esparza and S. Schwoon.
A BDD-based model checker for recursive programs.
In Proc. of CAV'01, number 2102 in Lecture Notes in Computer Science, pages 324-336. Springer-Verlag, 2001. [gzipped Postscript ]

JE95
P. Jancar and J. Esparza.
Deciding finiteness of Petri nets up to bisimulation.
SFB-Bericht Nr. 342/23/95A, TU München, 1995. [gzipped Postscript ]

JE96
P. Jancar and J. Esparza.
Deciding finiteness of Petri nets up to bisimulation.
In F. Meyer, der Heider, and B. Monien, editors, Proc. of ICALP'96, number 1099 in Lecture Notes in Computer Science, pages 478-489. Springer-Verlag, 1996. [gzipped Postscript ]

JEM99
P. Jancar, J. Esparza, and F. Moller.
Petri nets and regular behaviours.
Journal of Computer and System Sciences, 59(3):476-503, 1999. [gzipped Postscript ]

JKM98a
P. Jancar, A. Kucera, and R. Mayr.
Deciding bisimulation-like equivalences with finite-state processes.
Technical Report I9805, TU-München, 1998. [gzipped Postscript ]

JKM98b
P. Jancar, A. Kucera, and R. Mayr.
Deciding bisimulation-like equivalences with finite-state processes.
In Proc. of ICALP'98, number 1443 in Lecture Notes in Computer Science. Springer Verlag, 1998. [gzipped Postscript ]

KH97
A. Kiehn and M. Hennessy.
On the decidability of non-interleaving process equivalences.
Fundamenta Informaticae, 30:23-43, 1997.

Koe99a
B. König.
Description and Verification of Mobile Processes with Graph Rewriting Techniques.
PhD thesis, Technische Universität München, 1999. [gzipped Postscript ]

Koe99b
B. König.
Generating type systems for process graphs.
In Proc. of CONCUR '99, number 1664 in Lecture Notes in Computer Science, pages 352-367. Springer-Verlag, 1999. [gzipped Postscript ]

Koe00b
B. König.
Analysing input/output-capabilities of mobile processes with a generic type system.
In U. Montanari, J. D. P. Rolim, and E. Welzl, editors, Proceedings of the 27th International Conference on Automata, Languages, and Programming, number 1853 in Lecture Notes in Computer Science, pages 403-414. Springer-Verlag, July 2000. [gzipped Postscript ]

Koe00f
B. König.
Analysing input/output-capabilities of mobile processes with a generic type system (extended version).
Technical Report TUM-I0009, Technische Universität München, 2000. [gzipped Postscript ]

Koe00g
B. König.
A general framework for types in graph rewriting.
In Proc. of FST TCS 2000, number 1974 in Lecture Notes in Computer Science, pages 373-384. Springer-Verlag, 2000. [gzipped Postscript ]

Koe00h
B. König.
A general framework for types in graph rewriting.
Technical Report TUM-I0014, Technische Universität München, 2000. [gzipped Postscript ]

Kuc99
A. Kucera.
On finite representations of infinite-state behaviours.
Information Processing Letters, 70(1):23-30, 1999.

KM99b
A. Kucera and R. Mayr.
Simulation preorder on simple process algebras.
In J. Wiedermann, P. van Emde Boas, and M. Nielsen, editors, Proceedings of the 26th International Conference on Automata, Languages, and Programming, number 1644 in Lecture Notes in Computer Science, pages 503-512. Springer-Verlag, July 1999.

KM99a
A. Kucera and R. Mayr.
Weak bisimilarity with infinite-state systems can be decided in polynomial time.
In Proc. of 10th CONCUR, number 1664 in Lecture Notes in Computer Science, pages 368-382. Springer-Verlag, 1999.

Mad97
A. Mader.
Verification of Modal Properties Using Boolean Equation Systems.
PhD thesis, TU München, 1997.

May96
R. Mayr.
Semantic reachability for simple process algebras.
In Proc. of INFINITY'96, number Research Report MIP-9614. University of Passau, 1996. [gzipped Postscript ]

May97
R. Mayr.
Process rewrite systems.
Electronic Notes in Theoretical Computer Science (ENTCS), 7, 1997.
Proceedings of Expressiveness in Concurrency (EXPRESS'97). [gzipped Postscript ]

May98
R. Mayr.
Decidability and Complexity of Model Checking Problems for Infinite-State Systems.
PhD thesis, TU-München, 1998. [gzipped Postscript ]

Roe95
C. Röckl.
Proof tableaux for basic parallel processes.
Technical report, TU München, Dept. of Computer Science, 1995.
Term project. [gzipped Postscript ] [software ]

Roe96b
C. Röckl.
Charakterisierung von Halbordnungssemantiken durch Beweissysteme.
Master's thesis, TU München, Dept. of Computer Science, 1996.
In German. [gzipped Postscript ]

Roe97
C. Röckl.
How to make substitution preserve strong bisimilarity.
SFB-Bericht 342/11/97, TU München, Dept. of Computer Science, 1997. [gzipped Postscript ]

Roe00a
C. Röckl.
Proving write invalidate cache coherence with bisimulations in Isabelle/HOL.
In Proc. of FBT'00, pages 69-78. Shaker, 2000. [gzipped Postscript ]

RE99
C. Röckl and J. Esparza.
Proof-checking protocols using bisimulations.
In J. C. M. Baeten and S. Mauw, editors, Proc. of CONCUR'99, number 1664 in Lecture Notes in Computer Science, pages 525-540. Springer-Verlag, 1999. [gzipped Postscript ]

RS99
C. Röckl and D. Sangiorgi.
A -calculus process semantics of concurrent idealised ALGOL.
In Proc. of FOSSACS'99, number 1578 in Lecture Notes in Computer Science, pages 306-321. Springer-Verlag, 1999. [gzipped Postscript ]

KE99
A. Kucera und J. Esparza.
A logical viewpoint on process-algebraic quotients.
In Proc. of CSL'99, number 1683, pages 499-514. Springer-Verlag, 1999. [gzipped Postscript ]

Links to Related Sites

Formal Models of Concurrency:

Fully Automatic Tools:

Theorem Provers:

Formal Verification in Industry (examples):


Selected References

[Bra92]
J. Bradfield.
Verifying Temporal Properties of Systems.
Birkhäuser, 1992.

[Bro96]
S. Brookes.
The Essence of Parallel Algol.
In P. W. O'Hearn, R. D. Tennent, editors, ALGOL-like Languages. Birkhäuser, 1997.

[Cau92]
D. Caucal.
On the regular structure of prefix rewriting.
Journal of Theoretical Computer Science, 106:61-86, 1992.

[Eme94]
E. A. Emerson.
Temporal and modal logic.
In J. van Leeuwen, editor, Handbook of Theoretical Computer Science: Volume B, Formal Models and Semantics. Elsevier, 1994.

[GS95]
J. F. Groote and J. G. Springintveld
Focus Points and Convergent Process Operators.
Logic Group Preprint Series 142. Dept. of Philosophy, Utrecht University, 1995.

[GS96]
J. F. Groote and J. G. Springintveld
Algebraic Verification of a Distributed Summation Algorithm.
Technical Report CS-R9640. CWI, Amsterdam, 1996.

[HM98]
T. Hardin and B. Mammass.
Proving the Bounded Retransmission Protocol in the Pi-Calculus.
In Proceedings of INFINITY'98, 1998.

[Hir97]
D. Hirschkoff.
A Full Formalisation of π-Calculus Theory in the Calculus of Constructions.
In E. L. Gunter, A. Felty, editors, Proceedings of TPHOL'97, volume 1275 of Lecture Notes in Computer Science, 1997.

[HMS98]
F. Honsell, M. Miculan, and I. Scagnetto
-calculus in (Co)Inductive Type Theory.
Technical Report. Udine University, 1998.

[Mil89]
R. Milner.
Communication and Concurrency
Prentice-Hall, 1998.

[MPW89]
R. Milner, J. Parrow, and D. Walker.
A Calculus of Mobile Processes.
Information and Computation 100:1-77, 1992.

[MB96]
F. Moller and C. Birtwistle, editors.
Logics for Concurrency.
volume 1043 of Lecture Notes in Computer Science. Springer, 1996.

[Mol96]
F. Moller.
Infinite results.
In U. Montanari and V. Sassone, editors, Proceedings of CONCUR'96, volume 1119 of Lecture Notes in Computer Science. Springer, 1996.