Logics for Dependence and Independence: Expressivity and Complexity

While natural deduction- and Hilbert-style axiomatizations of logics employing team semantics such dependence logic and inquisitive logic have been extensively studied, the development of sequent calculi and proof theory in general for these logics appears to have been hindered by the factors such as the fact these logics are not closed under uniform substitution. The sequent calculi which have been constructed for these logics thus far have been labelled or multi-type systems. We propose a different approach: by appending a few deep inference-style rules (rules which can act not only on the immediate subformulas and main connectives of formulas, but also on subformulas and connectives deeper within a formula) to a standard Gentzen-style calculus, we obtain a very simple system for at least one of these logics.

Are team logics logics? In the 70’s, a similar criticism was addressed to quantum logic, on the basis that the latter lacks a (proof-theoretically) well-behaved conditional operator. Similarly, many of the languages considered in the literature on team semantics lack (and fail to define) an adequate conditional, and as a consequence they are not amenable to simple Hilbert-style axiomatizations. This situation was cleared by the discovery that downward closed languages can be enriched with a well-behaved conditional (the inquisitive implication), in many cases without increase in expressive power (propositional case) or, at least, without losing the property of downward closure.

It is less clear what could be taken as a conditional for languages that are not downward closed. As an interesting special case, the literature is rich with union-closed languages, e.g. inclusion logics and languages with possibility operators or relevant disjunctions. I will show that there is no conditional that preserves union closure and satisfies the key proof-theoretical constraints of modus ponens and the deduction theorem. Such an operator is missing not only for the whole class of union-closed languages, but also when trying to extend some specific individual languages.

I will then consider four candidates for the role of conditional for union closed languages: four binary operators that preserve union closure, respect restricted forms of modus ponens and the deduction theorem, and share many properties with what is usually considered a “conditional”.

Team semantics is the compositional infrastructure at the basis of so-called logics for (in)dependencies [1, 2, 3], making it possible to specify the set of first-order variables upon which another first-order variable value is allowed to depend on, overruling the standard linear dependence relation imposed by the quantification prefix.

On the one hand, this ability comes in handy for modeling games with incomplete information, where moves of one player may be dependent on only some of the moves of the other player, while being independent of the other ones. On the other hand, teams (i.e., sets of assignments) are meant to collect the uncertainty about possible evaluations of only a subset of variables, e.g., the universally quantified ones; it is thus possible to only specify dependencies for the remaining variables, e.g., the existentially quantified ones.

To overcome this asymmetry, which strides with the symmetric treatment of players in games, we extend the notion of teams with the one of hyperteams (i.e., sets of teams), thus allowing for a symmetric treatment of existentially and universally quantified variables.

We study variants of both Quantified Propositional Temporal Logic (QPTL) and First-Order Logic (FOL), replacing their standard semantics with one based on hyperteams, thus obtaining Good-for-Game QPTL (GFG-QPTL) [4] and Alternating Dependence/Independence-Friendly Logic (ADIF) [5]. Both these logics enjoy determinacy, which makes them particularly apt to model 2-player zero-sum games. We provide both compositional and game-theoretic semantics, and study the complexity of satisfiability (for GFG-QPTL) and model checking (for both GFG-QPTL and ADIF) problems.

We study the complexity of reasoning tasks for logics in team semantics. Our main focus is on the data complexity of model checking but we also derive new results for logically defined counting and enumeration problems. Our approach is based on modular reductions of these problems into the corresponding problems of various classes of Boolean formulas. We illustrate our approach via several new tractability/intractability results.

Logics based on team semantics often fail to be substitutional, limiting any algebraic treatment, and rendering schematic uniform proof systems impossible. This shortcoming can be attributed to the flatness principle, commonly adhered to when generating team semantics.

Investigating the formation of team semantics from algebraic semantics, and disregarding the flatness principle, we present the logic of teams, LT, a substitutional logic in which important propositional team logics are axiomatisable as fragments. Starting from classical propositional logic and Boolean algebras, we give a semantics for LT by considering the algebras that are powersets of Boolean algebras B, i.e., of the form P(B), equipped with internal (pointwise) and external (set theoretic) connectives. Furthermore, we present a well-motivated complete and sound labelled natural deduction system for LT.

We introduce Hyper2LTL, a temporal logic for the specification of hyperproperties that allows for second-order quantification over sets of traces. Unlike first-order temporal logics for hyperproperties, such as HyperLTL, Hyper2LTL can express complex epistemic properties like common knowledge, Mazurkiewicz trace theory, and asynchronous hyperproperties. The model checking problem of Hyper2LTL is, in general, undecidable. For the expressive fragment where second-order quantification is restricted to smallest and largest sets, we present an approximate model-checking algorithm that computes increasingly precise under- and overapproximations of the quantified sets, based on fixpoint iteration and automata learning. We report on encouraging experimental results with our model-checking algorithm, which we implemented in the tool HySO.

Much (although not all) of the work in the area of Team Semantics assumes that all expressions are in negation normal form (and, in particular, that no negated dependence atoms can appear).

I will argue that, even though this choice has valid historical reasons and is appropriate for certain logics based on Team Semantics, in general there is no compelling reason not to introduce (dual) negation; and I will re-examine the question of finding out which dependency families lead to logics that are reducible to First Order Logic in this more general setting.

We study hidden-variable models from quantum mechanics, and their abstractions in purely probabilistic and relational frameworks, by means of logics of dependence and independence, based on team semantics. We show that common desirable properties of hidden-variable models can be defined in an elegant and concise way in dependence and independence logic. The relationship between different properties, and their simultaneous realisability can thus been formulated and a proved on a purely logical level, as problems of entailment and satisfiability of logical formulae. Connections between probabilistic and relational entailment in dependence and independence logic allow us to simplify proofs. In many cases, we can establish results on both probabilistic and relational hidden-variable models by a single proof, because one case implies the other, depending on purely syntactic criteria. We also discuss the ‘no-go’ theorems by Bell and Kochen-Specker and provide purely logical variants of the latter, introducing non-contextual choice as a team-semantical property.

In this talk, we study a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We consider three logics: TeamLTL, TeamCTL and TeamCTL*, which are obtained by adding quantification over so-called time evaluation functions controlling the asynchronous progress of traces. We then relate synchronous to our new logics and show how it can be embedded into them. We discuss that the model checking problem for with Boolean disjunctions is highly undecidable by encoding recurrent computations of non-deterministic 2-counter machines. Finally, we present a translation from to Alternating Asynchronous Büchi Automata and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfiability problems.

Conditional independence plays a foundational role in database theory, probability theory, information theory, and graphical models. Many properties of conditional independence are shared across various domains, and to some extent these commonalities can be studied through a measure-theoretic approach. In this talk we consider an alternative approach via semiring relations, defined by extending database relations with tuple annotations from some commutative semiring. Integrating various interpretations of conditional independence in this context, we investigate how the choice of the underlying semiring impacts the corresponding axiomatic and decomposition properties.

A dependence or independence atom is a statement that some variables are in some sense (in)dependent. A set of atoms S is said to logically imply another atom s if every suitable object (e.g. a database or a distribution) that satisfies all of the atoms in S also satisfies the atom s. An implication problem is the task of deciding whether a given set of atoms S logically implies another given atom s.

In this talk, I will present some axiomatization results for implication problems for classes that combine different types of qualitative and quantitative atoms. We consider two different implication problems that combine well-known qualitative and quantitative atoms with two lesser-known quantitative atoms: unary marginal identity and unary marginal distribution equivalence. A unary marginal identity states that two variables x and y are identically distributed. A unary marginal distribution equivalence states that the multiset consisting of the marginal probabilities of all the values for variable x is the same as the corresponding multiset for y.

The first one of these implication problems combines unary marginal identity and unary marginal distribution equivalence with functional dependency. The second implication problem combines the two atoms with probabilistic independence. Both implication problems have a sound and complete axiomatization and a polynomial-time algorithm.

In the team semantic setting, Väänänen (2017) defined and axiomatized approximate dependence atoms suitable for cases when “almost dependence” is permittable. An approximate dependence atom is satisfied by a team if there exists a large enough subteam that satisfies the corresponding usual dependence atom.

We aim to define and axiomatize approximate versions of other dependence atoms, such as exclusion and inclusion. Depending on the properties of the atom, such as downward closure or the lack thereof, different definitions of the atoms’ approximate versions might be needed. We present some preliminary results regarding axiomatizations of approximate exclusion and anonymity atoms.

The graphical structure of Probabilistic Graphical Models (PGMs) represents the conditional independence (CI) relations that hold in the modeled distribution. The premise of all current systems-of-inference for deriving conditional independence relations in PGMs, is that the set of CIs used for the construction of the PGM hold exactly. In practice, algorithms for extracting the structure of PGMs from data discover approximate CIs that do not hold exactly in the distribution. In this work, we ask how the error in this set propagates to the inferred CIs read off the graphical structure. More precisely, what guarantee can we provide on the inferred CI when the set of CIs that entailed it hold only approximately? In this talk, I will describe new positive and negative results concerning this problem.

In recent work, Aloni, Anttila and Yang (2023) present two extensions of the modal team logic BSML, demonstrating their expressive completeness for all properties [invariant under bounded bisimulation] and all union-closed properties, respectively, and leave open the problem of characterizing the expressive power of BSML. Continuing this line of work, we solve this problem by showing that BSML is expressively complete for all convex, union-closed properties.

We then shift our focus to independence logic, characterizing the expressive power of propositional independence logic with the inquisitive disjunction.

Data dependencies are integrity constraints that the data at hand ought to obey. After functional dependencies were introduced by E.F. Codd in the 1970s, several other kinds of data dependencies were defined and extensively studied. Eventually, it was realized that essentially all data dependencies are either equality generating dependencies (egds) or tuple generating dependencies (tgds); the former generalize functional dependencies, while the latter generalize inclusion dependencies, multi-valued dependencies, and full tgds. In 1987, Makowsky and Vardi characterized full tgds and egds in terms of their structural properties, such as domain independence, closure under direct products, and modularity. The aim of this talk is to present characterizations of arbitrary tgds and egds that employ a new notion of locality. This is joint work with Marco Console and Andreas Pieris.

The probabilistic conditional independence implication problem is to decide whether a given statement on the conditional independence among several random variables is implied by a given list of such statements. This problem was shown to be undecidable, that is, there is no algorithm that is guaranteed to solve this problem. We will also describe the relation between this problem and the periodic tiling problem, and its implication on network coding.

This Talk is based on our recent article with the same title: Parameterized Complexity of Weighted Team Definability In this article, we study the complexity of weighted team definability for logics with team semantics. This is a natural analogue of one of the most studied problems in parameterized complexity, the notion of weighted Fagin-definability, which is formulated in terms of satisfaction of first-order formulas with free relation variables. We focus on the parameterized complexity of weighted team definability for a fixed formula $\phi$ of central team-based logics. Given a first-order structure $A$ and the parameter value $k\in N$ as input, the question is to determine whether $(A,T)\vDash \phi$ for some team $T$ of size $k$. We show several results on the complexity of this problem for dependence, independence, and inclusion logic formulas. Moreover, we also relate the complexity of weighted team definability to the complexity classes in the well-known W-hierarchy as well as paraNP.

In this talk, we give an overview of different parameterisations in propositional dependence logic as well as for first-order dependence logic. We start with a short primer on parameterised complexity theory and then dive into the results for the two dependence logic variants mentioned.

During the seminar at Dagstuhl, I gave a presentation about ER-complete problems. We gave many examples of ER-complete problems from different domains. We showed techniques to show ER-completeness, that are different from reductions for NP-completeness. Furthermore, we explained some common phenomena, like high solution precision and topological universality.

In this talk I will present a relaxed set based variant of asynchronous linear temporal logic under team semantics. Linear temporal logic (LTL) is used in system verification to write formal specifications for reactive systems. However, some relevant properties, e.g. non-inference in information flow security, cannot be expressed in LTL. A class of such properties that has recently received ample attention is known as hyperproperties. Team semantics offers an avenue to capture such hyperproperties. The asynchronous variant I will present gives a bottom-up approach to capturing hyperproperties, as the asynchronous variant is expressively equivalent with LTL, but it grows in expressivity quickly with extensions. I will introduce the extensions of TeamLTL with the Boolean disjunction and a fragment of the extension of TeamLTL with the Boolean negation, where the negation cannot occur in the left-hand side of the Until-operator or within the Global-operator. I will present complexity results of the model checking problem, as well as some results relating the logics with other logics capturing hyperproperties.

Based on Joint work with Juha Kontinen and Jonni Virtema.

In a recent manuscript [2], an abstract approach to conditional independence (CI) structures has been introduced. The approach was inspired by the idea of deriving further probabilistically valid implications among CI statements based on the idea of self-adhesion of CI models. That particular method is an abstraction of an information-theoretical method to derive non-Shannon information-theoretical inequalities, based on the so-called copy lemma [9, 4, 8, 3].

The talk was, however, devoted solely to a limited sub-topic of the manuscript. Specifically, it dealt with an important class of abstract CI frames which are closed under 3 basic operations: copying, marginalization and intersection. Many of standard classes of CI structures, including classic probabilistic CI structures fall into this class of CI frames.

The point is that then, for every variable set $N$, the family of respective CI models forms a lattice relative to inclusion of models. Therefore, one can apply the results from lattice theory [1] and formal concept analysis [5] to describe such lattices of models in terms of the corresponding abstract functional dependence relation [7]. Particular concepts of pseudo-closed sets relative to a Moore family and canonical implicational basis [6] then offer a kind of simplest standard description in terms of implications among CI statements. Such description can then be interpreted as a kind of “axiomatization” of the respective CI models.

In the talk, the above mentioned concept of an abstract CI frame was introduced, including three basic examples. Substantial related results from lattice theory and the formal concept analysis were then recalled and illustrated by a simple running example.

Hybrid team logics are inspired by hybrid modal logics where binders can be used to bind (and later reference) assignments. In the team setting, bound teams may be referenced as regular relations. We find that Hybrid Team Logic and its positive and negative fragments are equivalent to well-known team logics. Further, we can analyze guarded versions of these logics to find that guarded hybrid logics share some prominent properties of classical guarded logics, while also overcoming some of the limitations of atom-based guarded team logics.

In this talk I will give an introduction to team semantics. I will start by covering motivation, basic definitions, and results from the classical era of team semantics (2007-2017). I will cover the most important aspects first-order team semantics, and briefly discuss how this approach can be adapted to the propositional and modal contexts. In the second half of my talk, I will introduce two of the most important recent advancements in team semantics relevant to this meeting; namely probabilistic team semantics and temporal team semantics.

We consider database instances that may violate their primary key constraints. A repair of such a database instance is an inclusion-maximal consistent subset of it. For a fixed Boolean query q, the decision problem CERTAINTY(q) takes a database instance as input, and asks whether q holds true in every repair. It is known that for every self-join-free Boolean conjunctive query q, CERTAINTY(q) falls in one of three complexity classes: FO, L-complete, or coNP-complete; furthermore, it can be decided, given q, which of the three cases holds. However, the complexity classification of CERTAINTY(q) for Boolean conjunctive queries q with self-joins remains a notorious open problem. This presentation provides an overview of previous research and the ongoing challenges concerning the study of CERTAINTY(q) for Boolean conjunctive queries.