Confluence reduction for Markov automata

    Research output: Contribution to journalArticleAcademicpeer-review

    3 Citations (Scopus)
    97 Downloads (Pure)

    Abstract

    Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. As expected, the state space explosion threatens the analysability of these models. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep them small by omitting internal transitions. We define the notion of confluence directly on Markov automata, and discuss additionally how to syntactically detect confluence on the process-algebraic language MAPA that was introduced recently. 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
    Pages (from-to)193-219
    Number of pages27
    JournalTheoretical computer science
    Volume655
    Issue numberB
    Early online date19 Jan 2016
    DOIs
    Publication statusPublished - 6 Dec 2016

    Fingerprint

    Confluence
    Automata
    Explosions
    Nondeterminism
    Bisimulation
    Explosion
    Specifications
    Branching
    Divergence
    State Space
    Specification
    Internal
    Demonstrate

    Keywords

    • Markov automata
    • Confluence
    • State space reduction
    • Process algebra
    • Divergence-sensitive branching bisimulation
    • Partial order reduction

    Cite this

    @article{b1acb1c753294408ad4c6e6f368ab21c,
    title = "Confluence reduction for Markov automata",
    abstract = "Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. As expected, the state space explosion threatens the analysability of these models. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep them small by omitting internal transitions. We define the notion of confluence directly on Markov automata, and discuss additionally how to syntactically detect confluence on the process-algebraic language MAPA that was introduced recently. 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 = "Markov automata, Confluence , State space reduction, Process algebra, Divergence-sensitive branching bisimulation, Partial order reduction",
    author = "Mark Timmer and Katoen, {Joost P.} and {van de Pol}, Jaco and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
    year = "2016",
    month = "12",
    day = "6",
    doi = "10.1016/j.tcs.2016.01.017",
    language = "English",
    volume = "655",
    pages = "193--219",
    journal = "Theoretical computer science",
    issn = "0304-3975",
    publisher = "Elsevier",
    number = "B",

    }

    Confluence reduction for Markov automata. / Timmer, Mark ; Katoen, Joost P.; van de Pol, Jaco ; Stoelinga, Mariëlle Ida Antoinette.

    In: Theoretical computer science, Vol. 655, No. B, 06.12.2016, p. 193-219.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Confluence reduction for Markov automata

    AU - Timmer, Mark

    AU - Katoen, Joost P.

    AU - van de Pol, Jaco

    AU - Stoelinga, Mariëlle Ida Antoinette

    PY - 2016/12/6

    Y1 - 2016/12/6

    N2 - Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. As expected, the state space explosion threatens the analysability of these models. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep them small by omitting internal transitions. We define the notion of confluence directly on Markov automata, and discuss additionally how to syntactically detect confluence on the process-algebraic language MAPA that was introduced recently. 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. As expected, the state space explosion threatens the analysability of these models. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep them small by omitting internal transitions. We define the notion of confluence directly on Markov automata, and discuss additionally how to syntactically detect confluence on the process-algebraic language MAPA that was introduced recently. 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 - Markov automata

    KW - Confluence

    KW - State space reduction

    KW - Process algebra

    KW - Divergence-sensitive branching bisimulation

    KW - Partial order reduction

    U2 - 10.1016/j.tcs.2016.01.017

    DO - 10.1016/j.tcs.2016.01.017

    M3 - Article

    VL - 655

    SP - 193

    EP - 219

    JO - Theoretical computer science

    JF - Theoretical computer science

    SN - 0304-3975

    IS - B

    ER -