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 proceedingConference contributionAcademicpeer-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 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
    Publication statusPublished - Aug 2013
    Event10th International Conference on Quantitative Evaluation of Systems, QEST 2013 - University of Buenos Aires, Buenos Aires, Argentina
    Duration: 27 Aug 201330 Aug 2013
    Conference number: 10
    http://www.qest.org/qest2013/

    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

    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. https://doi.org/10.1007/978-3-642-40196-1_5