Markov Automata: Deciding Weak Bisimulation by means of non-naively Vanishing States

TL;DR

This paper introduces a decision algorithm for weak bisimulation in Markov Automata, utilizing vanishing states to connect naive and distribution-based bisimulation concepts, with a partition-refinement approach and exponential complexity.

Contribution

It defines vanishing states for Markov Automata and develops a partition-refinement algorithm for weak bisimulation decision-making.

Findings

Vanishing states are crucial for relating different bisimulation notions.

The proposed algorithm follows a partition-refinement scheme.

The algorithm has exponential time complexity.

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.