Algorithmic probabilistic game semantics
We present a detailed account of a translation from probabilistic call-by-value programs with procedures to Rabin's probabilistic automata. The translation is fully abstract in that programs exhibit the same computational behaviour if and only if the corresponding automata are language-equivale...
| Main Authors: | , , , , |
|---|---|
| Format: | Journal article |
| Published: |
2013
|
| _version_ | 1826302288509009920 |
|---|---|
| author | Kiefer, S Murawski, A Ouaknine, J Wachter, B Worrell, J |
| author_facet | Kiefer, S Murawski, A Ouaknine, J Wachter, B Worrell, J |
| author_sort | Kiefer, S |
| collection | OXFORD |
| description | We present a detailed account of a translation from probabilistic call-by-value programs with procedures to Rabin's probabilistic automata. The translation is fully abstract in that programs exhibit the same computational behaviour if and only if the corresponding automata are language-equivalent. Since probabilistic language equivalence is decidable, we can apply the translation to analyse the behaviour of probabilistic programs and protocols. We illustrate our approach on a number of case studies. © 2012 Springer Science+Business Media, LLC. |
| first_indexed | 2024-03-07T05:45:18Z |
| format | Journal article |
| id | oxford-uuid:e707dd46-893f-4316-aa5c-e0c000c5852f |
| institution | University of Oxford |
| last_indexed | 2024-03-07T05:45:18Z |
| publishDate | 2013 |
| record_format | dspace |
| spelling | oxford-uuid:e707dd46-893f-4316-aa5c-e0c000c5852f2022-03-27T10:35:26ZAlgorithmic probabilistic game semanticsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:e707dd46-893f-4316-aa5c-e0c000c5852fSymplectic Elements at Oxford2013Kiefer, SMurawski, AOuaknine, JWachter, BWorrell, JWe present a detailed account of a translation from probabilistic call-by-value programs with procedures to Rabin's probabilistic automata. The translation is fully abstract in that programs exhibit the same computational behaviour if and only if the corresponding automata are language-equivalent. Since probabilistic language equivalence is decidable, we can apply the translation to analyse the behaviour of probabilistic programs and protocols. We illustrate our approach on a number of case studies. © 2012 Springer Science+Business Media, LLC. |
| spellingShingle | Kiefer, S Murawski, A Ouaknine, J Wachter, B Worrell, J Algorithmic probabilistic game semantics |
| title | Algorithmic probabilistic game semantics |
| title_full | Algorithmic probabilistic game semantics |
| title_fullStr | Algorithmic probabilistic game semantics |
| title_full_unstemmed | Algorithmic probabilistic game semantics |
| title_short | Algorithmic probabilistic game semantics |
| title_sort | algorithmic probabilistic game semantics |
| work_keys_str_mv | AT kiefers algorithmicprobabilisticgamesemantics AT murawskia algorithmicprobabilisticgamesemantics AT ouakninej algorithmicprobabilisticgamesemantics AT wachterb algorithmicprobabilisticgamesemantics AT worrellj algorithmicprobabilisticgamesemantics |