AbstractsBiology & Animal Science

Hybrid automata are used to model systems with both discrete and continuous dynamics. A prototypical example is a thermostat which switches between the modes “heating” and “cooling”. We present new methods to construct and utilize abstractions for the analysis of hybrid automata. For guiding the exploration of the region space of a hybrid automaton, we propose distance functions which are based on abstractions of the original hybrid automaton and can be computed automatically. To analyze networks of hybrid automata, we lift the notion of assume-guarantee abstraction refinement to the class of hybrid automata. For this purpose, we introduce an abstraction of a hybrid automaton which can efficiently shrink the discrete structure. In order to apply symbolic reachability analysis to hybrid planning based on the planning language PDDL+ as studied in Artificial Intelligence, we present a semantics preserving translation of PDDL+ into a hybrid automaton. We have implemented our methods as extensions to the symbolic hybrid model checker SpaceEx. As the experiments show, our methods make it possible to analyze hybrid automata which were out of scope of existing methods. Hybrid-Automaten werden dazu verwendet, Systeme zu modellieren, die sowohl diskretes als auch kontinuierliches Verhalten aufweisen. Ein typisches Beispiel für ein solches System ist ein Thermostat, der zwischen den Modi “Heizen” and “Kühlen” wechselt. In dieser Arbeit stellen wir abstraktions-basierte Verfahren zur symbolischen Analyse von Hybrid-Automaten vor. Um das Explorieren des Zustandsraumes eines Hybrid-Automaten zu steuern, schlagen wir Abstandsfunktionen vor, die auf Abstraktionen des ursprünglichen Hybrid-Automaten beruhen und automatisch berechnet werden können. Um Netzwerke von Hybrid-Automaten zu analysieren, erweitern wir das Konzept von “Assume-Guarantee Abstraction Refinement” auf die Klasse der Hybrid-Automaten. Zu diesem Zweck führen wir eine Abstraktion ein, die die diskrete Struktur des Automaten effizient verkleinern kann. Weiterhin präsentieren wir eine semantik-erhaltende Übersetzung der Planungsspache PDDL+, die im Bereich der künstlichen Intelligenz untersucht wird, in einen Hybrid-Automaten, um symbolische Erreichbarkeitsanalyse für Handlungsplanung in hybriden Domänen anwenden zu können. Wir haben unsere Verfahren als Erweiterungen des symbolischen hybriden Modellprüfers SpaceEx implementiert. Unsere Experimente zeigen, dass unsere Verfahren es ermöglichen, Hybrid-Automaten zu analysieren, die mit existierenden Verfahren bisher nicht analysiert werden konnten.