Quantitative timed analysis of interactive Markov chains

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

doi:10.1007/978-3-642-28891-3_4

Quantitative timed analysis of interactive Markov chains

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

41 Citations (Scopus)

153 Downloads (Pure)

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 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	https://doi.org/10.1007/978-3-642-28891-3_4
Publication status	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/Territory	United States
City	Norfolk
Period	3/04/12 → 5/04/12

Keywords

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

Access to Document

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

Quantitative Timed AnalysisAccepted author version, 253 KB

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). Springer. https://doi.org/10.1007/978-3-642-28891-3_4

@inproceedings{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{\"a}u{\ss}er, {Martin R.}",

note = "10.1007/978-3-642-28891-3_4 ; 4th International Symposium on NASA Formal Methods, NFM 2012, NFM ; Conference date: 03-04-2012 Through 05-04-2012",

year = "2012",

month = apr,

doi = "10.1007/978-3-642-28891-3_4",

language = "English",

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",

address = "Germany",

}

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, Virginia, United States, 3/04/12. https://doi.org/10.1007/978-3-642-28891-3_4

Quantitative timed analysis of interactive Markov chains. / Guck, Dennis; Han, Tingting; Katoen, Joost-Pieter et al.
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: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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 - Conference code: 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

A2 - Goodloe, Alwyn E.

A2 - Person, Suzette

PB - Springer

CY - Berlin

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

Y2 - 3 April 2012 through 5 April 2012

ER -

Quantitative timed analysis of interactive Markov chains

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this