Ausdrucksstarke Automaten mit Zählfunktion

Projekttitel: Ausdrucksstarke Automaten mit Zählfunktion

Projektdauer: 3 Jahre

Forschungsbereich: Wissensrepräsentation und Wissensmodellierung

Endliche Automaten gehören zu den grundlegendsten Formalismen der theoretischen Informatik. Sie haben sich in vielen Bereichen als nützliches Werkzeug erwiesen, beispielsweise bei der formalen Verifikation oder als Mittel zum Nachweis der Entscheidbarkeit ausdrucksstarker Logiken, die zur Wissensrepräsentation eingesetzt werden. Insbesondere in den genannten Bereichen ist es wünschenswert, Situationen zu modellieren, die über die Regelmäßigkeit hinausgehen. Es gibt eine lange Tradition, endliche Automaten um Zählmechanismen zu erweitern, mit dem Ziel, Rechenmodelle zu erhalten, die sowohl ausdrucksstark sind als auch die Entscheidbarkeit relevanter Probleme gewährleisten. Für den Fall von Wörtern gibt es mittlerweile eine Fülle gut erforschter Modelle wie Pushdown-Automaten, Ein-Zähler-Automaten oder Parikh-Automaten. Für den Fall endlicher und unendlicher baumartiger Strukturen, die zur Beschreibung paralleler Prozesse oder zur Kodierung baumartiger Modelle logischer Formalismen verwendet werden, ist es jedoch von Interesse, die rechnerischen Eigenschaften ausdrucksstarker Baumautomatenmodelle besser zu verstehen.

Ziele

Ziel des Forschungsprojekts ist es, zu untersuchen, wie Baumautomaten durch Zählmechanismen erweitert werden können, um globale und lokale Eigenschaften von Bäumen zu prüfen. Ein Schwerpunkt liegt auf Modellen, mit denen sich die Entscheidbarkeit ausdrucksstarker Logiken nachweisen lässt. Ein Beispiel hierfür sind Parikh-Baumautomaten, deren Ausdruckskraft der eines Fragments der monadischen Logik zweiter Ordnung mit Kardinalitätsbeschränkungen über (unendlichen) Bäumen entspricht.

Problemstellung

Wir beabsichtigen, verschiedene Baumautomaten mit Zählmechanismen theoretisch zu untersuchen und sie im Kontext bestehender Ergebnisse einzuordnen. Zu den typischen Fragestellungen gehören:

• In welchem Verhältnis steht die Ausdruckskraft der verschiedenen Modelle zueinander?
• Welche Schließungseigenschaften gelten?
• Sind wichtige Probleme wie Leere und Zugehörigkeit entscheidbar?
• Gibt es logische Charakterisierungen?

Technologie

Wir verwenden Methoden und Beweistechniken aus verschiedenen Bereichen der theoretischen Informatik und erweitern oder passen sie an unseren Kontext an. Dazu gehören gängige Automatenkonstruktionen oder Reduktionen anderer Probleme.

Ausblick

Wir sind der Ansicht, dass die Ergebnisse dieses Projekts sowohl die theoretischen Grundlagen als auch konkrete Methoden liefern, um Entscheidbarkeits- und Komplexitätsergebnisse für Formalismen aus verschiedenen Bereichen der Informatik, wie beispielsweise der Wissensrepräsentation oder der Verifikation, zu ermitteln.

Publikationen

• Luisa Herrmann, Vincent Peth, and Sebastian Rudolph. Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Team

Teamleitung

• Prof. Dr. Sebastian Rudolph

Teamitglieder

• Dr. Luisa Herrmann