Koalgebraische Nominale Automaten mit Namensallozierung

• Antragsteller: Professor Dr. Stefan Milius; Professor Dr. Lutz Schröder
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 517924115

Jenseits klassischer formaler Sprachen über endlichen Alphabeten besteht in jüngerer Zeit wachsendes Interesse an Sprachen über unendlichen Alphabeten, die als Abstraktionen unendlicher Datentypen wie Zahlen oder Strings verwendet werden. Es gibt mittlerweile eine große Bandbreite an Formalismen für Datensprachen in diesem Sinne, die der Spezifikation und Verifikation von Anforderungen an Strukturen und Prozesse dienen, die Daten beinhalten oder austauschen, wie etwa XML-Dokumente, kryptographische Protokolle oder dynamisch konfigurierte parallele Prozesse. Viele dieser Formalismen verwenden Register, in denen aus einem Datenwort gelesene Datenwerte zum Vergleich mit später gelesenen Datenwerten gespeichert werden können. Solche Registerautomaten haben sich als äquivalent zu in neueren Arbeiten identifizierten Begriffen von nominalen Automaten erwiesen, die durch Uminterpretation der üblichen Definition von endlichen Automaten über nominalen Mengen, also Mengen mit Atomen (`Namen'), entstehen. Eine in Formalismen für Datensprachen häufig angetroffene Herausforderung liegt darin, dass zentrale Analyseprobleme, insbesondere das Sprachinklusionsproblem, in Abwesenheit radikaler Beschränkungen entweder der Berechnungsstärke (z.B. auf deterministische oder eindeutige Modelle) oder der Zahl der Register von nichtelementarer Komplexität oder sogar unentscheidbar sind. In unseren Vorarbeiten haben wir ein Prinzip identifiziert, das im Tausch gegen eine mäßige Reduktion der Ausdrucksstärke deutlich verbesserte Komplexität ermöglicht: Namenallozierende Automatenmodelle für endliche oder unendliche Wörter, in denen die Frische von Datenwerten (d.h. Distinktheit von vorherigen Werten) in einem nominalen Formalismus mittels alpha-Äquivalenz, also durch Umbenennung gebundener Namen, modelliert wird, erlauben Sprachinklusionsprüfung in moderater (insbesondere elementarer) Komplexität bei vergleichsweise hoher Ausdrucksstärke, insbesondere bei vollem Nichtdeterminismus (z.B. können namensallozierende Automaten somit die mit deterministischen oder eindeutigen Registerautomaten nicht akzeptierbare Sprache `mindestens ein Datenwert kommt zweimal vor' akzeptieren) und ohne Beschränkung der Registeranzahl. Gegenstand des Projekts CoNAN ist eine größer angelegte Entwicklung der Algorithmik und Metatheorie der namenallozierenden Automaten sowohl in der Breite als auch in der Tiefe. Forschungsziele sind unter anderem der Entwurf namenallozierender Temporallogiken, die Entwicklung algebraischer und spieltheoretischer Methoden zur Analyse der Algorithmik und Ausdruckstärke namenallozierender Logiken und Automatenmodelle, und die Erweiterung des Rahmenwerks auf Automatenmodelle mit zusätzlichen Ausdrucksmitteln wie Namensdeallokation und über Nichtdeterminismus hinausgehenden Verzweigungstypen; auf diese Weise soll ein umfassender Satz an Analysemethoden und Algorithmen für ein breites Spektrum von Datensprachen bereitgestellt werden.

• DFG-Verfahren: Sachbeihilfen