Model Checking, Temporal Logic, and Automata Theory

Lecturer: Bow-Yaw Wang 王柏堯

This module introduces basic model checking theory.


discrete mathematics and algorithms

Course Material


  • model of computation, formal verification
  • finite-state automata, finite-state omega-automata
  • linear temporal logic, computational tree logic, mu-calculus
  • automata-theoretic approach, explicit-state algorithm, implicit-state algorithm


  1. Model Checking. E. M. Clarke, Jr., O. Grumberg, and D. A. Peled
  1. Introduction to Automata THeory, Languages, and Computation. Hopcroft and Ullman

Creative Commons License Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki