Seminar Guarded Logics and Automata

WS 2017/18

Registration

  • Students with a subject in mathematics can apply by writing an email to seminar [AT] logic.rwth-aachen.de including their name, immatriculation no., subject of studies, no. of semesters of studies, and information about relevant modules they have passed (especially lectures from our group).
  • Students in computer science need to apply via the central assignment of seminar places.

Organisation

The talks are given at the end of the semester in a block in german or english.

  • Monday, 29. January
  • Tuesday, 30. January

Deadlines

06.11.17 Outline
12.12.17 First version of your paper
10.01.18 Final version
22.01.18 Slides
29.01. / 30.01. Talks

Topics

Thema Vortragende(r) Betreuer(in) Literatur
Guarded fragments and bisimulation invariance Miriam Wagner M. Hoelzel [GO14, ANB98]
Decidability, complexity and FMP of GF Isabel Klöter S. Schalthöfer [Gr99d, Hod02]
Characterization Theorem for GF Isabel Glasmacher M. Hoelzel [Gr02, ANB98]
Interpolation and Beth-Definability Alina Ibach S. Schalthöfer [HMO99, HM02]
Decidability of full μ-calculus Domenic Quirl R. Wilke [Var98]
Decidability of μGF Phillip Whittington R. Wilke [GW99]
Finite satisfiability of full μ-calculus Leon Bohn R. Wilke [Boj02]
Bisimulation invariant MSO corresponds to μ-calculus Timo Schumm F. Reinhardt [JW96]
Bisimulation invariant GSO corresponds to μGF Marcel Strohmann F. Reinhardt [GHO02]
Guarded Negation Lars Beckers K. Dannert [BCS11, CL13]

Literature

[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.

Classification

  • 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

Prerequisites

  • Module Mathematical Logic
  • Basic knowledge in the field automata theory
  • for B.Sc. Computer Science: Module "Einführung in das wissenschaftliche Arbeiten (Proseminar)"

Contact

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