Bisimulation of Labeled State-to-Function Transition Systems of Stochastic Process Languages

TL;DR

This paper introduces a bisimulation concept for labeled state-to-function transition systems (FuTS) used in stochastic process languages, establishing a formal correspondence with behavioral equivalence and connecting existing process algebra equivalences to FuTS bisimulation.

Contribution

It proposes a new bisimulation notion for FuTS and proves its equivalence with behavioral equivalence, providing coalgebraic justification for existing process algebra equivalences.

Findings

FuTS bisimulation coincides with behavioral equivalence

Established correspondence for ACP, PEPA, and IMC

Provides coalgebraic foundation for process algebra equivalences

Abstract

Labeled state-to-function transition systems, FuTS for short, admit multiple transition schemes from states to functions of finite support over general semirings. As such they constitute a convenient modeling instrument to deal with stochastic process languages. In this paper, the notion of bisimulation induced by a FuTS is proposed and a correspondence result is proven stating that FuTS-bisimulation coincides with the behavioral equivalence of the associated functor. As generic examples, the concrete existing equivalences for the core of the process algebras ACP, PEPA and IMC are related to the bisimulation of specific FuTS, providing via the correspondence result coalgebraic justification of the equivalences of these calculi.