We introduce a simple procedural probabilistic programming language which is suitable for coding a wide variety of randomised algorithms and protocols. This language is interpreted over finite datatypes and has a decidable equivalence problem. We have implemented an automated equivalence checker, which we call apex, for this language, based on game semantics. We illustrate our approach with three non-trivial case studies: (i) Herman's self-stabilisation algorithm; (ii) an analysis of the average shape of binary search trees obtained by certain sequences of random insertions and deletions; and (iii) the problem of anonymity in the Dining Cryptographers protocol. In particular, we record an exponential speed-up in the latter over state-of-the-art competing approaches. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Legay, A., Murawski, A. S., Ouaknine, J., & Worrell, J. (2008). On automated verification of probabilistic programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4963 LNCS, pp. 173–187). https://doi.org/10.1007/978-3-540-78800-3_13
Mendeley helps you to discover research relevant for your work.