Predicate transformers for extended probability and non-determinism

Klaus Keimel, Gordon Plotkin

Research output: Contribution to journalArticlepeer-review


We investigate laws for predicate transformers for the combination of non-deterministic choice and (extended) probabilistic choice, where predicates are taken to be functions to the extended non-negative reals, or to closed intervals of such reals. These predicate transformers correspond to state transformers, which are functions to conical powerdomains, which are the appropriate powerdomains for the combined forms of non-determinism. As with standard powerdomains for non-deterministic choice, these come in three flavours so there are also three kinds of predicate transformers. In order to make the connection, the powerdomains are first characterised in terms of relevant classes of functionals.

Much of the development is carried out at an abstract level, a kind of domain-theoretic functional analysis: one considers d-cones, which are dcpos equipped with a module structure over the non-negative extended reals, in place of topological vector spaces. Such a development still needs to be carried out for probabilistic choice per se; it would presumably be necessary to work with a notion of convex space rather than a cone.
Original languageEnglish
Pages (from-to)501-539
Number of pages39
JournalMathematical Structures in Computer Science
Issue number3
Publication statusPublished - Jun 2009

Fingerprint Dive into the research topics of 'Predicate transformers for extended probability and non-determinism'. Together they form a unique fingerprint.

Cite this