Late Weak Bisimulation for Markov Automata

TL;DR

This paper introduces late weak bisimilarity for Markov automata, a coarser behavioral equivalence that maintains key properties under specific scheduler restrictions, enhancing compositional analysis.

Contribution

It defines a new coarser bisimilarity notion for Markov automata that preserves compositionality under important scheduler subclasses.

Findings

Late weak bisimilarity is coarser than standard weak bisimilarity.

Trace distribution equivalence holds for partial information schedulers.

Compositionality is preserved under distributed schedulers.

Abstract

Weak bisimilarity is a distribution-based equivalence notion for Markov automata. It has gained some popularity as the coarsest reasonable behavioural equivalence on Markov automata. This paper studies a strictly coarser notion: Late weak bisimilarity enjoys valuable properties if restricting to important subclasses of schedulers: Trace distribution equivalence is implied for partial information schedulers, and compositionality is preserved by distributed schedulers. The intersection of the two scheduler classes thus spans a coarser and still reasonable compositional theory of Markov automata.