 |
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
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:
 |
 |
| Branching-time logics |
Linear-time 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 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.
|
|
bk) |
© Universität Stuttgart |
Impressum