State set representations and their usage in the reachability analysis of hybrid systems

• Zustandsmengenrepräsentierungen und ihre Verwendung in der Erreichbarkeitsanalyse Hybrider Systeme

Schupp, Stefan; Ábrahám, Erika (Thesis advisor); Frehse, Goran (Thesis advisor)

Aachen (2019)
Doktorarbeit

Dissertation, RWTH Aachen University, 2019

Kurzfassung

Unter hybriden Systemen in der Informatik versteht man Systeme, welche diskretes als auch kontinuierliches Verhalten vereinen. In dieser Arbeit werden Ergebnisse aus dem Bereich der Verifikation linearer hybrider Systeme vorgestellt. Das kontinuierliche Verhalten der betrachteten Systeme kann dabei durch lineare Differentialgleichungen beschrieben werden. Diese Arbeit beschäftigt sich im Besonderen mit der über-approximierenden Erreichbarkeitsanalyse, in der die Menge der erreichbaren Zustände durch eine endliche Vereinigung von Zustandsmengen approximiert wird. Zustandsmengen während der Berechnung werden dabei durch verschiedene geometrische als auch symbolische Repräsentierungen dargestellt. Die Wahl der Zustandsmengenrepräsentierung hat einen starken Einfluss auf die Präzision der Approximation als auch auf die Laufzeit der Analyse. Zusätzlich wird das Ergebnis der Analyse durch weitere Parameter und Heuristiken beeinflusst. In dieser Arbeit erforschen wir den Einfluss und die optimale Einstellung dieser Parameter. Unsere Ergebnisse sind in der öffentlichen C++ Bibliothek HyPro zur Verfügung gestellt. Die Beiträge dieser Arbeit lassen sich in drei Teile gliedern: 1) Wir präsentieren unsere HyPro Programmierbibliothek. Diese beinhaltet Implementierungen verschiedener Datentypen, die in Algorithmen für die Erreichbarkeitsanalyse hybrider Systeme verwendet werden können um Zustandsmengen hybrider Systeme zu repräsentieren. Eine vereinheitlichte Schnittstelle zusammen mit Reduktions- und Konvertierungsmethoden erlauben die schnelle Implementierung von flexiblen Analysemethoden für lineare hybride Systeme. 2) Wir zeigen die Anwendbarkeit der Methoden und Datenstrukturen in HyPro anhand der Einbettung eines üblichen Erreichbarkeitsanalyseansatzes in ein Framework, in welchem eine schnelle aber grobe Analyse iterativ durch die Verwendung von Gegenbeispielen verfeinert wird. Eine Parallelisierung des Ansatzes ist ebenfalls gegeben, welche die Laufzeiten weiter verbessert. 3) Die Einführung von Methoden, um teure Berechnungen in hoch-dimensionalen Zustandsräumen durch weniger aufwendigen Berechnungen in niedrig-dimensionalen Zustandsräumen zu ersetzen. Die vorgestellte Methode ist nur unter bestimmten Bedingungen verwendbar. Wir präsentieren ein automatisiertes Verfahren, um diese Bedingungen zu überprüfen und wenn möglich solche niedrig-dimensionale Räume zu identifizieren. Die Verwendung dedizierter Verfahren für die Analyse bestimmter Unterklassen von hybriden Systemen in Kombination mit der Entkopplung des Zustandsraumes vervollständigen unseren Ansatz.