Dagstuhl Seminar 24111
Logics for Dependence and Independence: Expressivity and Complexity
( Mar 10 – Mar 15, 2024 )
Permalink
Organizers
- Juha Kontinen (University of Helsinki, FI)
- Jonni Virtema (University of Sheffield, GB)
- Heribert Vollmer (Leibniz Universität Hannover, DE)
- Fan Yang (Utrecht University, NL)
Contact
- Andreas Dolzmann (for scientific matters)
- Jutka Gasiorowski (for administrative matters)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
Dependence and independence are interdisciplinary notions that are pervasive in many areas of science. They appear in domains such as mathematics, computer science, statistics, quantum physics, and game theory. The systematic development of logical and semantical structures for these notions via the logics of dependence and independence has exposed surprising connections between these areas.
Logics for dependence and independence are new tools for modeling dependencies and interaction in dynamical scenarios. Reflecting this, these logics often have higher expressive power and complexity than classical logics used for these purposes previously. During the past decade, pioneering results on logics for dependence and independence has been disseminated in a spectrum of respected international conferences such as LICS, MFCS, JELIA, LPAR, CSL, AiML, and FSTTCS, and in top journals in the areas of logic and theoretical computer science. Although significant progress has been made in understanding the computational side of these novel logics (see Section 2 in the full report for some examples) still many central questions remain unsolved so far. In addition to addressing the open questions, the seminar also aims at boosting the exchange of ideas and techniques between team-based logics and the application areas.
The complexity and expressivity aspects of logics in propositional, modal and first-order team semantics have been studied extensively during the past decade. Recently, the complexity theoretic focus has turned to the (parameterized) complexity of logically defined counting and enumeration problems as well as algebraic complexity of probabilistic and real-valued logics. Furthermore, the expressivity and complexity of the novel temporal team logics are also not yet well understood.
Logics for real valued data and probabilistic reasoning
Algorithmically, first-order dependence and independence logic correspond exactly to the complexity class NP and to the existential fragment of second-order logic (ESO) while inclusion logic corresponds to the complexity class P over ordered finite structures. Recent discoveries on the connections between so-called probabilistic independence logic and logics on real valued data have revealed similar fundamental connections to a computation paradigm that uses real numbers as primitive entities (so-called BSS paradigm). These probabilistic logics have fascinating connections to the area of information theory via the notion of entropy, which can be adopted as a dependency in the probabilistic team semantics framework.
Applications to Hyperproperties and Formal Verification
An emerging area of applications for team semantics is the area of Hyperproperties. In the field of formal verification an execution of a system is modeled by a trace depicting the evolution of the system over discrete time. Traceproperties, ubiquitous in formal verification, are properties of systems that boil down to verifying that each trace of the system satisfies that property. Hyperproperties on the other hand are properties of systems that cannot be reduced to checking properties of individual execution traces of the system in isolation, but are instead properties of sets of traces. These properties are of vital importance in applications concerning security and information flow. A canonical example here is bounded termination; one cannot check whether there exists a uniform time bound for some action by checking computation traces in isolation. Other examples include security policies such as non-interference and secure information flow.
Applications to Formal Linguistics
Team semantics was also proven to be a fruitful tool for formal linguistics, especially for inquisitive semantics and the study of free choice inferences. Inquisitive semantics is a unified formal framework for analyzing both statements and questions in natural language. It is known that inquisitive logic essentially adopts team semantics and can thus be viewed as a variant of propositional dependence logic. This connection has already sparked a significant amount of interest and new research at the interface of the two fields. On a different line of research, recently a bilateral modal logic based on team semantics, called BSML, was developed to model free choice inferences in natural language, where an atom NE studied in the context of propositional team logics plays a central role. Very recent works have studied the logical properties of BSML, and promising broader applications of the team semantics method along this line are yet to be explored.
Dependence and independence are interdisciplinary notions that are pervasive in many areas of science. They appear in domains such as mathematics, computer science, statistics, quantum physics, and game theory. The systematic development of logical and semantical structures for these notions via the logics of dependence and independence has exposed surprising connections between these areas.
Logics for dependence and independence are new tools for modelling dependencies and interaction in dynamical scenarios. Reflecting this, these logics often have higher expressive power and complexity than classical logics used for these purposes previously. During the past decade, pioneering results on logics for dependence and independence have been disseminated in a spectrum of respected international conferences and in top journals in the areas of logic and theoretical computer science. Although significant progress has been made in understanding the computational side of these novel logics, many central questions remain unsolved.
In addition to addressing the open questions, this Dagstuhl Seminar aims at boosting the exchange of ideas and techniques between team-based logics and the following application areas.
Logics for Real Valued Data and Probabilistic Reasoning
Algorithmically, first-order dependence and independence logic correspond exactly to the complexity class NP and to the existential fragment of second-order logic while inclusion logic corresponds to the complexity class P over ordered finite structures. Recent discoveries on the connections between the so-called probabilistic independence logic and logics on real valued data have revealed similar fundamental connections to a computation paradigm that uses real numbers as primitive entities (so-called BSS paradigm). Possible connections to real-valued circuits might also hold. The framework of probabilistic team semantics has fascinating connections to the area of information theory via the notion of entropy (which can be adopted as a dependency in the framework), as well as offers a setting for probabilistic reasoning.
Applications to Hyperproperties and Formal Verification
An emerging area of applications for team semantics is the area of Hyperproperties. In the field of formal verification, an execution of a system is modelled by a trace depicting the evolution of the system over discrete time. Trace properties, ubiquitous in formal verification, are properties of systems that boil down to verifying that each trace of the system satisfies that property. Hyperproperties on the other hand are properties of systems that cannot be reduced to checking properties of individual execution traces of the system in isolation, but are instead properties of sets of traces. These properties are of vital importance in applications concerning security and information flow. A canonical example here is bounded termination; one cannot check whether there exists a uniform time bound for some action by checking computation traces in isolation. Other examples include security policies such as non-interference and secure information flow. The introduction of team semantics for linear temporal logic (TeamLTL) in 2018 opened up a new logical approach for the specification and study of hyperproperties. From there on different logics have been developed in this area and related to existing logical paradigms such as HyperLTL and its progeny.
Applications to Formal Linguistics
Team semantics was also proven to be a fruitful tool for Formal Linguistics, especially for inquisitive semantics and the study of free choice inferences. Inquisitive semantics is a unified formal framework for analysing both statements and questions in natural language.
Inquisitive logic essentially adopts team semantics and can thus be viewed as a variant of propositional dependence logic. This connection has already sparked a significant amount of interest and new research at the interface of the two fields. On a different line of research, recently, team semantics was used to model free choice inferences in natural language, resulting in a bilateral modal logic, where an atom NE studied in the context of team logics plays a central role. Some very recent work has provided preliminary studies of this approach, and promising broader applications of the team semantics method along this line are yet to be explored.
- Erika Abraham (RWTH Aachen, DE) [dblp]
- Maria Aloni (University of Amsterdam, NL)
- Aleksi Ilari Anttila (University of Amsterdam, NL)
- Christel Baier (TU Dresden, DE) [dblp]
- Fausto Barbero (University of Helsinki, FI)
- Timon Barlag (Leibniz Universität Hannover, DE)
- Dario Della Monica (University of Udine, IT)
- Arnaud Durand (Paris Cité University, FR) [dblp]
- Fredrik Engström (University of Gothenburg, SE) [dblp]
- Hadar Frenkel (CISPA - Saarbrücken, DE)
- Nicolas Fröhlich (Leibniz Universität Hannover, DE)
- Pietro Galliani (University of Insubria - Varese, IT) [dblp]
- Erich Grädel (RWTH Aachen, DE) [dblp]
- Jens Gutsfeld (TU Braunschweig, DE)
- Matilda Häggblom (University of Helsinki, FI)
- Miika Hannula (University of Helsinki, FI) [dblp]
- Peter Harremoës (Niels Brock Copenhagen Business College, DK)
- Lauri Hella (Tampere University, FI) [dblp]
- Minna Eveliina Hirvonen (University of Helsinki, FI)
- Batya Kenig (Technion - Haifa, IL) [dblp]
- Søren Brinck Knudstorp (University of Amsterdam, NL)
- Phokion G. Kolaitis (University of California - Santa Cruz, US) [dblp]
- Juha Kontinen (University of Helsinki, FI) [dblp]
- Cheuk Ting Li (The Chinese University of Hong Kong, HK)
- Martin Lück (OHB System - Bremen, DE) [dblp]
- Yasir Mahmood (Universität Paderborn, DE)
- Alessio Mansutti (IMDEA Software Institute - Madrid, ES)
- Arne Meier (Leibniz Universität Hannover, DE) [dblp]
- Till Miltzow (Utrecht University, NL) [dblp]
- Christoph Ohrem (Universität Münster, DE)
- Ana Oliveira da Costa (IST Austria - Klosterneuburg, AT) [dblp]
- Martin Otto (TU Darmstadt, DE) [dblp]
- Nina Pardal (University of Sheffield, GB)
- Max Sandström (University of Sheffield, GB)
- Milan Studený (The Czech Academy of Sciences - Prague, CZ)
- Marius Tritschler (TU Darmstadt, DE)
- Jouko Väänänen (University of Helsinki, FI) [dblp]
- Jonni Virtema (University of Sheffield, GB) [dblp]
- Heribert Vollmer (Leibniz Universität Hannover, DE) [dblp]
- Jef Wijsen (University of Mons, BE) [dblp]
- Fan Yang (Utrecht University, NL) [dblp]
- Martin Zimmermann (Aalborg University, DK) [dblp]
Related Seminars
Classification
- Computational Complexity
- Databases
- Logic in Computer Science
Keywords
- team semantics
- hyperproperties
- finite model theory
- information theory
- formal linguistics