Tags:Concurrent games, Event structures, Measure theory and Probability
Abstract:
Probabilistic strategies were first introduced by Danos and Harmer in a probabilistic extension of Hyland-Ong games. They work particularly well for modelling probabilistic programs with state: the model is fully abstract for a probabilistic variant of Idealised Algol. Recently, concurrent games were introduced as an alternative framework for game semantics, based on event structures, a fundamental model for concurrent processes. Concurrent games can also be enriched with probability, using a notion of probabilistic event structure, and this makes possible an analysis of Probabilistic PCF (including an intensional full abstraction result).
However all the above do not readily support continuous distributions, making those models unsatisfactory for practical probabilistic languages, in which such distributions are essential. Vakar and Ong have recently announced a generalisation of the Danos-Harmer model, which supports continuous distributions. They also describe an application to a stateful probabilistic language. Here we present a new probabilistic concurrent games model in which strategies are equipped to support arbitrary distributions on the real numbers. We rely on methods of measure theory and introduce measurable event structures, which generalise event structures and form the basis for a model of measurable concurrent games. Then one may adjoin probability in the form of a family of stochastic kernels. We illustrate the model by giving semantics to a higher-order, affine version of Probabilistic PCF with continuous distributions on the reals.
Continuous probability distributions in concurrent games