Logik und Datenbanktheorie
Prof. Dr. Nicole Schweikardt
Logik und diskrete Systeme
Prof. Dr. Stephan Kreutzer

Logik in der Informatik, Institut für Informatik, Humboldt-Universität zu Berlin

Seminar Endliche Modelltheorie

   Aktuelles    Einführung    Zeit & Raum & Organisation    Vortragsthemen    Literatur    Vorträge     Programm    

Aktuelles:
An dieser Stelle finden Sie im Laufe des Seminars aktuelle Mitteilungen. Bitte sehen Sie regelmäßig nach, ob es Neues gibt.

  • Das Programm finden Sie hier.

  • Die Literatur zu den einzelnen Vortragsthemen kann bei Stephan Kreutzer bzw. Nicole Schweikardt abgeholt werden.

  • Das Seminar findet als Blockveranstaltung am Dienstag, den 31.01.2006 und am Mittwoch, den 01.02.2006 in Raum 4.410 des Johann von Neumann-Hauses statt.

  • Die Vorbesprechung und Themenvergabe findet in der ersten Semesterwoche am Freitag, den 21.10.2005 um 15:15 Uhr in Raum 4.410, Johann von Neumann-Haus, statt.

Programm:

Das Seminar findet in Raum 4.410 des Johann von Neumann-Hauses statt.
Für jeden Vortrag sind 60 Minuten plus 15 Minuten für die anschließende Diskussion eingeplant.

Dienstag, 31.01.06

  • 14:15 - 15:30:   Peter Liske, MSO Model Checking auf Bäumen
  • 15:30 - 15:40:   - Pause -
  • 15:40 - 16:55:   Gunar Maiwald, Untere Schranken für das MSO Model Checking auf Bäumen

Mittwoch, 01.02.06

  •   9:15 - 10:30:   Philipp Hussels, Baumzerlegungen von Graphen
  • 10:30 - 10:40:   - Pause -
  • 10:40 - 11:55:   Nannette Kase, MSO Model Checking auf baumähnlichen Strukturen
  • 11:55 - 12:05:   - Pause -
  • 12:05 - 13:20:   David Baehrens, Bildsprachen und existentielle MSO Logik

Einführung:
Das Seminar richtet sich an Studierende mit Interesse an Logik und theoretischer Informatik. Behandelt werden Themen zur Ausdrucksstärke und Komplexität logischer Systeme wie zum Beispiel temporaler Logiken, MSO oder XPath. Dabei kommen vor allem Methoden aus der Automaten- und Spieltheorie, der Graphentheorie und der Kombinatorik zum Einsatz.

Im Seminar werden Originalarbeiten zum Thema behandelt. Vorausgesetzt werden gute Kenntnisse der theoretischen Informatik.

Zeit, Raum und Organisation:

Vorbesprechung und Themenvergabe sind in der ersten Semesterwoche am Freitag, den 21.10.2005 um 15:15 Uhr in Raum 4.410, Johann von Neumann-Haus.

Das Seminar ist als Blockveranstaltung organisiert und findet am Dienstag, den 31.01.2006 und am Mittwoch, den 01.02.2006 in Raum 4.410 des Johann von Neumann-Hauses statt.
Für jedes Vortragsthema werden 75 Minuten eingeplant: 60 Minuten für den Vortrag und zusätzlich 15 Minuten für Zwischenfragen und Diskussion.

Bitte holen Sie möglichst bald die Literatur zu Ihrem Vortragsthema bei Stephan Kreutzer oder Nicole Schweikardt ab und erarbeiten Sie bis Anfang Dezember ein Vortragskonzept, das Sie in der Woche vom 5. bis 12.12.2005 bei Ihrem/r Betreuer/in vorlegen.
Die schriftliche Ausarbeitung Ihres Vortragsthemas (ca. 5 Seiten) sollten Sie bis spätestens 04.01.2006 bei Ihrem/r Betreuer/in abgeben.

Mögliche Vortragsthemen:
  1. MSO Model Checking auf Bäumen
  2. Untere Schranken für das MSO Model Checking auf Bäumen
  3. Baumzerlegungen von Graphen
  4. MSO Model Checking auf baumähnlichen Strukturen
  5. Bildsprachen und existentielle MSO Logik
  6. Quantoren in EMSO: Wörter, Bäume und Bilder
  7. Quantoren in EMSO: Graphen
  8. Modallogik und Bisimulation
  9. Prädikatenlogik, Bisimulation und Modallogik

Literatur:

Einführende Literatur:
[KS] S. Kreutzer und N. Schweikardt. Logik und Komplexität. Skript zur Vorlesung im Sommersemester 2005. 162 Seiten (pdf-Datei).
[EF] H.-D. Ebbinghaus und J. Flum. Finite Model Theory. Springer-Verlag, 2te Auflage, 1999.
[I] N. Immerman. Descriptive Complexity. Springer-Verlag, 1999.
[L] L. Libkin. Elements of Finite Model Theory. Springer-Verlag, 2004.
[G] E. Grädel. Finite Model Theory and Descriptive Complexity. Der Artikel ist hier erhältlich. Er wird im Buch Finite Model Theory and Its Applications (Springer-Verlag, 2005) erscheinen.
[K] P. Kolaitis. On the expressive power of logics on finite models. Der Artikel ist hier erhältlich. Er wird im Buch Finite Model Theory and Its Applications (Springer-Verlag, 2005) erscheinen.
[K] W. Thomas. Languages, automata, and logic. In G. Rozenberg und A. Salomaa, Herausgeber, Handbook of Formal Languages, volume III, Seiten 389-455. Springer, New York, 1997.
Auch als technischer Bericht Technical Report 9607, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, May 1996 erhältlich (ps-Datei).

Literatur zu den einzelnen Vorträgen:
  1. Kapitel 10.1 und 10.2. aus: J. Flum und M. Grohe. Parameterized Complexity Theory. Lehrbuch, erscheint voraussichtlich in 2006.

  2. Kapitel 10.3. aus: J. Flum und M. Grohe. Parameterized Complexity Theory. Lehrbuch, erscheint voraussichtlich in 2006.

  3. Kapitel 11.1-11.3. aus: J. Flum und M. Grohe. Parameterized Complexity Theory. Lehrbuch, erscheint voraussichtlich in 2006.

  4. Kapitel 11.4. aus: J. Flum und M. Grohe. Parameterized Complexity Theory. Lehrbuch, erscheint voraussichtlich in 2006.
    Und:
    H. Bodlaender. Treewidth: Algorithmic techniques and results. MFCS'97, Band 1295 von Lecture Notes in Computer Science, Springer-Verlag, Seiten 19-36, 1997.

  5. Kapitel 1 bis 3.1 aus: D. Giammarresi, A. Restivo, S. Seibert und W. Thomas. Monadic Second-Order Logic over Rectangular Pictures and Recognizability by Tiling Systems. Information and Computation 125, 32-45, 1996.
    Und:
    M. Latteux und D. Simplot. Context-Sensitive String Languages and Recognizable Picture Languages. Information and Computation 138, 160-169, 1997.

  6. Kapitel 2 aus: A. Potthoff. Logische Charakterisierung regulärer Baumsprachen. Dissertation an der Christian-Albrechts-Universität zu Kiel, 1994.
    Und:
    O. Matz. One Quantifier Will Do in Existential Monadic Second-Order Logic over Pictures. MFCS'98, Band 1450 von Lecture Notes in Computer Science, Springer-Verlag, Seiten 751-759, 1998.

  7. M. Otto. A note on the number of monadic quantifiers in monadic Σ_1^1. Information Processing Letters 53, 337-339, 1995.
    Und:
    Kapitel 1-5 aus: R. Fagin, L.J. Stockmeyer und M.Y. Vardi. On Monadic NP vs Monadic co-NP. Information and Computation 120, 78-92, 1995.

Vorträge:
Nr. Thema Vortragende/r Ansprechpartner
1. MSO Model Checking auf Bäumen Peter Liske Stephan Kreutzer
2. Untere Schranken für das MSO Model Checking auf Bäumen Gunar Maiwald Stephan Kreutzer
3. Baumzerlegungen von Graphen Philipp Hussels Stephan Kreutzer
4. MSO Model Checking auf baumähnlichen Strukturen Nannette Kase Stephan Kreutzer
5. Bildsprachen und existentielle MSO Logik David Baehrens Nicole Schweikardt
6. Quantoren in EMSO: Wörter, Bäume und Bilder Véronique Tietz Nicole Schweikardt
7. Quantoren in EMSO: Graphen Geneviève Grunert Nicole Schweikardt

 

Last modified: Fri Jan 27 15:16:43 CET 2006
Nicole Schweikardt