Demonic, angelic and unbounded probabilistic choices in sequential programs

A. K. McIver*, C. Morgan

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)


Probabilistic predicate transformers extend standard predicate transformers by adding probabilistic choice to (transformers for) sequential programs; demonic nondeterminism is retained. For finite state spaces, the basic theory is set out elsewhere [17], together with a presentation of the probabilistic 'healthiness conditions' that generalise the 'positive conjunctivity' of ordinary predicate transformers. Here we expand the earlier results beyond ordinary conjunctive transformers, investigating the structure of the transformer space more generally: as Back and von Wright [1] did for the standard (non-probabilistic) case, we nest deterministic, demonic and demonic/angelic transformers, showing how each subspace can be constructed from the one before. We show also that the results hold for infinite state spaces. In the end we thus find characteristic healthiness conditions for the hierarchies of a system in which deterministic, demonic, probabilistic and angelic choices all coexist.

Original languageEnglish
Pages (from-to)329-354
Number of pages26
JournalActa Informatica
Issue number4-5
Publication statusPublished - Jan 2001
Externally publishedYes


Dive into the research topics of 'Demonic, angelic and unbounded probabilistic choices in sequential programs'. Together they form a unique fingerprint.

Cite this