Model checking is a prominent technique used in the hardware and
software industries for automatic verification. While it is very
successful in finding subtle bugs in distributed systems, it faces the
state explosion problem - the number of reachable states grows
exponentially in the number of concurrent components.
In this book the authors introduce unfoldings, an approach to model
checking which alleviates the state explosion problem by means of
concurrency theory. They offer a gentle introduction to the basics of
the method, and in particular they detail an unfolding-based algorithm
for model checking concurrent systems against properties specified as
formulas of linear temporal logic (LTL). Self-contained chapters cover
transition systems and their products; unfolding products; search
procedures for basic verification problems, such as reachability and
livelocks; and model checking LTL. The final chapter summarizes the
results of the book, and points the reader to tools and case studies.
The book will be of value to researchers and graduate students engaged
in automatic verification and concurrency theory.