Dependence and Independence, Quantitative Aspects and Counting Constructs in Logic and Games
Final Report Abstract
Logiken fur Abhängigkeit, Unabhängigkeit, und imperfekte Information, auf der Basis der von Hodges eingeführten Teamsemantik wurden in den letzten zehn Jahren erfolgreich als interdisziplinäres Arbeitsgebiet etabliert. Die Bedeutung der Informatik und das Interesse an algorithmischen und anderen informatikrelevanten Fragestellungen hat dabei in den letzten Jahren stetig zugenommen. Die Teamsemantik liefert einen Ansatz, um logische Formeln auf viel größeren Datenmengen als bisher auszuwerten, ausgehend von der Idee, nicht einzelne Bewertungen der Variablen fur die Auswertung heranzuziehen, sondern von vornherein mit beliebig großen Mengen von solchen Bewertungen zu arbeiten. Solche Mengen von Bewertungen (mit einer gemeinsamen Variablenmenge und einem gemeinsamen Wertebereich) werden heute Teams genannt. Teamsemantik führt zu hoher Ausdrucksstärke der behandelten Logiken. Ausserdem beruhen diese Logiken auf dem Vorschlag von Vääanänen, Abhängigkeit und Unabhängigkeit als atomare Eigenschaften von Teams zu sehen. In diesem Forschungsvorhaben wurden diese Logiken in verschiedener Hinsicht erweitert, und mit modelltheoretischen Methoden und spieltheoretischen Konstruktionen untersucht. Die neuen Konzepte umfassen z.B. verschiedene Zählkonstruktionen, Abhängigkeiten bis auf Äquivalenz, bewachte Teams und bewachte Bisimulationen, myopische Formeln und neue teamsemantische Atome. Ein zweites Hauptziel des Vorhabens war die Erweiterung der Methodologie zur Synthese und Verifikation reaktiver Systeme, auf der Basis der Kombination von Logik, Automatentheorie und der Theorie endlicher und unendlicher Spiele, durch die Integration neuer quantitativer Aspekte. Aufgrund unterschiedlicher Anforderungen in verschiedensten Anwendungen gibt es sehr viele verschiedene Varianten von quantitativen Komponenten in Logiken, Automaten und Spielen. Die hier untersuchten Erweiterungen betreffen Relationen, welche mit Kosteninterpretationen bewertet sind, synchron arbeitende Cost-Transducers als wichtige automatentheoretisches Werkzeug, ressourcen-automatische Strukturen, Logiken mit Ressourcen-Relationen und Erweiterungen der monadischen Logik um Zählkonstruktionen, Kostenfunktionen und neue Mengen-Quantoren. In beiden Teilen des Vorhabens spielten neue spieltheoretische Konstruktionen eine zentrale Rolle. Diese umfassen u.a. Threshold-Spiele, Fallenkonstruktionen in Sicherheitsspielen, Inklusions-Exklusions-Spiele, Übersetzungen zwischen Spielen auf der Basis logischer Interpretationen, sowie quantitative Erweiterungen von Paritäts- und Mean-Payoff-Spielen. Insgesamt ist es in dem Vorhaben gelungen, mit neuen und innovativen spieltheoretischen Konzepten das Verständnis von Abhängigkeits- und Unabhängigkeitslogiken wesentlich zu verbessern und die auf der Kombination von Logik, Automatentheorie und Spiele beruhenden Methodik zur Analyse reaktiver System zu erweitern und zu vertiefen.
Publications
- Counting in Team Semantics. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), vol. 62 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 35:1–35:18, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2016
E. Grädel and S. Hegselmann
(See online at https://doi.org/10.4230/LIPIcs.CSL.2016.35) - Counting Logics and Games with Counters, Doctoral Dissertation, RWTH Aachen University, 2016
S. Lessenich
- Games for Inclusion Logic and Fixed-Point Logic. In Dependence Logic: Theory and Applications (S. Abramsky et al., Eds.), pp. 73–98. Birkhäuser, 2016
E. Grädel
(See online at https://doi.org/10.1007/978-3-319-31803-5_5) - Dependency Concepts up to Equivalence. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), vol. 119 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 25:1–25:21, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2018
E. Grädel and M. Hoelzel
(See online at https://doi.org/10.4230/LIPIcs.CSL.2018.25) - Fragments of Existential Second-Order Logic and Logics with Team Semantics, Doctoral Dissertation, RWTH Aachen University, 2019
M. Hoelzel
(See online at https://doi.org/10.18154/RWTH-2020-05121) - Guarded Teams. The Horizontally Guarded Case, Proceedings of CSL 2020
E. Grädel and M. Otto
(See online at https://doi.org/10.4230/LIPIcs.CSL.2020.22) - On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics. Proceedings of CSL 2020
M. Hoelzel and R. Wilke
(See online at https://doi.org/10.4230/LIPIcs.CSL.2020.25)
