Sven Johr (Universität Saarbrücken)

 

 

Uniformity by construction

 

Abstract:

 

Continuous-time Markov decision processes (CTMDPs) are behavioral
models with continuous-time, nondeterminism and memoryless
stochastics. Recently, an efficient timed reachability algorithm for
CTMDPs has been presented, allowing one to quantify, e.\,g., the
worst-case probability to hit an unsafe system state within a safety
critical mission time. This algorithm works only for uniform CTMDPs --
CTMDPs in which the sojourn time distribution is unique across all
states. In this talk we present a compositional theory for generating
CTMDPs which are uniform by construction. To analyze the scalability
of the method, this theory is applied to the construction of a
fault-tolerant workstation cluster example, and experimentally
evaluated using an innovative implementation of the timed reachability
algorithm. All previous attempts to model-check this seemingly
well-studied example needed to ignore the presence of nondeterminism,
because of lacking support for modelling and analysis.