Model Checking, Temporal Logic, and Automata Theory

Lecturer: Bow-Yaw Wang 王柏堯

This module introduces basic model checking theory.

Prerequisites

discrete mathematics and algorithms

Course Material

Syllabus

  • 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

References

  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