×

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.

MSC:

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

Software:

PRISM; LiQuor; Ymer; MRMC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S.; Schwichtenberg, H. (ed.); Steinbruggen, R. (ed.), Algorithmic games semantics: a tutorial introduction, 21-47 (2002), Dordrecht · doi:10.1007/978-94-010-0413-8_2
[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 (2000) Full abstraction for PCF. Inf Comput 163:409-470 · Zbl 1006.68028 · doi:10.1006/inco.2000.2930
[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 (1988) The dining cryptographers problem: unconditional sender and recipient untraceability. J Cryptol 1(1):65-75 · Zbl 0654.94012 · doi:10.1007/BF00206326
[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 (2002) Probabilistic game semantics. ACM Trans Comput Log 3(3):359-382 · Zbl 1365.68310 · doi:10.1145/507382.507385
[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 (1962) Some combinatorial properties of certain trees with applications to searching and sorting. J ACM 9(1):13-28 · Zbl 0116.09410 · doi:10.1145/321105.321108
[17] Honda K, Yoshida N (1999) Game-theoretic analysis of call-by-value computation. Theor Comput Sci 221(1-2):393-456 · Zbl 0930.68061 · doi:10.1016/S0304-3975(99)00039-0
[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 (2000) 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(2):285-408 · Zbl 1006.68027 · doi:10.1006/inco.2000.2917
[21] Jonassen AT, Knuth DE (1978) A trivial algorithm whose analysis isn’t. J Comput Syst Sci 16(3):301-322 · Zbl 0376.68030 · doi:10.1016/0022-0000(78)90020-X
[22] Kacprzak M, Lomuscio A, Niewiadomski A, Penczek W, Raimondi F, Szreter M (2006) Comparing bdd and sat based techniques for model checking Chaum’s dining cryptographers protocol. Fundam Inform 72(1-3):215-234 · 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 (2005) Abstraction and refinement in probabilistic systems. SIGMETRICS Perform Eval Rev 32(4):41-47 · doi:10.1145/1059816.1059824
[30] McIver, A.; Morgan, C., The thousand-and-one cryptographers (2010), Berlin · Zbl 1209.68231
[31] Milner R (1977) Fully abstract models of typed lambda-calculi. Theor Comput Sci 4(1):1-22 · Zbl 0386.03006 · doi:10.1016/0304-3975(77)90053-6
[32] Mohri M (2002) Generic e-removal and input e-normalization algorithms for weighted transducers. Int J Found Comput Sci 13(1):129-143 · Zbl 1066.68070 · doi:10.1142/S0129054102000996
[33] Motwani R, Raghavan P (1995) Randomized algorithms. Cambridge University Press, Cambridge · Zbl 0849.68039 · doi:10.1017/CBO9780511814075
[34] Murawski AS (2005) Functions with local state: regularity and undecidability. Theor Comput Sci 338(1/3):315-349 · Zbl 1108.68076 · doi:10.1016/j.tcs.2004.12.036
[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 (1963) Probabilistic automata. Inf Control 6(3):230-245 · Zbl 0182.33602 · doi:10.1016/S0019-9958(63)90290-0
[38] Rabin, MO, Probabilistic algorithms, 21-39 (1976), New York
[39] Reiter MK, Rubin AD (1998) Crowds: anonymity for web transactions. ACM Trans Inf Syst Secur 1(1):66-92 · doi:10.1145/290163.290168
[40] Reynolds, JC; Bakker, JW (ed.); Vliet, JC (ed.), The essence of Algol, 345-372 (1978), Amsterdam
[41] Sangiorgi D, Kobayashi N, Sumii E (2011) Environmental bisimulations for higher-order languages. ACM Trans Program Lang Syst 33(1):5 · doi:10.1145/1889997.1890002
[42] Schneider, S.; Sidiropoulos, A., Csp and anonymity, No. 1146, 198-218 (1996), Berlin · Zbl 1493.68049 · doi:10.1007/3-540-61770-1_38
[43] Shmatikov V (2004) Probabilistic model checking of an anonymity system. J Comput Secur 12(3/4):355-377
[44] Meyden, R.; Su, K., Symbolic model checking the knowledge of the dining cryptographers, 280 (2004), Washington
[45] van Glabbeek RJ, Smolka SA, Steffen B (1995) Reactive, generative and stratified models of probabilistic processes. Inf Comput 121(2):285-408
[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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.