Title: Counterexample-guided Abstraction Refinement for POMDPs,
Abstract: Partially Observable Markov Decision Process (POMDP) is widely used to model
probabilistic behavior for complex systems. Compared with MDPs, POMDP models a
system more accurate but solving a POMDP generally takes exponential time in
the size of its state space. This makes the formal verification and synthesis
problems much more challenging for POMDPs, especially when multiple system
components are involved. As a promising technique to reduce the verification
complexity, the abstraction method tries to find an abstract system with a
smaller state space but preserves enough properties for the verification
purpose. While abstraction based verification has been explored extensively for
MDPs, in this paper, we present the first result of POMDP abstraction and its
refinement techniques. The main idea follows the counterexample-guided
abstraction refinement (CEGAR) framework. Starting with a coarse guess for the
POMDP abstraction, we iteratively use counterexamples from formal verification
to refine the abstraction until the abstract system can be used to infer the
verification result for the original POMDP. Our main contributions have two
folds: 1) we propose a novel abstract system model for POMDP and a new
simulation relation to capture the partial observability then prove the
preservation on a fragment of Probabilistic Computation Tree Logic (PCTL); 2)
to find a proper abstract system that can prove or disprove the satisfaction
relation on the concrete POMDP, we develop a novel refinement algorithm. Our
work leads to a sound and complete CEGAR framework for POMDP.