In diesem Modul konzentrieren wir uns auf die Verifikation endlicher Systeme, wobei wir den Schwerpunkt auf reguläre Sicherheitseigenschaften und ω-reguläre Eigenschaften legen (einschließlich solcher, die als lineare temporale Logikformeln ausgedrückt werden). Wir werden eine Vielzahl von Verifikationstechniken untersuchen und uns mit den theoretischen Grundlagen befassen, die für das Verständnis der Verifikation endlicher Systeme wesentlich sind. Anhand detaillierter Beispiele und klarer, umfassender Erklärungen wollen wir ein tiefes Verständnis dafür vermitteln, wie diese Eigenschaften im Zusammenhang mit endlichen Systemen verifiziert werden.

In diesem Modul erforschen wir die Synthese von Reglern für endliche Systeme und konzentrieren uns dabei auf die Durchsetzung bestimmter Formeln der linearen temporalen Logik (LTL), einschließlich Sicherheit, Erreichbarkeit, Persistenz und Rekursion. Wir wollen verstehen, wie Regler entworfen werden können, um bestimmte LTL-Formeln für Systeme mit geschlossener Schleife zu erfüllen. Das Modul vermittelt wesentliche theoretische Rahmenbedingungen und praktische Algorithmen, die für die Synthese solcher Regler erforderlich sind, wobei der Schwerpunkt auf der Rolle von Festkomma-Operatoren und Algorithmen bei den Berechnungsprozessen liegt. Darüber hinaus werden wir verschiedene Synthesetechniken diskutieren, die von den Eigenschaften des Systems und den beteiligten LTL-Formeln abhängen.

In diesem Modul werden wir die Konzepte der Abstraktion und Verfeinerung im Zusammenhang mit Kontrollsystemen untersuchen. Wir werden uns mit den Beziehungen zwischen Feedback und Verfeinerung befassen, um zu verstehen, wie Regler geändert oder ersetzt werden können, um neue Spezifikationen zu erfüllen, ohne das Verhalten des Gesamtsystems zu verändern. Das Modul behandelt auch die Berechnung von Abstraktionen und zeigt, wie wir abstrakte Modelle aus komplexen Systemen ableiten, um Analyse und Entwurf zu erleichtern. Darüber hinaus werden wir praktische Methoden zur Abstraktion verschiedener Arten von Kontrollsystemen erörtern, die uns mit den Fähigkeiten ausstatten, theoretische Konzepte in realen Szenarien anzuwenden.