Under-Approximating Expected Total Rewards in POMDPs
This provides a scalable method for verifying safety or performance bounds in POMDPs, which is incremental as it builds on existing abstraction techniques.
The paper addresses the undecidable problem of determining if the optimal expected total reward in a POMDP is below a threshold by computing under-approximations using finite unfoldings of the belief MDP, with experimental results showing scalability and tight lower bounds.
We consider the problem: is the optimal expected total reward to reach a goal state in a partially observable Markov decision process (POMDP) below a given threshold? We tackle this -- generally undecidable -- problem by computing under-approximations on these total expected rewards. This is done by abstracting finite unfoldings of the infinite belief MDP of the POMDP. The key issue is to find a suitable under-approximation of the value function. We provide two techniques: a simple (cut-off) technique that uses a good policy on the POMDP, and a more advanced technique (belief clipping) that uses minimal shifts of probabilities between beliefs. We use mixed-integer linear programming (MILP) to find such minimal probability shifts and experimentally show that our techniques scale quite well while providing tight lower bounds on the expected total reward.