Edinburgh Research Explorer

Mixed powerdomains for probability and nondeterminism

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Access status

Open

Documents

  • Download as Adobe PDF

    Final published version, 753 KB, PDF-document

    License: Creative Commons: Attribution Non-Commercial (CC-BY-NC)

https://lmcs.episciences.org/2665
Original languageEnglish
Pages (from-to)1-84
Number of pages84
JournalLogical Methods in Computer Science
Volume13
Issue number1
DOIs
StatePublished - 24 Jan 2017

Abstract

We consider mixed powerdomains combining ordinary nondeterminism and probabilistic nondeterminism. We characterise them as free algebras for suitable (in)equation-al theories; we establish functional representation theorems; and we show equivalencies between state transformers and appropriately healthy predicate transformers. The extended nonnegative reals serve as `truth-values'. As usual with powerdomains, everything comes in three flavours: lower, upper, and order-convex. The powerdomains are suitable convex sets of subprobability valuations, corresponding to resolving nondeterministic choice before probabilistic choice. Algebraically this corresponds to the probabilistic choice operator distributing over the nondeterministic choice operator. (An alternative approach to combining the two forms of nondeterminism would be to resolve probabilistic choice first, arriving at a domain-theoretic version of random sets. However, as we also show, the algebraic approach then runs into difficulties.) Rather than working directly with valuations, we take a domain-theoretic functional-analytic approach, employing domain-theoretic abstract convex sets called Kegelspitzen; these are equivalent to the abstract probabilistic algebras of Graham and Jones, but are more convenient to work with. So we define power Kegelspitzen, and consider free algebras, functional representations, and predicate transformers. To do so we make use of previous work on domain-theoretic cones (d-cones), with the bridge between the two of them being provided by a free d-cone construction on Kegelspitzen.

ID: 29566916