Seminar Guarded Logics and Automata

WS 2017/18


  • Students with a subject in mathematics can apply by writing an email to seminar [AT] 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.


The talks are given at the end of the semester in a block in german or english in our seminar room (4116, E1, Ahornstr. 55).

Length of a talk: 30 minutes.

  • Monday, 05. February
  • Wednesday, 07. February


12.12.17First version of your paper
10.01.18Final version
05.02. / 07.02.Talks (our seminar room 4116)


Montag, 05. Februar
10:0010:40Miriam WagnerGuarded fragments and bisimulation invariance
10:4011:20Isabel KlöterDecidability, complexity and FMP of GF
11:2012:00Isabelle GlasmacherCharacterization Theorem for GF
13:0013:40Domenic QuirlDecidability of full μ-calculus
Mittwoch, 07. Februar
11:0011:40Leon BohnFinite satisfiability of full μ-calculus
11:4012:20Timo SchummBisimulation invariant MSO corresponds to μ-calculus
12:2013:00Marcel StrohmannBisimulation invariant GSO corresponds to μGF
13:0013:40Lars BeckersGuarded Negation
Donnerstag, 15. März
11:0011:30Alina IbachInterpolation and Beth-Definability


Guarded fragments and bisimulation invarianceMiriam WagnerM. Hoelzel[GO14, ANB98]
Decidability, complexity and FMP of GFIsabel KlöterS. Schalthöfer[Gr99d, Hod02]
Characterization Theorem for GFIsabelle GlasmacherM. Hoelzel[Gr02, ANB98]
Interpolation and Beth-DefinabilityAlina IbachS. Schalthöfer[HMO99, HM02]
Decidability of full μ-calculusDomenic QuirlR. Wilke[Var98]
Decidability of μGFPhillip WhittingtonR. Wilke[GW99]
Finite satisfiability of full μ-calculusLeon BohnR. Wilke[Boj02]
Bisimulation invariant MSO corresponds to μ-calculusTimo SchummF. Reinhardt[JW96]
Bisimulation invariant GSO corresponds to μGFMarcel StrohmannF. Reinhardt[GHO02]
Guarded NegationLars BeckersK. Dannert[BCS11, CL13]


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


  • 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


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


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