An expectation transformer approach to predicate abstraction and data independence for probabilistic programs

Ukachukwu Ndukwu
(Deptartment of Computing, Macquarie University, NSW 2109 Australia.)
Annabelle McIver
(Deptartment of Computing, Macquarie University, NSW 2109 Australia.)

In this paper we revisit the well-known technique of predicate abstraction to characterise performance attributes of system models incorporating probability. We recast the theory using expectation transformers, and identify transformer properties which correspond to abstractions that yield nevertheless exact bound on the performance of infinite state probabilistic systems. In addition, we extend the developed technique to the special case of "data independent" programs incorporating probability. Finally, we demonstrate the subtleness of the extended technique by using the PRISM model checking tool to analyse an infinite state protocol, obtaining exact bounds on its performance.

In Alessandra Di Pierro and Gethin Norman: Proceedings Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL 2010), Paphos, Cyprus, 27-28th March 2010 , Electronic Proceedings in Theoretical Computer Science 28, pp. 129–143.
Published: 26th June 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.28.9 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org