Leonore Winterer, M.Sc.
Technische Fakultät Georges Köhler Allee 51 79110 Freiburg Deutschland
Gebäude 051, Raum 01-030
+49 (0)761 203-8148
+49 (0)761 203-8142
winterel@informatik.uni-freiburg.de

Leonore Winterer

Liste filtern : Jahre: 2017 |

2015 | alle anzeigen nach oben zur Jahresübersicht Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Kaoten, Becker BMotion Planning under Partial Observability using Game-Based Abstraction 2017 Melbourne, VIC, Australia 56th IEEE Conf. on Decision and Control (CDC) , Seiten : 2201 - 2208» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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. nach oben zur Jahresübersicht Karsten Scheibler, Leonore Winterer, Ralf Wimmer, Bernd BeckerTowards Verification of Artificial Neural Networks 2015 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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.