TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 24111

Logics for Dependence and Independence: Expressivity and Complexity

( Mar 10 – Mar 15, 2024 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/24111

Organizers

Contact

Shared Documents


Schedule

Summary

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.

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

Motivation

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.

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

Participants

Related Seminars
  • Dagstuhl Seminar 13071: Dependence Logic: Theory and Applications (2013-02-10 - 2013-02-15) (Details)
  • Dagstuhl Seminar 15261: Logics for Dependence and Independence (2015-06-21 - 2015-06-26) (Details)
  • Dagstuhl Seminar 19031: Logics for Dependence and Independence (2019-01-13 - 2019-01-18) (Details)

Classification
  • Computational Complexity
  • Databases
  • Logic in Computer Science

Keywords
  • team semantics
  • hyperproperties
  • finite model theory
  • information theory
  • formal linguistics