This paper presents new algorithms and accompanying tool support for analyzing interactive Markov chains (IMCs), a stochastic timed 11/2-player game in which delays are exponentially distributed. IMCs are compositional and act as semantic model for engineering formalisms such as AADL and dynamic fault trees. We provide algorithms for determining the extremal expected time of reaching a set of states, and the long-run average of time spent in a set of states. The prototypical tool Imca supports these algorithms as well as the synthesis of ε-optimal piecewise constant timed policies for timed reachability objectives. Two case studies show the feasibility and scalability of the algorithms. © 2012 Springer-Verlag.
CITATION STYLE
Guck, D., Han, T., Katoen, J. P., & Neuhäußer, M. R. (2012). Quantitative timed analysis of interactive Markov chains. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7226 LNCS, pp. 8–23). https://doi.org/10.1007/978-3-642-28891-3_4
Mendeley helps you to discover research relevant for your work.