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 in unserem Seminarraum (4116, E1, Ahornstr. 55) gehalten.Vortragsdauer: 30 Minuten.
Die Vorträge finden statt am:
- Montag, 05. Februar
- Mittwoch, 07. Februar
Zeitplan
| 06.11.17 | Gliederung |
| 12.12.17 | Erste Version der Ausarbeitung |
| 10.01.18 | Endgültige Fassung |
| 22.01.18 | Folien |
| 05.02. / 07.02. | Vorträge (unser Seminarraum 4116) |
Programm
| Montag, 05. Februar | ||||
| 10:00 | – | 10:40 | Miriam Wagner | Bewachte Fragmente und Bisimulationsinvarianz |
| 10:40 | – | 11:20 | Isabel Klöter | Entscheidbarkeit, Komplexität und EME von GF |
| 11:20 | – | 12:00 | Isabelle Glasmacher | Charakterisierungssatz für GF |
| 12:00 | – | 13:00 | Pause | |
| 13:00 | – | 13:40 | Domenic Quirl | Entscheidbarkeit des vollständigen μ-Kalküls |
| Mittwoch, 07. Februar | ||||
| 11:00 | – | 11:40 | Leon Bohn | Endliche Erfüllbarkeit des vollständigen μ-Kalküls |
| 11:40 | – | 12:20 | Timo Schumm | Bisimulationsinvariantes MSO entspricht μ-Kalkül |
| 12:20 | – | 13:00 | Marcel Strohmann | Bisimulationsinvariantes GSO entspricht μGF |
| 13:00 | – | 13:40 | Lars Beckers | Bewachte Negation |
| Donnerstag, 15. März | ||||
| 11:00 | – | 11:30 | Alina Ibach | Interpolation und Beth-Definierbarkeit |
Themen
| Thema | Vortragende(r) | Betreuer(in) | Literatur |
| Bewachte Fragmente und Bisimulationsinvarianz | Miriam Wagner | M. Hoelzel | [GO14, ANB98] |
| Entscheidbarkeit, Komplexität und EME von GF | Isabel Klöter | S. Schalthöfer | [Gr99d, Hod02] |
| Charakterisierungssatz für GF | Isabelle Glasmacher | M. Hoelzel | [Gr02, ANB98] |
| Interpolation und Beth-Definierbarkeit | Alina Ibach | S. Schalthöfer | [HMO99, HM02] |
| Entscheidbarkeit des vollständigen μ-Kalküls | Domenic Quirl | R. Wilke | [Var98] |
| Entscheidbarkeit von μGF | Phillip Whittington | R. Wilke | [GW99] |
| Endliche Erfüllbarkeit des vollständigen μ-Kalküls | Leon Bohn | R. Wilke | [Boj02] |
| Bisimulationsinvariantes MSO entspricht μ-Kalkül | Timo Schumm | F. Reinhardt | [JW96] |
| Bisimulationsinvariantes GSO entspricht μGF | Marcel Strohmann | F. Reinhardt | [GHO02] |
| Bewachte Negation | Lars Beckers | K. 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