Unfoldings: A partial-order approach to model checking. (Q2426635)

Model checking is one of the possible solutions to the problem of ``interleavings'' for concurrent systems. This verification technique, fully automated, is very successful in finding bugs in distributed systems. It constructs a graph to represent all possible states of a system as well as the transitions between them. Unfortunately, the number of reachable states grows exponentially in the number of concurrent components, even for simple systems. In this book the authors show that the study of ``unfoldings'', a mathematical formalism for the description and analysis of concurrent systems, alleviates the state explosion problem. The presentation is given gradually, offering a step-by-step introduction to the basics of the method, detailing also an algorithm for model checking concurrent systems based on unfoldings. Most of the chapters are self-contained in order to increase the readability of the content. After a short introduction (viewed as a chapter), the second and the third chapters cover the basics on transition systems, their products and unfolding products. The next five chapters are devoted to search procedures for executability problems, reachability and livelocks problems, and model checking linear temporal logic. Some concluding remarks, experiments, applications and tools are summarized in the last chapter. The book provides a good overview on unfoldings techniques to researchers and graduate students engaged in model checking and concurrency theory. It can also be of interest to other people, outside computer science, since concurrency occurs everywere