Allgemeines

Veranstaltungsnummer  040603
Veranstalter Thomas Zeume
Klassifikation Proseminar
Semester Wintersemester 2019/2020
Ort und Zeit  Ort & Zeit siehe Moodle
Vorbesprechung n. a.
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

Allgemeines

Veranstaltungsnummer  
Veranstalter Nils Vortmeier
Klassifikation Proseminar
Semester Wintersemester 2017/18
Ort und Zeit OH12 2.063, Mi 12-14 Uhr
Vorbesprechung  
Querverbindungen DAP 2, GTI
Voraussetzungen DAP 2, GTI wünschenswert

Inhalt

Um Optimierungsprobleme zu lösen, wünscht man sich üblicherweise einen Algorithmus, der zu einer gegebenen Probleminstanz in möglichst geringer Laufzeit eine optimale Lösung erzeugt. Bedauerlicherweise ist es nicht immer möglich, gleichzeitig eine geringe Laufzeit und eine optimale Lösung zu garantieren. Wir beschäftigen uns in diesem Proseminar also mit Algorithmen, die zwar effizient sind (also höchstens polynomielle Laufzeit benötigen), allerdings nur eine näherungsweise optimale Lösung erzeugen. Dabei betrachten wir zwei verschiedene Sorten von Optimierungsproblemen, die jeweils auf ihre eigene Weise "zu schwierig" sind, um sie effizient exakt zu lösen.

  • Optimierungsprobleme, deren zugehörige Entscheidungsprobleme NP-schwierig sind, lassen sich (vermutlich) nicht effizient lösen. Da diese Probleme in der Praxis dennoch gelegentlich auftauchen, beschäftigen wir uns mit Approximationsalgorithmen, die in polynomieller Zeit eine "hinreichend gute" Lösung liefern sollen.
  • Speziell bei maschinennahen Optimierungsproblemen wie dem Paging-Problem, also der Frage, wann Speicherseiten aus einem schnellen, aber kleinen Speicher in einen großen, dafür langsamen Speicher ausgelagert werden sollen, kommt es öfters vor, dass die Eingabeinstanz (im Beispiel: eine Folge von Speicherzugriffen) nicht im Voraus bekannt ist sondern erst zur Laufzeit des Algorithmus Stück für Stück bekannt gegeben wird. Zu dieser Art von Problemen betrachten wir Online-Algorithmen, die darauf ausgelegt sind,  eine solche "streaming-artige" Form der Eingabe möglichst gut zu verarbeiten.

In beiden Fällen betrachten wir Algorithmen, die ein gegebenes Problem nicht exakt lösen, allerdings gewisse Qualitätsgarantien erfüllen (wie z.B. Paging-Algorithmen, die höchstens doppelt so viele Auslagerungs-Operationen durchführen wie ein Algorithmus, der die Eingabe bereits im Voraus kennt). Insbesondere werden Sie in diesem Proseminar diverse Techniken und Strategien zum Entwurf und zur Analyse entsprechender Algorithmen kennenlernen. Darüber hinaus beschäftigen wir uns mit der Komplexitätstheorie von Optimierungsproblemen und deren Approximierbarkeit, welche die aus der GTI-Vorlesung bekannte Theorie NP-vollständiger Probleme erweitert.

Die Vortragsthemen basieren auf Teilen der Lehrbücher Complexity and Approximation von Ausiello et al. und Online Computation and Competitive Analysis von Borodin und El-Yaniv. Abhängig von der Teilnehmerzahl könnten auch noch weitere Quellen in Frage kommen.

Als Voraussetzung für die Teilnahme an diesem Proseminar sind solide algorithmische Grundkenntnisse notwendig, wie sie in der Veranstaltung DAP2 vermittelt werden. Kenntnisse zur Theorie NP-vollständiger Probleme sind für viele Themen hilfreich. Einige Themen erfordern darüber hinaus grundlegende Kenntnisse der Wahrscheinlichkeitsrechnung.

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
Veranstaltungsnummer  
Veranstalter Martin Schuster
Klassifikation Proseminar
Semester Wintersemester 2014/15
Ort und Zeit  
Vorbesprechung 22.7.14 OH12 3.013
Querverbindungen DAP 2, GTI
Voraussetzungen DAP 2, GTI

Um Optimierungsprobleme zu lösen, wünscht man sich üblicherweise einen Algorithmus, der zu einer gegebenen Probleminstanz in möglichst geringer Laufzeit eine optimale Lösung erzeugt. Bedauerlicherweise ist es nicht immer möglich, gleichzeitig eine geringe Laufzeit und eine optimale Lösung zu garantieren. Wir beschäftigen uns in diesem Proseminar also mit Algorithmen, die zwar effizient sind (also höchstens polynomielle Laufzeit benötigen), allerdings nur eine näherungsweise optimale Lösung erzeugen. Dabei betrachten wir zwei verschiedene Sorten von Optimierungsproblemen, die jeweils auf ihre eigene Weise "zu schwierig" sind, um sie effizient exakt zu lösen.

  • Optimierungsprobleme, deren zugehörige Entscheidungsprobleme NP-schwierig sind, lassen sich (vermutlich) nicht effizient lösen. Da diese Probleme in der Praxis dennoch gelegentlich auftauchen, beschäftigen wir uns mit Approximationsalgorithmen, die in polynomieller Zeit eine "hinreichend gute" Lösung liefern sollen.
  • Speziell bei maschinennahen Optimierungsproblemen wie dem Paging-Problem, also der Frage, wann Speicherseiten aus einem schnellen, aber kleinen Speicher in einen großen, dafür langsamen Speicher ausgelagert werden sollen, kommt es öfters vor, dass die Eingabeinstanz (im Beispiel: eine Folge von Speicherzugriffen) nicht im Voraus bekannt ist sondern erst zur Laufzeit des Algorithmus Stück für Stück bekannt gegeben wird. Zu dieser Art von Problemen betrachten wir Online-Algorithmen, die darauf ausgelegt sind,  eine solche "streaming-artige" Form der Eingabe möglichst gut zu verarbeiten.

In beiden Fällen betrachten wir Algorithmen, die ein gegebenes Problem nicht exakt lösen, allerdings gewisse Qualitätsgarantien erfüllen (wie z.B. Paging-Algorithmen, die höchstens doppelt so viele Auslagerungs-Operationen durchführen wie ein Algorithmus, der die Eingabe bereits im Voraus kennt). Insbesondere werden Sie in diesem Proseminar diverse Techniken und Strategien zum Entwurf und zur Analyse entsprechender Algorithmen kennenlernen. Darüber hinaus beschäftigen wir uns mit der Komplexitätstheorie von Optimierungsproblemen und deren Approximierbarkeit, welche die aus der GTI-Vorlesung bekannte Theorie NP-vollständiger Probleme erweitert.

Die Vortragsthemen basieren auf Teilen der Lehrbücher Complexity and Approximation von Ausiello et al. und Online Computation and Competitive Analysis von Borodin und El-Yaniv. Abhängig von der Teilnehmerzahl könnten auch noch weitere Quellen in Frage kommen.

Als Voraussetzung für die Teilnahme an diesem Proseminar sind solide algorithmische Grundkenntnisse sowie ein gutes Verständnis für die Theorie NP-vollständiger Probleme notwendig. Einige Themen erfordern darüber hinaus grundlegende Kenntnisse der Wahrscheinlichkeitsrechnung.

22.7.14 14:00-15:00 OH12 3.013 Vorbesprechung und Themenvorstellung
29.7.14 14:15-15:45 OH16 205 Präsentationskurs: Schreiben
6.8.14 14:15-15:45 OH16 205 Präsentationskurs: Schreiben
29.9.14 14:15-15:45 OH12 3.031 Präsentationskurs: Vortragen
7.10.14 8:15-9:45 OH12 3.031 Präsentationskurs: Vortragen
27.10.14 12:00   Abgabe Exposé
11.11.14 8:30-10:00 OH12 3.031 Kurzvorträge A2, A3, A5 (Folienplan bis 31.10.14 12:00 Uhr)
18.11.14 8:30-10:00 OH12 3.031 Kurzvorträge A4, B6-B9 (Folienplan bis 7.11.14 12:00 Uhr)
25.11.14 8:30-10:00  OH12 3.031 Kurzvorträge C10-C12 (Folienplan bis 14.11.14 12:00 Uhr)
2.12.14 8:30-10:00  OH12 3.031 Kurzvorträge C13-C17 (Folienplan bis 21.11.14 12:00 Uhr)
22.12.14 12:00   Abgabe Ausarbeitung
9.2.15 8:30-17:00 OH12 3.031 Langvorträge A2-A5, B6-B9
17.2.15 8:30-17:00 OH12 3.031 Langvorträge C10-C17

 Hier finden Sie eine Übersicht über die angebotenen Themen des Proseminars. Weitere Themen sind auf Absprache möglich.

  Montag, 9.2.15

8:30-10:30 Vorträge A2, A3
10:30-11:00 Pause
11:00-13:00 Vorträge A4, A5
13:00-14:00 Mittagspause
14:00-17:00 Vorträge B6, B8, B9

  Dienstag, 17.2.15

8:30-11:30 Vorträge C10, C11, C12
11:30-12:30 Mittagspause
12:30-14:30 Vorträge C13, C15
14:30-15:00 Pause
15:00-17:00 Vorträge C16, C17