Allgemeines

Inhalt

Ist eine gegebene aussagenlogische Formel erfüllbar? Mit dieser Frage beschäftigt sich das SAT-Problem, welches eines der zentralen Entscheidungsprobleme der theoretischen Informatik ist.
Da dieses Problem NP-vollständig ist (Satz von Cook und Levin), ist insbesondere unklar, ob es Algorithmen gibt, die das Problem in polynomieller Zeit lösen können.
Das SAT-Problem ist auch in der Praxis von großer Bedeutung, da es in vielen Bereichen der Informatik, beispielsweise in der Soft- und Hardwareverifikation, in der künstlichen Intelligenz und in verschiedenen Schedulingalgorithmen, Anwendungen hat.
Aus diesem Grund ist es von besonderem Interesse, möglichst effiziente Algorithmen (sog. SAT-Solver) zu konstruieren, die das SAT-Problem mit akzeptabler Laufzeit lösen.

In diesem Proseminar betrachten wir SAT-Solver sowohl aus der theoretischen als auch aus der algorithmischen Sichtweise.

Für die Teilnahme an dem Proseminar sind ein solider Umgang mit mathematischer Notation sowie algorithmische Grundkenntnisse, wie sie in DAP2 vermittelt werden, notwendig.

Die Vortragsthemen basieren auf Teilen der Buches Handbook of Satisfiability von Biere et. al. . Es können auch weitere Quellen infrage kommen.

Allgemeines

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

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

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

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.

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

Read more ...