Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
On Model Checking Techniques forRandomized Distributed Systems
Christel Baier
Technische Universität Dresden
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 27 October 2010
14:00
60 Minutes
E1 4
024
Saarbrücken
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 time-bounded 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.
As in the nonprobabilistic case, the commutativity of independent concurrent
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 computationally they are much
harder. A wide range of verification problems that impose conditions on all
partial-information schedulers turns out to be undecidable.
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 time-bounded 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.
As in the nonprobabilistic case, the commutativity of independent concurrent
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 computationally they are much
harder. A wide range of verification problems that impose conditions on all
partial-information schedulers turns out to be undecidable.
Contact
Christina Fries
--email hidden
passcode not visible
logged in users only
Christina Fries, 10/27/2010 13:26
Christina Fries, 10/26/2010 15:16
Christina Fries, 10/22/2010 11:34 -- Created document.
Christina Fries, 10/26/2010 15:16
Christina Fries, 10/22/2010 11:34 -- Created document.