Verification of indefinite-horizon POMDPs
This work addresses verification challenges for POMDPs, which are crucial for safety-critical systems but often suffer from scalability issues, representing an incremental advancement over existing approaches.
The paper tackles the verification problem for partially observable MDPs (POMDPs) by developing an abstraction-refinement framework that extends prior methods, resulting in significantly improved scalability as demonstrated in experiments.
The verification problem in MDPs asks whether, for any policy resolving the nondeterminism, the probability that something bad happens is bounded by some given threshold. This verification problem is often overly pessimistic, as the policies it considers may depend on the complete system state. This paper considers the verification problem for partially observable MDPs, in which the policies make their decisions based on (the history of) the observations emitted by the system. We present an abstraction-refinement framework extending previous instantiations of the Lovejoy-approach. Our experiments show that this framework significantly improves the scalability of the approach.