Enforcing almost-sure reachability in POMDPs

DOI10.1007/978-3-030-81688-9_28zbMATH Open1493.68213arXiv2007.00085OpenAlexW3185890095MaRDI QIDQ832296FDOQ832296

Authors: Sebastian Junges, Nils Jansen, Sanjit A. Seshia 

Publication date: 25 March 2022

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/2007.00085

Recommendations

• Optimal cost almost-sure reachability in POMDPs
• Robust almost-sure reachability in multi-environment MDPs
• Verification of Indefinite-Horizon POMDPs
• POMDPs under probabilistic semantics
• Reachability in MDPs: refining convergence of value iteration
• Reachability in Recursive Markov Decision Processes
• Reachability in recursive Markov decision processes
• Reachability in continuous-time Markov reward decision processes
• Approximability and efficient algorithms for constrained fixed-horizon POMDPs with durative actions

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40)

Cites Work

• Planning and acting in partially observable stochastic domains
• Optimal cost almost-sure reachability in POMDPs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Qualitative analysis of partially-observable Markov decision processes
• Probabilistic ω-automata
• Title not available (Why is that?)
• Minimal counterexamples for linear-time probabilistic verification
• Algorithms for Omega-Regular Games with Imperfect Information
• Temporal logic motion planning using POMDPs with parity objectives
• A General Safety Framework for Learning-Based Control in Uncertain Robotic Systems
• Verification and control of partially observable probabilistic systems
• Deep reinforcement learning with temporal logics
• Permissive Controller Synthesis for Probabilistic Systems
• Title not available (Why is that?)
• Shield Synthesis:
• Title not available (Why is that?)
• Omega-Regular Objectives in Model-Free Reinforcement Learning

Cited In (6)

• Verification of Indefinite-Horizon POMDPs
• Robust almost-sure reachability in multi-environment MDPs
• Task-guided IRL in POMDPs that scales
• Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes
• Risk-aware shielding of partially observable Monte Carlo planning policies
• Under-approximating expected total rewards in POMDPs

Uses Software

• POMDP
• z3
• Storm
• Jani

This page was built for publication: Enforcing almost-sure reachability in POMDPs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832296)