Forward and Backward Simulations for Partially Observable Probability
Chris Chen, Annabelle McIver, Carroll Morgan
TL;DR
This work tackles datatype refinement in settings where probability and nondeterminism interact, which invalidates traditional simulation-based proofs. It introduces Kuifje$_{\sqcap}$, a POMDP-based language, together with a weakest pre-loss semantics $\mathsf{wpl}$ built from loss transformers to reason about data refinement across encapsulated state and program contexts. The authors prove healthiness properties (superlinearity, partiality, Scott-continuity) for these loss transformers and establish context-extended commutation with hidden assignments, enabling sound forward and backward simulation rules with a duality: forward simulations must not leak information, while backward simulations must not exploit leaks. The framework provides a rigorous theoretical basis for reasoning about datatype encapsulation under mixed probability and nondeterminism, including nontermination and context extension, and demonstrates soundness results that extend beyond traditional pGCL semantics. Overall, the work advances formal refinement theory for partially observable probabilistic systems and offers a robust foundation 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.