An Adequacy Theorem Between Mixed Powerdomains and Probabilistic Concurrency

TL;DR

This paper establishes an adequacy theorem linking mixed powerdomains with probabilistic concurrency, providing a topological framework that supports semi-decidability of program properties in probabilistic concurrent programming.

Contribution

It introduces a novel adequacy theorem for a probabilistic concurrent language using mixed powerdomains and topological methods, extending prior theoretical frameworks.

Findings

Proves a topological generalisation of K"onig's lemma for probabilistic programming

Demonstrates semi-decidability of program property satisfaction

Connects the theorem to semi-decidability in probabilistic testing

Abstract

We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains, which combine non-determinism with probabilistic behaviour. The theorem itself is formulated via M. Smyth's idea of treating observable properties as open sets of a topological space. The proof hinges on a 'topological generalisation' of K\"onig's lemma in the setting of probabilistic programming (a result that is proved in the paper as well). One application of the theorem is that it entails semi-decidability w.r.t. whether a concurrent program satisfies an observable property (written in a certain form). This is related to M. Escardo's conjecture about semi-decidability w.r.t. may and must probabilistic testing.