Automata-Theoretic Model Checking


  • 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


  • 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.
zh-tw/lecture/automata.txt · 上一次變更: 2011/04/29 04:49 來自 mht208