Confluence Reduction for Markov Automata

TitleConfluence Reduction for Markov Automata
Publication TypeConference Paper
Year of Publication2013
AuthorsTimmer M., van de Pol J.C, Stoelinga M.IA
EditorBraberman V.A, Fribourg L.
Conference NameProceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Buenos Aires, Argentina
Date PublishedAugust
PublisherSpringer Verlag
Conference LocationBerlin
KeywordsConfluence, Divergence-sensitive branching bisimulation, Markov automata, Process algebra, State space reduction

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.