Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Algorithmic probabilistic game semantics – Playing games with automata


Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Algorithmic probabilistic game semantics – playing games with automata. Formal Methods in System Design, 43(2):285–312, 2013.


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.

Suggested BibTeX entry:

    author = {Stefan Kiefer and Andrzej S. Murawski and Jo{\"e}l Ouaknine and Bj{\"o}rn Wachter and James Worrell},
    journal = {Formal Methods in System Design},
    number = {2},
    pages = {285--312},
    title = {Algorithmic probabilistic game semantics -- Playing games with automata},
    volume = {43},
    year = {2013}

PDF (1 MB)