Model Checking: Theory and Practice

Lecture Slides
  • Omega automata
  • Monadic logic and decidability
  • Temporal Logics CTL* , CTL and LTL
  • Explicit State Model Checking of CTL and LTL
  • Symbolic Model Checking
  • Timed Automata: Theory and Practice

  • Reading Assignment

  • Tutorial on MONA and its applications
  • Mona User Manual

  • Reading Material

    1. Wolfgang Thomas. Languages, Automata, and Logic. Manuscript, May 1996.
    2. Wolfgang Thomas Handbook of TCS article
    3. Madhavan Automata tutorial
    4. Madhavan TL model checking tutorial
    5. Ken McMillan: Book
    6. Alur Dill: TCS article
    7. Alur Henzinger: Survey of Real-time logics
    8. Larsen: Uppal papers
    9. Hybrid automata paper: TCS 138



      Some papers of M. Vardi:

      R. Kaivola, Using Automata to Characterise Fixed Point Temporal Logics, PhD thesis, University of Edinburgh, Dept. of Computer Science, Report CST-135-97, April 1997.

      A. Mader, Verification of Modal Properties Using Boolean Equation Systems, PhD thesis, Fakultät für Informatik, Technische Universität München, September 1997.
      Some papers of A. Arnold:

      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 (1995), 69-107.