An adequacy theorem between mixed powerdomains and probabilistic concurrency (extended version)

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 probabilistic concurrent programming using mixed powerdomains and topological methods, extending previous theoretical frameworks.

Findings

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

Shows semi-decidability of program property satisfaction in probabilistic concurrency

Connects the theorem to semi-decidability in probabilistic testing scenarios

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. Escard\'o's conjecture about semi-decidability w.r.t. may and must probabilistic testing.