Confluence Reduction for Markov Automata

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    21 Citations (Scopus)
    64 Downloads (Pure)

    Abstract

    Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. Recently, the process algebra MAPA was introduced to efficiently model such systems. As always, the state space explosion threatens the analysability of the models generated by such specifications. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep these models small. We define the notion of confluence directly on Markov automata, and discuss how to syntactically detect confluence on the MAPA language as well. That way, Markov automata generated by MAPA specifications can be reduced on-the-fly while preserving divergence-sensitive branching bisimulation. Three case studies demonstrate the significance of our approach, with reductions in analysis time up to an order of magnitude.
    Original languageUndefined
    Title of host publicationProceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)
    EditorsVictor Braberman, Laurent Fribourg
    Place of PublicationBerlin
    PublisherSpringer
    Pages243-257
    Number of pages15
    ISBN (Print)978-3-642-40228-9
    DOIs
    Publication statusPublished - Aug 2013
    Event11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013 - Universidad de Buenos Aires, Buenos Aires, Argentina
    Duration: 29 Aug 201331 Aug 2013
    Conference number: 11

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume8053
    ISSN (Print)0302-9743

    Conference

    Conference11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013
    Abbreviated titleFORMATS
    CountryArgentina
    CityBuenos Aires
    Period29/08/1331/08/13

    Keywords

    • Confluence
    • METIS-318706
    • EC Grant Agreement nr.: FP7/318003
    • Markov Automata
    • State space reduction
    • EWI-23541
    • Divergence-sensitive branching bisimulation
    • EC Grant Agreement nr.: FP7/318490
    • EC Grant Agreement nr.: FP7/2007-2013
    • IR-87074
    • Process Algebra

    Cite this

    Timmer, M., van de Pol, J. C., & Stoelinga, M. I. A. (2013). Confluence Reduction for Markov Automata. In V. Braberman, & L. Fribourg (Eds.), Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS) (pp. 243-257). (Lecture Notes in Computer Science; Vol. 8053). Berlin: Springer. https://doi.org/10.1007/978-3-642-40229-6_17