Markov Automata: Deciding Weak Bisimulation by means of non-naively Vanishing States
arXiv:1205.6192
Abstract
This paper develops a decision algorithm for weak bisimulation on Markov Automata (MA). For that purpose, different notions of vanishing state (a concept known from the area of Generalised Stochastic Petri Nets) are defined. Vanishing states are shown to be essential for relating the concepts of (state-based) naive weak bisimulation and (distribution-based) weak bisimulation. The bisimulation algorithm presented here follows the partition-refinement scheme and has exponential time complexity.
arXiv commentMain results stay the same as in the previous versions, but the proofs have completely changed