Confluence reduction for Markov automata (extended version)

    Research output: Book/ReportReportProfessional

    82 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
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages26
    Publication statusPublished - Jun 2013

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
    No.TR-CTIT-13-14
    ISSN (Print)1381-3625

    Keywords

    • Divergence-sensitive branching bisimulation
    • Markov automata
    • Confluence
    • State space reduction
    • Process algebra
    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/318490
    • EC Grant Agreement nr.: FP7/318003

    Fingerprint

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

    Cite this