SOS rule formats for convex and abstract probabilistic bisimulations

P.R. D'Argenio, M.D. Lee, D. Gebler

Research output: Contribution to JournalArticleAcademicpeer-review


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.
Original languageEnglish
Pages (from-to)31-45
JournalElectronic Proceedings in Theoretical Computer Science
Issue number190
Publication statusPublished - 2015

Bibliographical note

PT: J; NR: 26; TC: 0; J9: ELECTRON PROC THEOR; PG: 15; GA: CZ8HF; UT: WOS:000367340100004


Dive into the research topics of 'SOS rule formats for convex and abstract probabilistic bisimulations'. Together they form a unique fingerprint.

Cite this