Programming and Reasoning in Partially Observable Probabilistic Environments

TL;DR

This paper introduces pBLIMP, a probabilistic belief programming language designed for environments with partial observability, featuring symbolic modeling, belief updates, and a weakest-precondition calculus for reasoning about programs with unbounded loops.

Contribution

It develops the first theoretical framework for pBLIMP, enabling symbolic modeling, belief updates, and formal reasoning about probabilistic, partially observable environments with unbounded loops.

Findings

pBLIMP can model and reason about complex probabilistic environments.

The wp calculus is sound and handles unbounded loops with invariants.

The language supports explicit observations and belief state conditioning.

Abstract

Probabilistic partial observability is a phenomenon occuring when computer systems are deployed in environments that behave probabilistically and whose exact state cannot be fully observed. In this work, we lay the theoretical groundwork for a probabilistic belief programming language pBLIMP, which maintains a probability distribution over the possible environment states, called a belief state. pBLIMP has language features to symbolically model the behavior of and interaction with the partially observable environment and to condition the belief state based on explicit observations. In particular, pBLIMP programs can perform state estimation and base their decisions (i.e. the control flow) on the likelihood that certain conditions hold in the current state. Furthermore, pBLIMP features unbounded loops, which sets it apart from many other probabilistic programming languages. For reasoning about pBLIMP programs and the situations they model, we present a weakest-precondition-style calculus (wp) that is capable of reasoning about unbounded loops. Soundness of our wp calculus is proven with respect to an operational semantics. We further demonstrate how our wp calculus reasons about (unbounded) loops with loop invariants.