Comparative evaluation and improvement of computational approaches to reachability analysis of linear hybrid systems

Ben Makhlouf, Ibtissem; Frehse, Goran; Kowalewski, Stefan

doi:35479

Comparative evaluation and improvement of computational approaches to reachability analysis of linear hybrid systems = Methoden zur Erreichbarkeitsanalyse hybrider Systeme

Ben Makhlouf, Ibtissem

2016

Verantwortlichkeitsangabevorgelegt von Diplom-Informatikerin Ibtissem Ben Makhlouf aus Djerba/Tunesien

ImpressumAachen : Shaker Verlag 2016

Umfangviii, 221 Seiten : Illustrationen, Diagramme

ISBN978-3-8440-4376-1

ReiheAachener Informatik-Berichte ; 2016-02

Dissertation, RWTH Aachen, 2016

Auch veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Kowalewski, Stefan (Thesis advisor) ; Frehse, Goran (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2016-01-26

Online
URN: urn:nbn:de:hbz:82-rwth-2016-021745
URL: https://publications.rwth-aachen.de/record/571624/files/571624.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; hybrid systems (frei) ; reachability (frei) ; verification (frei) ; zonotope (frei) ; support functions (frei) ; platooning (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Diese Dissertation befasst sich mit dem Problem der Erreichbarkeitsanalyse, fokussiert auf lineare hybride Systeme. Hybride Systeme sind eine Mischung von kontinuierlichen und diskreten Verhalten. Ein hybrider Automat, bestehend aus einem Graph, in dem die Knoten das kontinuierliche und die Kanten das diskrete Verhalten beschreiben, bietet sich als das passende formale Modell für solche Systeme an. Es besteht aus einen Formalismus, das Differentialgleichungen und logische Ausdrücke im gleichen Rahmen umfasst und damit neue Horizonte für die Forschung und Entwicklung, vor allem in Richtung neuer Methoden und neuer Algorithmen, eröffnet. Trotz des Fortschrittes, der in den letzten Jahren zu verzeichnen war, gibt es vor allem in Hinsicht auf die praktische Anwendung noch viele offene Fragen. Begonnen haben wir diese Arbeit mit der Bewertung einiger Verifikationstools. Speziell für diese Aufgabe wurde eine Reihe von Benchmarks erdacht und zusammengefasst. Die Benchmarks besitzen besondere Eigenschaften in Bezug auf die Prüfung der Effizienz, Anwendbarkeit, Skalierbarkeit und Leistungsfähigkeit dieser Tools. Wir geben einen ausführlichen Überblick über bestehende Methoden zum Berechnen einer Überapproximation der erreichbaren Mengen für lineare zeitinvariante hybride Systeme. Dieser erfasst unterschiedliche Ansätze für die Berechnung einer Überapproximation für die kontinuierliche Dynamik mit und ohne Invarianten sowie auch für die Berechnung der Schnittmenge bei Übergängen. Basierend auf diesen Ergebnissen wurden neue Approximationsmethoden zur Berechnung der erreichbaren Mengen für den kontinuierlichen Teil als auch für den diskreten Teil des hybriden Automaten sowie eine modulare skalierbare Implementierung verschiedene Ansätze vorgeschlagen. Für diese Implementierungen werden zuerst Stützfunktionen und danach Zonotopen verwendet. Für die jeweiligen geometrischen Darstellungen wurde eine Reihe von verschiedenen Ansätzen für den Umgang mit Invarianten,Sprungbedingungen und Transitionen vorgestellt. Zwei Tools sind daraus entstanden. Beide Tools integrieren die oben beschriebenen Methoden und erlauben möglicher Kombinationen. Sie verfügen über eine GUI und ermöglichen eine vom Benutzer konfigurierbare Erreichbarkeitsanalyse. Beide Tools wurden zur Durchführung eines Leistungsvergleiches verschiedener Methoden verwendet. Einen Zusammenhang zwischen diesen Leistungen und die Komplexität der Benchmarks wurde dabei festgestellt. Die Studie mit den vorgeschlagenen Benchmarks führte zu dem Ergebnis, dass der Unterschied zwischen Methoden in Bezug auf die Genauigkeit der Überapproximation und die Rechenzeit unbedeutend ist. Um die Vielfältigkeit der Anwendbarkeit der Erreichbarkeitsanalyse zu veranschaulichen, kam es zum Vorschlag einer vernetzten Fahrzeugkolonne. Zuerst wurde die Analyse verwendet, um sichere und kurze Abständen zwischen Fahrzeugen in einer LMI-geregelten Kolonne zu bestimmen. Nachfolgend wurde eine Erreichbarkeitsanalyse durchgeführt um bei der Entscheidung über den leistungsfähigsten H2- or Hinf-Regler der gleiche Kolonne zu unterstützen. Sie wurde außerdem eingesetzt um zeitkritische Bedingungen für eine Kreuzung mit einer annähernden Kolonne zu bestimmen und damit den Verkehr innerhalb der Kreuzung sicher zu verwalten.

This thesis addresses the problem of reachability analysis with the focus on linear hybrid systems. Hybrid systems are a mixture of continuous and discrete behaviors.The Hybrid automaton consisting of a graph, in which the locations describe the continuous and the transitions the discrete behavior, represents the best formal model for such kind of systems. It provides a formalism integrating differential equations and logic expressions in a same framework, thus opening new horizons in research and development of new methods and novel algorithms. Despite recent progress made in this field in the last years, actual verification methods and available tools have exhibited their shortcomings.We started this work with the assessment of some verification tools using a suite of benchmarks conceived specially for this task. The benchmarks possess particular characteristics for testing of efficiency, applicability, scalability, capability and performances of these tools. We offer a theoretical overview of existing methods for computing an overapproximation of reachable sets for linear time invariant hybrid systems. This covers approaches for overapproximating reachable sets of the continuous dynamics with and without invariants as well as methods for solving the problem of guard intersection at transitions. We furthermore propose new overapproximation techniques for treating the continuous part as well as the discrete part of the hybrid automaton.We suggest scalable, modular implementations of these diverse methods allowing thereby possible combinations between them first using support functions and then with zonotopes. The implementations include different approaches for handling invariants, guards and transitions for the above-mentioned set representations. Two toolboxes are the results of this implementation effort. Both tools integrate the methods described above. They offer a GUI and allow for a user-configurable reachability analysis. We use both tools to carry out a performance comparison of different methods. We note thereby that there is a correlation between these performances and the complexity of the tested example. However, we note during this survey using the proposed benchmark suite that the difference in the performance with regards to the tightness of the overapproximation and the computation time is not so crucial for low dimensional systems. We propose a networked platoon of vehicles to demonstrate different context where reachability analysis can be useful. We first perform a reachability analysis to determine unsafe gaps between the vehicles which are controlled using LMI formalism. Reachability analysis can be helpful for control design. The choice between controllers on the basis of reachability results has led to controller ensuring the best compromise between safe and small gaps when applying H2 or Hinf control design techniques. Reachability can also be used to determine time-critical conditions. As demonstration, we opt for a platoon approaching an intersection.

OpenAccess:
PDF
(additional files)