Seminar Bewachte Logiken und Automaten

WS 2017/18

Anmeldung

  • Studierende in Mathematik-Studiengängen können sich per Email an seminar [AT] logic.rwth-aachen.de bewerben. Bitte geben Sie dazu Ihren vollständigen Namen, Matrikelnummer, Studiengang, Fachsemester und Ihre Vorkenntnisse (insbesondere an unserem Lehrgebiet besuchte Vorlesungen) an.
  • Studierende in Informatik-Studiengängen können sich über die zentrale Vergabe von Seminarplätzen bewerben.

Organisation

Die Veranstaltung wird als Blockseminar angeboten, die Vorträge werden am Ende des Semesters wahlweise auf deutsch oder englisch gehalten.

Die Vorträge finden statt am:

  • Montag, 29. Januar
  • Dienstag, 30. Januar

Zeitplan

06.11.17Gliederung
12.12.17Erste Version der Ausarbeitung
10.01.18Endgültige Fassung
22.01.18Folien
29.01. / 30.01.Vorträge

Themen

ThemaVortragende(r)Betreuer(in)Literatur
Bewachte Fragmente und BisimulationsinvarianzMiriam WagnerM. Hoelzel[GO14, ANB98]
Entscheidbarkeit, Komplexität und EME von GFIsabel KlöterS. Schalthöfer[Gr99d, Hod02]
Charakterisierungssatz für GFIsabel GlasmacherM. Hoelzel[Gr02, ANB98]
Interpolation und Beth-DefinierbarkeitAlina IbachS. Schalthöfer[HMO99, HM02]
Entscheidbarkeit des vollständigen μ-KalkülsDomenic QuirlR. Wilke[Var98]
Entscheidbarkeit von μGFPhillip WhittingtonR. Wilke[GW99]
Endliche Erfüllbarkeit des vollständigen μ-KalkülsLeon BohnR. Wilke[Boj02]
Bisimulationsinvariantes MSO entspricht μ-KalkülTimo SchummF. Reinhardt[JW96]
Bisimulationsinvariantes GSO entspricht μGFMarcel StrohmannF. Reinhardt[GHO02]
Bewachte NegationLars BeckersK. Dannert[BCS11, CL13]

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.
[BB02]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.
[BB12]V. Bárány and M. Bojanczyk. Finite satisfiability for guarded fixpoint logic. Information Processing Letters, vol. 112(10), pp. 371 - 375, 2012.
[BBB17]M. Benedikt, P. Bourhis, and M. Vanden Boom. Characterizing Definability in Decidable Fixpoint Logics. CoRR, vol. abs/1705.01823, 2017.
[BCS11]V. Bárány, B. ten Cate, and L. Segoufin (L. Aceto, M. Henzinger, and J. Sgall, Eds.). Guarded Negation. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011.
[BG01]D. Berwanger and E. Grädel. Games and Model Checking for Guarded Logics. In Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, {LPAR 2001, Havana} (R. Nieuwenhuis and A. Voronkov, Eds.), vol. 2250 of LNCS. Springer, 2001.
[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.
[BW15]J. Bradfield and I. Walukiewicz. The mu-calculus and model-checking. In Handbook of Model Checking (E. Clarke, T. Henzinger, and H. Veith, Eds.). Springer-Verlag, 2015.
[Boj02]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, 2002.
[CL13]L. Segoufin and B. ten Cate. Unary negation. Logical Methods in Computer Science, vol. Volume 9, Issue 3, 2013.
[GGV02]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.
[GHO02]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.
[GO14]E. Grädel and M. Otto. The Freedoms of (Guarded) Bisimulation. In Johan van Benthem on Logic and Information Dynamics (A. Baltag and S. Smets, Eds.), vol. 5 of Outstanding Contributions to Logic, pp. 3-31. Springer, 2014.
[GTW02]E. Grädel, W. Thomas, and T. Wilke (Eds.). Automata, Logics, and Infinite Games. Springer, 2002.
[GW99]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.
[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.
[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.
[Her95]B. Herwig. Extending partial isomorphisms on finite structures. Combinatorica, vol. 15(3), pp. 365–371, 1995.
[Hod02]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.
[JW96]D. Janin and I. Walukiewicz (U. Montanari and V. Sassone, Eds.). On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996.
[Var98]M. Y. Vardi (K. G. Larsen, S. Skyum, and G. Winskel, Eds.). Reasoning about the past with two-way automata. Springer Berlin Heidelberg, Berlin, Heidelberg, 1998.

Zuordnung

  • Informatik (B.Sc.)/Seminare
  • Informatik (B.Sc.)/Zusätzliche Veranstaltungen
  • Informatik (M.Sc.)/Theoretische Informatik
  • Mathematik (B.Sc.)
  • Mathematik (M.Sc.)/Reine Mathematik
  • Mathematik (GYM+GS,BK,SII)/Mathematik
  • TK 2. Fach-Grundlagen der Informatik (M.Sc.)/Seminar

Voraussetzungen

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

Rückfragen

Erich Grädel, Matthias Hoelzel, Frederic Reinhardt, Svenja Schalthöfer, Richard Wilke