Confluence reduction for Markov automata

Research output: Contribution to journalArticle

  • 2 Citations

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.
LanguageEnglish
Pages193-219
Number of pages27
JournalTheoretical computer science
Volume655
Issue numberB
Early online date19 Jan 2016
DOIs
StatePublished - 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",

}

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

T2 - Theoretical computer science

JF - Theoretical computer science

SN - 0304-3975

IS - B

ER -