Algorithmische Theorie der Baumautomaten

Projektbeschreibung

Förderung

Dieses Projekt wird durch eine Sachbeihilfe von der Deutschen Forschungsgemeinschaft (DFG) gefördert.

Mitarbeiter

Zeitraum

  • Dauer: Zwei Jahre
  • Projektstart: Mai 2005

Inhalt

Die Theorie der (endlichen) Baumautomaten ist Grundlage für die Beschreibung und Lösung vieler algorithmischer Probleme in so unterschiedlichen Gebieten wie Termersetzung, Type-Checking, Model-Checking und Datenbank-Anfragesprachen. In den letztgenannten Anwendungsbereichen stellte sich heraus, dass das klassische Modell des Baumautomaten modifiziert werden muss, um die gewünschten Anwendungen zu ermöglichen. So müssen im Kontext semistruktierter Daten (XML) Bäume mit unbeschränktem Verzweigungsgrad ("unranked trees") berücksichtigt werden, und es müssen (für die Modellierung von Anfrageoperationen) pfadorientiert arbeitende Automaten betrachtet werden (sog. "tree walking automata"), die längs der Baumkanten durch Bäume navigieren.

Eine handhabbare und algorithmisch nutzbare Grundlagentheorie dieser Modelle von Baumautomaten ist erst in Ansätzen vorhanden. Erstes Ziel unseres Vorhabens ist es, algorithmische Lösungen zur Synthese und Analyse dieser Automaten in allgemeinerer Form als bisher verfügbar zu entwickeln und ebenso eine klarere Vernetzung mit Logik-Formalismen zu erreichen.

Ein zweites Ziel besteht darin, neue Anwendungen in der algorithmischen Verifikation über unendlichen Zustandsräumen zu erschließen (mit Fallstudien zur formalen Analyse von Kryptoprotokollen). Hier verfolgen wir die Methode, Mengen erreichbarer Zustände durch Baumautomaten über unbeschränkt verzweigten Bäumen zu beschreiben (und auch effektiv zu berechnen).

Publikationen

2007

[Rad08a] Frank G. Radmacher. An automata theoretic approach to rational tree relations. In Proceedings of the 34th International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2008, volume 4910 of Lecture Notes in Computer Science, pages 424-435. Springer, 2008.
[KL07] Wong Karianto, Christof Löding. Unranked Tree Automata with Sibling Equalities and Disequalities. Proceedings of the 34th International Colloquium on Automata, Languages and Programming, ICALP 2007. Lecture Notes in Computer Science 4596, pages 875–887. Springer, 2006.
[LS07] Christof Löding, Alex Spelten. Transition Graphs of Rewriting Systems over Unranked Trees. In Proceedings of the 32nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2007., volume 4708 of Lecture Notes in Computer Science, pages 67-77. Springer 2007.
Eine Vorab-Version wurde bei der internationalen Konferenz AutoMathA 2007, Automata: from Mathematics to Applications, Palermo, Italy, 2007, akzeptiert.
[Rad07] Frank Radmacher. Automatendefinierbare Relationen über XML-Bäumen. Diplomarbeit, RWTH Aachen, März 2007.

2006

[BLS06] Vince Bárány, Christof Löding, and Olivier Serre. Regularity problems for visibly pushdown languages. Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006. Lecture Notes in Computer Science 3884, pages 420-431. Springer, 2006.
[Gro06] Benoît Groz. Counting over Unranked Trees. Praktikumsbericht, RWTH Aachen, August 2006.
[KKT06] Wong Karianto, Aloys Krieg, Wolfgang Thomas. On Intersection Problems for Polynomially Generated Sets. Proceedings of the 33rd International Colloquium on Automata, Languages and Programming, ICALP 2006, Part II. Lecture Notes in Computer Science 4052, pages 516–527. Springer, 2006.
[KL06] Wong Karianto, Christof Löding. Unranked Tree Automata with Sibling Equalities and Disequalities. Technical Report AIB-2006-13, RWTH Aachen, Oktober 2006.
[Spe06] Alex Spelten. Rewriting Systems over Unranked Trees. Diplomarbeit, RWTH Aachen, September 2006.

2005

[CLT05] Julien Cristau, Christof Löding, Wolfgang Thomas. Deterministic Automata on Unranked Trees. Proceedings of the 15th International Symposium on Fundamentals of Computation Theory, FCT 2005. Lecture Notes in Computer Science 3623, pages 68-79. Springer, 2005.
[Hin05] Gregor Hink. Pfadorientierte Automaten und Logiken über Bäumen. Diplomarbeit, RWTH Aachen, August 2005.

Aktivitäten

Diplomarbeiten

Abgeschlossene Diplomarbeiten