SOS rule formats for convex and abstract probabilistic bisimulations

TL;DR

This paper introduces SOS rule formats for convex and abstract probabilistic bisimulations, ensuring these equivalences are congruences in probabilistic transition systems, and compares their properties and logical characterizations.

Contribution

It extends existing PTSS formats to guarantee congruence for new coarser bisimulation equivalences, including convex, probability obliterated, and probability abstracted bisimulations.

Findings

Convex bisimulation is a congruence under the new format.

Probability obliterated bisimulation is characterized and compared.

A logic characterization is provided for each bisimulation.

Abstract

Probabilistic transition system specifications (PTSSs) in the $nt \mu f\theta / nt\mu x\theta$ format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that bisimilarity is a congruence for all operator defined in such format. Starting from the $nt \mu f\theta / nt\mu x\theta$ format, we obtain restricted formats that guarantee that three coarser bisimulation equivalences are congruences. We focus on (i) Segala's variant of bisimulation that considers combined transitions, which we call here "convex bisimulation"; (ii) the bisimulation equivalence resulting from considering Park & Milner's bisimulation on the usual stripped probabilistic transition system (translated into a labelled transition system), which we call here "probability obliterated bisimulation"; and (iii) a "probability abstracted bisimulation", which, like bisimulation, preserves the structure of the distributions but instead, it ignores the probability values. In addition, we compare these bisimulation equivalences and provide a logic characterization for each of them.