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

From MaRDI portal
Importer (talk | contribs)
Created a new Item
 
Import240304020342 (talk | contribs)
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 / namelinks / 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
    0 references
    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
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references