|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| Search | ||
| ||
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
| ASCII Text | x | ||
| Holger Hermanns, Sven Johr, "Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems," IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2012), pp. 718-728, 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN'07), 2007. | |||
| BibTex | x | ||
| @article{ 10.1109/DSN.2007.96, author = {Holger Hermanns and Sven Johr}, title = {Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems}, journal ={IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2012)}, volume = {0}, year = {2007}, isbn = {0-7695-2855-4}, pages = {718-728}, doi = {http://doi.ieeecomputersociety.org/10.1109/DSN.2007.96}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2012) TI - Uniformity by Construction in the Analysis of Nondeterministic Stochastic Systems SN - 0-7695-2855-4 SP718 EP728 A1 - Holger Hermanns, A1 - Sven Johr, PY - 2007 KW - null VL - 0 JA - IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2012) ER - | |||
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DSN.2007.96
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
Usage of this product signifies your acceptance of the Terms of Use.
