Seminars

On Model Checking Techniques for Randomized Distributed Systems. PDF slides

Christel Baier, Professor
Technische Universität Dresden , Germany

12/03/2010, 2:00 PM, GHC-6501

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 com­pute 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 time-bounded graph algorithm with methods for solving linear programs. In the classical approach, the “worst-case” is determined when rang­ing 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.

As in the nonprobabilistic case, the commutativity of independent concur­rent actions can be used to avoid redundancies in the system model and to increase the efficiency of the quantitative analysis. However, there are certain phenomena that are specific for the probabilistic case and require additional conditions for the reduced model to ensure that the worst-case probabilities are preserved. Related to this observation is also the fact that the worst-case analysis that ranges over all schedulers is often too pessimistic and leads to extreme probability values that can be achieved only by schedulers that are unrealistic for parallel systems. This motivates the switch to more realistic classes of schedulers that respect the fact that the individual processes only have partial information about the global system states. Such classes of partial-information schedulers yield more realistic worst-case probabilities, but compu­tationally they are much harder. A wide range of verification problems turns out to be undecidable when the goal is to check that certain probability bounds hold under all partial-information schedulers.

Biography

Christel Baier received the PhD degree (1994) and the venia legendi (1999), both from the Department of Computer Science at the University of Mannheim (Germany). In 1999-2006, she has been an associate professor of computer science at the Rheinische Friedrich-Wilhelms Universit\"at Bonn. Since October 2006, she is a full professor for computer science at the Technical University Dresden. Her expertise is on modeling, specification and verification techniques for reactive systems. In particular, she is interested in algorithms for the quantitative analysis of stochastic systems, probabilistic model checking, verification of infinite-state systems, coordination languages, compatibility of components, temporal and modal logics, and automata over infinite structures..