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

TL;DR

This paper introduces an expectation transformer-based method for predicate abstraction in probabilistic programs, enabling precise performance bounds for infinite state systems and extending to data-independent cases, demonstrated via PRISM.

Contribution

It recasts predicate abstraction using expectation transformers and extends the technique to data-independent probabilistic programs, providing exact performance bounds.

Findings

Exact bounds on infinite state probabilistic systems achieved

Extension of predicate abstraction to data-independent programs

Successful analysis of an infinite state protocol with PRISM

Abstract

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.