Forward and Backward Simulations for Partially Observable Probability

TL;DR

This paper extends simulation techniques to probabilistic and nondeterministic programs with partial observability, introducing a weakest precondition semantics and proving soundness of forward/backward simulations in this complex setting.

Contribution

It introduces a weakest precondition semantics for partially observable probabilistic programs and proves the soundness of forward/backward simulations under this new framework.

Findings

Soundness of simulations in probabilistic nondeterministic models

Duality between information leakage and exploitation in simulations

Framework for modeling probabilistic datatypes with encapsulated state

Abstract

Data refinement is the standard extension of a refinement relation from programs to datatypes (i.e. a behavioural subtyping relation). Forward/backward simulations provide a tractable method for establishing data refinement, and have been thoroughly studied for nondeterministic programs. However, for standard models of mixed probability and nondeterminism, ordinary assignment statements may not commute with (variable-disjoint) program fragments. This (1) invalidates a key assumption underlying the soundness of simulations, and (2) prevents modelling probabilistic datatypes with encapsulated state. We introduce a weakest precondition semantics for Kuifje$_\sqcap$, a language for partially observable Markov decision processes, using so-called loss (function) transformers. We prove soundness of forward/backward simulations in this richer setting, modulo healthiness conditions with a remarkable duality: forward simulations cannot leak information, and backward simulations cannot exploit leaked information.