Modelling, Reduction and Analysis of Markov Automata (extended version)

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

Research output: Book/ReportReport

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.
LanguageUndefined
Place of PublicationIthaca, NY, USA
PublisherCornell University
Number of pages27
StatePublished - 30 May 2013

Publication series

Name
PublisherCornell University
No.arXiv:1305.7050

Keywords

  • EC Grant Agreement nr.: FP7/2007-2013
  • IR-86179
  • EC Grant Agreement nr.: FP7/318490
  • Continuous time
  • Process Algebra
  • Markov Automata
  • EC Grant Agreement nr.: FP7/257005
  • Quantitative analysis
  • EC Grant Agreement nr.: FP7/295261
  • METIS-297670
  • EWI-23394

Cite this

Guck, D., Hatefi, H., Hermanns, H., Katoen, J. P., & Timmer, M. (2013). Modelling, Reduction and Analysis of Markov Automata (extended version). Ithaca, NY, USA: Cornell University.
Guck, Dennis ; Hatefi, Hassan ; Hermanns, H. ; Katoen, Joost P. ; Timmer, Mark. / Modelling, Reduction and Analysis of Markov Automata (extended version). Ithaca, NY, USA : Cornell University, 2013. 27 p.
@book{592db5c4a538467b967a58febef04444,
title = "Modelling, Reduction and Analysis of Markov Automata (extended version)",
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, IR-86179, EC Grant Agreement nr.: FP7/318490, Continuous time, Process Algebra, Markov Automata, EC Grant Agreement nr.: FP7/257005, Quantitative analysis, EC Grant Agreement nr.: FP7/295261, METIS-297670, EWI-23394",
author = "Dennis Guck and Hassan Hatefi and H. Hermanns and Katoen, {Joost P.} and Mark Timmer",
note = "eemcs-eprint-23394",
year = "2013",
month = "5",
day = "30",
language = "Undefined",
publisher = "Cornell University",
number = "arXiv:1305.7050",
address = "United States",

}

Guck, D, Hatefi, H, Hermanns, H, Katoen, JP & Timmer, M 2013, Modelling, Reduction and Analysis of Markov Automata (extended version). Cornell University, Ithaca, NY, USA.

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

Ithaca, NY, USA : Cornell University, 2013. 27 p.

Research output: Book/ReportReport

TY - BOOK

T1 - Modelling, Reduction and Analysis of Markov Automata (extended version)

AU - Guck,Dennis

AU - Hatefi,Hassan

AU - Hermanns,H.

AU - Katoen,Joost P.

AU - Timmer,Mark

N1 - eemcs-eprint-23394

PY - 2013/5/30

Y1 - 2013/5/30

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 - IR-86179

KW - EC Grant Agreement nr.: FP7/318490

KW - Continuous time

KW - Process Algebra

KW - Markov Automata

KW - EC Grant Agreement nr.: FP7/257005

KW - Quantitative analysis

KW - EC Grant Agreement nr.: FP7/295261

KW - METIS-297670

KW - EWI-23394

M3 - Report

BT - Modelling, Reduction and Analysis of Markov Automata (extended version)

PB - Cornell University

CY - Ithaca, NY, USA

ER -

Guck D, Hatefi H, Hermanns H, Katoen JP, Timmer M. Modelling, Reduction and Analysis of Markov Automata (extended version). Ithaca, NY, USA: Cornell University, 2013. 27 p.