Verification of indefinite-horizon POMDPs

针对具有可达性目标的无折扣 POMDP 的可靠启发式搜索值迭代

Sound Heuristic Search Value Iteration for Undiscounted POMDPs with Reachability Objectives

本文研究无折扣 POMDP 的最大可达性概率问题，提出一种基于试验的启发式搜索值迭代新算法，通过值边界引导信念空间探索并解决循环处理缺陷，提供双侧概率界限，实验证明其在概率保证和计算时间上优于现有方法。

Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks

We study strategy synthesis for partially observable Markov decision processes (POMDPs). The particular problem is to determine strategies that provably adhere to (probabilistic) temporal logic constraints. This problem is computationally intractable and theoretically hard. We propose a novel method that combines techniques from machine learning and formal verification. First, we train a recurrent neural network (RNN) to encode POMDP strategies. The RNN accounts for memory-based decisions without the need to expand the full belief space of a POMDP. Secondly, we restrict the RNN-based strategy …

Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints

Recurrent neural networks (RNNs) have emerged as an effective representation of control policies in sequential decision-making problems. However, a major drawback in the application of RNN-based policies is the difficulty in providing formal guarantees on the satisfaction of behavioral specifications, e.g. safety and/or reachability. By integrating techniques from formal methods and machine learning, we propose an approach to automatically extract a finite-state controller (FSC) from an RNN, which, when composed with a finite-state system model, is amenable to existing formal verification tool…

Strategy Synthesis in POMDPs via Game-Based Abstractions

We study synthesis problems with constraints in partially observable Markov decision processes (POMDPs), where the objective is to compute a strategy for an agent that is guaranteed to satisfy certain safety and performance specifications. Verification and strategy synthesis for POMDPs are, however, computationally intractable in general. We alleviate this difficulty by focusing on planning applications and exploiting typical structural properties of such scenarios; for instance, we assume that the agent has the ability to observe its own position inside an environment. We propose an abstracti…

Human-in-the-Loop Synthesis for Partially Observable Markov Decision Processes

We study planning problems where autonomous agents operate inside environments that are subject to uncertainties and not fully observable. Partially observable Markov decision processes (POMDPs) are a natural formal model to capture such problems. Because of the potentially huge or even infinite belief space in POMDPs, synthesis with safety guarantees is, in general, computationally intractable. We propose an approach that aims to circumvent this difficulty: in scenarios that can be partially or fully simulated in a virtual environment, we actively integrate a human user to control an agent. W…

用于隐模型部分可观测马尔可夫决策过程（HM-POMDPs）的鲁棒有限记忆策略梯度

Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs

针对隐模型POMDPs（HM-POMDPs）中策略对环境扰动鲁棒性不足的问题，结合演绎形式验证技术与子梯度上升优化，提出鲁棒有限记忆策略梯度方法，提升策略鲁棒性与泛化性并实现大规模扩展。