Unfoldings --A Partial-Order Approach to Model Checking

EATCS Monographs in Theoretical Computer Science, 2008.

Model checking is a very popular technique for the automatic verification of systems, widely applied by the hardware industry and already receiving considerable attention from software companies. It is based on the (possibly exhaustive) exploration of the states reached by the system along all its executions. Model checking is very successful in finding bugs in concurrent systems. These systems are notoriously hard to design correctly, mostly because of the inherent uncertainty about the order in which components working in parallel execute actions. Since $n$ independent actions can occur in $n!$ different orders, humans easily overlook some of them, often the one causing a bug. On the contrary, model checking exhaustively examines all execution orders. Unfortunately, naive model checking techniques can only be applied to very small systems. The number of reachable states grows so quickly, that even a modern computer fails to explore them all in reasonable time. In this book we show that concurrency theory, the study of mathematical formalisms for the description and analysis of concurrent systems, helps to solve this problem. Unfoldings are one of these formalisms, belonging to the class of so-called

- Introduction
- Transition Systems and Products
- Transition Systems
- Products of Transition Systems
- Petri Ne Representation of Products
- Interleaving Representation of Products

- Unfolding Products
- Branching Processes and Unfoldings
- Some Properties of Branching Processes
- Verification Using Unfoldings
- Constructing the Unfolding of a Product
- Search Procedures
- Goals and Milestones for Next Chapters

- Search Procedures for the Executability Problem
- Search Strategies for Transition Systems
- Search Scheme for Transition Systems
- Search Strategies for Products
- Search Scheme for Products
- Adequate Search Strategies
- Complete Search Scheme for Arbitrary Strategies

- More on the Executability Problem
- Complete Prefixes
- Least Representatives
- Breadth-First and Depth-First Strategies
- Strategies Preserved by Extensions are Well-Founded

- Search Procedures for the Repeated Executability Problem
- Search Scheme for Transition Systems
- Search Scheme for Products

- Search Procedures for the Livelock Problem
- Search Scheme for Transition Systems
- Search Scheme for Products

- Model Checking LTL
- Linear Temporal Logic
- Interpreting LTL on Products
- Testers for LTL Properties
- Model Checking with Testers: A First Attempt
- Stuttering Synchronization

- Summary, Applications, Extensions, and Tools
- Looking Back: A Two-Page Summary of This Book
- Some Experiments
- Some Applications
- Some Extensions
- Some Tools

- References

This is the final draft of the book, as produced by Keijo and myself. Our publishing agreement with Springer allows us to make the file available in our homepages. Notice, however, that it cannot be made available through any other web page.

The book can be purchased from the publisher. If you're interested, or if you wish your library to order a copy, click here.