The synthesis problem for partially observable Markov decision processes (POMDPs) is to compute a policy that provably adheres to one or more specifications. Yet, the general problem is undecidable, and policies require full (and thus potentially unbounded) traces of execution history. To provide good approximations of such policies, POMDP agents often employ randomization over action choices. We consider the problem of computing simpler policies for POMDPs, and provide several approaches to still ensure their expressiveness. Key aspects are (1) the combination of an arbitrary number of specifications the policies need to adhere to, (2) a restricted form of randomization, and (3) a light-weight preprocessing of the POMDP model to encode memory. We provide a novel encoding as a mixed-integer linear program as baseline to solve the underlying problems. Our experiments demonstrate that the policies we obtain are more robust, smaller, and easier to implement for an engineer than those obtained from state-of-the-art POMDP solvers.

Albeit an important and versatile model for many practical applications, partially observable Markov Decision Processes (POMDPs) are notoriously hard to analyze. Many interesting properties are either of high complexity or even theoretically undecidable, and while approximative methods often provide good results for, e. g., policy synthesis and the computation of probabilities, other problems remain still unsolved. One such issue is diagnosis – figuring out why a certain specification cannot be met, and what can be done to repair the system. While in deterministic systems like digital circuits, a single execution trace is a sufficient proof of an unsafe system, the situation is less easy in probabilistic systems – typically large sets of traces are required whose joint probability exceeds a maximally tolerable probability. For POMDPs, the restricted observability adds another layer of uncertainty. In this paper we focus on analyzing where the restricted observability needs to be refined in order to satisfy a required safety or performance property. We propose and evaluate different approaches for obtaining such diagnostic information.

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 abstraction refinement framework which turns such a POMDP model into a (fully observable) probabilistic two-player game (PG). For the obtained PGs, efficient verification and synthesis tools allow to determine strategies with optimal safety and performance measures, which approximate optimal schedulers on the POMDP. If the approximation is too coarse to satisfy the given specifications, an refinement scheme improves the computed strategies. As a running example, we use planning problems where an agent moves inside an environment with randomly moving obstacles and restricted observability. We demonstrate that the proposed method advances the state of the art by solving problems several orders-of-magnitude larger than those that can be handled by existing POMDP solvers. Furthermore, this method gives guarantees on safety constraints, which is not supported by the majority of the existing solvers.

The synthesis problem for partially observable Markov decision processes (POMDPs) is to compute a policy that satisfies a given specification. Such policies have to take the full execution history of a POMDP into account, rendering the problem undecidable in general. A common approach is to use a limited amount of memory and randomize over potential choices. Yet, this problem is still NP-hard and often computationally intractable in practice. A restricted problem is to use neither history nor randomization, yielding policies that are called stationary and deterministic. Previous approaches to compute such policies employ mixed-integer linear programming (MILP). We provide a novel MILP encoding that supports sophisticated specifications in the form of temporal logic constraints. It is able to handle an arbitrary number of such specifications. Yet, randomization and memory are often mandatory to achieve satisfactory policies. First, we extend our encoding to deliver a restricted class of randomized policies. Second, based on the results of the original MILP, we employ a preprocessing of the POMDP to encompass memory-based decisions. The advantages of our approach over state-of-the-art POMDP solvers lie (1) in the flexibility to strengthen simple deterministic policies without losing computational tractability and (2) in the ability to enforce the provable satisfaction of arbitrarily many specifications. The latter point allows to take trade-offs between performance and safety aspects of typical POMDP examples into account. We show the effectiveness of our method on a broad range of benchmarks.

RSS 2019: Robust autonomy: tools for safety in real-world uncertain environments, Freiburg, Germany, Jan 23rd 2019. Workshop on Safe Autonomy

Summary. In this extended abstract, we discuss how to compute policies with finite memory---so-called finite-state controllers (FSCs)---for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. In particular, for a POMDP M and a specification ϕ, we want to solve the decision problem whether there is a policy σ for M with k memory states, such that ϕ is satisfied by M and σ (Mσ |= ϕ). The underlying method is achieved via a marriage of formal verification and artificial intelligence. The key insight is that computing (randomized) FSCs on POMDPs is equivalent to---and computationally as hard as---synthesis for parametric Markov chains (pMCs). The parameter synthesis problem is to decide whether for a parametric Markov chain (pMC) M and a specification ϕ there is a parameter instantiation u such that in the Markov chain (MC) induced by u the specification is satisfied (M[u] |= ϕ) . The correspondence---depicted in Figure 1---allows to utilize efficient tools for synthesis in pMCs to compute correct-by-construction FSCs on POMDPs.

We study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. The key insight is that computing (randomised) FSCs on POMDPs is equivalent to - and computationally as hard as - synthesis for parametric Markov chains (pMCs). This correspondence allows to use tools for parameter synthesis in pMCs to compute correct-by-construction FSCs on POMDPs for a variety of specifications. Our experimental evaluation shows comparable performance to well-known POMDP solvers.

Uncertainty in Artificial Intelligence: Thirty-Fourth Conference (2018) August 6-10, 2018, Monterey, California, USA

We study motion planning problems where agents move inside environments that are not fully observable and subject to uncertainties. The goal is to compute a strategy for an agent that is guaranteed to satisfy certain safety and performance specifications. Such problems are naturally modeled by partially observable Markov decision processes (POMDPs). Because of the potentially huge or even infinite belief space of POMDPs, verification and strategy synthesis is in general computationally intractable. We tackle this difficulty by exploiting typical structural properties of such scenarios; for instance, we assume that agents have the ability to observe their own positions inside an environment. Ambiguity in the state of the environment is abstracted into non-deterministic choices over the possible states of the environment. Technically, this abstraction transforms POMDPs into probabilistic two-player games (PGs). For these PGs, efficient verification tools are able to determine strategies that approximate certain measures on the POMDP. If an approximation is too coarse to provide guarantees, an abstraction refinement scheme further resolves the belief space of the POMDP. We demonstrate that our method improves the state of the art by orders of magnitude compared to a direct solution of the POMDP.

ion-based Model Checking of POMDPs in Motion Planning∗ Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, and Bernd Becker 1 BrainLinks-BrainTools Cluster of Excellence Albert-Ludwigs-Universität Freiburg, Freiburg im Breisgau, Germany {winterel | wimmer | becker}@informatik.uni-freiburg.de 2 RWTH Aachen University, Aachen, Germany {sebastian.junges | katoen}@informatik.rwth-aachen.de 3 The University of Texas at Austin, Austin, Texas, USA utopcu@utexas.edu 4 Radboud University, Nijmegen, The Netherlands n.jansen@science.ru.nl

We consider the safety verification of controllers obtained via machine learning. This is an important problem as the employed machine learning techniques work well in practice, but cannot guarantee safety of the produced controller, which is typically represented as an artificial neural network. Nevertheless, such methods are used in safety-critical environments. In this paper we take a typical control problem, namely the Cart Pole System (a. k. a. inverted pendulum), and a model of its physical environment and study safety verification of this system. To do so, we use bounded model checking (BMC). The created formulas are solved with the SMT-solver iSAT3. We examine the problems that occur during solving these formulas and show that extending the solver by special deduction routines can reduce both memory consumption and computation time on such instances significantly. This constitutes a first step towards verification of machine-learned controllers, but a lot of challenges remain.