37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN'07)
Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems
Edinburgh, UK
June 25-June 28
ISBN: 0-7695-2855-4
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 [2], 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 paper we develop 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.
Citation:
Holger Hermanns, Sven Johr, "Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems," dsn, pp.718-728, 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN'07), 2007