von Matthias Lange ; Christine Happle ; Juliane Hamel ; Michael Dördelmann ; Mathieu Bangert ; Rolf Kramer ; Frank Eberhardt ; Marcus Panning ; Axel Heep ; Gesine Hansen ; Martin Wetzke
Fahrerassistenzsysteme werden immer autonomer und damit auch immer komplexer. Hier kann automatisiertes logisches Schließen für Verkehrsmanöver helfen, um solche Systeme zu analysieren. Multi-Lane Spatial Logic ist eine räumliche Logik, welche auf die Analyse von Verkehrsmanövern spezialisiert ist. Für diese Logik untersuchen wir Möglichkeiten der Automatisierung unter Berücksichtigung von ungenauen Sensordaten. Zusätzlich erweitern wir die Logik Duration Calculus mit der Möglichkeit temporale Präferenzen auszudrücken. Wir zeigen, dass Model Checking für ein relevantes Fragment der resultierenden Logik entscheidbar ist. Wir verbinden dies mit unserer Arbeit an Verkehrsmanövern, indem wir unsere Erweiterung verwenden, um ein Gefahrenwarnprotokoll für Autobahnen zu analysieren.
There is a trend in developing more and more autonomous driver assistance systems. Here, automation of formal spatio-temporal reasoning about traffic manoeuvres can help to analyse such systems. Multi-Lane Spatial Logic is a logic tailored towards formal reasoning about spatial aspects of motorways. For this logic we investigate means of automation, while paying special attention to imprecise information resulting from sensor readings. Additionally, we extend the logic Duration Calculus by introducing temporal discounting. We show that for a relevant fragment of our extension, model checking is decidable. We connect this to our work on traffic manoeuvres by using our extension to analyse the temporal quality of a hazard warning protocol for motorways.
Durch das steigende Interesse an autonomen Fahrzeugen gewinnt deren Sicherheit immer stärker an Bedeutung. Hierbei ist Sicherheit gleichbedeutend mit Kollisionsfreiheit, eine grundsätzlich räumliche Eigenschaft. Fahrzeugmodelle in der Informatik beinhalten Spezifikationen des dynamischen Verhaltens, so dass der zum sicheren Betrieb nötige Raum abhängig von der Zeit ist. Dies erschwert Sicherheitsbeweise enorm. In dieser Arbeit stellen wir Methoden vor, um Schlussfolgerungen über den Raum vom Fahrzeugverhalten abzutrennen. Hierzu definieren wir ein abstraktes Modell mit dem Schwerpunkt auf den räumlichen Veränderungen der Straßensituation. Darauf aufbauend entwickeln wir zwei Formalismen: Wir definieren eine Modallogik, mit der Aussagen über die Sicherheit von beliebig vielen Fahrzeugen bewiesen werden können. Weiterhin stellen wir Diagramme zur einfacheren Spezifikation solcher Eigenschaften vor. Wir beweisen die Kollisionsfreiheit zwischen Fahrzeugen, die wenige Anforderungen erfüllen. <dt.>
Due to the increasing interest in autonomously driving cars, safety issues of such systems are of utmost importance. Safety in this sense is primarily the absence of collisions, which is inherently a spatial property. Within computer science, typical models of cars include specifications of their behaviour, where the space a car needs for operating safely is a function of time. This complicates proofs of safety properties tremendously. In this thesis, we present methods to separate reasoning on space from the dynamical behaviour of cars. To that end, we define an abstract model with an emphasis on spatial transformations of the situation on the road. Based on this model, we develop two formalisms: We give the definitions of a modal logic suited to reason about safety properties of arbitrarily many cars. Furthermore, we present a diagrammatic language to ease the specification of such properties. We formally prove that no collisions arise between cars obeying a small set of requirements. <engl.>
