Algorithmic probabilistic game semantics. Playing games with automata. (English) Zbl 1291.68294

Summary: 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.


68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68Q45 Formal languages and automata
91A80 Applications of game theory


MRMC; Ymer; LiQuor; PRISM
Full Text: DOI


[1] Abramsky, S; Schwichtenberg, H (ed.); Steinbruggen, R (ed.), Algorithmic games semantics: a tutorial introduction, 21-47, (2002), Dordrecht
[2] Abramsky, S; McCusker, G, Call-by-value games, No. 1414, 1-17, (1997), Berlin · Zbl 0908.03035
[3] Abramsky, S; McCusker, G; Schwichtenberg, H (ed.); Berger, U (ed.), Game semantics, (1998), Berlin
[4] Abramsky, S; Jagadeesan, R; Malacaria, P, Full abstraction for PCF, Inf Comput, 163, 409-470, (2000) · Zbl 1006.68028
[5] Bause, F; Buchholz, P; Kemper, P, A toolbox for functional and quantitative analysis of DEDS, No. 1469, (1998)
[6] Bernardo, M; Cleaveland, R; Sims, S; Stewart, W, Twotowers: a tool integrating functional and performance analysis of concurrent systems, No. 135, (1998)
[7] Bhargava, M; Palamidessi, C, Probabilistic anonymity, No. 3653, 171-185, (2005), Berlin · Zbl 1134.68426
[8] Chaum, D, The dining cryptographers problem: unconditional sender and recipient untraceability, J Cryptol, 1, 65-75, (1988) · Zbl 0654.94012
[9] Ciesinski, F; Baier, C, Liquor: a tool for qualitative and quantitative linear time analysis of reactive systems, (2006), Washington
[10] Cormen TH, Leiserson CE, Rivest RL, Stein C (2001) Introduction to algorithms, 2nd edn. MIT Press, Cambridge
[11] Danos, V; Harmer, R, Probabilistic game semantics, ACM Trans Comput Log, 3, 359-382, (2002) · Zbl 1365.68310
[12] D’Argenio, PR; Jeannet, B; Jensen, HE; Larsen, KG, Reachability analysis of probabilistic systems by successive refinements, No. 2165, (2001) · Zbl 1007.68131
[13] Dreyer, D; Neis, G; Birkedal, L, The impact of higher-order state and control effects on local relational reasoning, 143-156, (2010), New York · Zbl 1323.68203
[14] Hartonas-Garmhausen, V; Vale Aguiar Campos, S; Clarke, EM, Probverus: probabilistic symbolic model checking, No. 1601, (1999)
[15] Hermanns, H; Katoen, J-P; Meyer-Kayser, J; Siegle, M, A Markov chain model checker, No. 1785, (2000) · Zbl 0960.68108
[16] Hibbard, TN, Some combinatorial properties of certain trees with applications to searching and sorting, J ACM, 9, 13-28, (1962) · Zbl 0116.09410
[17] Honda, K; Yoshida, N, Game-theoretic analysis of call-by-value computation, Theor Comput Sci, 221, 393-456, (1999) · Zbl 0930.68061
[18] Hopkins, D; Murawski, AS; Ong, C-HL, A fragment of ML decidable by visibly pushdown automata, No. 6756, 149-161, (2011), Berlin · Zbl 1333.68079
[19] Hurd J (2002) Formal verification of probabilistic algorithms. PhD thesis, University of Cambridge · Zbl 1013.68193
[20] Hyland, JME; Ong, C-HL, On full abstraction for PCF: I. models, observables and the full abstraction problem, II. dialogue games and innocent strategies, III. A fully abstract and universal game model, Inf Comput, 163, 285-408, (2000) · Zbl 1006.68027
[21] Jonassen, AT; Knuth, DE, A trivial algorithm whose analysis isn’t, J Comput Syst Sci, 16, 301-322, (1978) · Zbl 0376.68030
[22] Kacprzak, M; Lomuscio, A; Niewiadomski, A; Penczek, W; Raimondi, F; Szreter, M, Comparing bdd and sat based techniques for model checking chaum’s dining cryptographers protocol, Fundam Inform, 72, 215-234, (2006) · Zbl 1097.68074
[23] Katoen, J-P; Khattri, M; Zapreev, IS, A Markov reward model checker, (2005), Washington
[24] Kiefer, S; Murawski, AS; Ouaknine, J; Wachter, B; Worrell, J, Language equivalence for probabilistic automata, No. 6806, 526-540, (2011), Berlin
[25] Knott GD (1975) Deletion in binary storage trees. PhD thesis, Stanford University. Computer Science Technical Report STAN-CS-75-491 · Zbl 0654.94012
[26] Knuth, DE, Sorting and searching, (1973), Reading
[27] Kwiatkowska, MZ; Norman, G; Parker, D, Prism 4.0: verification of probabilistic real-time systems, 585-591, (2011)
[28] Legay, A; Murawski, AS; Ouaknine, J; Worrell, J, On automated verification of probabilistic programs, No. 4963, 173-187, (2008), Berlin
[29] McIver, A; Morgan, C, Abstraction and refinement in probabilistic systems, SIGMETRICS Perform Eval Rev, 32, 41-47, (2005)
[30] McIver, A; Morgan, C, The thousand-and-one cryptographers, (2010), Berlin · Zbl 1209.68231
[31] Milner, R, Fully abstract models of typed lambda-calculi, Theor Comput Sci, 4, 1-22, (1977) · Zbl 0386.03006
[32] Mohri, M, Generic e-removal and input e-normalization algorithms for weighted transducers, Int J Found Comput Sci, 13, 129-143, (2002) · Zbl 1066.68070
[33] Motwani R, Raghavan P (1995) Randomized algorithms. Cambridge University Press, Cambridge · Zbl 0849.68039
[34] Murawski, AS, Functions with local state: regularity and undecidability, Theor Comput Sci, 338, 315-349, (2005) · Zbl 1108.68076
[35] Murawski, AS; Ouaknine, J, On probabilistic program equivalence and refinement, No. 3653, 156-170, (2005), Berlin · Zbl 1134.68351
[36] Nickau, H, Hereditarily sequential functionals, (1994), Berlin · Zbl 0946.03053
[37] Rabin, MO, Probabilistic automata, Inf Control, 6, 230-245, (1963) · Zbl 0182.33602
[38] Rabin, MO, Probabilistic algorithms, 21-39, (1976), New York
[39] Reiter, MK; Rubin, AD, Crowds: anonymity for web transactions, ACM Trans Inf Syst Secur, 1, 66-92, (1998)
[40] Reynolds, JC; Bakker, JW (ed.); Vliet, JC (ed.), The essence of algol, 345-372, (1978), Amsterdam
[41] Sangiorgi, D; Kobayashi, N; Sumii, E, Environmental bisimulations for higher-order languages, ACM Trans Program Lang Syst, 33, 5, (2011)
[42] Schneider, S; Sidiropoulos, A, Csp and anonymity, No. 1146, 198-218, (1996), Berlin
[43] Shmatikov, V, Probabilistic model checking of an anonymity system, J Comput Secur, 12, 355-377, (2004)
[44] Meyden, R; Su, K, Symbolic model checking the knowledge of the dining cryptographers, 280, (2004), Washington
[45] Glabbeek, RJ; Smolka, SA; Steffen, B, Reactive, generative and stratified models of probabilistic processes, Inf Comput, 121, 285-408, (1995)
[46] Younes, HLS, Ymer: a statistical model checker, No. 3576, (2005) · Zbl 1081.68642
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.