### Abstract

Original language | Undefined |
---|---|

Title of host publication | 4th International Symposium on NASA Formal Methods, NFM 2012 |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 8-23 |

Number of pages | 15 |

ISBN (Print) | 978-3-642-28890-6 |

DOIs | |

State | Published - Apr 2012 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

Volume | 7226 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Fingerprint

### Keywords

- expected time
- interactive Markov chain
- EWI-22672
- METIS-296168
- Reachability
- Quantitative analysis
- IR-83449
- Long-run average

### Cite this

*4th International Symposium on NASA Formal Methods, NFM 2012*(pp. 8-23). (Lecture Notes in Computer Science; Vol. 7226). Berlin: Springer. DOI: 10.1007/978-3-642-28891-3_4

}

*4th International Symposium on NASA Formal Methods, NFM 2012.*Lecture Notes in Computer Science, vol. 7226, Springer, Berlin, pp. 8-23. DOI: 10.1007/978-3-642-28891-3_4

**Quantitative timed analysis of interactive Markov chains.** / Guck, Dennis; Han, Tingting; Katoen, Joost P.; Neuhausser, M.

Research output: Scientific - peer-review › Conference contribution

TY - CHAP

T1 - Quantitative timed analysis of interactive Markov chains

AU - Guck,Dennis

AU - Han,Tingting

AU - Katoen,Joost P.

AU - Neuhausser,M.

N1 - 10.1007/978-3-642-28891-3_4

PY - 2012/4

Y1 - 2012/4

N2 - 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.

AB - 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.

KW - expected time

KW - interactive Markov chain

KW - EWI-22672

KW - METIS-296168

KW - Reachability

KW - Quantitative analysis

KW - IR-83449

KW - Long-run average

U2 - 10.1007/978-3-642-28891-3_4

DO - 10.1007/978-3-642-28891-3_4

M3 - Conference contribution

SN - 978-3-642-28890-6

T3 - Lecture Notes in Computer Science

SP - 8

EP - 23

BT - 4th International Symposium on NASA Formal Methods, NFM 2012

PB - Springer

ER -