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.

Creative Commons BY 4.0

Juha Kontinen, Jonni Virtema, Heribert Vollmer, and Fan Yang