Roderick Bloem

Igor Konnov

Swen Jacobs

Ayrat Khalimov

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 ∈ N, whether, for all n ∈ 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.

Decidability of Parameterized Verification

Ayrat Kalimov

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 ∈ N, whether, for all n ∈ 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.

Variational inequalities proved to be a very useful tool for investigation and solution of various equilibrium type problems arising in Economics, Operations Research, Mathematical Physics, and Transportation. This book is devoted to a new general approach to constructing solution methods for variational inequalities, which was called the combined relaxation approach. This approach is rather flexible and allows one to construct various methods both for single-valued and for multi-valued variational inequalities, including nonlinear constrained problems. The other essential feature of the combined relaxation methods is that they are convergent under very mild assumptions. The book can be viewed as an attempt to discribe the existing combined relaxation methods as a whole.

Igor Konnov

About

Books

Join the club