Provenienzanalyse für Logik und Spiele

• Antragsteller: Professor Dr. Erich Grädel
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 434376062

Provenienzanalyse und Halbringsemantik beruhen auf der Idee, logische Formeln nicht nur durch wahr oder falsch, sondern durch Elemente eines kommutativen Halbrings zu bewerten. Die klassische Semantik erscheint in diesem Kontext als der durch den booleschen Halbring gegebene Speziallfall. Andere wichtige Halbringe liefern zusätzliche Informationen, z.B. für Kostenberechnungen, für das Zählen von Auswertungsstrategien und Beweisen, für Zugangsberechtigungen und Sicherheitsanalysen usw. Eine besondere Rolle spielen Provenienz-Halbringe von Polynomen oder formalen Potenzreihen. Als Halbringe mit universellen Eigenschaften (im algebraischen Sinn) liefern sie allgemeinste Provenienzbewertungen. Insbesondere erlauben Provenienz-Halbringe das Tracken atomarer Fakten und damit genaue Einsichten, welche Kombinationen von atomaren Fakten eine komplexe Formel implizieren, und wie oft diese in der Auswertung verwendet werden. Die Provenienzanalyse wird für positive Datenbanksprachen seit mehr als 15 Jahren erfolgreich angewandt. Das Ziel unseres Vorhabens ist die systematische Erweiterung und Vertiefung der Provenienzanalyse und Halbringsemantik auf ein breites Spektrum logischer Formalismen, welche in verschiedenen Gebieten der Informatik wichtig sind, und andererseits auf Klassen von endlichen und unendlichen Spielen. Damit sollen auch neue Anwendungsgebiete für die Provenienzanalyse erschlossen werden. Wichtige Ausgangspunkte waren unser neuer Zugang zur Behandlung der Negation in Polynom-Halbringen mit dualen Unbekannten, und die Zusammenhänge von Halbringsemantik mit der Theorie endlicher und unendlicher Spiele. In der ersten Projektphase wurden wesentliche Fortschritte im Hinblick auf diese Zielsetzungen gemacht und das Gebiet der Provenienzanalyse deutlich vorangebracht. Algebraische, logische und spieltheoretische Grundlagen der Halbringsemantik sind nun wesentlich besser verstanden. Geeignete Halbringe für Fixpunktberechnungen wurden identifiziert und eine adäquate Halbringsemantik für Fixpunktlogiken mit Negation und Verschachtelungen von kleinsten und größten Fixpunkten wurde gefunden, inklusive ihrer algorithmischen Auswertungen und der zugehörigen Model-Checking-Spiele. Einige wichtige modelltheoretische Grundlagen der Halbringsemantik konnten geklärt werden. Die Provenienzanalyse konnte auch als neue Methode zur Strategieanalyse von Spielen etabliert werden, es wurden Sum-of-Strategies-Theoreme für verschiedene Klassen von Spielen bewiesen, und die Tragfähigkeit dieser Methode durch eine ausführliche Fallanalyse für Büchi-Spiele illustriert. In der zweiten Projektphase wollen wir unsere Resultate in mehrere Richtungen ausweiten und Lücken der Theorie schließen. Dies umfasst logische, algorithmische und spieltheoretische Fragen, sowie Anwendungen z.B. im Bereich Fehlerkorrektur und logische Lerntheorie. Ziel ist es, bis zum Abschluss dieses Projekts die Provenienzanalyse und Halbringsemantik zu einer ausgereiften Theorie zu machen.

• DFG-Verfahren: Sachbeihilfen