# On the Verification of Belief Programs

arXiv: https://arxiv.org/abs/2204.12562 · HTML: https://mlsanity.com/paper/2204.12562/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 34 references that are in the map.
- First posted on arXiv 26 Apr 2022.

## Builds on (most cited first, 6 of 6)

- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [What is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives](https://mlsanity.com/paper/1309.2802/) (2013)
- [Optimal Cost Almost-sure Reachability in POMDPs](https://mlsanity.com/paper/1411.3880/) (2014)
- [Verification of indefinite-horizon POMDPs](https://mlsanity.com/paper/2007.00102/) (2020)
- [Under-Approximating Expected Total Rewards in POMDPs](https://mlsanity.com/paper/2201.08772/) (2022)
- [Reasoning about Discrete and Continuous Noisy Sensors and Effectors in Dynamical Systems](https://mlsanity.com/paper/1809.05314/) (2018)

## Abstract (arXiv)

In a recent paper, Belle and Levesque proposed a framework for a type of program called belief programs, a probabilistic extension of GOLOG programs where every action and sensing result could be noisy and every test condition refers to the agent's subjective beliefs. Inherited from GOLOG programs, the action-centered feature makes belief programs fairly suitable for high-level robot control under uncertainty. An important step before deploying such a program is to verify whether it satisfies properties as desired. At least two problems exist in doing verification: how to formally specify properties of a program and what is the complexity of verification. In this paper, we propose a formalism for belief programs based on a modal logic of actions and beliefs. Among other things, this allows us to express PCTL-like temporal properties smoothly. Besides, we investigate the decidability and undecidability for the verification problem of belief programs.