Programming and Reasoning in Partially Observable Probabilistic Environments

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.