Algorithmische Theorie der Baumautomaten

点击翻译按钮获取中文摘要

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).