Hybride Systeme dienen der Beschreibung der Interaktion von zeitkontinuierlichem und zeitdiskretem Verhalten, wie sie beispielsweise in eingebetteten Systemen stattfindet. Ein Beschreibungsmittel für solche Systeme sind hybride Automatenmodelle, endliche Automaten angereichert mit Differentialgleichungen. Im Rahmen dieser Arbeit wird eine wichtige Eigenschaft solcher Systeme untersucht: Stabilität. Stabile Systeme sind in der Lage, temporäre Störungen auszuregeln, indem sie wieder zu einem Arbeitspunkt zurückkehren. Der Hauptbeitrag der Arbeit ist eine Methodik zum automatischen, dekompositionellen Nachweise dieser Eigenschaft. Den Kern bildet hier die graphentheoretische Zerlegung des Automaten mit Hilfe von Ljapunow-Funktionen, welche die Komponierbarkeit sicherstellen. Hiermit ist es möglich, die Komplexität der zu lösenden Stabilitätsbeweise signifikant zu reduzieren, sowie Aussagen über das Ergebnis einer Komposition zweier Automaten zu treffen. <dt.>
Hybrid systems describe the interaction between discrete time and continuous time behavior. For instance, they can be used to model the interactions between physics and digital controllers as they arise in embedded systems. One means for modeling such systems are so-called hybrid automata, consisting of finite automata enriched with differential equations. In the scope of this thesis, one important property of such systems is examined: stability. Stable systems compensate for temporary disturbances by returning to a pre-defined system state as soon as the disturbances cease. The main contribution of the thesis is a method for automated, decompositional stability verification, using graph theoretical methods and Lyapunov functions. The result is a divide-and-conquer approach that significantly reduces the complexity of the individual verification problems, and also can be used to predict the effects of a composition of two stable systems. <engl.>
