Temporale Logiken über endlichen Wörtern und der Präfixordnung

• Antragstellerin: Dr. Karin Quaas
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 504343613

Temporale Logiken gehören zu den wichtigsten logischen Formalismen, mit denen sich abstrakte Eigenschaften ausdrücken lassen. Zu den prominentesten Beispielen zählen LTL, CTL und CTL*. Ein Nachteil dieser Logiken ist, dass sie sich nicht dazu eignen, Eigenschaften mit Bezug auf konkrete Datenwerte zu beschreiben. Um dem Abhilfe zu verschaffen, wurden in jüngster Zeit viele Erweiterungen von temporalen Logiken vorgeschlagen und studiert. In diesem Projekt betrachten wir temporale Logiken mit Constraints, welche über sogenannten konkreten Domänen definiert sind. Eine konkrete Domäne besteht aus einer Datenmenge und einer Menge von Relationssymbolen, welche über der Datenmenge interpretiert werden. Typische Beispiele von konkrete Domänen sind (N;=) - die natürlichen Zahlen mit Gleichheit - und (R;<) - die reellen Zahlen mit der Ordnungsrelation. Es wurden bereits viele interessante Resultate für temporale Logiken mit Constraints erzielt. Das dabei meist untersuchteste Problem ist das Erfüllbarkeitsproblem, also die Frage, ob für eine gegebene Formel ein Modell existiert. Während dieses Problem für die klassischen temporalen Logiken entscheidbar ist (PSPACE-vollständig für LTL, 2EXPTIME-vollständig für CTL*), hängt die Komplexität für temporale Logiken mit Constraints offensichtlich von der konkreten Domäne ab. So ist z.B. das Problem für (N;+) unentscheidbar, aber PSPACE-vollständig für LTL über linearen Ordnungen. Der Ausgangspunkt für dieses Projekt ist die konkrete Domäne der Präfixordnung über der Menge der endlichen Wörter über einem Alphabet. Diese ist interessant aus praktischer Sicht, mit vielen möglichen Anwendungen z.B. in Datenbanken oder der Bioinformatik. Aber auch aus theoretischer Sicht stellt die Präfixordnung einen interessanten Fall dar: sie ist eine partielle Ordnung, und Standardmethoden für lineare Ordnungen sind nicht einfach auf sie anwendbar. Sie stimmt mit der Vorgängerrelation über vollständigen Bäumen überein, und die monadische Logik zweiter Ordnung über dieser konkreten Domäne ist entscheidbar. Auch wurde bereits für alle oben genannten temporale Logiken bewiesen, dass das Erfüllbarkeitsproblem entscheidbar ist, und PSPACE-vollständig für LTL. Diese Resultate wurden mittels verschiedener interessanter Techniken bewiesen, inklusive einer Enkodierung der konkreten Domäne in (N;<) und Methoden aus der Theorie der Wohlquasiordnungen und Modelltheorie. Wir beabsichten in diesem Projekt, diese Techniken weiterzuentwickeln. Konkret wollen wir, unter anderem, die präzise Komplexität des Erfüllbarkeitsproblems für verzweigende temporale Logiken und die Entscheidbarkeit für temporale Logiken über konkreten Domänen, die neben der Präfixrelation auch andere Relationen enthalten (z.B. Regularitätsprädikate, Suffix) bestimmen. Neben dem Ziel, ausdrucksstärkere Logiken für realistische Anwendungen zur Verfügung stellen zu können, wollen wir damit auch ein tieferes Verständnis über temporale Logiken mit Constraints erwerben.

• DFG-Verfahren: Sachbeihilfen