Enforcing Almost-Sure Reachability in POMDPs
This work addresses the problem of safe exploration in POMDPs for applications like reinforcement learning agents, though it appears incremental as it builds on existing methods for reachability.
The paper tackles the EXPTIME-hard problem of synthesizing policies in POMDPs that almost-surely reach a goal state while avoiding bad states, presenting two algorithms (SAT-based iterative and decision-diagram based) that are shown to be feasible and effective in empirical evaluation.
Partially-Observable Markov Decision Processes (POMDPs) are a well-known stochastic model for sequential decision making under limited information. We consider the EXPTIME-hard problem of synthesising policies that almost-surely reach some goal state without ever visiting a bad state. In particular, we are interested in computing the winning region, that is, the set of system configurations from which a policy exists that satisfies the reachability specification. A direct application of such a winning region is the safe exploration of POMDPs by, for instance, restricting the behavior of a reinforcement learning agent to the region. We present two algorithms: A novel SAT-based iterative approach and a decision-diagram based alternative. The empirical evaluation demonstrates the feasibility and efficacy of the approaches.