Seminar über Automatentheorie

» Diese Veranstaltung wird auf deutsch gehalten.

Aktuelles/Ankündigungen

  • Die vorläufigen Termine der Vorträge stehen fest. Kurzfristige Terminänderungen sind jedoch nicht auszuschließen.
  • Die Folien aus der Vorbesprechung.

Inhalt

Gegenstand dieses Seminars sind Originalarbeiten und Überblicksartikel zur Automatentheorie, mit einem Schwerpunkt im Umkreis der Vorlesungen Automaten auf unendlichen Wörtern und Unendliche Spiele des WS 2008/09. Aktive Teilnahme an diesen Vorlesungen inklusive Übung ist hilfreich zur Bearbeitung der Themen und wird bei der Zuteilung von Plätzen berücksichtigt.

Termine

Das Seminar wird in 3 Blöcken zum Ende der Vorlesungszeit im Sommer 2009 gehalten. Nach der bisherigen Terminplanung sind dies die folgenden Tage:

  • Freitag 17.7.09
  • Freitag 24.7.09
  • Montag 27.7.09
Die Vorträge finden im Seminarraum am Lehrstuhl 7 statt.

Bei Fragen wenden Sie sich bitte an Christof Löding.

Themen am 17.7.09:

  1. 9 Uhr
    Potenzmengenkonstruktion für omega-Automaten
    Quelle: [DEK07]
    Vortrag: Sebastian Kaufmann
    Betreuung: A. Spelten
  2. 10:15 Uhr
    Entscheidbarkeit der linearen Arithmetik über ganzen und reellen Zahlen mittels schwacher Büchi-Automaten
    Quelle: [BJW01]
    Vortrag: Dimitri Isaak
    Betreuung: F. Radmacher
  3. 11:30 Uhr
    Von LTL zu Büchi-Automaten
    Quelle: [GO01]
    Vortrag: Norbert Wiechowski
    Betreuung: K. Wong
  4. 14 Uhr Uhr
    On-The-Fly Model-Checking
    Quelle: [HKM05]
    Vortrag: Robert Schulte
    Betreuung: K. Wong
  5. 15:15 Uhr
    Vacuity Detection
    Quelle: [KV99]
    Vortrag: Michael Wolf
    Betreuung: M. Slaats

Themen am 24.7.09:

  1. 9 Uhr
    Planungsalgorithmen für LTL
    Quelle: [PV03]
    Vortrag: Andreas Weigelt
    Betreuung: M. Slaats
  2. 10:15 Uhr
    Entscheidbarkeit für Pfadlogiken mit Synchronisation
    Quelle: [Tho09]
    Vortrag: Andrea Hutter
    Betreuung: M. Zimmermann / W. Thomas
  3. 11:30 Uhr
    Zielonka-Bäume I: Obere Speicherschranken für omega-Spiele
    Quelle: [DJW97]
    Vortrag: Christoph Abel
    Betreuung: M. Holtmann
  4. 14 Uhr
    Zielonka-Bäume II: Untere Speicherschranken für omega-Spiele
    Quelle: [DJW97]
    Vortrag: Marcus Gelderie
    Betreuung: M. Holtmann
  5. 15:15 Uhr
    Komplexität von Muller-Spielen
    Quellen: [Hor08], [HD08]
    Vortrag: Andrea Dieris
    Betreuung: C. Löding

Themen am 27.7.09:

  1. 9 Uhr
    Model-Checking für ATL mit schwachen Spielen
    Quelle: [HMS06]
    Vortrag: David Bulczak
    Betreuung: J. Olschewski
  2. 10:15 Uhr
    Permissive Strategien
    Quelle: [BJW02]
    Vortrag: Bastian Manske
    Betreuung: J. Olschewski
  3. 11:30 Uhr
    Nebenläufige Spiele
    Quelle: [AHK07]
    Vortrag: Michael Mussil
    Betreuung: M. Zimmermann
  4. 14 Uhr
    Spiele transfiniter Länge
    Quelle: [CH08]
    Vortrag: Patrick Jüptner
    Betreuung: D. Neider

Quellen

[AHK07] L. de Alfaro, T.A. Henzinger, O. Kupferman. Concurrent Reachability Games. In Theoretical Computer Science 386 (3), 188-217. Elsevier, 2007.
[BHJ03] B. Boigelot, F. Herbreteau, S. Jodogne. Hybrid Acceleration using Real Vector Automata. Proc. 15th International Conference on Computer-Aided Verification, volume 2725, Lecture Notes in Computer Science, pages 193-205, Boulder, July 2003.
[BJW01] B. Boigelot, S. Jodogne, P. Wolper. On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables. In Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR 2001). Volume 2083 of Lecture Notes in Computer Science, pages 611-625, Springer-Verlag, 2001.
[BJW02] Julien Bernet, David Janin, Igor Walukiewicz. Permissive strategies: from parity games to safety games. Informatique Théorique et Applications (ITA), Volume 36, 2002
[CH08] Julien Cristau and Florian Horn. Graph Games on Ordinals. In Proceedings of the 28th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'08, pages 143-154. Dagstuhl Research Online, 2008.
[DEK07] Christian Dax, Jochen Eisinger, Felix Klaedtke. Mechanizing the Powerset Construction for Restricted Classes of omega-Automata. Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007). Volume 4762 of Lecture Notes in Computer Science, pages 223-236, Springer-Verlag, 2007.
[DJW97] Stefan Dziembowski, Igor Walukiewicz, Marcin Jurdzinski. How much memory is needed to win infinite games? Proceedings of 12th Annual IEEE Symp. on Logic in Computer Science, LICS'97, July 1997
[EK06] Jochen Eisinger, Felix Klaedtke. Don't Care Words with an Application to the Automata-based Approach for Real Addition. In the Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006). Volume 4144 of Lecture Notes in Computer Science, pages 67--80. Springer-Verlag, 2006.
[GO01] P. Gastin and D. Oddoux. Fast LTL to Büchi Automata Translation. In CAV'01, LNCS 2102, pages 53-65. Springer, 2001.
[HD08] Paul Hunter, Anuj Dawar. Complexity Bounds for Muller Games. Theoretical Computer Science (TCS), 2008. Submitted.
[HKM05] Moritz Hammer, Alexander Knapp, and Stephan Merz Truly On-The-Fly LTL Model Checking. 11th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems (2005). Springer-Verlag, LNCS 3440, pp. 191-205 (2005)
[HMS06] Malte Helmert, Robert Mattmüller, and Sven Schewe. Selective Approaches for Solving Weak Games. ATVA 2006
[Hor08] Florian Horn. Explicit Muller Games are PTIME. In Proceedings of the 28th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'08, pages 235-243. Dagstuhl Research Online, 2008.
[KV99] Orna Kupferman, Moshe Y. Vardi. Vacuity Detection in Temporal Model Checking. CHARME'99
[PV03] Marco Pistore, Moshe Y. Vardi. The Planning Spectrum: One, Two, Three, Infinity. Proceedings of the 8th IEEE Symposium on Logic in Computer Science (LICS 2003), IEEE Computer Society 2003, pp. 234-243.
[Tho09] W. Thomas. Path logics with synchronization. In Perspectives in Concurrency Theory (K. Lodaya et al., editors). Univerties Press India, 2009. pp. 469-481.