HomeNewsCase StudiesPeoplePublications
[GHKN12] D. Guck, T. Han, J.-P. Katoen and M. R. Neuhäußer. Quantitative Timed Analysis of Interactive Markov Chains. In Proceeding of NASA Formal Methods Symposium (NFM), Volume 7226 of Lecture Notes in Computer Science, pages 8–23, Springer-Verlag. 2012. [pdf] [bib]
Downloads:  pdf pdf (571 KB)  bib bib
Notes: The original publication is available at www.springerlink.com.
Abstract. This paper presents new algorithms and accompanying tool support for analyzing interactive Markov chains (IMCs), a stochastic timed 1 1/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.