Handbook of Model Checking

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 Systems

2.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 Time

2.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 Modeling

3.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 Introduction

4.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

4.6 Automata-Based Algorithms

4.6.1 Translating LTL to Büchi Automata

4.6.1.1 A Translation via ABWs

4.6.1.2 A Direct Translation to NBWs

4.6.1.3 The Blow-up in the LTL to NBW Translation

4.6.2 Model Checking and Satis?ability

References

Chapter 5: Explicit-State Model Checking

5.1 Introduction

5.1.1 The Importance of Abstraction

5.2 Basic Search Algorithms

5.3 Linear Temporal Logic

5.4 Omega Automata

5.5 Nested Depth-First Search

5.6 Abstraction

5.6.1 Tic-Tac-Toe

5.7 Model-Driven Veri?cation

5.8 Incomplete Storage

5.8.1 Bitstate Hashing and Bloom Filters

5.9 Extensions

5.10 Synopsis

References

Chapter 6: Partial-Order Reduction

6.1 Introduction

6.2 Partial Order Reduction

Reduction for LTL

On-the-Fly Model Checking

Reduction for CTL

Reduction for Process Algebra

Reducing Visibility

6.3 Reducing Edges While Preserving States

Sleep Sets

Trace Normal Form

Edge Lean Algorithm

6.4 Conclusions

References

Chapter 7: Binary Decision Diagrams

7.1 Introduction

7.2 Terminology

7.3 A Boolean Function API

7.4 OBDD Representation

7.5 Implementing OBDD Operations

7.6 Implementation Techniques

7.7 Variable Ordering and Reordering

7.8 Variant Representations

7.9 Representing Non-Boolean Functions

7.10 Scaling OBDD Capacity

Comparison to SAT Checking

7.11 Concluding Remarks

References

Chapter 8: BDD-Based Symbolic Model Checking

8.1 Introduction

8.2 Preliminaries

8.3 Binary Decision Diagrams: The Basics

8.3.1 Representing Sets and Relations

8.3.1.1 Characteristic Function

8.3.1.2 Representing Sets

8.3.1.3 Representing Relations

8.3.2 Image Computation

8.3.3 Partitioned Transition Relation

8.3.3.1 Disjunctive Decomposition

8.3.3.2 Conjunctive Decomposition

8.3.4 Historical Perspective

8.4 Model Checking Kripke Structures

8.4.1 Reachability/Invariant/AG

8.4.2 CTL Model Checking

8.4.3 Fair CTL Model Checking

8.4.3.1 Function egFairStates

8.4.3.2 Function ctlFairStates

8.4.4 LTL Model Checking

8.4.4.1 Restricted Path Formula

8.4.4.2 Algorithm ltlTableau

8.5 Push-Down Symbolic Model Checking

8.6 Conclusion

References

Chapter 9: Propositional SAT Solving

9.1 Introduction

9.2 Preliminaries

9.3 CDCL SAT Solvers: Organization

9.4 CDCL SAT Solvers

9.4.1 Clause Learning and Non-chronological Backtracking

9.4.2 Unique Implication Points

9.4.3 Learned Clause Minimization

9.4.4 Lazy Data Structures

9.4.5 Search Restarts

9.4.6 Lightweight Branching Heuristics

9.4.7 Additional Techniques and Recent Trends

9.5 SAT-Based Problem Solving

9.5.1 Incremental SAT

9.5.2 Unsatis?able Cores

9.5.3 CNF Encodings

9.5.4 Optimization

9.5.5 Model Enumeration

9.5.6 Minimal Sets

9.5.7 Quanti?cation

9.6 Research Directions

References

Chapter 10: SAT-Based Model Checking

10.1 Introduction

10.2 Bounded Model Checking on Kripke Structures

10.2.1 Kripke Structures

10.2.2 Safety Properties

10.2.3 Liveness Properties

10.2.3.1 Liveness to Safety Translation

10.2.3.2 k-Liveness

10.3 Bounded Model Checking for Hardware Designs

10.3.1 Hardware Description Languages (HDLs)

10.3.2 BMC on Net-Lists

10.4 Bounded Model Checking for Software

10.4.1 Monolithic Encodings

10.4.2 Path-Based Encodings

10.4.3 Completeness for Bounded Programs

10.4.4 BMC for Multi-threaded Programs

10.4.5 Bounded Model Checking for HW/SW Co-veri?cation

10.5 Encodings into Propositional SAT

10.5.1 Encoding Bit Vectors

10.5.2 Encoding Memory

10.5.3 Encodings with Under- and Over-approximation

10.6 Complete Model Checking with SAT

10.6.1 Completeness Thresholds

10.6.2 Image Computation with SAT

10.6.3 Basic Inductive Techniques

10.6.3.1 Strengthening the Inductive Argument

10.6.3.2 Equivalence Reasoning

10.6.3.3 Temporal Decomposition

10.6.3.4 k-Induction

10.6.4 Craig Interpolation

10.6.5 Iterative Inductive Strengthening

10.7 Abstraction Techniques Using SAT

10.7.1 Overview of Predicate Abstraction

10.7.2 Computing Abstractions with SAT

10.7.3 Simulation with SAT

10.7.4 Abstraction-Based Tools

10.8 Outlook and Conclusions

References

Chapter 11: Satis?ability Modulo Theories

11.1 Introduction

11.1.1 Technical Preliminaries

11.2 SMT in Model Checking

11.3 The Lazy Approach to SMT

11.3.1 A Basic Lazy SMT Solver

11.3.2 SAT Engine and Theory Solver Features

11.3.3 A General Framework and Architecture

11.4 Theory Solvers for Speci?c Theories

11.4.1 Uninterpreted Function Symbols

11.4.2 Real Arithmetic

11.4.3 Integer Arithmetic

11.4.4 Mixed Integer and Real Arithmetic

11.4.5 Difference Logic

11.4.6 Bit Vectors

11.4.7 Arrays

11.4.8 Other Theories

11.5 Combining Theory Solvers

11.5.1 A Basic Combination Method

11.5.2 Combination Variants and Extensions

11.6 SMT Solving Extensions and Enhancements

11.7 Eager Encodings to SAT

11.8 Additional Functionalities of SMT Solvers

References

Chapter 12: Compositional Reasoning

12.1 Introduction

12.2 Reasoning with Assertions

12.2.1 The (Non-compositional) Owicki-Gries Method

12.2.2 The Assume-Guarantee View: Localized Inductive Invariants

12.2.2.1 The Shared-Variable Program Model

A Note on Notation

Invariant Assertions

12.2.2.2 Split Invariants

12.2.3 Computing the Strongest Split Invariant

Split Invariance for N Processes

12.2.4 Relationship to Rely-Guarantee

12.2.5 Completeness Issues

12.2.6 Deadlock Detection with Local Invariants

12.2.7 Local Proofs for Termination, Temporal Properties, and Fairness

12.2.7.1 Background

12.2.7.2 Local Proof Rules for Liveness Properties

12.2.8 Algorithms for Local Analysis of Temporal Properties

12.2.9 Automating the Discovery of Auxiliary Variables

12.2.10 Local Symmetry

12.2.11 Further Reading

12.3 Automata-Based Assume-Guarantee Reasoning

12.3.1 Formalisms

12.3.1.1 Finite-State Machines

12.3.1.2 Parallel Composition of FSMs

12.3.1.3 Properties

12.3.1.4 Complementation

12.3.2 Assume-Guarantee Reasoning

12.3.2.1 Assume-Guarantee Triples

12.3.2.2 Weakest Assumption

12.3.2.3 Basic Assume-Guarantee Rule

Rule ASym

12.3.2.4 Soundness and Completeness

12.3.3 Automation of Basic Assume-Guarantee Rule

12.3.3.1 The L* algorithm

12.3.3.2 Learning-Based Assumption Generation

12.3.3.3 Correctness Arguments

12.3.4 Example

12.3.5 Additional Assume-Guarantee Rules and Their Automation

Rule ASymN

Rule Circ-0

Rule Sym

Rule SymN

Rule Circ

Rule Circ-Ind

12.4 Related Approaches

12.4.1 Learning for Compositional Veri?cation

12.4.2 Assumption Generation by Abstraction-Re?nement

12.4.3 Components and Interfaces

12.4.4 Other Modular Reasoning Frameworks

12.5 Conclusion

References

Chapter 13: Abstraction and Abstraction Re?nement

13.1 Introduction

13.2 Preliminaries

13.2.1 Abstraction Frameworks

13.2.2 Kripke Structures

13.2.3 The µ-Calculus

13.2.3.1 Some Notes on the Difference Between Lµ and CTL/CTL*

13.3 Simulation and Bisimulation Relations

13.3.1 Simulation Relation

13.3.2 Bisimulation Relation

13.3.3 Additional Reading

13.4 Abstraction Based on Simulation

13.4.1 Existential Abstraction

13.4.1.1 Speci?c Abstractions: Examples

13.4.2 Additional Reading

13.5 CounterExample-Guided Abstraction Re?nement (CEGAR)

13.5.1 The CEGAR Framework

13.5.1.1 Identifying Spurious Path Counterexamples

13.5.2 Additional Reading

13.6 Abstraction Based on Modal Simulation

13.6.1 A Three-Valued Setting

13.6.2 Re?nement

13.6.3 Additional Reading

13.7 Completeness

13.7.1 Additional Reading

References

Chapter 14: Interpolation and Model Checking

14.1 Introduction

14.2 Preliminaries

14.3 Model of Abstraction Re?nement

14.3.1 A Simple Programming Language and Proof System

14.3.2 The Abstractor

14.3.3 The Re?ner

14.4 Re?nement, Local Proofs, and Interpolants

14.4.1 Craig Interpolation

14.4.2 Feasible Interpolation in Model Checking

14.4.3 Interpolants and Local Proofs

14.5 Re?ners as Local Proof Systems

14.5.1 Strongest Post-condition

14.5.2 Weakest Pre-condition

14.5.3 Bounded Provers

14.5.4 Split Provers and Language Strati?cation

14.5.5 Constraint-Based Interpolation

14.5.6 Feasible Interpolation and Re?nement

14.5.7 Improving Interpolants

14.6 Abstractors as Proof Generalizers

14.7 Summary

References

Chapter 15: Predicate Abstraction for Program Veri?cation

15.1 Introduction

15.2 De?nitions

15.2.1 Programs

15.2.2 Correctness: Safety and Termination

15.3 Characterizing Correctness via Reachability

15.3.1 Safety and Reachability

15.3.2 Termination and Binary Reachability

15.4 Characterizing Correctness via Inductiveness

15.4.1 Safety and Closure Under post

15.4.2 Termination and Transitive Closure

15.5 Abstraction

15.5.1 Safety and Predicate Abstraction

15.5.2 Termination and Transition Predicate Abstraction

15.6 Abstraction Re?nement

15.6.1 Re?nement of Predicate Abstraction

15.6.2 Re?nement of Transition Predicate Abstraction

15.7 Solving Re?nement Constraints for Predicate Abstraction

15.7.1 Least Solution

15.7.2 Greatest Solution

15.7.3 Intermediate Solution Using Interpolation

15.8 Tools

15.9 Conclusion

References

Chapter 16: Combining Model Checking and Data-Flow Analysis

16.1 Introduction

16.2 General Considerations

16.2.1 Type Checking

16.2.2 Data-Flow Analysis

16.2.3 Model Checking

16.3 Unifying Formal Framework/Comparison of Algorithms

16.3.1 Preliminaries

16.3.2 Algorithm of Data-Flow Analysis

16.3.3 Algorithm of Model Checking

16.3.4 Uni?ed Algorithm Using Con?gurable Program Analysis

16.3.5 Discussion

16.3.6 Composition of Con?gurable Program Analyses

16.4 Classic Examples (Component Analyses)

16.4.1 Reachable-Code Analysis

16.4.2 Constant Propagation

16.4.3 Reaching De?nitions

16.4.4 Predicate Analysis

16.4.5 Explicit-Heap Analysis

16.4.6 BDD Analysis

16.4.7 Observer Automata

16.5 Combination Examples (Composite Analyses)

16.5.1 Predicate Analysis + Constant Propagation

16.5.2 Predicate Analysis + Constant Propagation + Strengthen

16.5.3 Predicate Analysis + Explicit-Heap Analysis

16.5.4 Predicate Analysis + Observer Automata

16.6 Algorithms for Constructing Program Invariants

16.6.1 Iterative and Monotonic Fixed-Point Approaches

16.6.2 Counterexample-Guided Abstraction Re?nement

16.6.3 Template- and Constraint-Based Approaches

16.6.4 Proof-Rule-Based Approaches

16.6.5 Iterative, but Non-monotonic Approaches

16.6.6 Comparison with Standard Recurrence Solving

16.6.7 Discussion

16.7 Combinations in Tool Implementations

16.8 Conclusion

References

Chapter 17: Model Checking Procedural Programs

17.1 Introduction

17.2 Models of Procedural Programs

17.2.1 (Extended) Recursive State Machines

17.2.2 Pushdown Systems

17.2.3 From RSMs to PDSs

17.3 Basic Veri?cation Algorithms

17.3.1 The State Reachability Problem: Computing Summaries

17.3.2 The Fair Computation Problem

17.3.3 The Con?guration Reachability Problem: Saturating Automata

17.3.3.1 Computing pre*(C) for a Regular Set C by Saturation

17.3.3.2 Computing post*(C) for a Regular Set C by Saturation

17.3.4 The Generalized Fair Computation Problem

17.4 Specifying Requirements

17.4.1 Nested Words

17.4.2 Nested Word Automata

17.4.2.1 RSMs as NWAs

17.4.2.2 NWAs for Requirements

17.4.2.3 Closure Properties

17.4.2.4 Decision Problems

17.4.2.5 MSO Equivalence

17.4.3 Temporal Logics

17.4.3.1 Abstract Next

17.4.3.2 Abstract Paths

17.4.3.3 Summary Paths

17.4.3.4 Model Checking

17.5 Bibliographical Remarks

17.5.1 Summarization

17.5.2 Saturation

17.5.3 Temporal Logic Model Checking

References

Chapter 18: Model Checking Concurrent Programs

18.1 Introduction

18.2 Concurrent System Model and Notation

18.2.1 Synchronization and Communication

18.2.2 Speci?cation Logic

18.2.3 Interacting Pushdown System (PDS) Model

18.3 PDS-Based Model Checking: Synchronization Patterns

18.3.1 Programs with Nested Locks

18.3.1.1 Pair-wise Reachability for Nested Locks

18.3.1.2 Model-Checking Programs with Nested Locks

18.3.2 Programs with Locks: Lock Causality Graph

18.3.3 Programs with Bounded Lock Chains

18.3.4 Discussion: Lock Patterns

18.3.5 Programs with Rendezvous

18.3.5.1 Computing Over-approximations of Path Languages

18.3.5.2 De?ning Re?nable Finite-Chain Abstractions

18.3.5.3 Checking Whether the Counterexample Is Spurious

18.3.5.4 The Semi-decision Procedure

18.4 PDS-Based Model-Checking: Communication Patterns

18.4.1 Reasoning About Programs with State Observation

18.4.1.1 Symbolic Representation of PDN Con?gurations

18.4.1.2 Reachability Analysis of PDNs

18.4.2 Multiphase Acyclic Pushdown Networks

18.4.2.1 The Reachability Problem for MAPNs

18.4.2.2 For MAPNs

18.4.2.3 A Semi-algorithm for k-Bounded Reachability for MAPNs

18.4.2.4 A Semi-algorithm for the Reachability Problem for General PDNs

18.4.3 Threads Communicating via Lossy Channels

18.5 Other Models: Finite State Systems and Sequential Programs

18.5.1 Partial-Order Reduction

18.5.2 Symbolic Reasoning with Memory Consistency Constraints

18.5.3 Concurrent Data?ow Analysis and Invariant Generation

18.5.4 Trace-Based Dynamic Model-Checking

18.5.5 Other Related Techniques

References

Chapter 19: Combining Model Checking and Testing

19.1 Introduction

19.2 Systematic Testing of Concurrent Software

19.2.1 Classical Model Checking

19.2.2 Software Model Checking Using a Dynamic Semantics

19.2.3 Systematic Testing with a Run-Time Scheduler

19.2.4 Stateless vs. Stateful Search

19.2.5 Systematic Testing for Multi-threaded Programs

19.2.6 Tools and Applications

19.3 Systematic Testing of Sequential Software

19.3.1 Classical Symbolic Execution

19.3.2 Static Test Generation

19.3.3 Dynamic Test Generation

19.3.4 Systematic Dynamic Test Generation

19.3.5 Strengths and Limitations

19.3.6 Tools and Applications

19.4 Systematic Testing of Concurrent Software with Data Inputs

19.4.1 Example

19.4.2 Comparison with Related Work

19.5 Other Related Work

19.6 Conclusion

References

Chapter 20: Combining Model Checking and Deduction

20.1 Introduction

20.2 Logic Background

20.2.1 Propositional Logic

20.2.2 First-Order Logic

20.2.3 Higher-Order Logic

20.2.4 PVS: Computation and Deduction

20.2.5 Hoare Logic

20.3 Deduction and Model Checking

20.3.1 Abstract Interpretation

20.3.2 Symbolic Model Checking

20.3.3 Predicate Abstraction

20.3.4 Bounded Model Checking and k-Induction

20.3.5 Symbolic Execution and Test Generation

20.3.6 Interpolation-Based Model Checking

20.3.7 Con?ict-Directed Reachability

20.4 Conclusions

References

Chapter 21: Model Checking Parameterized Systems

21.1 Introduction

21.2 Petri Nets

21.2.1 Simple Protocol

21.2.2 Petri Nets

21.2.3 Safety Properties

21.2.4 Backward Reachability Analysis

21.2.5 Liveness Properties

21.3 Regular Model Checking

21.3.1 Near-Neighbor Communication

21.3.2 Regular Model Checking

21.3.3 Acceleration Techniques

Safety Properties

Column Transducer

Quotienting

Example

21.4 Monotonic Abstraction

21.4.1 Example

21.4.2 Model

21.4.3 Over-Approximation

21.4.4 Backward Reachability Algorithm

21.5 Compositional Reasoning for Parameterized Veri?cation

21.5.1 Parameterized Protocols

Index Variables

States

Expressions

Assignments

Rules

Protocols

Safety Properties

21.5.2 The CMP Method

21.5.2.1 German's Protocol

21.5.2.2 Abstraction

21.5.2.3 Strengthening

21.5.2.4 Correctness

21.5.3 Evolution of the CMP Method

21.5.4 Applications

21.6 Related Work

References

Chapter 22: Model Checking Security Protocols

22.1 Introduction

22.2 History

22.3 Formal Model

22.3.1 Notational Preliminaries

22.3.2 Terms and Events

22.3.3 Protocols and Threads

22.3.4 Initial Adversary Knowledge

22.3.5 Execution Model

22.3.6 Property Speci?cation

22.3.7 Alternatives

22.4 Issues in Developing Model-Checking Algorithms for Security Protocols

22.4.1 Forward Versus Backward Search

22.4.2 Bounded Instances

22.4.3 Representing States

22.4.4 Partial-Order Reduction

22.4.5 Handling Equations

22.5 Systems and Algorithms

22.5.1 NPA and Maude-NPA

22.5.2 AVISPA and Related Tools

22.5.3 Athena, Scyther, and Tamarin

22.5.4 ProVerif

22.6 Research Problems

22.6.1 Link to Computational Soundness

22.6.2 Corruption Models

22.6.3 Channel Properties

22.6.4 Other Properties, Including Non-trace Properties

22.6.5 Probabilities

22.7 Conclusions

References

Chapter 23: Transfer of Model Checking to Industrial Practice

23.1 Introduction

23.1.1 Anything Worth Inventing Is Worth Reinventing

23.1.2 The Interplay Between Theory and Application

23.2 The Technology Transfer Problem

23.2.1 Initial Challenges

23.2.2 Barriers to Technology Transfer

23.2.3 Methodological Differences and New Potential Bene?ts

23.2.4 The Cost of Writing Properties vs. a Test Bench

23.2.5 Settling on a Scope for Model Checking

23.2.6 The First Commercial Successes

23.2.7 The Essentiality of Being Able to Compare Tools

23.2.8 In Summary

23.3 False Starts

23.4 A Framework for Technology Transfer

23.5 Formal Functional Veri?cation in Commercial Use Today

23.6 Algorithms

23.7 Future

23.8 Conclusion

References

Chapter 24: Functional Speci?cation of Hardware via Temporal Logic

24.1 Introduction

24.2 From LTL to Regular-Expression-Based Temporal Logic

24.2.1 Adding Expressive Power-Suf?x Implication

24.2.2 Adding Succinctness

24.2.2.1 Counting

24.2.2.2 First Match

24.2.2.3 Intersection

24.2.2.4 Fusion

24.2.2.5 Past Operators

24.2.3 Distinguishing Between Weak and Strong Regular Expressions

24.3 Clocks and Sampling

24.3.1 Hardware Clocks

24.3.2 Using a Clock as a Time-Sampling Abstraction

24.4 Hardware Resets and Other Sources of Truncated Paths

24.4.1 Hardware Resets

24.4.2 Other Sources of Truncated Paths

24.4.3 The Truncated Semantics and Classi?cation of Safety Formulas

24.5 The Simple Subset

24.6 Quanti?ed and Local Variables

24.6.1 Quanti?ed Variables

24.6.2 Local Variables

24.7 Summary and Open Issues

24.7.1 One-to-One Correspondence

24.7.2 Triggering Procedural Code from Within a Formula

24.7.3 Separation of Concerns

References

Chapter 25: Symbolic Trajectory Evaluation

25.1 Introduction

25.2 Notational Preliminaries

25.3 Sequential Circuit Models in STE

25.3.1 States and Sequences

25.3.2 Abstraction

25.3.3 Time-Dependent Behaviour

25.3.4 The Next State Function and Trajectories

25.4 Trajectory Evaluation Logic

25.4.1 Correctness Properties for Veri?cation

25.4.2 Correctness Properties Under Assumptions

25.4.3 Internal Combinational Circuitry

25.5 The Fundamental Theorem of Trajectory Evaluation

25.6 STE Model Checking

25.6.1 The Symbolic Model-Checking Algorithm

25.6.2 Some Small Examples in Detail

25.6.3 Model Checking Properties Under Assumptions

25.7 Abstraction and Symbolic Indexing

25.7.1 Symbolic Indexing

25.8 Compositional Reasoning

25.8.1 The STE Deductive System

25.8.2 Relational STE

25.9 GSTE and Other Extensions

25.9.1 Generalized Symbolic Trajectory Evaluation

25.10 Summary and Prospects

References

Chapter 26: The mu-calculus and Model Checking

26.1 Introduction

26.2 Basics

26.2.1 Syntax and Semantics

26.2.2 Alternation Depth

26.2.3 Semantics in Terms of Games

26.2.3.1 Games

26.2.3.2 Veri?cation Game

26.2.4 Model Checking

26.3 Fundamental Properties

26.3.1 Bisimulation Invariance and the Tree-Model Property

26.3.2 Modal Automata

26.3.3 Satis?ability

26.3.4 Alternation Hierarchy

26.3.5 Proof System

26.3.6 Interpolation Property

26.3.7 Division Property

26.4 Relations with Other Logics

26.4.1 MSOL, Binary Trees and Bisimulation Invariance

26.4.2 Embedding of Program Logics

26.4.3 Beyond µ-Calculus

26.4.3.1 Iterated Structures

26.4.3.2 Guarded Logics

26.5 Related Work

References

Chapter 27: Graph Games and Reactive Synthesis

27.1 Introduction

27.2 Theory of Graph-Based Games

27.2.1 Game Graphs and Strategies

27.2.2 Objectives

27.2.3 Winning and Optimal Strategies; Decision Problems

27.2.4 Complexity and Algorithms for Graph Games with Qualitative Objectives

27.2.5 Complexity and Algorithms for Graph Games with Quantitative Objectives

27.2.6 Reducibility Between Graph Games

27.2.7 Extensions

27.3 Reactive Synthesis

27.3.1 Introduction

27.3.2 Games, Transducers, Trees, and Automata

27.3.3 Realizability and Synthesis Problem

27.3.4 Classical Approach to LTL Synthesis

Step 1: LTL to NBW

Step 2: NBW to DPW

Step 3: DPW to DPT

Step 4: DPT Emptiness Check

Step 5: Construction of Finite-State Transducer

27.3.5 Recent Approaches to LTL Synthesis

27.3.5.1 Bounded (or Safraless) Approaches

Step 1: LTL to UCT

Step 2: UCT to k-UCT

Step 3: k-UCT Emptiness Check

Step 4: System Construction

27.3.5.2 Approaches for Fragments of LTL

27.4 Related Topics

References

Chapter 28: Model Checking Probabilistic Systems

28.1 Introduction

28.1.1 Temporal Logics for Specifying Probabilistic Properties

28.1.2 Model-Checking Algorithms for Probabilistic Systems

28.1.3 Outline

28.2 Modelling Probabilistic Concurrent Systems

28.2.1 Preliminaries

28.2.2 Markov Decision Processes

28.2.3 Markov Chains

28.2.4 Schedulers

28.2.5 Probability Measures in MDPs

28.2.6 Maximal and Minimal Probabilities for Path Events

28.2.7 Maximal and Minimal Expected Cost

28.3 Probabilistic Computation Tree Logic

28.3.1 Syntax of PCTL

28.3.2 Semantics of PCTL

28.3.3 Derived Operators

28.4 Model-Checking Algorithms for MDPs and PCTL

28.4.1 Probability Operator

28.4.2 Expectation Operator

28.5 Linear Temporal Logic

28.5.1 Syntax of LTL

28.5.2 Semantics of LTL

28.5.3 Derived Operators

28.5.4 LTL Model-Checking Problem

28.6 Model-Checking Algorithms for MDPs and LTL

28.7 Tools, Applications and Model Construction

28.7.1 Tool Support

28.7.2 Applications

28.7.3 Construction of Probabilistic Models

28.8 Extensions of the Model and Speci?cation Notations

28.9 Conclusion

References

Chapter 29: Model Checking Real-Time Systems

29.1 Introduction

29.2 Timed Automata

29.3 Checking Reachability

29.3.1 Region Equivalence

29.3.2 Some Extensions of Timed Automata

29.4 (Bi)simulation Checking

29.4.1 (Bi)simulations for Timed Automata

29.4.2 Checking (Bi)simulations

29.5 Language-Theoretic Properties

29.5.1 Language of a Timed Automaton

29.5.2 Timed Automata with epsilon-Transitions

29.5.3 Clock Constraints as Acceptance Conditions

29.5.4 Intersection, Union, and Complement

29.5.5 Language Emptiness, Inclusion

29.6 Timed Temporal Logics

29.6.1 Linear-Time Temporal Logics

Continuous Semantics

Pointwise Semantics

29.6.2 Veri?cation of Linear-Time Temporal Logics

29.6.3 Branching-Time Temporal Logics

29.6.4 Veri?cation of Branching-Time Temporal Logics

29.7 Symbolic Algorithms, Data Structures, Tools

29.7.1 Zones and Operations

29.7.2 Symbolic Datastructures

29.7.3 Practical Ef?ciency

29.7.4 Tools and Applications

29.8 Weighted Timed Automata

29.8.1 Cost-Optimal Schedules

29.8.2 Weighted Temporal Logics

29.8.3 Energy Constraints

29.9 Timed Games

29.10 Ongoing and Future Challenges

References

Chapter 30: Veri?cation of Hybrid Systems

30.1 Introduction

30.2 Basic De?nitions

30.2.1 Predicates

30.2.2 Hybrid Automata

30.3 Decidability and Undecidability Results

30.4 Set-Based Reachability Analysis

30.4.1 Reachability Algorithm

30.4.2 Piecewise Constant Dynamics

30.4.3 Piecewise Af?ne Dynamics

30.4.3.1 Successor Computations

30.4.3.2 Set Representations

30.4.3.3 Clustering

30.4.4 Nonlinear Dynamics

30.5 Abstraction-Based Veri?cation

30.5.1 Discrete Abstractions

30.5.2 Phase-Portrait Approximation

30.5.3 Predicate Abstractions

30.5.4 Abstraction Re?nement

30.5.5 Approximate Bisimulations

30.6 Logic-Based Veri?cation

30.6.1 Polynomial Barrier Certi?cates

30.6.2 Equational Certi?cates

30.6.3 Differential Invariants and Logical Certi?cates

30.7 Veri?cation Tools

HSolver: Interval Constraint Propagation

HyTech: The HYbrid TECHnology Tool

KeYmaera: Logic and Differential Invariants for Compositional Veri?cation

PHAVer: Polyhedral Hybrid Automaton Verifyer

SpaceEx: State Space Explorer

ToolboxLS: Level Set Methods

References

Chapter 31: Symbolic Model Checking in Non-Boolean Domains

31.1 Introduction

31.2 Transition Systems and Symbolic Veri?cation

31.2.1 Systems: Transition Systems

31.2.2 Properties and Algorithms: The µ-Calculus

31.2.3 Symbolic Model Checking

31.2.4 Examples of Properties and Their Veri?cation Algorithms

31.2.5 Equivalence Relations and Termination

31.3 Examples of Symbolic Veri?cation

31.3.1 Program Veri?cation

31.3.2 Antichain-Based Algorithms for Finite-State Automata

31.3.3 Timed and Hybrid Systems

31.3.4 Well-Structured Transition Systems

31.4 Games and Symbolic Synthesis

31.4.1 Deterministic Games

31.4.2 The Boolean µ-Calculus on Games

31.4.3 Linear-Time Properties

31.4.4 From Veri?cation to Synthesis

31.4.5 Examples of Synthesis

31.5 Probabilistic Systems

31.5.1 Probabilistic Games and Objectives

31.5.2 The Quantitative µ-calculus

31.6 Conclusion

References

Chapter 32: Process Algebra and Model Checking

32.1 Introduction

32.2 Foundations

32.2.1 CCS: Process Algebra via Operational Semantics

32.2.1.1 Syntax of CCS

Actions in CCS

CCS Operators

32.2.1.2 The Operational Semantics of CCS

32.2.1.3 CCS and Labeled Transition Systems

32.2.1.4 Bisimulation

32.2.1.5 A Logical Characterization of Bisimilarity

Syntax of HML

Semantics of HML

Bisimulation vis-à-vis HML

32.2.1.6 Observational Equivalence and Congruence for CCS

32.2.1.7 Axiomatizations of Bisimilarity and Observational Congruence

Inference Rules for Equational Reasoning

Axiomatizing Bisimilarity

Axiomatizing Observational Congruence

Axiomatizing Full CCS

32.2.2 CSP: Process Algebra via Denotational Semantics

32.2.2.1 CSP Syntax

Actions in CSP

CSP Constructs

32.2.2.2 Models for CSP Processes

32.2.2.3 A Denotational Semantics for CSP

32.2.2.4 Timed CSP

32.2.3 ACP: Process Algebra via Equational Semantics

32.2.3.1 BPA

32.2.3.2 PA

32.2.3.3 ACP

32.3 Algorithms and Methodologies

32.3.1 Bisimulation and Simulation

32.3.2 Checking Re?nement over Behavioral Models

32.3.3 Diagnostic Information (HML , FD)

32.3.4 Compositional Veri?cation

32.4 Tools

32.4.1 FDR

32.4.1.1 Using FDR

32.4.2 The Concurrency Workbench

32.4.3 XMC

32.4.4 mCRL2

32.5 Case Studies

32.5.1 Distributed Leadership Election (FDR)

32.5.2 Active-Structure Control System (CWB)

32.5.3 GNU i-Protocol (XSB)

32.6 Conclusions

References

Index