Aktuelles

• Auch am Freitag finden die Vorträge im Raum 4105 (Seminarraum I4) statt.
• Sie finden nun auf dieser Webseite die Themen des Seminars mit ersten Literaturangaben, die Zuteilung der Themen zu den Betreuern sowie die Deadlines.
• Die Seminarvorbesprechung findet am 6.10. um 11 Uhr im Seminarraum des Lehrstuhls Informatik 7 (Raum 4116 im Erweiterungsgebäude 1, Ahornstr. 55) statt.

Organisation

Die Veranstaltung wird als Blockseminar am Ende der Vorlesungszeit durchgeführt.

Zeitplan

25.10.	Gliederung
22.11.	Ausarbeitung
20.12.	Endgültige Fassung
10.01.	Folien
03.02.-04.02.	Vorträge

Programm

Donnerstag, 03. Februar
12:30	–	13:20	Sebastian Goderbauer	Bewachte Bisimulation und das bewachte Fragment
13:20	–	14:10	Nicolas Breuckmann	Charakterisierungssatz für GF
14:20	–	15:10	Inga Herber	Endliche Modelleigenschaft von GF
Freitag, 04. Februar
9:00	–	9:50	Marcel Klinzing	Entscheidbarkeit und Komplexität von GF
9:50	–	10:40	Andreas Krüger	Bewachte Fixpunktlogik und Baumtheorien
10:50	–	11:40	Moses Ganardi	Charakterisierungssatz für die bewachte Fixpunktlogik
12:40	–	13:30	Yannic Maus	Endliche Erfüllbarkeit von bewachter Fixpunktlogik (1)
13:30	–	14:20	Malte Milatz	Endliche Erfüllbarkeit von bewachter Fixpunktlogik (2)

Inhalt

Warum haben modale Logiken so gute und robuste algorithmische Eigenschaften? Ein wichtiger Grund für die Bedeutung modaler, temporaler und dynamischer Logiken in der Informatik sind die günstigen algorithmischen und modelltheoretischen Eigenschaften wie Entscheidbarkeit, Endliche-Modell-Eigenschaft, Bisimulationsinvarianz, Model-Checking Algorithmen mit moderater Komplexität etc. Dies trifft nicht nur auf die klassische Modallogik ML zu sondern auch auf Erweiterungen wie CTL, PDL, GL und den modalen mu-Kalkül. Der Grund dafür wurde jedoch lange nicht richtig verstanden.

Bei der Übersetzung von Modallogik in die Prädikatenlogik fällt auf, dass die Formeln einerseits nur zwei Variablen benötigen und dass andererseits alle Quantoren bezüglich der Kantenrelation relativiert, d.h. von atomaren Formeln (den sogenannten Guards) der Form Exy "bewacht", sind. Es hat sich herausgestellt, dass der erste Punkt alleine diese Robustheit nicht erklären kann, da bereits schwache Erweiterungen der Prädikatenlogik mit nur zwei Variablen unentscheidbar sind. Jedoch konnte gezeigt werden, dass Einschränkungen der Prädikatenlogik, in der alle Quantoren durch geeignete Guards relativiert sind (z.B. das guarded fragment), die günstigen Eigenschaften der Modallogik erben.

In diesem Seminar werden verschiedene solcher Einschränkungen bekannter Logiken wie Logik erster und zweiter Stufe und Fixpunktlogiken im Hinblick auf ihre Ausdrucksstärke und algorithmischen Eigenschaften untersucht.

Themen

Thema	Vortragende(r)	Betreuer(in)	Literatur
Bewachte Bisimulation und das bewachte Fragment	Sebastian Goderbauer	Diana Fischer	[ANB98, Gr99d, Gr02]
Charakterisierungssatz für GF	Nicolas Breuckmann	Diana Fischer	[ANB98, Gr02, Hod93]
Entscheidbarkeit und Komplexität von GF	Marcel Klinzing	Bernd Puchala	[Gr99d]
Endliche Modelleigenschaft von GF	Inga Herber	Bernd Puchala	[Gr99d, Ho02]
Bewachte Fixpunktlogik und Baumtheorien	Andreas Krüger	Roman Rabinovich	[Gr02, GrWa99]
Bewachte Fixpunktlogik und Automaten	Jan Rappen	Roman Rabinovich	[GrWa99, BBl02]
Charakterisierungssatz für die bewachte Fixpunktlogik	Moses Ganardi	Roman Rabinovich	[GrHiOt00, GrWa99]
Beth-Definierbarkeit und Interpolation für GF	Michaela Wehling	Diana Fischer	[HM02, HMO99]
Endliche Erfüllbarkeit von bewachter Fixpunktlogik (1)	Yannic Maus	Bernd Puchala	[BGO10,Bo02]
Endliche Erfüllbarkeit von bewachter Fixpunktlogik (2)	Malte Milatz	Bernd Puchala	[BGO10,Bo02]
Datalog LITE	Michael Hackstein	Tobias Ganzow	[GoGrVe99]

Literatur

[ANB98]	H. Andréka, I. Németi, and J. van Benthem. Modal Logic and Bounded Fragments of Predicate Logic. Journal of Philosophical Logic, vol. 27(3), pp. 217–274, 1998.
[BBl02]	Dietmar Berwanger and Achim Blumensath. Automata for Guarded Fixed Point Logics. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), LNCS, pp. 343-355. Springer Verlag, 2002.
[BGO10]	V. Bárány, G. Gottlob, and M. Otto. Querying the Guarded Fragment. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pp. 1-10, 2010.
[Bo02]	M. Bojanczyk. Two-Way Alternating Automata and Finite Models. In Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings, vol. 2380 of Lecture Notes in Computer Science, pp. 833-844, 20022002.
[GoGrVe99]	G. Gottlob, E. Grädel, and H. Veith. Datalog LITE: A deductive query language with linear time model checking. ACM Transactions on Computational Logic, vol. 3(1), pp. 1–35, 2002.
[Gr02]	E. Grädel. Guarded fixed point logic and the monadic theory of trees. Theoretical Computer Science, vol. 288, pp. 129–152, 2002.
[Gr99d]	E. Grädel. On the restraining power of guards. Journal of Symbolic Logic, vol. 64, pp. 1719–1742, 1999.
[GrHiOt00]	E. Grädel, C. Hirsch, and M. Otto. Back and Forth Between Guarded and Modal Logics. ACM Transactions on Computational Logics, vol. 3(3), pp. 418 – 463, 2002.
[GrWa99]	E. Grädel and I. Walukiewicz. Guarded Fixed Point Logic. In Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS `99, Trento, pp. 45–54, 1999.
[HM02]	E. Hoogland and M. Marx. Interpolation and Definability in Guarded Fragments. Studia Logica, vol. 70(3), pp. 373-409, 2002.
[HMO99]	E. Hoogland, M. Marx, and M. Otto. Beth Definability for the Guarded Fragment. In Proceedings of LPAR'99, LNAI. Springer, 1999.
[Ho02]	I. M. Hodkinson. Loosely Guarded Fragment of First-Order Logic has the Finite Model Property. Studia Logica, vol. 70(2), pp. 205-240, 2002.
[Hod93]	W. Hodges. Model theory. Cambridge University Press, 1993.

Zuordnung

• Informatik (B.Sc.)/Seminar Informatik
• Mathematik (B.Sc.)/Seminar: Logik, Komplexität, Spiele
• Informatik (M.Sc.)/Seminar Theoretische Informatik
• Mathematik (M.Sc.)/Seminar: Logik, Komplexität, Spiele (Reine Mathematik)
• Informatik (D)/Hauptstudium/Theoretische Informatik
• Mathematik (D)/Hauptstudium/Reine Mathematik
• Informatik (S II)
• Mathematik (S II)/Hauptstudium/Modul Algebra
• Mathematik (S II)/Hauptstudium/Modul Angewandte Mathematik

Voraussetzungen

• Modul Mathematische Logik
• für B.Sc. Informatik: bestandenes Modul "Einführung in das wissenschaftliche Arbeiten (Proseminar)"

Rückfragen

Erich Grädel, Diana Fischer, Tobias Ganzow, Bernd Puchala, Roman Rabinovich