Allgemeines

Veranstaltungsnummer  040604
Veranstalter Thomas Zeume
Klassifikation Proseminar
Semester Wintersemester 2017/2018
Ort und Zeit  OH12-2.063, Zeit siehe Moodle
Vorbesprechung  4. Oktober, 14.00 Uhr
Querverbindungen GTI, Logik
Voraussetzungen wünschenswert MafI I + II, GTI

 

Inhalt

Automatenmodelle spielen in der Informatik in vielen Anwendungen eine wichtige Rolle. In diesem Proseminar werden wir verschiedene Automatenmodelle und ihre Verbindung zu Anwendungen kennenlernen:

  • w-Automaten sind den bereits bekannten endlichen Automaten sehr ähnlich, lesen jedoch unendlich lange Wörter. Sie werden bspw. in der formalen Verifikation von Hardware und Software verwendet.
  • Zeitautomaten ergänzen endliche Automaten um eine Komponente zur Modellierung von Zeit. Auch sie werden in der Verifikation verwendet.
  • Baumautomaten arbeiten auf Baumstrukturen. Im Kontext von XML finden sie Anwendung in Schema- und Anfragesprachen. In der Theorie finden sie Anwendung bei dem Nachweis, dass das Erfüllbarkeitsproblem bestimmter Logiken entscheidbar ist.
  • Zusätzlich können nach Wunsch andere Automatenmodelle wie zelluläre Automaten, Automaten für Wörter über unendlich-großen Symbolmengen sowie probabilistische Automaten behandelt werden.

Wir werden uns jeweils auf die theoretischen Eigenschaften der Automatenmodelle konzentrieren und in einzelnen Vorträgen eine Verbindung zur Praxis herstellen.

Für die Teilnahme am Proseminar sind ein solider Umgang mit mathematischer Notation sowie grundlegende Kenntnisse aus der theoretischen Informatik notwendig (erworben beispielsweise in den Vorlesungen Mathematik für Informatiker 1 und 2 sowie den Grundlagen der theoretischen Informatik).

Lust und Interesse an Theorie und ihren Anwendungen in der Praxis sind für eine erfolgreiche Seminarteilnahme sehr hilfreich!

Das Proseminar basiert auf verschiedenen Lehrbüchern und Forschungsarbeiten. Für einzelne Themen dienen die genannten Arbeiten nur als Einstieg für eine Literaturrecherche:

  • w-Wörter und Verifikation:
    • Bakhadyr Khoussainov and Anil Nerode. Automata theory and its applications, volume 21. Springer Science & Business Media, 2012
    • Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. Principles of model checking. MIT press, 2008
    • Mordechai Ben-Ari. Principles of the Spin model checker. Springer Science & Business Media, 2008
  • Zeitautomaten:
    • Béatrice Bérard. An introduction to timed automata. In Control of Discrete-Event Systems, pages 169–187. Springer, 2013
    • Kim G Larsen, Paul Pettersson, and Wang Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer (STTT), 1(1):134–152, 1997
    • Gerd Behrmann, Alexandre David, and Kim G Larsen. A tutorial on UPPAAL. In Formal methods for the design of real-time systems, pages 200–236. Springer, 2004
  • Baumautomaten:
    • Meghyn Bienvenu. Automata on infinite words and trees, 2009. Lecture Notes
    • Hubert Comon, Max Dauchet, Remi Gilleron, Florent Jacquemard, Christof Löding, Denis Lugiez, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications, 1997
    • Nils Klarlund, Thomas Schwentick, and Dan Suciu. XML: model, schemas, types, logics, and queries. In Logics for Emerging Applications of Databases, pages 1–41. Springer, 2004
    • Frank Neven. Automata theory for XML researchers. ACM Sigmod Record, 31(3):39–46, 2002
    • Wolfgang Thomas. Languages, automata, and logic. In Handbook of formal languages, pages 389–455. Springer, 1997
    • Wolfgang Thomas, Thomas Wilke, et al. Automata, logics, and infinite games: a guide to current research, volume 2500. Springer Science & Business Media, 2002
  • Weitere Automatenmodelle
    • Jarkko Kari. Cellular automata, 2016. Lecture Notes
    • Mikołaj Bojańczyk. Slightly infinite sets. Unpublished book draft