A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs

The qualitative problem is of great importance as in several applications it is The de facto model for dynamic systems with probabilistic required that the correct behavior happens with probability 1, and nondeterministic behavior are Markov decision processes e.g., in the analysis of randomized embedded schedulers, (MDPs) (Howard 1960). MDPs provide the appropriate the important question is whether every thread progresses model to solve control and probabilistic planning problems with probability 1. Also in applications where it might be (Filar and Vrieze 1997; Puterman 1994), where the nondeterminism sufficient that the correct behavior happens with probability represents the choice of the control actions for at least λ 1,the correct choice of the threshold λ can the controller (or planner), while the stochastic response of be still challenging, due to simplifications and imprecisions the system to control actions is represented by the probabilistic introduced during modeling.