Dieses Modul bietet eine prägnante Einführung in normierte Vektorräume und Stabilitätskonzepte in autonomen Systemen, die sowohl asymptotische Stabilität als auch globale asymptotische Stabilität umfassen. Der Schwerpunkt liegt auf der Anwendung des Ljapunowschen Stabilitätstheorems zur formalen Überprüfung dieser Eigenschaften in komplexen Systemen, einschließlich seiner Anwendung auf verschiedene einfache Systeme, wie z. B. lineare Systeme. Anhand anschaulicher Beispiele wird die Bedeutung dieser Konzepte für die Analyse und Gewährleistung der Stabilität von Systemen aufgezeigt.

Vertiefen Sie sich in das Thema der erreichbaren Mengen und entdecken Sie deren entscheidende Rolle bei der Gewährleistung der Systemsicherheit. In diesem Modul werden Rahmenbedingungen für die Erforschung von Berechnungstechniken zur Überapproximation erreichbarer Mengen in verschiedenen Systemklassen vorgestellt. Sie werden die Möglichkeit haben, Ihr Wissen in realen Kontexten anzuwenden, die Verwendung von Zonotopen zu untersuchen und deren vorteilhafte Eigenschaften bei der Berechnung von erreichbaren Mengen zu erkennen. Darüber hinaus befassen wir uns mit grundlegenden Konzepten formaler Sprachen sowie regulärer und omega-regulärer Ausdrücke und bieten prägnante und formale Methoden zum Ausdruck regulärer bzw. omega-regulärer Sprachen.

In diesem Modul lernen Sie die grundlegenden Prinzipien regulärer und ω-regulärer Eigenschaften kennen und wie diese durch nichtdeterministische endliche Automaten (NFA) bzw. Büchi-Automaten (NBA) dargestellt werden. Sie lernen die Notation und Architektur von NFAs und NBAs kennen, beherrschen die Konstruktion von regulären und ω-regulären Ausdrücken und verstehen deren Zusammenhang mit diesen Automaten. Der Kurs führt Sie durch die Umwandlung von NFAs in reguläre Ausdrücke und NBAs in ω-reguläre Ausdrücke und deren Umkehrung und erläutert die Bedeutung dieser Konzepte bei der Verifikation von endlichen und unendlichen Verhaltensweisen von Systemen.

Dieses Modul befasst sich eingehend mit den Formeln der linearen temporalen Logik (LTL), einem mathematischen Formalismus zur Beschreibung von Sprachen mit unendlich vielen Wörtern. Es stellt einen Rahmen für die Artikulation der zeitlichen Dimensionen des Systemverhaltens dar und bietet eine Syntax, die der natürlichen Sprache sehr ähnlich ist. Durch die Verschmelzung von Aussagenlogik mit zeitlichen Operatoren bietet LTL ein leistungsfähiges Instrumentarium zur Spezifizierung der vielfältigen Verhaltensweisen von Systemen