Automata-Theoretic Model Checking
Lecturer: 蔡益坤 Yih-Kuen Tsay
Syllabus
- 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
Course Materials
- Automata-Based Model Checking [slides]
- Linear Temporal Logic and Büchi Automata [slides] [example: PTL to GBA]
References
- 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.