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 in our seminar room (4116, E1, Ahornstr. 55).Length of a talk: 30 minutes.
- Monday, 05. February
- Wednesday, 07. February
Deadlines
| 06.11.17 | Outline |
| 12.12.17 | First version of your paper |
| 10.01.18 | Final version |
| 22.01.18 | Slides |
| 05.02. / 07.02. | Talks (our seminar room 4116) |
Schedule
| Montag, 05. Februar | ||||
| – | Miriam Wagner | Guarded fragments and bisimulation invariance | ||
| – | Isabel Klöter | Decidability, complexity and FMP of GF | ||
| – | Isabelle Glasmacher | Characterization Theorem for GF | ||
| – | ||||
| – | Domenic Quirl | Decidability of full μ-calculus | ||
| Mittwoch, 07. Februar | ||||
| – | Leon Bohn | Finite satisfiability of full μ-calculus | ||
| – | Timo Schumm | Bisimulation invariant MSO corresponds to μ-calculus | ||
| – | Marcel Strohmann | Bisimulation invariant GSO corresponds to μGF | ||
| – | Lars Beckers | Guarded Negation | ||
| Donnerstag, 15. März | ||||
| – | Alina Ibach | Interpolation and Beth-Definability | ||
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 | Isabelle 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