2020

 back to the year overview

• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker
  Strategy Synthesis for POMDPs in Robot Planning using Game-Based Abstractions
  2020 IEEE T Automat Contr
  » show abstract« hide abstract
  Abstract

  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.
• Leonore Winterer, Ralf Wimmer, Nils Jansen, Bernd Becker
  Strengthening Determinstic Policies for POMPDs
  2020 Proceedings of the 12th NASA Formal Methods Symposium (NFM)
  » show abstract« hide abstract
  Abstract

  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.

2018

 back to the year overview

• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Kaoten, Becker B
  Abstraktions-basierte Verifikation von POMDPs im Motion-Planning-Kontext
  2018 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » show abstract« hide abstract
  Abstract

  Wir untersuchen Pfadplanungsprobleme aus der Robotik und die Berechnung von Stra- tegien, die beweisbare Garantien für Sicherheitseigenschaften liefern. Dabei soll ein Agent mit hoher Wahrscheinlichkeit einen Zielort erreichen, ohne mit einem Hindernis zusammenzustoßen, das sich probabilistisch durch den Raum bewegt. Schwierig wird dieses Problem dadurch, dass der Agent seine Umgebung nur eingeschränkt beobachten kann. Dieses Szenario lässt sich auf na- türliche Art und Weise als ein sogenannter partiell beobachtbarer Markow-Entscheidungsprozess (POMDP) modellieren. Da viele interessante Eigenschaften auf POMDPs unentscheidbar sind, beschäftigt sich die hier vorgestellte Arbeit mit der Entwicklung einer spielbasierten Abstraktionsmethode, um für solche Pfadplanungsprobleme und Sicherheitseigenschaften gute Approximationen zu berechnen.
• Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker
  Finite-State Controllers of POMDPs via Parameter Synthesis
  2018 Proceedings of the 34th Conference on Uncertainty in Artificial Intelligence (UAI), AUAI Press, pages: 519 - 529
  » show abstract« hide abstract
  Abstract

  e 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 enables using black-box techniques to compute correct-by-construction FSCs for POMDPs for a wide range of properties. Our experimental evaluation on typical POMDP problems shows that we are competitive to state-of-the-art POMDP solvers.

2017

 back to the year overview

• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Kaoten, Becker B
  Motion Planning under Partial Observability using Game-Based Abstraction
  2017 Melbourne, VIC, Australia 56th IEEE Conf. on Decision and Control (CDC), pages: 2201 - 2208
  » show abstract« hide abstract
  Abstract

  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 evironment. 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.
• Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker
  Permissive Finite-State Controllers of POMDPs using Parameter Synthesis
  2017
  » show abstract« hide abstract
  Abstract

  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.

2015

 back to the year overview

• Karsten Scheibler, Leonore Winterer, Ralf Wimmer, Bernd Becker
  Towards Verification of Artificial Neural Networks
  2015 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » show abstract« hide abstract
  Abstract

  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.