Modelling, Reduction and Analysis of Markov Automata

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

  • 22 Citations

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 languageUndefined
Title of host publicationProceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST)
EditorsK.R. Joshi, M. Siegle, Mariëlle Ida Antoinette Stoelinga, P.R. d' Argenio
Place of PublicationBerlin
PublisherSpringer
Pages55-71
Number of pages17
ISBN (Print)978-3-642-40195-4
DOIs
StatePublished - Aug 2013
Event10th International Conference on Quantitative Evaluation of Systems, QEST 2013 - Buenos Aires, Argentina

Publication series

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

Conference

Conference10th International Conference on Quantitative Evaluation of Systems, QEST 2013
Abbreviated titleQEST
CountryArgentina
CityBuenos Aires
Period27/08/1330/08/13
Internet address

Fingerprint

Petri nets
Static analysis
Semantics
Chemical analysis

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

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. DOI: 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). 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: Scientific - peer-reviewConference contribution

@inbook{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",
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ë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-30 August. DOI: 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: Scientific - peer-reviewConference contribution

TY - CHAP

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)

PB - Springer

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). Available from, DOI: 10.1007/978-3-642-40196-1_5