Seminar Logik, Komplexität, Spiele: Guarded Logics

WS 2010/11

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