Confluence reduction for Markov automata (extended version)

    Research output: Book/ReportReportProfessional

    21 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
    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
    • IR-86237
    • METIS-297688
    • Process Algebra
    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/318490
    • EC Grant Agreement nr.: FP7/318003
    • EWI-23418
    • State space reduction

    Cite this

    Timmer, M., van de Pol, J. C., & Stoelinga, M. I. A. (2013). Confluence reduction for Markov automata (extended version). (CTIT Technical Report Series; No. TR-CTIT-13-14). Enschede: Centre for Telematics and Information Technology (CTIT).
    Timmer, Mark ; van de Pol, Jan Cornelis ; Stoelinga, Mariëlle Ida Antoinette. / Confluence reduction for Markov automata (extended version). Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 26 p. (CTIT Technical Report Series; TR-CTIT-13-14).
    @book{803bde2922fc4253b121c22a3fef4ebd,
    title = "Confluence reduction for Markov automata (extended version)",
    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.",
    keywords = "Divergence-sensitive branching bisimulation, Markov Automata, Confluence, IR-86237, METIS-297688, Process Algebra, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318490, EC Grant Agreement nr.: FP7/318003, EWI-23418, State space reduction",
    author = "Mark Timmer and {van de Pol}, {Jan Cornelis} and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
    note = "Foreground = 20{\%}; Type of activity = technical report; Main leader = UT; Type of audience = scientific community; Size of audience = n.a.; Countries addressed = international;",
    year = "2013",
    month = "6",
    language = "Undefined",
    series = "CTIT Technical Report Series",
    publisher = "Centre for Telematics and Information Technology (CTIT)",
    number = "TR-CTIT-13-14",
    address = "Netherlands",

    }

    Timmer, M, van de Pol, JC & Stoelinga, MIA 2013, Confluence reduction for Markov automata (extended version). CTIT Technical Report Series, no. TR-CTIT-13-14, Centre for Telematics and Information Technology (CTIT), Enschede.

    Confluence reduction for Markov automata (extended version). / Timmer, Mark; van de Pol, Jan Cornelis; Stoelinga, Mariëlle Ida Antoinette.

    Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 26 p. (CTIT Technical Report Series; No. TR-CTIT-13-14).

    Research output: Book/ReportReportProfessional

    TY - BOOK

    T1 - Confluence reduction for Markov automata (extended version)

    AU - Timmer, Mark

    AU - van de Pol, Jan Cornelis

    AU - Stoelinga, Mariëlle Ida Antoinette

    N1 - Foreground = 20%; Type of activity = technical report; Main leader = UT; Type of audience = scientific community; Size of audience = n.a.; Countries addressed = international;

    PY - 2013/6

    Y1 - 2013/6

    N2 - 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.

    AB - 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.

    KW - Divergence-sensitive branching bisimulation

    KW - Markov Automata

    KW - Confluence

    KW - IR-86237

    KW - METIS-297688

    KW - Process Algebra

    KW - EC Grant Agreement nr.: FP7/2007-2013

    KW - EC Grant Agreement nr.: FP7/318490

    KW - EC Grant Agreement nr.: FP7/318003

    KW - EWI-23418

    KW - State space reduction

    M3 - Report

    T3 - CTIT Technical Report Series

    BT - Confluence reduction for Markov automata (extended version)

    PB - Centre for Telematics and Information Technology (CTIT)

    CY - Enschede

    ER -

    Timmer M, van de Pol JC, Stoelinga MIA. Confluence reduction for Markov automata (extended version). Enschede: Centre for Telematics and Information Technology (CTIT), 2013. 26 p. (CTIT Technical Report Series; TR-CTIT-13-14).