CiteULike is a free online bibliography manager. Register and you can start organising your references online.
Tags

# Quantitative Timed Analysis of Interactive Markov Chains

## edited by: AlwynE Goodloe, Suzette Person

In NASA Formal Methods, Vol. 7226 (2012), pp. 8-23, doi:10.1007/978-3-642-28891-3_4  Key: citeulike:12017153

## Likes (beta)

This copy of the article hasn't been liked by anyone yet.

### Abstract

This paper presents new algorithms and accompanying tool support for analyzing interactive Markov chains (IMCs), a stochastic timed $1\frac12$ -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.