Algorithmische Theorie der Baumautomaten

• Applicant: Privatdozent Dr. Christof Löding
• Subject Area: Theoretical Computer Science
• Term: from 2005 to 2011
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5445837

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 semistrukturierter Daten (XML) B¨aume mit unbeschr¨anktem Verzweigungsgrad (”unranked trees“) berücksichtigt werden. 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. Hier verfolgen wir die Methode, Mengen erreichbarer Zustände durch Baumautomaten über unbeschränkt verzweigten Bäumen zu beschreiben (und auch effektiv zu berechnen).

• DFG Programme: Research Grants
• Participating Person: Professor Dr. Wolfgang Thomas