Abstract
We study notions of equivalence and refinement for probabilistic programs formalized in the second-order fragment of Probabilistic Idealized Algol. Probabilistic programs implement randomized algorithms: a given input yields a probability distribution on the set of possible outputs. Intuitively, two programs are equivalent if they give rise to identical distributions for all inputs. We show that equivalence is decidable by studying the fully abstract game semantics of probabilistic programs and relating it to probabilistic finite automata. For terms in β-normal form our decision procedure runs in time exponential in the syntactic size of programs; it is moreover fully compositional in that it can handle open programs (probabilistic modules with unspecified components).
In contrast, we show that the natural notion of program refinement, in which the input-output distributions of one program uniformly dominate those of the other program, is undecidable.
Work supported by the UK EPSRC (GR/R88861/01) and St John’s College, Oxford.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Rabin, M.O.: Algorithms and Complexity. Academic Press, London (1976)
Motwani, R., Raghavan, P.: Randomized Algorithms. CUP (1995)
Reynolds, J.: The essence of Algol. In: de Bakker, J.W., van Vliet, J.C. (eds.) Algorithmic Languages. North-Holland, Amsterdam (1981)
Ghica, D.R., McCusker, G.: Reasoning about Idealized Algol using regular expressions. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853. Springer, Heidelberg (2000)
Abramsky, S., Ghica, D.R., Murawski, A.S., Ong, C.H.L.: Applying game semantics to compositional software modelling and verification. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 421–435. Springer, Heidelberg (2004)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 52. Springer, Heidelberg (2002)
Bustan, D., Rubin, S., Vardi, M.: Verifying ω-Regular Properties of Markov Chains. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 189–201. Springer, Heidelberg (2004)
Giacalone, A., Jou, C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: IFIP WG 2.2/2.3 Conference on Programming Concepts and Methods (1990)
Lowe, G.: Probabilistic and prioritized models of Timed CSP. Theoretical Computer Science 138(2) (1995)
Danos, V., Harmer, R.: Probabilistic game semantics. ACM Trans. on Comp. Logic 3(3) (2002)
Hyland, J.M.E., Ong, C.H.L.: On Full Abstraction for PCF. Information and Computation 163(2), 2000.
Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In: O’Hearn, P.W., Tennent, R.D. (eds.) Algol-like languages, Birkhaüser (1997)
Rabin, M.O.: Probabilistic automata. Information and Control 6(3) (1963)
Paz, A.: Introduction to Probabilistic Automata. Academic Press, London (1971)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT. Available as Technical Report MIT/LCS/TR-676 (1995)
Stoelinga, M.I.A.: An introduction to probabilistic automata. In: Rozenberg, G. (ed.) EATCS bulletin, vol. 78 (2002)
Tzeng, W.G.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing 21 (1992)
Blondel, V.D., Canterini, V.: Undecidable problems for probabilistic automata of fixed dimension. Theoretical Computer Science 36(3) (2003)
Mohri, M.: Generic e-removal and input e-normalization algorithms for weighted transducers. International Journal of Foundations of Computer Science 13 (2002)
Mohri, M.: Semiring frameworks and algorithms for shortest-distance problems. Journal of Automata, Languages and Combinatorics 7 (2002)
Abramsky, S.: Algorithmic games semantics: a tutorial introduction. In: Schwichtenberg, H., Steinbruggen, R. (eds.) Proof and System Reliability. Kluwer, Dordrecht (2002)
Murawski, A.: Games for complexity of second-order call-by-name programs. Theoretical Computer Science (to appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Murawski, A.S., Ouaknine, J. (2005). On Probabilistic Program Equivalence and Refinement. In: Abadi, M., de Alfaro, L. (eds) CONCUR 2005 – Concurrency Theory. CONCUR 2005. Lecture Notes in Computer Science, vol 3653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11539452_15
Download citation
DOI: https://doi.org/10.1007/11539452_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28309-6
Online ISBN: 978-3-540-31934-4
eBook Packages: Computer ScienceComputer Science (R0)