Temporale Logiken mit Constraints

• Antragstellerin: Dr. Karin Quaas
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2018 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 406907430

Temporale Logiken sind logische Sprachen, die sich zur Spezifikation von abstrakten Systemen eignen. Bekannte temporale Logiken sind LTL (welche von einer linearen Abfolge von Zeitpunkten ausgeht) sowie CTL und CTL* (welche verzweigende Zeitfolgen beschreiben). Mit dem Ziel, mehr als nur abstrakte Eigenschaften ausdrücken zu können, wurden in der jüngeren Vergangenheit zahlreiche Erweiterungen dieser Logiken vorgestellt. Temporale Logiken mit lokalen Constraints entsprechen klassischen temporalen Logiken, in denen die atomaren Propositionen durch Constraints über einer konkreten Domäne ersetzt werden. Solche Constraints erlauben es, Beziehungen zwischen den Datenwerten von endlich vielen Variablen an lokal begrenzten Positionen eines Wortes auszudrücken. Im Gegensatz dazu kann man mit temporalen Logiken mit globalen Constraints Bedingungen über die Datenwerte an a priori unbegrenzten Positionen innerhalb eines Wortes ausdrücken. Um dies zu ermöglichen, werden klassische temporale Logiken wie LTL mit verschiedenen syntaktischen Werkzeugen ausgestattet; z.B. werden in der Logik MTL die temporalen Operatoren mit zeitlichen Constraints annotiert, und die Logik Freeze LTL verwendet einen sogenannten Freeze Operator, mit Hilfe dessen die Werte für spätere Vergleiche in Registervariablen gespeichert werden können. Beide Arten von temporalen Logiken mit Constraints sind im Fokus aktueller Forschungsarbeit im Bereich der formalen Verifikation. Für die zwei wichtigsten Forschungsprobleme, das Erfüllbarkeitsproblem und das Model-Checking-Problem, wurden erst kürzlich bemerkenswerte neue Resultate erzielt, in einigen Fällen mit Hilfe innovativer vielversprechender neuer Methoden. Das Ziel unseres Projektes ist es, diese und andere Methoden weiterzuentwickeln, um ein tiefgründigeres Verständnis über die Entscheidbarkeit und Komplexität temporaler Logiken mit Constraints zu erlangen. Unser Arbeitsprogramm gliedert sich in drei Hauptstränge: temporale Logiken mit (i) lokalen Constraints, (ii) globalen Constraints, sowie (iii) lokalen und globalen Constraints. Für (i) ist die wichtigste Frage für welche konkreten Domänen die Logik ein entscheidbares Erfüllbarkeitsproblem besitzt. Wir planen hier, das volle Potenzial von kürzlich vorgestellten Methoden zu studieren. Für Logiken mit entscheidbarem Erfüllbarkeitsproblem wollen wir die Komplexität untersuchen. Weiterhin interessiert uns die Frage, ob sich Methoden aus dem Bereich der Constraint Satisfaction Problems auf unsere Problemstellungen anwenden lassen können. Für (ii) legen wir das Hauptaugenmerk auf Datenwörtern über natürlichen Zahlen und Fragmenten von MTL und Freeze LTL, für welche im Bereich der Echtzeitverifikation vielversprechende Ergebnisse erzielt wurden. In der letzten Phase des Projektes planen wir für (iii) die bisher erlangten Ergebnisse zu kombinieren und lokale und globale Constraints zu integrieren. Überdies wollen wir parametrisierte Versionen der behandelten Logiken betrachten.

• DFG-Verfahren: Sachbeihilfen