Spektren von Verhaltensdistanzen und quantitativen Logiken

• Antragstellerinnen / Antragsteller: Professorin Dr. Barbara König; Professor Dr. Lutz Schröder
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 434050016

Ein zentrales Problem der Systemanalyse ist der Vergleich von Zuständen bezüglich ihres beobachtbaren Verhaltens. Während man sich bei solchen Vergleichen in klassischen Ansätzen oft auf Ja/Nein-Antworten beschränkt, beispielsweise hinsichtlich Bisimularität oder Sprachinklusion, ist es bei Systemen mit quantitativen Aspekten - wie Wahrscheinlichkeiten oder Transitionsgewichten - in vielen Fällen angemessener, Verhaltensabstände zu messen. Wie bei zweiwertigen Vergleichen gibt es bei Verhaltensabständen ein Spektrum von Granularitäten, das vom verzweigenden Zeitbegriff bis zum linearen Zeitbegriff (Branching Time bzw. Linear Time) reicht. Ziel des Projektes SpeQt ist, mittels Parametrisierung entlang dreier orthogonaler Achsen eine einheitliche semantische, logische und algorithmische Behandlung einer Vielzahl von unterschiedlichen Verhaltensabständen bereitzustellen: Wir beschreiben den Systemtyp gemäß dem Paradigma der universellen Koalgebra als einen Funktor auf einer geeigneten Basiskategorie; wir erfassen die Granularität von Verhaltensäquivalenzen und -abständen mittels Galoisverbindungen und des in jüngeren Arbeiten entwickelten universell-algebraischen Instruments der gradierten Monaden; und wir arbeiten mit quantalwertigen Verhaltensabständen, wodurch insbesondere per Instanziierung auf das Boolesche Quantal bzw. das Einheitsintervallquantal der zweiwertige und der quantitative Fall einheitlich abgedeckt werden. Die beabsichtigten Projektergebnisse beinhalten insbesondere die Identifikation von expressiven quantitativen Modallogiken in Verallgemeinerung des klassischen Hennessy-Milner-Theorems sowie spieltheoretische Charakterisierungen von Verhaltensabständen. Im gesamten Projekt streben wir an, nicht nur existierende Resultate zu vereinheitlichen, sondern gerade auch durch Instanziierung unserer allgemeinen Resultate neue Ergebnisse für konkrete Abstände und Systemtypen zu erhalten. In der zweiten Projektphase SpeQt2 werden wir verstärktes Gewicht auf die algorithmische Behandlung von Verhaltensabständen legen; dies betrifft sowohl die Berechnung von Abständen als solchen als auch die von Zeugen für solche Abstände, wie etwa von quantitativen Bisimulationen, Gewinnstrategien in quantitativen Spielen oder unterscheidenden Formeln. Besondere Aufmerksamkeit gilt ferner approximativen Ansätzen, beispielsweise der Definition und Berechnung von Verhaltensabständen in Systemen, in denen Werte nur geschätzt werden können und daher mit Unsicherheit behaftet sind, sowie der Entwicklung von Verhaltensabständen, die auf approximativen Varianten von Transportproblemen beruhen.

• DFG-Verfahren: Sachbeihilfen