Sos Rule Formats For Convex And Abstract Probabilistic Bisimulations

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, 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.