Verification of finite state systems with temporal logic model checking

Abstract

These tutorial notes contain an introduction to the logical theory and computational aspects of computer aided verification of finite state reactive systems with linear and branching temporal logic model checking. As a general recipe, computer science applications and algorithms are derived from logical notions and proofs. First, the expressivity of various temporal logics is compared to first and second order logic, and to w-automata and formal languages. Then, temporal safety and liveness properties are reviewed. From the completeness proof for natural and tree models, local and global decision procedures are developed. These in turn give rise to the corresponding model checking procedures. Various modelling techniques for reactive systems are presented. Finally, symbolic techniques for global model checking with binary decision diagrams, and partial order techniques for local model checking with stubborn sets are discussed.