Lecturer: Bow-Yaw Wang 王柏堯

This module introduces basic model checking theory.

discrete mathematics and algorithms

• Slides (revised)

• 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