Decidability of Parameterized Verification (Synthesis Lectures on Distributed Computing Theory) - Softcover
Synopsis
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.
"synopsis" may belong to another edition of this title.
About the Author
Roderick Bloem is a professor at Graz University of Technology. He received an M.Sc. in computer science from Leiden University in the Netherlands (1996) and a Ph.D. from the University of Colorado at Boulder (2001). His thesis work, under the supervision of Fabio Somenzi, was on formal verification using Linear Temporal Logic.
Since 2002, he has been an assistant professor at Graz University of Technology and a full professor since 2008. His research interests are in formal methods for the design and verification of digital systems, including hardware, software, and combinations such as embedded systems. He studies applications of game theory to the automatic synthesis of systems from their specifications, connections between temporal logics and omega-automata, model checking, and automatic fault localization and repair.
"About this title" may belong to another edition of this title.
