che-chandler.de
|
| Der Artikel wird am Ende des Bestellprozesses zum Download zur Verfügung gestellt. |
Decidability of Parameterized Verification
Beschreibung:
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.
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.
Table of 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