---

DAT5/E98 Course for Master Students
in the Formal Methods Group

---

Course Tutor

• Luca Aceto

Project Proposals and Project Supervisors

The following projects are also available:

• Model checking via reachability testing.
• Z-trees. (This link is not yet active!)

• Luca Aceto
• Kim Guldstrand Larsen
• Carsten Weise

International and National Projects

• BRICS
• VHS, a Long Term Research Reactive Scheme (Task 4.2) on the Verification of Hybrid Systems funded by the EEC as Esprit Project 26270.
• Development of Uppaal.
• VVS, Verification and Validation of large State-machines.

Contents of the Course

Part 1: An Automata-Theoretic Approach to LTL

Background References

• Alternating automata and program verification by Moshe Vardi (LNCS Vol. 1000).

• An Automata-Theoretic Approach to Branching-Time Model Checking by O. Bernholtz, Moshe Vardi and P. Wolper (CAV'94 paper).

• Linear vs. Branching Time: A Complexity-Theoretic Perspective (invited LICS'98 paper) by Moshe Vardi.

• M. Dam. ``Temporal Logics, Automata, and Classical Theories - An Introduction''. Lecture Notes for the 6th European Summer School on Logic, Language and Information, 1994.

Other Interesting Links

• The FIDO/MONA Project.
• W. Thomas' Research Group on Automata Theory in Kiel.

Papers for Student Presentations

• Present the material in Sections 2.5, 2.6 and 3 of An automata-theoretic approach to linear temporal logic by Moshe Vardi.

• Mona: Monadic Second-Order Logic in Practice by Klarlund et al.. TACAS '95. The first paper on the implementation of M2L on finite strings. The authors discuss data structures, algorithms, and an application to verification of safety and liveness properties of a parameterized distributed system.

• Alternating Refinement Relations (CONCUR'98 paper by R. Alur, T. Henzinger, O. Kupferman and M. Vardi).

• Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar, Symbolic Model Checking with Rich Assertional Languages in O. Grumberg (Ed.) Proc. CAV'97 , 424-435, LNCS 1254, Springer, 1997. [Abstract and Postscript]

• An Improvement in Formal Verification, by G.J. Holzmann and D. Peled, Proc. FORTE 1994 Conference, Bern, Switzerland. (gzipped postscript.)

• Simple On-the-fly Automatic Verification of Linear Temporal Logic (PSTV'95 paper with coauthors R. Gerth, D. Peled, and P. Wolper).

Part 2: Binary Decision Diagrams

Henrik Reif Andersen. An Introduction to Binary Decision Diagrams. (Version of October 1997 with minor revisions April 1998. 36 pp.)

As supplementary reading, I also strongly recommend the survey article Symbolic Boolean manipulation with ordered binary-decision diagrams by Randal E. Bryant. ACM Computing Surveys, 24(3):293-318, September 1992.

There are several BDD packages available on the web. For example, you might wish to check out the following:

• Jørn Lind-Nielsen's BuDDy package (written in C and featuring both a Mosml- and a C++-interface).
• Fabio Somenzi's comprehensive and efficient CUDD Package.
• Jesper Møller and Christian Østergaard's package with a simple C++ interface
• Geert Janssen's online BDD package.
• The BDD package used in SMV
• Henrik Reif Andersen's ROBDD Package in Standard ML.

Papers for Student Presentations

• J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang, "Symbolic Model Checking: 10^20 states and beyond", Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, Philadelphia, PA, 4-7 June 1990, pp. 428-39.

• Hervé J. Touati, Robert K. Brayton, and Robert Kurshan. Testing language containment for omega-automata using BDD's. Information and Computation, 118(1):101-109, April 1995. (Note: This is a link to the I&C; page for this paper. A hard copy of this work will be made available for photocopying.)

• Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kåre Kristoffersen, Kim G. Larsen Verification of Large State/Event Systems using Compositionality and Dependency Analysis. Appears in Proceedings of TACAS'98, Bernhard Steffen (ed), LNCS 1384, April 1998. Springer-Verlag. NOTE: The technique described in this paper is being patented by Baan Visualstate (formerly Beologic), which has all commercial rights.

• Henrik Reif Andersen and Henrik Hulgaard. Boolean Expression Diagrams. In Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29-July 2, 1997, pp. 88-98. IEEE Computer Society.

Part 3: Timed and Hybrid Automata

Background References

• R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science 126:183-235, 1994 (preliminary versions appeared in Proc. 17th ICALP, LNCS 443, 1990, and < i>Real Time: Theory in Practice, LNCS 600, 1991). Abstract. Full paper. (This is the seminal paper on timed automata, and will be our main reference dur ing this part of the course.)

• R. Alur and D. L. Dill. Automata-theoretic verification of real-time systems. In Formal Methods for Real-Time Computing, Trends in Software Series, John Wiley & Sons Publishers, pp. 55-82, 1996. Abstract. Full paper.

Ian Parberry's Speaker's Guide

This page will be actively modified over the autumn term 1998. You are invited to check it regularly.