Modelling, Reduction and Analysis of Markov Automata

Dennis Guck; Hassan Hatefi; H. Hermanns; Joost P. Katoen; Mark Timmer

doi:10.1007/978-3-642-40196-1_5

Modelling, Reduction and Analysis of Markov Automata

Dennis Guck, Hassan Hatefi, H. Hermanns, Joost P. Katoen, Mark Timmer

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

30 Citations (Scopus)

127 Downloads (Pure)

Abstract

Markov automata (MA) constitute an expressive continuous-time compositional modelling formalism. They appear as semantic backbones for engineering frameworks including dynamic fault trees, Generalised Stochastic Petri Nets, and AADL. Their expressive power has thus far precluded them from effective analysis by probabilistic (and statistical) model checkers, stochastic game solvers, or analysis tools for Petri net-like formalisms. This paper presents the foundations and underlying algorithms for efficient MA modelling, reduction using static analysis, and most importantly, quantitative analysis. We also discuss implementation pragmatics of supporting tools and present several case studies demonstrating feasibility and usability of MA in practice.

Original language	Undefined
Title of host publication	Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST)
Editors	K.R. Joshi, M. Siegle, Mariëlle Ida Antoinette Stoelinga, P.R. d' Argenio
Place of Publication	Berlin
Publisher	Springer
Pages	55-71
Number of pages	17
ISBN (Print)	978-3-642-40195-4
DOIs	https://doi.org/10.1007/978-3-642-40196-1_5
Publication status	Published - Aug 2013
Event	10th International Conference on Quantitative Evaluation of Systems, QEST 2013 - University of Buenos Aires, Buenos Aires, Argentina Duration: 27 Aug 2013 → 30 Aug 2013 Conference number: 10 http://www.qest.org/qest2013/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	8054
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Conference on Quantitative Evaluation of Systems, QEST 2013
Abbreviated title	QEST
Country	Argentina
City	Buenos Aires
Period	27/08/13 → 30/08/13
Internet address	http://www.qest.org/qest2013/

Keywords

EC Grant Agreement nr.: FP7/2007-2013
EC Grant Agreement nr.: FP7/295261
EC Grant Agreement nr.: FP7/318490
EC Grant Agreement nr.: FP7/257005
EWI-23542
Process Algebra
Quantitative analysis
IR-87075
Continuous time
Markov Automata
METIS-297747

Access to Document

10.1007/978-3-642-40196-1_5

paper
open
paperSpringer
open
paper
open

Cite this

Guck, D., Hatefi, H., Hermanns, H., Katoen, J. P., & Timmer, M. (2013). Modelling, Reduction and Analysis of Markov Automata. In K. R. Joshi, M. Siegle, M. I. A. Stoelinga, & P. R. d' Argenio (Eds.), Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST) (pp. 55-71). (Lecture Notes in Computer Science; Vol. 8054). Berlin: Springer. https://doi.org/10.1007/978-3-642-40196-1_5

Guck, Dennis ; Hatefi, Hassan ; Hermanns, H. ; Katoen, Joost P. ; Timmer, Mark. / Modelling, Reduction and Analysis of Markov Automata. Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST). editor / K.R. Joshi ; M. Siegle ; Mariëlle Ida Antoinette Stoelinga ; P.R. d' Argenio. Berlin : Springer, 2013. pp. 55-71 (Lecture Notes in Computer Science).

@inproceedings{540e2b664a5c46edb2f0a837711397b5,

title = "Modelling, Reduction and Analysis of Markov Automata",

abstract = "Markov automata (MA) constitute an expressive continuous-time compositional modelling formalism. They appear as semantic backbones for engineering frameworks including dynamic fault trees, Generalised Stochastic Petri Nets, and AADL. Their expressive power has thus far precluded them from effective analysis by probabilistic (and statistical) model checkers, stochastic game solvers, or analysis tools for Petri net-like formalisms. This paper presents the foundations and underlying algorithms for efficient MA modelling, reduction using static analysis, and most importantly, quantitative analysis. We also discuss implementation pragmatics of supporting tools and present several case studies demonstrating feasibility and usability of MA in practice.",

keywords = "EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/295261, EC Grant Agreement nr.: FP7/318490, EC Grant Agreement nr.: FP7/257005, EWI-23542, Process Algebra, Quantitative analysis, IR-87075, Continuous time, Markov Automata, METIS-297747",

author = "Dennis Guck and Hassan Hatefi and H. Hermanns and Katoen, {Joost P.} and Mark Timmer",

note = "eemcs-eprint-23542",

year = "2013",

month = "8",

doi = "10.1007/978-3-642-40196-1_5",

language = "Undefined",

isbn = "978-3-642-40195-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "55--71",

editor = "K.R. Joshi and M. Siegle and Stoelinga, {Mari{\"e}lle Ida Antoinette} and {d' Argenio}, P.R.",

booktitle = "Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST)",

}

Guck, D, Hatefi, H, Hermanns, H, Katoen, JP & Timmer, M 2013, Modelling, Reduction and Analysis of Markov Automata. in KR Joshi, M Siegle, MIA Stoelinga & PR d' Argenio (eds), Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST). Lecture Notes in Computer Science, vol. 8054, Springer, Berlin, pp. 55-71, 10th International Conference on Quantitative Evaluation of Systems, QEST 2013, Buenos Aires, Argentina, 27/08/13. https://doi.org/10.1007/978-3-642-40196-1_5

Modelling, Reduction and Analysis of Markov Automata. / Guck, Dennis; Hatefi, Hassan; Hermanns, H.; Katoen, Joost P.; Timmer, Mark.

Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST). ed. / K.R. Joshi; M. Siegle; Mariëlle Ida Antoinette Stoelinga; P.R. d' Argenio. Berlin : Springer, 2013. p. 55-71 (Lecture Notes in Computer Science; Vol. 8054).

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

TY - GEN

T1 - Modelling, Reduction and Analysis of Markov Automata

AU - Guck, Dennis

AU - Hatefi, Hassan

AU - Hermanns, H.

AU - Katoen, Joost P.

AU - Timmer, Mark

N1 - eemcs-eprint-23542

PY - 2013/8

Y1 - 2013/8

N2 - Markov automata (MA) constitute an expressive continuous-time compositional modelling formalism. They appear as semantic backbones for engineering frameworks including dynamic fault trees, Generalised Stochastic Petri Nets, and AADL. Their expressive power has thus far precluded them from effective analysis by probabilistic (and statistical) model checkers, stochastic game solvers, or analysis tools for Petri net-like formalisms. This paper presents the foundations and underlying algorithms for efficient MA modelling, reduction using static analysis, and most importantly, quantitative analysis. We also discuss implementation pragmatics of supporting tools and present several case studies demonstrating feasibility and usability of MA in practice.

AB - Markov automata (MA) constitute an expressive continuous-time compositional modelling formalism. They appear as semantic backbones for engineering frameworks including dynamic fault trees, Generalised Stochastic Petri Nets, and AADL. Their expressive power has thus far precluded them from effective analysis by probabilistic (and statistical) model checkers, stochastic game solvers, or analysis tools for Petri net-like formalisms. This paper presents the foundations and underlying algorithms for efficient MA modelling, reduction using static analysis, and most importantly, quantitative analysis. We also discuss implementation pragmatics of supporting tools and present several case studies demonstrating feasibility and usability of MA in practice.

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/295261

KW - EC Grant Agreement nr.: FP7/318490

KW - EC Grant Agreement nr.: FP7/257005

KW - EWI-23542

KW - Process Algebra

KW - Quantitative analysis

KW - IR-87075

KW - Continuous time

KW - Markov Automata

KW - METIS-297747

U2 - 10.1007/978-3-642-40196-1_5

DO - 10.1007/978-3-642-40196-1_5

M3 - Conference contribution

SN - 978-3-642-40195-4

T3 - Lecture Notes in Computer Science

SP - 55

EP - 71

BT - Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST)

A2 - Joshi, K.R.

A2 - Siegle, M.

A2 - Stoelinga, Mariëlle Ida Antoinette

A2 - d' Argenio, P.R.

PB - Springer

CY - Berlin

ER -

Guck D, Hatefi H, Hermanns H, Katoen JP , Timmer M. Modelling, Reduction and Analysis of Markov Automata. In Joshi KR, Siegle M, Stoelinga MIA, d' Argenio PR, editors, Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST). Berlin: Springer. 2013. p. 55-71. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-40196-1_5