### Abstract

Language | English |
---|---|

Title of host publication | NASA Formal Methods |

Subtitle of host publication | 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings |

Editors | Alwyn E. Goodloe, Suzette Person |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 8-23 |

Number of pages | 15 |

ISBN (Electronic) | 978-3-642-28891-3 |

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

DOIs | |

State | Published - Apr 2012 |

Event | 4th International Symposium on NASA Formal Methods, NFM 2012 - Norfolk, United States Duration: 3 Apr 2012 → 5 Apr 2012 Conference number: 4 |

### Publication series

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

Publisher | Springer Verlag |

Volume | 7226 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

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

Abbreviated title | NFM |

Country | United States |

City | Norfolk |

Period | 3/04/12 → 5/04/12 |

### Fingerprint

### Keywords

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

### Cite this

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

}

*NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings.*Lecture Notes in Computer Science, vol. 7226, Springer, Berlin, pp. 8-23, 4th International Symposium on NASA Formal Methods, NFM 2012, Norfolk, United States, 3/04/12. DOI: 10.1007/978-3-642-28891-3_4

**Quantitative timed analysis of interactive Markov chains.** / Guck, Dennis; Han, Tingting; Katoen, Joost-Pieter; Neuhäußer, Martin R.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Quantitative timed analysis of interactive Markov chains

AU - Guck,Dennis

AU - Han,Tingting

AU - Katoen,Joost-Pieter

AU - Neuhäußer,Martin R.

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 - NASA Formal Methods

PB - Springer

CY - Berlin

ER -