Linked e-resources
Details
Table of Contents
Intro; Handbook of Model Checking; Foreword; Preface; Acknowledgements; Contents; Contributors; Chapter 1: Introduction to Model Checking; 1.1 The Case for Computer-Aided Veri cation; 1.2 Temporal-Logic Model Checking in a Nutshell; 1.2.1 Kripke Structures; 1.2.2 The Temporal Logic CTL; 1.2.3 The Temporal Logic CTL; 1.2.4 The Temporal Logic LTL; 1.3 A Very Brief Guide Through the Chapters of the Handbook; 1.3.1 The Algorithmic Challenge; 1.3.2 The Modeling Challenge; 1.4 The Future of Model Checking; References; Chapter 2: Temporal Logic and Fair Discrete Systems; 2.1 Introduction
2.2 Fair Discrete Systems2.2.1 Kripke Structures; 2.2.2 De nition of Fair Discrete System; 2.2.3 Representing Programs; 2.2.4 Algorithms; 2.3 Linear Temporal Logic; 2.3.1 De nition of Linear Temporal Logic; 2.3.2 Safety Versus Liveness and the Temporal Hierarchy; 2.3.3 Extensions of LTL; 2.3.4 Temporal Testers, Satis ability, and Model Checking; 2.4 Computation Tree Logic; 2.4.1 De nition of Computation Tree Logic; 2.4.2 Extensions; 2.4.3 Model Checking and Satis ability; 2.5 Examples for LTL and CTL; 2.5.1 Invariance and Safety; 2.5.2 Liveness; 2.5.3 Additional Examples; 2.6 CTL*
2.6.1 Branching vs. Linear Time2.6.2 CTL* De nition; 2.6.3 Examples of Usage of CTL*; 2.6.4 Model Checking and Satis ability; References; Chapter 3: Modeling for Veri cation; 3.1 Introduction; 3.2 Major Considerations in System Modeling; 3.2.1 Selecting a Modeling Formalism and Language; 3.2.1.1 Type of System; 3.2.1.2 Type of Property; 3.2.1.3 Modeling the Environment; 3.2.1.4 Level of Abstraction; 3.2.1.5 Clarity and Modularity; 3.2.1.6 Form of Composition; 3.2.1.7 Computational Engines; 3.2.1.8 Practical Ease of Modeling and Expressiveness; 3.2.2 Modeling Languages
3.2.3 Challenges in Modeling3.2.4 Scope of This Chapter; 3.3 Modeling Basics; 3.3.1 Syntax; 3.3.2 Dynamics; 3.3.3 Modeling Concepts; 3.4 Examples; 3.4.1 Synchronous Circuits; 3.4.1.1 Router Design; 3.4.1.2 Simpli cations and sml Model; 3.4.1.3 Veri cation Task: Progress Through the Router; 3.4.1.4 Data Type Abstraction; 3.4.1.5 Environment Modeling; 3.4.1.6 Summary; 3.4.2 Synchronous Control Systems; 3.4.3 Concurrent Software; 3.5 Kripke Structures; 3.5.1 Transition Systems; 3.5.2 From sml Programs to Kripke Structures; 3.6 Summary; References; Chapter 4: Automata Theory and Model Checking
4.1 Introduction4.2 Nondeterministic Büchi Automata on In nite Words; 4.2.1 De nitions; 4.2.2 Closure Properties; 4.2.2.1 Closure Under Union and Intersection; 4.2.2.2 Closure Under Complementation; 4.2.3 Determinization; 4.3 Additional Acceptance Conditions; 4.3.1 Translations Among the Different Classes; 4.3.1.1 Translations Among the Different Conditions; 4.3.1.2 Typeness; 4.3.1.3 Translations That Require a New State Space; 4.3.2 Determinization of NBWs; 4.4 Decision Procedures; 4.5 Alternating Automata on In nite Words; 4.5.1 De nition; 4.5.2 Closure Properties; 4.5.3 Decision Procedures
2.2 Fair Discrete Systems2.2.1 Kripke Structures; 2.2.2 De nition of Fair Discrete System; 2.2.3 Representing Programs; 2.2.4 Algorithms; 2.3 Linear Temporal Logic; 2.3.1 De nition of Linear Temporal Logic; 2.3.2 Safety Versus Liveness and the Temporal Hierarchy; 2.3.3 Extensions of LTL; 2.3.4 Temporal Testers, Satis ability, and Model Checking; 2.4 Computation Tree Logic; 2.4.1 De nition of Computation Tree Logic; 2.4.2 Extensions; 2.4.3 Model Checking and Satis ability; 2.5 Examples for LTL and CTL; 2.5.1 Invariance and Safety; 2.5.2 Liveness; 2.5.3 Additional Examples; 2.6 CTL*
2.6.1 Branching vs. Linear Time2.6.2 CTL* De nition; 2.6.3 Examples of Usage of CTL*; 2.6.4 Model Checking and Satis ability; References; Chapter 3: Modeling for Veri cation; 3.1 Introduction; 3.2 Major Considerations in System Modeling; 3.2.1 Selecting a Modeling Formalism and Language; 3.2.1.1 Type of System; 3.2.1.2 Type of Property; 3.2.1.3 Modeling the Environment; 3.2.1.4 Level of Abstraction; 3.2.1.5 Clarity and Modularity; 3.2.1.6 Form of Composition; 3.2.1.7 Computational Engines; 3.2.1.8 Practical Ease of Modeling and Expressiveness; 3.2.2 Modeling Languages
3.2.3 Challenges in Modeling3.2.4 Scope of This Chapter; 3.3 Modeling Basics; 3.3.1 Syntax; 3.3.2 Dynamics; 3.3.3 Modeling Concepts; 3.4 Examples; 3.4.1 Synchronous Circuits; 3.4.1.1 Router Design; 3.4.1.2 Simpli cations and sml Model; 3.4.1.3 Veri cation Task: Progress Through the Router; 3.4.1.4 Data Type Abstraction; 3.4.1.5 Environment Modeling; 3.4.1.6 Summary; 3.4.2 Synchronous Control Systems; 3.4.3 Concurrent Software; 3.5 Kripke Structures; 3.5.1 Transition Systems; 3.5.2 From sml Programs to Kripke Structures; 3.6 Summary; References; Chapter 4: Automata Theory and Model Checking
4.1 Introduction4.2 Nondeterministic Büchi Automata on In nite Words; 4.2.1 De nitions; 4.2.2 Closure Properties; 4.2.2.1 Closure Under Union and Intersection; 4.2.2.2 Closure Under Complementation; 4.2.3 Determinization; 4.3 Additional Acceptance Conditions; 4.3.1 Translations Among the Different Classes; 4.3.1.1 Translations Among the Different Conditions; 4.3.1.2 Typeness; 4.3.1.3 Translations That Require a New State Space; 4.3.2 Determinization of NBWs; 4.4 Decision Procedures; 4.5 Alternating Automata on In nite Words; 4.5.1 De nition; 4.5.2 Closure Properties; 4.5.3 Decision Procedures