Central Library

Normal view MARC view ISBD view

Decidability of Parameterized Verification [electronic resource] / by Roderick Bloem, Swen Jacobs, Ayrat Kalimov, Igor Konnov.

By: Bloem, Roderick [author.].
Contributor(s): Jacobs, Swen [author.] | Kalimov, Ayrat [author.] | Konnov, Igor [author.] | SpringerLink (Online service).
Material type: materialTypeLabelBookSeries: Synthesis Lectures on Distributed Computing Theory: Publisher: Cham : Springer International Publishing : Imprint: Springer, 2015Edition: 1st ed. 2015.Description: XI, 158 p. online resource.Content type: text Media type: computer Carrier type: online resourceISBN: 9783031020117.Subject(s): Computer science | Coding theory | Information theory | Data structures (Computer science) | Computer Science | Coding and Information Theory | Data Structures and Information TheoryAdditional physical formats: Printed edition:: No title; Printed edition:: No titleDDC classification: 004 Online resources: Click here to access online
Contents:
Acknowledgments -- Introduction -- System Model and Specification Languages -- Standard Proof Machinery -- Token-passing Systems -- Rendezvous and Broadcast -- Guarded Protocols -- Ad Hoc Networks -- Related Work -- Parameterized Model Checking Tools -- Conclusions -- Bibliography -- Authors' Biographies .
In: Springer Nature eBookSummary: While the classic model checking problem is to decide whether a finite system satisfies a specification, the goal of parameterized model checking is to decide, given finite systems ����(n) parameterized by n ∈ ℕ, whether, for all n ∈ ℕ, the system ����(n) satisfies a specification. In this book we consider the important case of ����(n) being a concurrent system, where the number of replicated processes depends on the parameter n but each process is independent of n. Examples are cache coherence protocols, networks of finite-state agents, and systems that solve mutual exclusion or scheduling problems. Further examples are abstractions of systems, where the processes of the original systems actually depend on the parameter. The literature in this area has studied a wealth of computational models based on a variety of synchronization and communication primitives, including token passing, broadcast, and guarded transitions. Often, different terminology is used in the literature, and results are based on implicit assumptions. In this book, we introduce a computational model that unites the central synchronization and communication primitives of many models, and unveils hidden assumptions from the literature. We survey existing decidability and undecidability results, and give a systematic view of the basic problems in this exciting research area.
    average rating: 0.0 (0 votes)
No physical items for this record

Acknowledgments -- Introduction -- System Model and Specification Languages -- Standard Proof Machinery -- Token-passing Systems -- Rendezvous and Broadcast -- Guarded Protocols -- Ad Hoc Networks -- Related Work -- Parameterized Model Checking Tools -- Conclusions -- Bibliography -- Authors' Biographies .

While the classic model checking problem is to decide whether a finite system satisfies a specification, the goal of parameterized model checking is to decide, given finite systems ����(n) parameterized by n ∈ ℕ, whether, for all n ∈ ℕ, the system ����(n) satisfies a specification. In this book we consider the important case of ����(n) being a concurrent system, where the number of replicated processes depends on the parameter n but each process is independent of n. Examples are cache coherence protocols, networks of finite-state agents, and systems that solve mutual exclusion or scheduling problems. Further examples are abstractions of systems, where the processes of the original systems actually depend on the parameter. The literature in this area has studied a wealth of computational models based on a variety of synchronization and communication primitives, including token passing, broadcast, and guarded transitions. Often, different terminology is used in the literature, and results are based on implicit assumptions. In this book, we introduce a computational model that unites the central synchronization and communication primitives of many models, and unveils hidden assumptions from the literature. We survey existing decidability and undecidability results, and give a systematic view of the basic problems in this exciting research area.

There are no comments for this item.

Log in to your account to post a comment.