Unfoldings: A partial-order approach to model checking. (Q2426635): Difference between revisions
From MaRDI portal
Created a new Item |
Set profile property. |
||
(6 intermediate revisions by 2 users not shown) | |||
Property / describes a project that uses | |||
Property / describes a project that uses: Punf / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: POEM / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: Smodels / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: LTL2BA / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: SPIN / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 07:08, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Unfoldings: A partial-order approach to model checking. |
scientific article |
Statements
Unfoldings: A partial-order approach to model checking. (English)
0 references
23 April 2008
0 references
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
0 references
unfoldings
0 references
model checking
0 references
interleavings
0 references