Recent work in probabilistic programming semantics has provided a relatively simple probabilistic extension to predicate transformers, making it possible to treat small imperative probabilistic programs containing both demonic and angelic nondeterminism [1, 2, 6]. That work in turn haws extended to provide a probabilistic basis for the modal ?-calculus of Kozen [3], and leads to a quantitative ?-calculus [4, 5].

Standard (non-probabilistic) ?-calculus can be interpreted either 'normally,' over its semantic domain, or as a two-player game between an 'angel' and a 'demon' representing the two forms of choice. Stirling [7] has argued that the two interpretations correspond.