Koalgebraische Deduktionssysteme für quantitative Systemanalyse

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

Die Modallogik dient als Formalismus für die Beschreibung von Systemen, die Wechselbeziehungen zwischen Knotenpunkten, zu verstehen z.B. als Zustände, Welten oder Individuen, abbilden. Ihre Anwendungsgebiete reichen von der Nebenläufigkeit über Agentensysteme bis zur Wissensrepäsentation. Quantitative Modallogiken weichen vom üblichen zweiwertigen Ansatz ab, indem sie über Wahrheitswertebereichen interpretiert werden, die Wahrheitsgrade zwischen vollständiger Wahrheit und vollständiger Falschheit zulassen. Ein typisches Beispiel für einen solchen Wertebereich ist das reelle Einheitsintervall. Wahrheitswerte in diesem Bereich können z.B. als Zuschreibung vager Eigenschaften im Sinne der Fuzzy-Logik gelesen werden, wie etwa 'Person X ist groß'. Reelle Wahrheitswerte treten jedoch auch in anderen Zusammenhängen auf, z.B. in probabilistischen Systemen oder in Transitionssystemen, in denen Zustände oder Transitionen Label aus einem metrischen Raum tragen. Eine geeignete Abstraktion von allgemeineren Wahrheitsdomänen, die eine Messung der Abweichung zwischen Wahrheitswerten erlauben, findet sich im Begriff des Quantals. Das Ziel von CoRSA ist es, automatische Schlussfolgerungsmechanismen für quantitative Modallogiken in diesem Sinne zur Verfügung zu stellen, wobei wir Generizität der entsprechenden Algorithmen sowohl über dem Systemtyp (probabilistisch, spielbasiert, metrisch usw.) als auch über der Semantik der Modalitäten anstreben, die ihrerseits von unscharfen relationalen Modalitäten des Typs 'es gibt einen Nachfolger / für alle Nachfolger' über erwartungswertbasierte probabilistische Modalitäten des Typs 'wahrscheinlich' bis hin zu spielbasierten Modalitäten des Typs `eine Koalition von Agenten kann eine quantitative Eigenschaft erzwingen' reichen. Zu diesem Zweck werden wir im Rahmenwerk der universellen Koalgebra und der koalgebraischen Logik arbeiten, die kategorielle Abstraktionen für den Systemtyp und die Modalitäten bereitstellen. Aus Arbeiten über automatisches Schlussfolgern in Fuzzy-Beschreibungslogiken ist bekannt, dass die Berechenbarkeitseigenschaften quantitativer modaler Logiken stark von der Wahl der aussagenlogischen Konnektive abhängen, bis hin zur Unentscheidbarkeit von Schlussfolgerungsproblemen. Die Bestimmung eines geeigneten Satzes von aussagenlogischen Konnektiven ist daher ein wichtiger Gegenstand des Projekts; neuere Arbeiten über die Verbindung zwischen quantitativen Modallogiken und Verhaltensdistanzen legen nahe, dass ein Gleichgewicht zwischen Ausdrucksmächtigkeit und vertretbarer Komplexität durch Fokussierung auf nicht-expansive (d.h. nicht abstandsvergrößernde) aussagenlogische Konnektive gefunden werden kann. Wir zielen somit darauf ab, einen generischen Rahmen für quantitative Modallogiken zu schaffen, der sich durch Nähe zu semantischen Verhaltensabstandsbegriffen auszeichnet und automatische Deduktion in angemessener Komplexität unterstützt.

• DFG-Verfahren: Sachbeihilfen