SOS rule formats for convex and abstract probabilistic bisimulations

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

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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
DOIs
Publication statusPublished - 2015

Fingerprint

Semantics
Specifications

Bibliographical note

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

Cite this

@article{9690962c0837433aba2c4cab16280336,
title = "SOS rule formats for convex and abstract probabilistic bisimulations",
abstract = "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.",
author = "P.R. D'Argenio and M.D. Lee and D. Gebler",
note = "PT: J; NR: 26; TC: 0; J9: ELECTRON PROC THEOR; PG: 15; GA: CZ8HF; UT: WOS:000367340100004",
year = "2015",
doi = "10.4204/EPTCS.190.3",
language = "English",
pages = "31--45",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",
number = "190",

}

SOS rule formats for convex and abstract probabilistic bisimulations. / D'Argenio, P.R.; Lee, M.D.; Gebler, D.

In: Electronic Proceedings in Theoretical Computer Science, No. 190, 2015, p. 31-45.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - SOS rule formats for convex and abstract probabilistic bisimulations

AU - D'Argenio, P.R.

AU - Lee, M.D.

AU - Gebler, D.

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

PY - 2015

Y1 - 2015

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

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

U2 - 10.4204/EPTCS.190.3

DO - 10.4204/EPTCS.190.3

M3 - Article

SP - 31

EP - 45

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

IS - 190

ER -