Quantitative timed analysis of interactive Markov chains

Dennis Guck, Tingting Han, Joost P. Katoen, M. Neuhausser

  • 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 languageUndefined
Title of host publication4th International Symposium on NASA Formal Methods, NFM 2012
Place of PublicationBerlin
PublisherSpringer
Pages8-23
Number of pages15
ISBN (Print)978-3-642-28890-6
DOIs
StatePublished - Apr 2012

Publication series

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

Fingerprint

Markov processes
Scalability
Semantics

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., & Neuhausser, M. (2012). Quantitative timed analysis of interactive Markov chains. In 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

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

4th International Symposium on NASA Formal Methods, NFM 2012. 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 Katoen, {Joost P.} and M. Neuhausser",
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",
booktitle = "4th International Symposium on NASA Formal Methods, NFM 2012",

}

Guck, D, Han, T, Katoen, JP & Neuhausser, M 2012, Quantitative timed analysis of interactive Markov chains. in 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.

4th International Symposium on NASA Formal Methods, NFM 2012. 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 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 -

Guck D, Han T, Katoen JP, Neuhausser M. Quantitative timed analysis of interactive Markov chains. In 4th International Symposium on NASA Formal Methods, NFM 2012. Berlin: Springer. 2012. p. 8-23. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-28891-3_4