Publication year: 2008
ISBN: 978-3-540-77426-6
Internet Resource: Please Login to download book
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.
Subject: Computer Science, Software Engineering, Programming and Operating Systems, Logics and Meanings of Programs, Theory of Computation, Algorithms, Automat, algorithm, distributed systems, logic, model checking, verification