Partial observability is an increasingly important issue for computer systems, as they are frequently deployed to environments where the exact state of the environment cannot be fully observed. One way to address partial observability is belief programming: A programming methodology where the program automatically performs state estimation in non-deterministic environments.

Our work lifts belief programming to a quantitative realm, which enables us to write and verify programs for probabilistic partially observable environments. A probabilistic belief program dynamically updates a probability distribution over all possible states of the environment in the form of a belief state, and enables sound inferences based on that distribution. Furthermore we introduce P-BLIMP, a model probabilistic programming language specialized for partial observability. P-BLIMP offers language features to symbolically model the behavior of the partially observable environment, to condition the belief state based on observations and to make inferences about the state of the environment. We also introduce a weakest pre-expectation calculus for probabilistic belief programs and present a case study on how predicates can be manipulated efficiently.