Informatik-Oberseminar, 25 Jan 2010, 13:00
Dipl.-Inform. Martin Richard Neuhäußer
Model Checking Nondeterministic and Randomly Timed Systems
Quantitative model checking has become an indispensable tool to analyze performance
and dependability characteristics such as the expected round trip time in a
packet switched network or the failure probability of a safety-critical system.
and dependability characteristics such as the expected round trip time in a
packet switched network or the failure probability of a safety-critical system.
So far, the existing model checking techniques lack support for models which
combine stochastic timing and nondeterminism. This is surprising, as nondeterminism
is the key for compositional modeling and occurs naturally in distributed systems.
In this talk, we overcome this limitation. More precisely, we consider continuous-time
Markov decision processes (CTMDPs), a model which closely entangles stochasticity
and nondeterminism. Our main contribution is a discretization which allows to compute
the maximum and minimum probability to enter a set of goal states in a CTMDP
within a given time-bound.
Markov decision processes (CTMDPs), a model which closely entangles stochasticity
and nondeterminism. Our main contribution is a discretization which allows to compute
the maximum and minimum probability to enter a set of goal states in a CTMDP
within a given time-bound.
By applying value iteration techniques to the induced discrete-time model, we
compute the desired probabilities up to an a priori specified precision.
compute the desired probabilities up to an a priori specified precision.
This result provides the basis for model checking important performance and dependability
characteristics and has been extended to a variety of other nondeterministic
and randomly timed system models.
characteristics and has been extended to a variety of other nondeterministic
and randomly timed system models.
