Modul "Beyond First-Order Logic" (2 Sem)

 

1 Organisatorisches

Samstag, 15.09.2007, 14-16

A3-209

A. Schäfer

 

2 Ziele

Kennenlernen verschiedener Logiken, die über die aus dem Grundstudium bekannte Aussagenlogik und Prädikatenlogik hinausgehen sowie das Einüben von Präsentationstechniken.

 

3 Inhalt

In der Grundstudiumsvorlesung Theoretische Informatik I werden Aussagenlogik, Prädikatenlogik und die Lineare Temporale Logik vorgestellt und Eigenschaften dieser Formalismen untersucht. Darüber hinaus gibt es jedoch eine Vielzahl von weiteren Logiken, die Gegenstand aktueller Forschung sind. Beispiele hierfür sind Monadische Logik zweiter Stufe, Modallogik, Mehrdimensionale Modallogik, Hybride Logik, Region Connection Calculus, Timed PTL, Timed CTL, Spatiale Logik für Mobile Systeme. Viele dieser Logiken werden für die Spezifikation von Systemen verwendet. Wichtige Fragestellungen sind deshalb (effiziente) Entscheidbarkeit des Gültigkeits- und des Model-Checking Problems. In den Seminarvorträgen soll jeweils eine Logik zusammen mit ihren grundlegenden Eigenschaften vorgestellt werden.

 

4 Themen

4.1 Sven Linker: Monadische Logik zweiter Stufe

Zusammenfassung: Diese Ausarbeitung stellt die Monadische Logik zweiter Stufe (MSO) interpretiert über endlichen und unendlichen Wörtern vor. Es wird der Beweis des Satzes von Büchi skizziert, der besagt, dass durch diese Logik genau die regulären Sprachen beschrieben werden. Analog gilt dieser Zusammenhang auch zwischen MSO über unendlichen Wörtern und omega-regulären Sprachen, die durch Büchi-Automaten akzeptiert werden. Aus dieser Äquivalenz folgt direkt die Entscheidbarkeit des Erfüllbarkeitsproblems für MSO. Dadurch können in dieser Logik beschriebene Systeme automatisch verifiziert werden, z.B. durch Werzeuge wie MONA.

[Ausarbeitung] [Folien]

4.2 Eike Möhlmann: Regular Model-Checking

Zusammenfassung: Diese Ausarbeitung beschäftigt sich mit Verfahren zum Modellieren komplexer Systeme mit unendlichen Zustandsmengen, bei denen die Konfigurationen durch Wörter über einem endlichen Alphabet dargestellt werden. Es werdem reguläre Sprachen verwendet, um Mengen von Konfigurationen zu beschreiben. Weiterhin werden Möglichkeiten zum Model-Checking vorgestellt.

[Ausarbeitung] [Folien]