Confluence reduction for Markov automata

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    96 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 languageEnglish
    Title of host publicationProceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013)
    Place of PublicationTrieste
    PublisherUniversity of Trieste
    Pages18
    Number of pages4
    Publication statusPublished - Mar 2013
    Event11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013 - Rome, Italy
    Duration: 23 Mar 201324 Mar 2013
    Conference number: 11
    http://eptcs.web.cse.unsw.edu.au/content.cgi?QAPL2013

    Workshop

    Workshop11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013
    Abbreviated titleQAPL 2013
    Country/TerritoryItaly
    CityRome
    Period23/03/1324/03/13
    Internet address

    Keywords

    • EC Grant Agreement nr.: FP7/318003
    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/318490

    Fingerprint

    Dive into the research topics of 'Confluence reduction for Markov automata'. Together they form a unique fingerprint.

    Cite this