Proceedings Eighth Asia-Pacific Software Engineering Conference (2001)
Dec. 4, 2001 to Dec. 7, 2001
<p>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 , and leads to a quantitative ?-calculus [4, 5].</p> <p>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  has argued that the two interpretations correspond.</p>
C. Morgan and A. McIver, "Cost Analysis of Games, Using Program Logic," Proceedings Eighth Asia-Pacific Software Engineering Conference(APSEC), Macao, China, 2001, pp. 351.