Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Quantitative Timed Analysis of Interactive Markov Chains
verfasst von : Dennis Guck, Tingting Han, Joost-Pieter Katoen, Martin R. Neuhäußer
Erschienen in: NASA Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper presents new algorithms and accompanying tool support for analyzing interactive Markov chains (IMCs), a stochastic timed
$1\frac{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.