Handbook of Automated Reasoning

Chapter 24

Model Checking

Edmund M. Clarke

Bernd-Holger Schlingloff

Contents

1  Introduction   1637

2  Logical Languages, Expressiveness   1641

2.1  Prepositional and First Order Logic   1642

2.2  Multimodal and Temporal Logic   1644

2.3  Expressive Completeness of Temporal Logic   1648

3  Second Order Languages   1654

3.1  Linear and Branching Time Logics   1654

3.2  Propositionally Quantified Logics   1656

3.3  ω-automata and ω-languages   1665

3.4  Automata and Logics   1668

4  Model Transformations and Properties   1670

4.1  Models, Automata and Transition Systems   1671

4.2  Safety and Liveness Properties   1673

4.3  Simulation Relations   1676

5  Equivalence reductions   1681

5.1  Bisimulations ...