Lecturer: 蔡益坤 Yih-Kuen Tsay

• Lecture 1: Automata-Based Model Checking (3 hours)
  • Büchi automata, generalized Büchi automata, model checking using automata, intersection and emptiness test, parallel compositions, on-the-fly state exploration, fairness, the SPIN model checker
• Lecture 2: Linear Temporal Logic and Büchi Automata (3 hours)
  • propositional temporal logic, past temporal operators, translation algorithms, classification of temporal properties, quantified propositional temporal logic, expressiveness, equivalences, congruences

• Automata-Based Model Checking [slides]
• Linear Temporal Logic and Büchi Automata [slides] [example: PTL to GBA]
• Suggested solutions to homework assignment

• 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.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking, The MIT Press, 1999.
• E.A. Emerson. Temporal and modal logic, Handbook of Theoretical Computer Science (Vol. B), MIT Press, 1990.
• G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, 2003.
• Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer, 1992.
• Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety, Springer, 1995.
• W. Thomas. Automata on infinite objects, Handbook of Theoretical Computer Science (Vol. B), 1990.
• M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification, in LICS 1986.