Seminar: Hyperlogiken

Seminar im Sommersemester 2023 an der Westfälischen Wilhelms-Universität Münster

Veranstalter: Prof. Dr. Markus Müller-Olm, Jens Gutsfeld, Roman Lakenbrink, Christoph Ohrem

Eintrag für diese Veranstaltung im HIS/LSF

Hinweise

Es sind noch Plätze frei. Falls Sie an diesem Seminar teilnehmen möchten, schicken Sie bitte eine Mail an Christoph Ohrem (christoph.ohrem@uni-muenster.de).
DIe Folien der Vorbesprechung stehen im Learnwebkurs zur globalen Seminar- und Projektseminarvorstellung zur Verfügung.
Die Vorbesprechung findet am Montag, dem 30.1.2023 um 14:15 Uhr im SRZ 115 statt.

Thema und Zielgruppe

Reaktive Systeme sind Systeme die Ihre Umgebung kontinuierlich mithilfe von Sensoren beobachten und mit Aktoren auf beobachtete Änderungen reagieren und damit Ihre Umgebung steuern und kontrollieren. Derartige Systeme sind in der Praxis weiterverbreitet, insbesondere im Bereich eingebetteter Systeme. Ansätze zur Verifikation reaktiver Systeme umfassen unter anderem Model Checking, Monitoring und Synthese. Dabei werden die zu untersuchenden Software- oder Hardwaresysteme durch Transitionsgraphen modelliert, an deren Knoten atomare Systemigenschaften annotiert sind. Weiterhin gehört bei diesen Verifikationsansätzen die zu untersuchende Eigenschaft, gegeben durch eine Formel in einer Spezifikationslogik, mit zur Eingabe des Verifikationsalgorithmus. Prominente Beispiele für Spezifikationslogiken sind die temporalen Logiken Linear Temporal Logic (LTL) und Computational Tree Logic (CTL). Diese Logiken erlauben es, neben atomaren Programmeigenschaften auch Eigenschaften von einzelnen Systemausführungen (LTL) oder möglichem Verzweigungsverhalten (CTL) eines Systems über die Zeit zu spezifizieren. Ein Beispiel für eine in LTL ausdrückbare Eigenschaft wäre Die Ausführung des Systems erreicht irgendwann einen Zustand, der mit der Eigenschaft p annotiert ist. In der Literatur werden solche Eigenschaften häufig als Trace Properties bezeichnet. Es gibt jedoch auch Systemeigenschaften, die sich nicht durch Betrachtung einzelner Ausführungen eines Systems ausdrücken lassen, beispielsweise die Eigenschaft Alle Ausführungen des Systems erreichen nach der gleichen Anzahl an Schritten einen Zustand, der mit der Eigenschaft p annotiert ist. Im Gegensatz zu Trace Properties, die Eigenschaften einzelner Systemausführungen spezifizieren, handelt es sich hierbei um Eigenschaften, bei denen mehrere Systemausführungen miteinander verglichen werden. Eigenschaften dieser Art werden in der Literatur als Hyperproperties bezeichnet. Da Spezifikationslogiken wie LTL Hyperproperties nicht ausdrücken können, wurden in den letzten Jahren verschiedene so genannte Hyperlogiken zur Spezifikation und Verifikation von Hyperproperties entwickelt. Ein Beispiel hierfür ist HyperLTL, in dem die oben genannte Hyperproperty ausgedrückt werden kann.

In diesem Seminar wollen wir uns mit ausgewählten Originalartikeln aus dem Bereich der Hyperlogiken auseinandersetzen, in denen verschiedene Logiken und Verifikationsansätze vorgestellt werden. Vorkenntnisse über die genannten Verifikationsmethoden wie das Model Checking sind für die Teilnahme am Seminar nicht erforderlich, wohl aber das Interesse und die Bereitschaft sich mit anspruchsvollen informatisch/mathematischen Fragestellungen auseinanderzusetzen.

Das Seminar richtet sich an Masterstudierende im Fach Informatik oder im Fach Mathematik mit Nebenfach Informatik. In den M.Sc. Studiengängen kann es für das Modul „Informatikseminar“ angerechnet werden, im M.Sc. Informatik auch für das Modul "Seminar Formale Methoden". Im M.Ed. kann es für eines der Seminarmodule im Fach Informatik gewählt werden.

Ort und Zeit

Die Vorträge finden im Semester montags 14:15-15:45 Uhr in SRZ 113 statt.

Die genauen Termine der einzelnen Vorträge werden zu gegebener Zeit bekannt gegeben.