Instructor: Yih-Kuen Tsay 蔡益坤

This lecture series covers the basics, including fundamental properties and algorithms, of various kinds of ω-automata (which are finite automata over infinite words) and linear temporal logic (in particular variants with past temporal operators and quantifiers).

Elementary Logic and Automata Theory

• Büchi Automata and Model Checking
  1. Büchi and generalized Büchi automata
  2. Automata-based model checking
  3. Basic algorithms: intersection and emptiness test
• Linear Temporal Logic and Büchi Automata
  1. Propositional Temporal Logic (PTL)
  2. Quantified Propositional Temporal Logic (QPTL)
  3. Basic properties of PTL/QPTL
  4. From temporal formulae to automata
• Büchi Complementation
  1. Why is Büchi complementation hard?
  2. Complementation via determinization: Muller-Schupp, Safra, and Safra-Piterman
  3. Other approaches

• Büchi Automata and Model Checking [slides for print] [slides for display]
• Linear Temporal Logic and Büchi Automata [slides for print] [slides for display]
• Büchi Complementation [slides for print] [slides for display]

ω-Automata

• J.R. Büchi. On a decision method in restricted second-order arithmetic, in Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science, Stanford University Press, 1962.
• E. Grädel, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games (LNCS 2500), Springer, 2002.
• O. Kupferman and M.Y. Vardi. Weak alternating automata are not that weak, ACM Transactions on Computational Logic, 2(3):408–429, 2001.
• D.E. Muller and P.E. Schupp, Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra, Theoretical Computer Science, 141:69-107, 1995.
• N. Piterman. From nondeterministic Buechi and Streett automata to deterministic parity automata, LICS 2006, Pages 255-264.
• S. Safra. On the Complexity of ω-automta, FOCS 1988, Pages 319-327.
• C. Schulte Althoff, W. Thomas, and N. Wallmeier. Observations on determinization of Büchi automata, Theoretical Computer Science, 363: 224-233, 2006.
• A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic, Theoretical Computer Science, 49:217-237, 1987.
• W. Thomas. Automata on infinite objects, Handbook of Theoretical Computer Science (Vol. B), 1990.

Linear Temporal Logic

• E.A. Emerson. Temporal and modal logic, Handbook of Theoretical Computer Science (Vol. B), 1990.
• Y. Kesten and A. Pnueli. Complete proof system for QPTL, Journal of Logic and Computation, 12(5):701-745, 2002.
• Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
• Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.

Model Checking

• E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking, The MIT Press, 1999.
• G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, 2003.
• K. Schneider. Verification of Reactive Systems: Formal Methods and Algorithms, Springer-Verlag, 2004.