SOS rule formats for convex and abstract probabilistic bisimulations
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. Sta...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2015-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1508.06710v1 |
| _version_ | 1818315307930877952 |
|---|---|
| author | Pedro R. D'Argenio Matias David Lee Daniel Gebler |
| author_facet | Pedro R. D'Argenio Matias David Lee Daniel Gebler |
| author_sort | Pedro R. D'Argenio |
| collection | DOAJ |
| description | 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θ 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. |
| first_indexed | 2024-12-13T09:03:28Z |
| format | Article |
| id | doaj.art-9213a5bb80c141bcb4c4f7af4336be44 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-13T09:03:28Z |
| publishDate | 2015-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-9213a5bb80c141bcb4c4f7af4336be442022-12-21T23:53:08ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-08-01190Proc. EXPRESS/SOS 2015314510.4204/EPTCS.190.3:10SOS rule formats for convex and abstract probabilistic bisimulationsPedro R. D'Argenio0Matias David Lee1Daniel Gebler2 FaMAF, Universidad Nacional de Córdoba - CONICET FaMAF, Universidad Nacional de Córdoba - CONICET Department of Computer Science, VU University Amsterdam 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θ 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.http://arxiv.org/pdf/1508.06710v1 |
| spellingShingle | Pedro R. D'Argenio Matias David Lee Daniel Gebler SOS rule formats for convex and abstract probabilistic bisimulations Electronic Proceedings in Theoretical Computer Science |
| title | SOS rule formats for convex and abstract probabilistic bisimulations |
| title_full | SOS rule formats for convex and abstract probabilistic bisimulations |
| title_fullStr | SOS rule formats for convex and abstract probabilistic bisimulations |
| title_full_unstemmed | SOS rule formats for convex and abstract probabilistic bisimulations |
| title_short | SOS rule formats for convex and abstract probabilistic bisimulations |
| title_sort | sos rule formats for convex and abstract probabilistic bisimulations |
| url | http://arxiv.org/pdf/1508.06710v1 |
| work_keys_str_mv | AT pedrordargenio sosruleformatsforconvexandabstractprobabilisticbisimulations AT matiasdavidlee sosruleformatsforconvexandabstractprobabilisticbisimulations AT danielgebler sosruleformatsforconvexandabstractprobabilisticbisimulations |