Quantitative timed analysis of interactive Markov chains

Dennis Guck, Tingting Han, Joost-Pieter Katoen, Martin R. Neuhäußer

  • 28 Citations

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.
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings
EditorsAlwyn E. Goodloe, Suzette Person
Place of PublicationBerlin
PublisherSpringer
Pages8-23
Number of pages15
ISBN (Electronic)978-3-642-28891-3
ISBN (Print)978-3-642-28890-6
DOIs
StatePublished - Apr 2012
Event4th International Symposium on NASA Formal Methods, NFM 2012 - Norfolk, United States

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume7226
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference4th International Symposium on NASA Formal Methods, NFM 2012
Abbreviated titleNFM
CountryUnited States
CityNorfolk
Period3/04/125/04/12

Fingerprint

Markov processes
Scalability
Semantics
Chemical analysis

Keywords

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

Cite this

Guck, D., Han, T., Katoen, J-P., & Neuhäußer, M. R. (2012). Quantitative timed analysis of interactive Markov chains. In A. E. Goodloe, & S. Person (Eds.), 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

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

NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. ed. / Alwyn E. Goodloe; Suzette Person. Berlin : Springer, 2012. p. 8-23 (Lecture Notes in Computer Science; Vol. 7226).

Research output: Scientific - peer-reviewConference contribution

@inbook{e93fbfefc7814ba29c259049320cd976,
title = "Quantitative timed analysis of interactive Markov chains",
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.",
keywords = "expected time, interactive Markov chain, EWI-22672, METIS-296168, Reachability, Quantitative analysis, IR-83449, Long-run average",
author = "Dennis Guck and Tingting Han and Joost-Pieter Katoen and Neuhäußer, {Martin R.}",
note = "10.1007/978-3-642-28891-3_4",
year = "2012",
month = "4",
doi = "10.1007/978-3-642-28891-3_4",
isbn = "978-3-642-28890-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "8--23",
editor = "Goodloe, {Alwyn E.} and Suzette Person",
booktitle = "NASA Formal Methods",

}

Guck, D, Han, T, Katoen, J-P & Neuhäußer, MR 2012, Quantitative timed analysis of interactive Markov chains. in AE Goodloe & S Person (eds), 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-5 April. 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.

NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. ed. / Alwyn E. Goodloe; Suzette Person. Berlin : Springer, 2012. p. 8-23 (Lecture Notes in Computer Science; Vol. 7226).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

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

ER -

Guck D, Han T, Katoen J-P, Neuhäußer MR. Quantitative timed analysis of interactive Markov chains. In Goodloe AE, Person S, editors, NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. Berlin: Springer. 2012. p. 8-23. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-28891-3_4