On Model Checking Techniques for Randomized Distributed Systems

10 years 1 months ago
On Model Checking Techniques for Randomized Distributed Systems
Abstract. The automata-based model checking approach for randomized distributed systems relies on an operational interleaving semantics of the system by means of a Markov decision process and a formalization of the desired event E by an ω-regular linear-time property, e.g., an LTL formula. The task is then to compute the greatest lower bound for the probability for E that can be guaranteed even in worst-case scenarios. Such bounds can be computed by a combination of polynomially timebounded graph algorithm with methods for solving linear programs. In the classical approach, the “worst-case” is determined when ranging over all schedulers that decide which action to perform next. In particular, all possible interleavings and resolutions of other nondeterministic choices in the system model are taken into account. The worst-case analysis relying on this general notion of schedulers is often too pessimistic and leads to extreme probability values that can be achieved only by scheduler...
Christel Baier
Added 27 Jan 2011
Updated 27 Jan 2011
Type Journal
Year 2010
Where IFM
Authors Christel Baier
Comments (0)