Probabilistic transition system specifications (PTSSs) in the ntμfθ=ntμxθ 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μfθ=ntμxθ, 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.
|Journal||Electronic Proceedings in Theoretical Computer Science|
|Publication status||Published - 2015|
Bibliographical notePT: J; NR: 26; TC: 0; J9: ELECTRON PROC THEOR; PG: 15; GA: CZ8HF; UT: WOS:000367340100004
D'Argenio, P. R., Lee, M. D., & Gebler, D. (2015). SOS rule formats for convex and abstract probabilistic bisimulations. Electronic Proceedings in Theoretical Computer Science, (190), 31-45. https://doi.org/10.4204/EPTCS.190.3