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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Murawski, A. S., & Ouaknine, J. (2005). On probabilistic program equivalence and refinement. In Lecture Notes in Computer Science (Vol. 3653, pp. 156–170). Springer Verlag. https://doi.org/10.1007/11539452_15
Mendeley helps you to discover research relevant for your work.