Confluence reduction for Markov automata

详细信息    查看全文

• 作者：Mark Timmer^a ; ^{timmer@cs.utwente.nl} ; Joost-Pieter Katoen^a ; ^b ; ^{katoen@cs.rwth-aachen.de} ; Jaco van de Pol^a ; ^{vdpol@cs.utwente.nl} ; Marië ; lle Stoelinga^a ; ^{marielle@cs.utwente.nl}
• 关键词：Markov automata ; Confluence ; State space reduction ; Process algebra ; Divergence-sensitive branching bisimulation ; Partial order reduction
• 刊名：Theoretical Computer Science
• 出版年：2016
• 出版时间：6 December 2016
• 年：2016
• 卷：655
• 期：part_PB
• 页码：193-219
• 全文大小：1015 K
• 卷排序：655

文摘

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.