Symbolic orthogonal projections : a new polyhedral representation for reachability analysis of hybrid systems

Abstract

This thesis deals with reachability analysis of linear hybrid systems. Special importance is given to the treatment of the necessary geometrical operations. In the first part, we introduce a new representation class for convex polyhedra, the symbolic orthogonal projections (sops). A sop encodes a polyhedron as an orthogonal projection of a higher-dimensional polyhedron. This representation is treated purely symbolically, in the sense that the actual computation of the projection is avoided. We show that fundamental geometrical operations, like affine transformations, intersections, Minkowski sums, and convex hulls, can be performed by block matrix operations on the representation. Compared to traditional representations, like half-space representations, vertex representations, or representations by support functions, this is a unique feature of sops. Linear programming helps us to evaluate sops. In the second part, we investigate the application of sops in reachability analysis of hybrid systems. It turns out that sops are well-suited for the discrete computations. Thereupon, we demonstrate also the applicability of sops for the continuous computation of reachability analysis. By a subtle parallel computation of a precise sop-based representation and a simplified representation, we tackle the problem of monotonic growing sizes of the sops. Additionally, we present experimental results which also show that sops allow an efficient and accurate computation of the reachable states.

Die vorliegende Arbeit beschäftigt sich mit der Erreichbarkeitsanalyse linearer hybrider Systeme, wobei wir besonderen Wert auf die Betrachtung der notwendigen geometrischen Operationen legen. Im ersten Teil führen wir eine neue Darstellungsklasse für konvexe Polyeder ein: die symbolischen Orthogonalprojektionen (Sops). Basierend auf der Idee, einen Polyeder rein symbolisch als Orthogonalprojektion eines höherdimensionalen Polyeders zu beschreiben, zeigen wir, wie sich viele geometrische Operationen – u.a. affine Abbildungen, Schnitte, Minkowski-Summen und konvexe Hüllen – als einfache Blockmatrix-Operationen darstellen lassen. Diese Eigenschaft ist ein Alleinstellungsmerkmal der Sops gegenüber herkömmlichen Darstellungen wie der Halbraum-, der Vertexdarstellung oder der Repräsentation durch Supportfunktionen. Zudem lassen sich Sops durch lineare Optimierungen auswerten. Im zweiten Teil setzen wir Sops zur Berechnung der erreichbaren Zustände hybrider Systeme ein. Die diskreten Zustandsübergänge lassen sich exakt durch Sops darstellen. Danach zeigen wir, dass sich Sops auch zur Berechnung der kontinuierlichen Entwicklung des hybriden Systems eignen. Durch paralleles Berechnen einer präzisen, sop-basierten Darstellung sowie einer vereinfachten Darstellung lösen wir das Problem der stetigen Zunahme der Darstellungsgröße der Sops. Zudem zeigen wir auch anhand von experimentellen Ergebnissen, dass sich Sops zur effizienten und präzisen Berechnung der erreichbaren Zustäande eignen.