Markov Automata: Deciding weak bisimulation by means of non-naievely vanishing states

摘要

This paper develops a decision algorithm for weak bisimulation on Markov Automata (MA). For this purpose, different notions of vanishing states (a concept originating from the area of Generalised Stochastic Petri Nets) are defined. In particular, non-naively vanishing states are shown to be essential for relating the concepts of (state-based) naieve weak bisimulation and (distribution-based) weak bisimulation. The bisimulation algorithm presented here follows the partition-refinement scheme and has exponential time complexity.