\hideLIPIcs

University of Helsinki, Department of Mathematics and Statistics, Helsinki, Finlandemailhttps://orcid.org/0000-0003-0115-5154Funded by grants 308712 and 338259 of the Academy of Finland Leibniz Universität Hannover, Institut für Theoretische Informatik, Hannover, [email protected]://orcid.org/0000-0002-8061-5376Funded by the German Research Foundation (DFG), project ME4279/1-2 Leibniz Universität Hannover, Institut für Theoretische Informatik, Hannover, [email protected]://orcid.org/0000-0002-5651-5391Funded by the German Research Foundation (DFG), project ME4279/1-2 \CopyrightJuha Kotinen, Arne Meier, and Yasir Mahmood {CCSXML} <ccs2012> <concept> <concept_id>10003752.10003790.10003800</concept_id> <concept_desc>Theory of computation Higher order logic</concept_desc> <concept_significance>500</concept_significance> </concept> <concept> <concept_id>10003752.10003777.10003779</concept_id> <concept_desc>Theory of computation Problems, reductions and completeness</concept_desc> <concept_significance>500</concept_significance> </concept> </ccs2012> \ccsdesc[500]Theory of computation Higher order logic \ccsdesc[500]Theory of computation Problems, reductions and completeness

A Parameterized View on the Complexity of Dependence Logic

Juha Kontinen Arne Meier Yasir Mahmood

Abstract

In this paper, we investigate the parameterized complexity of model checking for Dependence Logic which is a well studied logic in the area of Team Semantics. We start with a list of nine immediate parameterizations for this problem, namely: the number of disjunctions (i.e., splits)/(free) variables/universal quantifiers, formula-size, the tree-width of the Gaifman graph of the input structure, the size of the universe/team, and the arity of dependence atoms. We present a comprehensive picture of the parameterized complexity of model checking and obtain a division of the problem into tractable and various intractable degrees. Furthermore, we also consider the complexity of the most important variants (data and expression complexity) of the model checking problem by fixing parts of the input.

keywords:

Team Semantics, Dependence Logic, Parameterized Complexity, Model Checking

1 Introduction

In this article, we explore the parameterized complexity of model checking for dependence logic ( $\mathcal{D}$ ). We give a concise classification of this problem and its standard variants (expression and data complexity) with respect to several syntactic and structural parameters. Our results lay down a solid foundation for a systematic study of the parameterized complexity of team-based logics.

The introduction of Dependence Logic [27] in 2007 marks also the birth of the general semantic framework of team semantics that has enabled a systematic study of various notions of dependence and independence during the past decade. Team semantics differs from Tarski’s semantics by interpreting formulas by sets of assignments instead of a single assignment as in first-order logic. Syntactically, dependence logic is an extension of first-order logic by new dependence atoms ${\mathsf{dep}}({\mathbf{x}};{\mathbf{y}})$ expressing that the values of variables $\mathbf{x}$ functionally determine values of the variables $\mathbf{y}$ (in the team under consideration). Soon after the introduction of dependence logic many other interesting team-based logics and atoms were introduced such as inclusion, exclusion, and independence atoms that are intimately connected to the corresponding inclusion, exclusion, and multivalued dependencies studied in database theory [13, 9]. Furthermore, the area has expanded, e.g., to propositional, modal and probabilistic variants (see [15, 19, 14] and the references therein).

For the applications, it is important to understand the complexity theoretic aspects of dependence logic and its variants. In fact, during the past few years, these aspects have been addressed in several studies. For example, on the level of sentences dependence logic and independence logic are equivalent to existential second-order logic while inclusion logic corresponds to positive greatest fixed point logic and thereby captures P over finite (ordered) structures [11]. Furthermore, there are (non-parameterized) studies that restrict the syntax and try to pin the intractability of a problem to a particular (set of) connective(s). For instance, Durand and Kontinen [5] characterize the data complexity of fragments of dependence logic with bounded arity of dependence atoms/number of universal quantifiers, and Grädel [12] characterizes the combined and the expression complexity of the model checking problem of dependence logic. These studies will be of great help in developing our parameterized approach.

A formalism to enhance the understanding of the inherent intractability of computational problems is brought by the framework of parameterized complexity [4]. Initiated by the founding fathers Downey and Fellows, in this area within computational complexity theory one strives for more structure within the darkness of intractability. Essentially, one tries to identify so-called parameters of a considered problem $\Pi$ to find algorithms solving $\Pi$ with runtimes of the form $f(k)\cdot|x|^{O(1)}$ for inputs $x$ , corresponding parameter values $k$ , and a computable function $f$ . These kind of runtimes are called FPT-runtimes (from fixed-parameter tractable; short FPT) and tame the combinatoric explosion of the solution space to a function $f$ in the parameter. As a very basic example in this vein, we can consider the propositional satisfiability problem $\mathrm{SAT}$ . An immediate parameter that pulls the problem into the class FPT is the number of variables, as one can solve $\mathrm{SAT}$ in time $2^{k}\cdot|\varphi|$ if $k$ is the number of variables of a given propositional formula $\varphi$ . Yet, this parameter is not very satisfactory as it neither is seen fixed nor slowly growing in its practical instances. However, there are several interesting other parameters under which $\mathrm{SAT}$ becomes fixed-parameter tractable, e.g., the so-called treewidth of the underlying graph representations of the considered formula [26]. This term was coined by Robertson and Seymour in 1984 [25] and established a profound position (currently DBLP lists 812 papers with treewidth in its title) also in the area of parameterized complexity in the last years [3, 4].

Coming back to fpt-runtimes, a runtime of a very different quality (yet still polynomial for fixed parameters) than FPT is summarized by the complexity class XP: $|x|^{f(k)}$ for inputs $x$ , corresponding parameter values $k$ , and a computable function $f$ . Furthermore, analogously as XP but on nondeterministic machines, the class XNP will be of interest in this paper. Further up in the hierarchy, classes of the form $\textbf{para}\mathcal{C}$ for a classical complexity class $\mathcal{C}\in\{\textbf{NP},\textbf{PSPACE},\textbf{NEXP}\}$ play a role in this paper. Such classes intuitively capture all problems that are in the complexity class $\mathcal{C}$ after fpt-time preprocessing. In Fig. 1 an overview of these classes and their relations are depicted (for further details see, e.g., the work of Elberfeld et al. [7]).

Figure 1: Landscape showing relations of relevant parameterized complexity classes with machine definitions.

Recently, the propositional variant of dependence logic ( $\mathcal{PDL}$ ) has been investigated regarding its parameterized complexity [23, 20]. Moreover, propositional independence and inclusion logic have also been studied from the perspective of parameterized complexity [21]. In this paper, we further pursue the parameterized journey through the world of team logics and will visit the problems of first-order dependence logic $\mathcal{D}$ . As this paper is the first one that investigates $\mathcal{D}$ from the parameterized point of view, we need to gather the existing literature and revisit many results particularly from this perspective. As a result, this paper can be seen as a systematic study with some of the result following in a straightforward manner from the known non-parameterized results and some shedding light also on the non-parameterized view of model checking.

We give an example below to illustrate how the concept of dependence arises as a natural phenomenon in the physical world.

Example 1.1.

Flight	Destination	Gate	Date	Time
FIN-70	HEL – FI	C1	04.10.2021	09:55
SAS-475	OSL – NO	C3	04.10.2021	12:25
SAS-476	HAJ – DE	C2	04.10.2021	12:25
FIN-80	HEL – FI	C1	04.10.2021	19:55
KLM-615	ATL – USA	A5	05.10.2021	11:55
QR-70	DOH – QR	B6	05.10.2021	12:25
THY-159	IST – TR	A1	05.10.2021	15:55
FIN-80	HEL – FI	C1	05.10.2021	19:55

Table 1: An example flight departure screen at an airport

The database in Table 1 presents a screen at an airport for showing details about departing flights. Alternatively, it can be seen as a team $T$ over attributes in the top row as variables. Clearly, $T\models{\mathsf{dep}}({\texttt{Flight,Date,Time}};{\texttt{Destination,Gate}})$ , as well as $T\models{\mathsf{dep}}({\texttt{Gate,Date,Time}};{\texttt{Destination, Flight}})$ . Whereas, $T\not\models{\mathsf{dep}}({\texttt{Destination,Gate}};{\texttt{Time}})$ as witnessed by the pair (FIN- $70$ , HEL – FI, C $1$ , $04.10.2021$ , $09:55$ ) and (FIN- $80$ , HEL – FI, C $1$ , $04.10.2021$ , $19:55$ ).

Contribution.

Our classification is two-dimensional:

1.

We consider the model checking problem of $\mathcal{D}$ under various parameterizations: number of split-junctions in a formula $\#\mathsf{splits}$ , the length of the formula $|\Phi|$ , number of free variables $\#\mathsf{free\text{-}variables}$ , the treewidth of the structure $\mathsf{tw}(\mathcal{A})$ , the size of the structure ${|\mathcal{A}|}$ , the size of the team $|T|$ , the number of universal quantifiers in the formula $\#\forall$ , the arity of the dependence atoms $\mathsf{dep\text{-}arity}$ , as well as the total number of variables $\#\mathsf{variables}$ .
2.

We distinguish between expression complexity $\mathsf{ec}$ (the input structure is fixed), data complexity $\mathsf{dc}$ (the formula is fixed), and combined complexity $\mathsf{cc}$ .

The results are summarized in Table 2. For instance, the parameters $\#\forall,\mathsf{dep\text{-}arity},$ and $\#\mathsf{variables}$ impact in lowering the complexity for $\mathsf{ec}$ (and not for $\mathsf{cc}$ or $\mathsf{dc}$ ), while the parameter ${|\mathcal{A}|}$ impacts for $\mathsf{dc}$ but not for $\mathsf{cc}$ or $\mathsf{ec}$ .

Related work.

The parameterized complexity analyses in the propositional setting [23, 20, 21] have considered the combined complexity of model checking and satisfiability as problems of interest. On the $\mathsf{cc}$ -level, the picture there is somewhat different, e.g., team size as a parameter for propositional dependence logic enabled a FPT algorithm while in our setting it has no effect on the complexity (paraNEXP). Grädel [12] studied the expression and the combined complexity for $\mathcal{D}$ in the classical setting, whereas the data complexity was considered by Kontinen [16].

Organization of the paper.

In Section 2, we introduce the foundational concepts of dependence logic as well as parameterized complexity. In Section 3 our results are presented while Section 4 concludes the article.

2 Preliminaries

We require standard notions from classical complexity theory [24]. We encounter the classical complexity classes $\textbf{P},\textbf{NP},\textbf{PSPACE},\textbf{NEXP}$ and their respective completeness notions, employing polynomial time many-one reductions ( $\leq^{\textbf{P}}_{m}$ ).

Parameterized Complexity Theory.

A parameterized problem (PP) $P\subseteq\Sigma^{*}\times\mathbb{N}$ is a subset of the crossproduct of an alphabet and the natural numbers. For an instance $(x,k)\in\Sigma^{*}\times\mathbb{N}$ , $k$ is called the (value of the) parameter. A parameterization is a polynomial-time computable function that maps a value from $x\in\Sigma^{*}$ to its corresponding $k\in\mathbb{N}$ . The problem $P$ is said to be fixed-parameter tractable (or in the class FPT) if there exists a deterministic algorithm $\mathcal{A}$ and a computable function $f$ such that for all $(x,k)\in\Sigma^{*}\times\mathbb{N}$ , algorithm $\mathcal{A}$ correctly decides the membership of $(x,k)\in P$ and runs in time $f(k)\cdot|x|^{O(1)}$ . The problem $P$ belongs to the class XP if $\mathcal{A}$ runs in time $|x|^{f(k)}$ on a deterministic machine, whereas XNP is the non-deterministic counterpart of XP. Abusing a little bit of notation, we write $\mathcal{C}$ -machine for the type of machines that decide languages in the class $\mathcal{C}$ , and we will say a function $f$ is “ $\mathcal{C}$ -computable” if it can be computed by a machine on which the resource bounds of the class $\mathcal{C}$ are imposed.

Also, we work with classes that can be defined via a precomputation on the parameter.

Definition 2.1.

Let $\mathcal{C}$ be any complexity class. Then $\textbf{para}\mathcal{C}$ is the class of all PPs $P\subseteq\Sigma^{*}\times\mathbb{N}$ such that there exists a computable function $\pi\colon\mathbb{N}\to\Delta^{*}$ and a language $L\in\mathcal{C}$ with $L\subseteq\Sigma^{*}\times\Delta^{*}$ such that for all $(x,k)\in\Sigma^{*}\times\mathbb{N}$ we have that $(x,k)\in P\Leftrightarrow(x,\pi(k))\in L$ .

Notice that $\textbf{para}\textbf{P}=\textbf{FPT}$ . The complexity classes $\mathcal{C}\in\{\textbf{NP},\textbf{PSPACE},\textbf{NEXP}\}$ are used in the $\textbf{para}\mathcal{C}$ context by us.

A problem $P$ is in the complexity class W[P], if it can be decided by a NTM running in time $f(k)\cdot|x|^{O(1)}$ steps, with at most $g(k)$ -many non-deterministic steps, where $f,g$ are computable functions. Moreover, W[P] is contained in the intersection of paraNP and XP (for details see the textbook of Flum and Grohe [8]).

Let $c\in\mathbb{N}$ and $P\subseteq\Sigma^{*}\times\mathbb{N}$ be a PP, then the $c$ -slice of $P$ , written as $P_{c}$ is defined as $P_{c}:=\{\,(x,k)\in\Sigma^{*}\times\mathbb{N}\mid k=c\,\}$ . Notice that $P_{c}$ is a classical problem then. Observe that, regarding our studied complexity classes, showing membership of a PP $P$ in the complexity class $\textbf{para}\mathcal{C}$ , it suffices to show that for each slice $P_{c}\in\mathcal{C}$ is true.

Definition 2.2.

Let $P\subseteq\Sigma^{*}\times\mathbb{N},Q\subseteq\Gamma^{*}$ be two PPs. One says that $P$ is fpt-reducible to $Q$ , $P\leq^{\textbf{FPT}}Q$ , if there exists an FPT-computable function $f\colon\Sigma^{*}\times\mathbb{N}\to\Gamma^{*}\times\mathbb{N}$ such that

•

for all $(x,k)\in\Sigma^{*}\times\mathbb{N}$ we have that $(x,k)\in P\Leftrightarrow f(x,k)\in Q$ ,
•

there exists a computable function $g\colon\mathbb{N}\to\mathbb{N}$ such that for all $(x,k)\in\Sigma^{*}\times\mathbb{N}$ and $f(x,k)=(x^{\prime},k^{\prime})$ we have that $k^{\prime}\leq g(k)$ .

Finally, in order to show that a problem $P$ is $\textbf{para}\mathcal{C}$ -hard (for some complexity class $\mathcal{C}$ ) it is enough to prove that for some $c\in\mathbb{N}$ , the slice $P_{c}$ is $\mathcal{C}$ -hard in the classical setting.

Dependence Logic.

We assume basic familiarity with predicate logic [6]. We consider first-order vocabularies $\tau$ that are sets of function symbols and relation symbols with an equality symbol $=$ . Let $\mathrm{VAR}$ be a countably infinite set of first-order variables. Terms over $\tau$ are defined in the usual way, and the set of well-formed formulas of first order logic ( $\mathcal{FO}$ ) is defined by the following BNF:

\psi\Coloneqq t_{1}=t_{2}\mid R(t_{1},\dots,t_{k})\mid\lnot R(t_{1},\dots,t_{k})\mid\psi\land\psi\mid\psi\lor\psi\mid\exists x\psi\mid\forall x\psi,

where $t_{i}$ are terms $1\leq i\leq k$ , $R$ is a $k$ -ary relation symbol from $\sigma$ , $k\in\mathbb{N}$ , and $x\in\mathrm{VAR}$ . If $\psi$ is a formula, then we use $\mathrm{VAR}(\psi)$ for its set of variables, and $\mathrm{Fr}(\psi)$ for its set of free variables. We evaluate $\mathcal{FO}$ -formulas in $\tau$ -structures, which are pairs of the form $\mathcal{A}=(A,\tau^{\mathcal{A}})$ , where $A$ is the domain of $\mathcal{A}$ (when clear from the context, we write $A$ instead of $\mathrm{dom}(\mathcal{A})$ ), and $\tau^{\mathcal{A}}$ interprets the function and relational symbols in the usual way (e.g., $t^{\mathcal{A}}\langle s\rangle=s(x)$ if $t=x\in\mathrm{VAR}$ ). If $\mathbf{t}=(t_{1},\dots,t_{n})$ is a tuple of terms for $n\in\mathbb{N}$ , then we write $\mathbf{t}^{\mathcal{A}}\langle s\rangle$ for $(t_{1}^{\mathcal{A}}\langle s\rangle,\dots,t_{n}^{\mathcal{A}}\langle s\rangle)$ .

Dependence logic ( $\mathcal{D}$ ) extends $\mathcal{FO}$ by dependence atoms of the form ${\mathsf{dep}}({\mathbf{t}};{\mathbf{u}})$ where $\mathbf{t}$ and $\mathbf{u}$ are tuples of terms. The semantics is defined through the concept of a team. Let $\mathcal{A}$ be a structure and $X\subseteq\mathrm{VAR}$ , then an assignment $s$ is a mapping $s\colon X\rightarrow A$ .

Definition 2.3.

Let $X\subseteq\mathrm{VAR}$ . A team $T$ in $\mathcal{A}$ with domain $X$ is a set of assignments $s\colon X\to A$ .

For a team $T$ with domain $X\supseteq Y$ define its restriction to $Y$ as $T\upharpoonright Y\coloneqq\{\,s\upharpoonright Y\mid s\in T\,\}$ . If $s\colon X\to A$ is an assignment and $x\in\mathrm{VAR}$ is a variable, then $s^{x}_{a}\colon X\cup\{x\}\to A$ is the assignment that maps $x$ to $a$ and $y\in X\setminus\{x\}$ to $s(y)$ . Let $T$ be a team in $\mathcal{A}$ with domain $X$ . Then we define $f\colon T\to\mathcal{P}(A)\setminus\{\emptyset\}$ as the supplementing function of $T$ . This is used to extend or modify $T$ to the supplementing team $T^{x}_{f}\coloneqq\{\,s^{x}_{a}\mid s\in T,a\in f(s)\,\}$ . For the case $f(s)=A$ is the constant function we simply write $T^{x}_{\mathcal{A}}$ for $T^{x}_{f}$ . The semantics of $\mathcal{D}$ -formulas is defined as follows.

Definition 2.4.

Let $\tau$ be a vocabulary, $\mathcal{A}$ be a $\tau$ -structure and $T$ be a team over $\mathcal{A}$ with domain $X\subseteq\mathrm{VAR}$ . Then,

$\displaystyle(\mathcal{A},T)\models t_{1}=t_{2}$	iff	$\displaystyle\forall s\in T:t_{1}^{\mathcal{A}}\langle s\rangle=t_{2}^{\mathcal{A}}\langle s\rangle$
$\displaystyle(\mathcal{A},T)\models R(t_{1},\ldots,t_{n})$	iff	$\displaystyle\forall s\in T:(t_{1}^{\mathcal{A}}\langle s\rangle,\ldots,t_{n}^{\mathcal{A}}\langle s\rangle)\in R^{\mathcal{A}}$
$\displaystyle(\mathcal{A},T)\models\neg R(t_{1},\ldots,t_{n})$	iff	$\displaystyle\forall s\in T:(t_{1}^{\mathcal{A}}\langle s\rangle,\ldots,t_{n}^{\mathcal{A}}\langle s\rangle)\not\in R^{\mathcal{A}}$
$\displaystyle(\mathcal{A},T)\models{\mathsf{dep}}({\mathbf{t}};{\mathbf{u}})$	iff	$\displaystyle\forall s_{1},s_{2}\in T:\mathbf{t}^{\mathcal{A}}\langle s_{1}\rangle=\mathbf{t}^{\mathcal{A}}\langle s_{2}\rangle\implies\mathbf{u}^{\mathcal{A}}\langle s_{1}\rangle=\mathbf{u}^{\mathcal{A}}\langle s_{2}\rangle$
$\displaystyle(\mathcal{A},T)\models\phi_{0}\land\phi_{1}$	iff	$\displaystyle(\mathcal{A},T)\models\phi_{0}\quad\text{ and }\quad(\mathcal{A},T)\models\phi_{1}$
$\displaystyle(\mathcal{A},T)\models\phi_{0}\lor\phi_{1}$	iff	$\displaystyle\exists T_{0}\exists T_{1}:T_{0}\cup T_{1}=T\quad\text{ and }\quad(\mathcal{A},T_{i})\models\phi_{i}\,\text{ for }i=0,1$
$\displaystyle(\mathcal{A},T)\models\exists x\phi$	iff	$\displaystyle(\mathcal{A},T^{x}_{f})\models\phi\text{ for some }f\colon T\to\mathcal{P}(A)\setminus\{\emptyset\}$
$\displaystyle(\mathcal{A},T)\models\forall x\phi$	iff	$\displaystyle(\mathcal{A},T^{x}_{\mathcal{A}})\models\phi$

Notice that we only consider formulas in negation normal form (NNF) as any formula of dependence logic can be transformed into logically equivalent NNF-form. Further note that $(\mathcal{A},T)\models\phi$ for all $\phi$ when $T=\emptyset$ (this is also called the empty team property). Furthermore, $\mathcal{D}$ -formulas are local, that is, for a team $T$ in $\mathcal{A}$ over domain $X$ and a $\mathcal{D}$ -formula $\phi$ , we have that $(\mathcal{A},T)\models\phi$ if and only if $(\mathcal{A},T\upharpoonright\mathrm{Fr}(\phi))\models\phi$ . Finally, every $\mathcal{D}$ -formula $\phi$ , if $(\mathcal{A},T)\models\phi$ then $(\mathcal{A},P)\models\phi$ for every $P\subseteq T$ . This property is known as the downwards closure.

Definition 2.5 (Gaifman graph).

Given a vocabulary $\tau$ and a $\tau$ -structure $\mathcal{A}$ , the Gaifman graph $G_{\mathcal{A}}=(A,E)$ of $\mathcal{A}$ is defined as

\displaystyle E\mathrel{\mathop{:}}=\big{\{}\,\{u,v\}\;\big{|}\;

\displaystyle\text{ if there is an }R^{n}\in\tau\text{ and }\mathbf{a}\in A^{n}\text{ with }R^{\mathcal{A}}(\mathbf{a})\text{ and }u,v\in\mathbf{a}\,\big{\}}.

That is, there is a relation $R\in\tau$ of arity $n$ such that $u$ and $v$ appear together in $R^{\mathcal{A}}$ .

Intuitively, the Gaifman graph of a structure $\mathcal{A}$ is an undirected graph with the universe of $\mathcal{A}$ as vertices and connects two vertices when they share a tuple in a relation (see also Fig. 2).

Definition 2.6 (Treewidth).

The tree decomposition of a given graph $G=(V,E)$ is a tree $T=(B,E_{T})$ , where the vertex set $B\subseteq\mathcal{P}(V)$ is the collection of bags and $E_{T}$ is the edge relation such that the following is true.

•

$\bigcup_{b\in B}=V$ ,
•

for every $\{u,v\}\in E$ there is a bag $b\in B$ with $u,v\in b$ , and
•

for all $v\in V$ the restriction of $T$ to $v$ (the subset with all bags containing $v$ ) is connected.

The width of a given tree decomposition $T=(B,E_{T})$ is the size of the largest bag minus one: $\max_{b\in B}|b|-1$ . The treewidth of a given graph $G$ is the minimum over all widths of tree decompositions of $G$ .

Observe that if $G$ is a tree then the treewidth of $G$ is one. Intuitively, one can say that treewidth accordingly is a measure of tree-likeness of a given graph.

Example 2.7.

Flight	Gate	Time
FIN-70	C1	09:55
SAS-475	C3	12:25
SAS-476	C2	12:25
FIN-80	C1	19:55

Figure 2: An

\mathcal{FO}

-structure

\mathcal{A}=(A,S^{\mathcal{A}},R^{\mathcal{A}})

(Left) with the Gaifman graph

G_{\mathcal{A}}

(Middle) and a possible treedecomposition of

G_{\mathcal{A}}

(Right) of Example 2.7. For brevity, universe elements are written in short forms.

Consider the database form our previous example. Recall that the universe $A$ consists of entries in each row. Let $\tau=\{\mathrm{S}^{2},\mathrm{R}^{3}\}$ include a binary relation $\mathrm{S}$ ( $\mathrm{S}(x,y):$ flights $x$ and $y$ are owed by the same company) and a ternary relation $\mathrm{R}$ ( $\mathrm{R}(x,y,z):$ the gate $x$ is reserved by the flight $y$ at time $z$ ). For simplicity, we only consider first four rows with the corresponding three columns from Table 3, see Figure 2 for an explanation. Since the largest bag size in our decomposition is $3$ , the treewidth of this decomposition is $2$ . Furthermore, the presence of cycles of length $3$ suggests that there is no better decomposition. As a consequence the given structure has treewidth $2$ .

The decision problem to determine whether the treewidth of a given graph $\mathcal{G}=(V,E)$ is at most $k$ , is NP-complete [1]. See Bodlaender’s Guide [2] for an overview of algorithms that compute tree decompositions. When considering the parameter treewidth, one usually assumes it as a given value and does not need to compute it. We consider only the model checking problem ( $\mathrm{MC}$ ) and two variants in this paper. First, let us define the most general version.

Problem:	$\mathsf{cc}$ (combined complexity of model checking)
Input:	a structure $\mathcal{A}$ , team $T$ and a $\mathcal{D}$ -formula $\Phi$ .
Question:	$(\mathcal{A},T)\models\Phi$ ?

We further consider the following two variants of the model checking problem.

Problem:	$\mathsf{dc}$ (data complexity of model checking, $\Phi$ is fixed)
Input:	a structure $\mathcal{A}$ , team $T$ .
Question:	$(\mathcal{A},T)\models\Phi$ ?

Problem:	$\mathsf{ec}$ (expression complexity of model checking, $\mathcal{A},T$ are fixed)
Input:	a $\mathcal{D}$ -formula $\Phi$ .
Question:	$(\mathcal{A},T)\models\Phi$ ?

List of Parameterizations.

Now let us turn to the parameters that are under investigation in this paper. We study the model checking problem of $\mathcal{D}$ under nine various parameters that naturally occur in an $\mathrm{MC}$ -instance. Let $\langle\mathcal{A},T,\Phi\rangle$ be an instance of $\mathrm{MC}$ , where $\Phi$ is a $\mathcal{D}$ -formula, $\mathcal{A}$ is a structure and $T$ is a team over $\mathcal{A}$ . The parameter $\#\mathsf{splits}$ denotes the number of occurrences of the split operator ( $\lor$ ), $\#\forall$ is the number of universal quantifiers in $\Phi$ . Moreover, $\#\mathsf{variables}$ (resp., $\#\mathsf{free\text{-}variables}$ ) denotes the total number of (free) variables in $\Phi$ . The parameter $|\Phi|$ is the size of the input formula $\Phi$ , and similarly the two other size parameters are $|\mathcal{A}|$ and $|T|$ . The treewidth of the structure $\mathcal{A}$ (see Def. 2.6) is defined as the treewidth of $G_{\mathcal{A}}$ and denoted by $\mathsf{tw}(\mathcal{A})$ . Note that for formulas using the dependence atom ${\mathsf{dep}}({\mathbf{x}};{\mathbf{y}})$ , one can translate to a formula using only dependence atoms where $|\mathbf{y}|=1$ (via conjunctions). That is why the arity of a dependence atom ${\mathsf{dep}}({\mathbf{x}};{\mathbf{y}})$ is defined as $|\mathbf{x}|$ and $\mathsf{dep\text{-}arity}$ is the maximum arity of any dependence atom in $\Phi$ .

Let $k$ be any parameterization and $P\in\{\mathsf{dc},\mathsf{ec},\mathsf{cc}\}$ , then by $k$ - $P$ we denote the problem $P$ when parameterized by $k$ . If more than one parameterization is considered, then we use ‘ $+$ ’ as a separator and write these parameters in brackets, e.g., $(|\Phi|+\#\mathsf{free\text{-}variables})\text{-}\mathsf{dc}$ as the problem $\mathsf{dc}$ with parameterization $|\Phi|+\#\mathsf{free\text{-}variables}$ . Finally, notice that since the formula $\Phi$ is fixed for $\mathsf{dc}$ this implies that ${|\Phi|}\text{-}\mathsf{dc}$ is nothing but $\mathsf{dc}$ . That is, bounding the parameter does not make sense for $\mathsf{dc}$ as the problem $\mathsf{dc}$ remains NP-complete.

3 Complexity results

Parameter	$\mathsf{cc}$	$\mathsf{dc}$	$\mathsf{ec}$
$\#\mathsf{splits}$	$\textbf{para}\textbf{PSPACE}\text{-h}^{L\ref{ec-splits}}$	$\textbf{para}\textbf{NP}^{L\ref{dc-many}}$	$\textbf{para}\textbf{PSPACE}\text{-h}^{L\ref{ec-splits}}$
$\|\Phi\|$	$\textbf{para}\textbf{NP}^{L\ref{cc-formula}}$	$\textbf{para}\textbf{NP}^{R\ref{rem:dc-formulasize}}$	$\textbf{FPT}^{\ref{ec-formula}}$
$\#\mathsf{free\text{-}variables}$	$\textbf{para}\textbf{NEXP}^{L\ref{cc-many}}$	$\textbf{para}\textbf{NP}^{L\ref{dc-many}}$	$\textbf{para}\textbf{NEXP}^{L\ref{cc-many}}$
$\mathsf{tw}(\mathcal{A})$	$\textbf{para}\textbf{NEXP}^{L\ref{cc-many}}$	$\textbf{para}\textbf{NP}^{P\ref{dc-all}}$	$\textbf{para}\textbf{NEXP}^{L\ref{cc-many}}$
${\|\mathcal{A}\|}$	$\textbf{para}\textbf{NEXP}^{L\ref{cc-many}}$	$\textbf{FPT}^{L\ref{dc-strucsize}}$	$\textbf{para}\textbf{NEXP}^{L\ref{cc-many}}$
$\|T\|$	$\textbf{para}\textbf{NEXP}^{L\ref{cc-many}}$	$\textbf{para}\textbf{NP}^{L\ref{dc-teamsize}}$	$\textbf{para}\textbf{NEXP}^{L\ref{cc-many}}$
$\#\forall$	$\textbf{para}\textbf{NP}\text{-h}^{L\ref{cc-universal}}$	$\textbf{para}\textbf{NP}^{L\ref{dc-many}}$	$\textbf{para}\textbf{NP}^{L\ref{ec-universal}}$
$\mathsf{dep\text{-}arity}$	$\textbf{para}\textbf{PSPACE}\text{-h}^{L\ref{cc-arity}}$	$\textbf{para}\textbf{NP}^{L\ref{dc-many}}$	$\textbf{para}\textbf{PSPACE}^{L\ref{ec-arity}}$
$\#\mathsf{variables}$	$\textbf{para}\textbf{NP}^{L\ref{cc-variables}}$	$\textbf{para}\textbf{NP}^{L\ref{dc-many}}$	$\textbf{FPT}^{L\ref{ec-variables}}$

Table 2: Complexity classification overview. A suffix -h represents the hardness result, whereas other results are completeness. The numbers in the exponent point to the corresponding result (

Lx

means Lemma

x

Px

means Proposition

x

Rx

means Remark

x

). Fig. 3 on page 3 is a graphical presentation of this table with a different angle.

We begin by proving relationships between various parameterizations.

Lemma 3.1.

The following relations among parameters hold.

1.

$|\Phi|\geq k$ for any $k\in\{\,\#\mathsf{splits},\#\forall,\mathsf{dep\text{-}arity},\#\mathsf{free\text{-}variables},\#\mathsf{variables}\,\}$ ,
2.

${|\mathcal{A}|}\geq\mathsf{tw}(\mathcal{A})$ . Moreover, for $\mathsf{dc}$ , ${|\mathcal{A}|}^{O(1)}\geq|T|$ ,
3.

For $\mathsf{ec}$ , $\#\mathsf{free\text{-}variables}$ is constant.

Proof 3.2.

1.

Clearly, the size of the formula limits all parts of it including the parameters mentioned in the list.
2.

Notice that for data complexity, the formula $\Phi$ and consequently the number of free variables in $\Phi$ is fixed. Moreover, due to locality of $\mathcal{D}$ it holds that $T\subseteq A^{r}$ , where $r$ is the number of free variables in $\Phi$ . That is, the team $T$ can be considered only over the free variables of $\Phi$ . This implies that teamsize is polynomially bounded by the universe size, as $|T|\leq|\mathcal{A}|^{r}$ . Finally, the result for $\mathsf{tw}(\mathcal{A})$ follows due to Definition 2.6. This is due to the reason that in the worst case all universe elements belong to one bag in the decomposition and $\mathsf{tw}(\mathcal{A})=|\mathcal{A}|-1$ .
3.

Notice that the team $T$ is fixed in $\mathsf{ec}$ . Together with the locality of $\mathcal{D}$ -formulas (see Def. 2.4), this implies that the domain of $T$ (which is same as the set of free variables in the formula $\Phi$ ) is also fixed and as a result, of constant size.

Remark 3.3.

If the number of free variables ( $\#\mathsf{free\text{-}variables}$ ) in a formula $\Phi$ is bounded then the total number of variables ( $\#\mathsf{variables}$ ) is not necessarily bounded, on the other hand, bounding $\#\mathsf{variables}$ also bounds $\#\mathsf{free\text{-}variables}$ .

3.1 Data complexity ( $\mathsf{dc}$ )

Classically, the data complexity of model checking for a fixed $\mathcal{D}$ -formula $\Phi$ is NP-complete [27].

Proposition 3.4.

For a fixed formula, the problem whether an input structure $\mathcal{A}$ and a team $T$ satisfies the formula is NP-complete. That is, the data complexity of dependence logic is NP-complete.

In this section we prove that none of the considered parameter lowers this complexity, except $|\mathcal{A}|$ . The proof relies on the fact that the complexity of model checking for already a very simple formula (see below) is NP-complete.

Lemma 3.5.

Let $k\in\{\#\mathsf{splits},\#\mathsf{free\text{-}variables},\#\mathsf{variables},\#\forall,\mathsf{dep\text{-}arity},\mathsf{tw}(\mathcal{A})\}$ . Then the problem ${k}\text{-}\mathsf{dc}$ , is paraNP-c.

Proof 3.6.

The upper bound follows from Proposition 3.4. Kontinen [16, Theorem 4.9] proves that the data complexity for a fixed $\mathcal{D}$ -formula of the form ${\mathsf{dep}}({x};{y})\lor{\mathsf{dep}}({u};{v})\lor{\mathsf{dep}}({u};{v})$ is already NP-complete. For clearity, we briefly sketch the reduction presented by Kontinen [16]. Let $\phi=\bigwedge\limits_{i\leq m}(\ell_{i,1}\lor\ell_{i,2}\lor\ell_{i,3})$ be an instance of $3\text{-}\mathrm{SAT}$ . Consider the structure $\mathcal{A}$ over the empty vocabulary, that is, $\tau=\emptyset$ . Let $A=\mathrm{Var}(\phi)\cup\{0,1,\ldots,m\}$ . The team $T$ is constructed over variables $\{x,y,u,v\}$ that take values from $A$ . As an example, the clause $(p_{1}\lor\neg p_{2}\lor\neg p_{3})$ gives rise to assignments in Table 3.

$x=$ ‘variable’	$y=$ ‘parity’	$u=$ ‘clause’	$v=$ ‘position’
$p_{1}$	$1$	$1$	$0$
$p_{2}$	$0$	$1$	$1$
$p_{3}$	$0$	$1$	$2$

Table 3: An example team for

(p_{1}\lor\neg p_{2}\lor\neg p_{3})

Notice that, a truth assignment $\theta$ for $\phi$ is constructed using the division of $T$ according to each split. That is, $T\models{\mathsf{dep}}({x};{y})\lor{\mathsf{dep}}({u};{v})\lor{\mathsf{dep}}({u};{v})$ if and only if $\exists P_{0},P_{1},P_{2}$ such that $\cup_{i}P_{i}=T$ for $i\leq 2$ and each $P_{i}$ satisfies $i$ th dependence atom. Let $P_{0}$ be such that $P_{0}\models{\mathsf{dep}}({x};{y})$ , then we let $\theta(p_{j})=1\iff\exists s\in P,\text{ s.t. }s(x)=p_{j}$ and $s(y)=1$ . That is, one literal in each clause must be chosen in such a way that satisfies this clause, whereas, the remaining two literals per each clause are allowed to take values that does not satisfy it. As a consequence, each clause is satisfied by the variables chosen in this way, which proves correctness.

This implies that the $2$ -slice (for ${\#\mathsf{splits}}\text{-}\mathsf{dc}$ ), $4$ -slice (for ${\#\mathsf{free\text{-}variables}}\text{-}\mathsf{dc}$ as well as ${\#\mathsf{variables}}\text{-}\mathsf{dc}$ ), $0$ -slice (for ${\#\forall}\text{-}\mathsf{dc}$ ), and $1$ -slice (for ${\mathsf{dep\text{-}arity}}\text{-}\mathsf{dc}$ ) are NP-complete. Consequently, the paraNP-hardness for these cases follow. Finally, the case for $\mathsf{tw}(\mathcal{A})$ also follows due to the reason that the vocabulary of the reduced structure is empty. As a consequence, our definition 2.6 yields a tree decomposition of width $1$ trivially as no elements of the universe are related.

This completes the proof to our lemma.

Remark 3.7.

Recall that $|\Phi|$ as a parameter for $\mathsf{dc}$ does not make sense as the input consists of $\langle\mathcal{A},T\rangle$ . That is, the formula $\Phi$ is already fixed which is stronger than fixing the size of $\Phi$ .

We now prove the only tractable case for the data complexity.

Lemma 3.8.

${{|\mathcal{A}|}}\text{-}\mathsf{dc}\in\textbf{FPT}$ .

Proof 3.9.

Notice first that restricting the universe size $|\mathcal{A}|$ polynomially bounds the teamsize $|T|$ , due to Lemma 3.1. This implies that the size of whole input is (polynomially) bounded by the parameter $|\mathcal{A}|$ . The result follows trivially because any PP $P$ is FPT when the input size is bounded by the parameter [8].

Lemma 3.10.

${|T|}\text{-}\mathsf{dc}$ is paraNP-complete.

Proof 3.11.

For a fixed sentence $\Phi\in\mathcal{D}$ (that is, with no free variables) and for all models $\mathcal{A}$ and team $T$ we have that $(\mathcal{A},T)\models\Phi\iff(\mathcal{A},\{\emptyset\})\models\Phi$ . As a result, the problem $\leq^{\textbf{FPT}}$ -reduces to the model checking problem with $|T|=1$ . Consequently, 1-slice of ${|T|}\text{-}\mathsf{dc}$ is NP-complete because model checking for a fixed $\mathcal{D}$ -sentence is also NP-complete [27]. This gives paraNP-hardness.

For the membership, note that given a structure $\mathcal{A}$ and a team $T$ then for a fixed formula $\Phi$ the question whether $(\mathcal{A},T)\models\Phi$ is in NP. Consequently, giving paraNP-membership.

A comparison with the propositional dependence logic ( $\mathcal{PDL}$ ) at this point might be interesting. If the formula size is a parameter then the model checking for $\mathcal{PDL}$ can be solved in FPT-time [20]. However, this is not the case for $\mathcal{D}$ even if the formula is fixed in advance.

3.2 Expression and Combined Complexity ( $\mathsf{ec},\mathsf{cc}$ )

Now we turn towards the expression and combined complexity of model checking for $\mathcal{D}$ . Here again, in most cases the problem is still intractable for the combined complexity. However, expression complexity when parameterized by the formula size ( $|\Phi|$ ) and the total number of variables ( $\#\mathsf{variables}$ ) yields membership in FPT. Similar to the previous section, we first present results that directly translate from the known reductions for proving the NEXP-completeness for $\mathcal{D}$ .

Lemma 3.12.

Let $k\in\{\,{|\mathcal{A}|},\mathsf{tw}(\mathcal{A}),|T|,\#\mathsf{free\text{-}variables}\,\}$ . Then both ${k}\text{-}\mathsf{cc}$ and ${k}\text{-}\mathsf{ec}$ are paraNEXP-complete.

Proof 3.13.

In the classical setting, NEXP-completeness of the expression and the combined complexity for $\mathcal{D}$ was shown by Grädel [12, Theorem 5.1]. This immediately gives membership in paraNEXP. Interestingly, the universe in the reduction consists of $\{0,1\}$ with empty vocabulary and the formula obtained is a $\mathcal{D}$ -sentence. This implies that $2$ -slice (for $|\mathcal{A}|$ ), $1$ -slice (for $\mathsf{tw}(\mathcal{A})$ ), $1$ -slice (for $|T|$ ), and $0$ -slice (for the number of free variables) are NEXP-complete. As a consequence, paraNEXP-hardness for the mentioned cases follows and this completes the proof.

For the number of splits as a parameterization, we only know that this is also highly intractable, with the precise complexity open for now.

Lemma 3.14.

${\#\mathsf{splits}}\text{-}\mathsf{ec}$ and ${\#\mathsf{splits}}\text{-}\mathsf{cc}$ are both paraPSPACE-h.

Proof 3.15.

Consider the equivalence of $\{\exists,\forall,\land\}\text{-}\mathcal{FO}\text{-}\mathrm{MC}$ to quantified constraint satisfaction problem (QCSP) [22, p. 418]. That is, the fragment of $\mathcal{FO}$ with only operations in $\{\exists,\forall,\land\}$ allowed. Then QCSP asks, whether the conjunction of quantified constraints ( $\mathcal{FO}$ -relations) is true in a fixed $\mathcal{FO}$ -structure $\mathcal{A}$ . This implies that already in the absence of a split operator (even when there are no dependence atoms), the model checking problem is PSPACE-hard. Consequently, the mentioned results follow.

The formula size as a parameter presents varying behaviour depending upon if we consider the expression or the combined complexity.

Lemma 3.16.

${|\Phi|}\text{-}\mathsf{cc}$ is paraNP-complete.

Proof 3.17.

Notice that, due to Lemma 3.1, the size $k$ of a formula $\Phi$ also bounds the maximum number of free variables in any subformula of $\Phi$ . This gives the membership in conjunction with [12, Theorem 5.1]. That is, the combined complexity of $\mathcal{D}$ is NP-complete if maximum number of free variables in any subformuala of $\Phi$ is fixed. The lower bound follows because of the construction by Kontinen [16] (see also Lemma 3.5) since for a fixed formula (of fixed size), the problem is already NP-complete.

Lemma 3.18.

${|\Phi|}\text{-}\mathsf{ec}$ is in FPT.

Proof 3.19.

Recall that in expression complexity, the team $T$ and the structure $\mathcal{A}$ are fixed. Whereas, the size of the input formula $\Phi$ is a parameter. The result follows trivially because any PP $P$ is FPT when the input size is bounded by the parameter.

The expression complexity regarding the number of universal quantifiers as a parameter drops down to paraNP-completeness, which is still intractable but much lower than paraNEXP-completeness. However, regarding the combined complexity we can only prove the membership in XNP, with paraNP-lower bound.

Lemma 3.20.

${\#\forall}\text{-}\mathsf{ec}$ is paraNP-complete.

Proof 3.21.

We first prove the lower bound through a reduction form the satisfiability problem for propositional dependence logic ( $\mathcal{PDL}$ ). That is, given a $\mathcal{PDL}$ -formula $\phi$ , whether there is a team $T$ such that $T\models\phi$ ? Let $\phi$ be a $\mathcal{PDL}$ -formula over propositional variables $p_{1},\ldots,p_{n}$ . For $i\leq n$ , let $x_{i}$ denote a variable corresponding to the proposition $p_{i}$ . Let $\mathcal{A}=\{0,1\}$ be the structure over empty vocabulary. Clearly $\phi$ is satisfiable iff $\exists p_{1}\ldots\exists p_{n}\phi$ is satisfiable iff $(\mathcal{A},\{\emptyset\})\models\exists x_{1}\ldots\exists x_{n}\phi^{\prime}$ , where $\phi^{\prime}$ is a $\mathcal{D}$ -formula obtained from $\phi$ by simply replacing each proposition $p_{i}$ by the variable $x_{i}$ . Notice that the reduced formula does not have any universal quantifier, that is $\#\forall(\phi^{\prime})=0$ . This gives paraNP-hardness since the satisfiability for $\mathcal{PDL}$ is NP-complete [18].

For membership, notice that a $\mathcal{D}$ -sentence $\Phi$ with $k$ universal quantifiers can be reduced in P-time to an $\mathcal{ESO}$ -sentence $\Psi$ of the form $\exists f_{1}\ldots\exists f_{r}\forall x_{1}\ldots\forall x_{k}\psi$ [5, Cor. 3.9], where $\psi$ is a quantifier free $\mathcal{FO}$ -formula, $r\in\mathbb{N}$ , and each function symbol $f_{i}$ is at most $k$ -ary for $1\leq i\leq r$ . Finally, $(\mathcal{A},\{\emptyset\})\models\Phi\iff\mathcal{A}\models\bigvee\limits_{f_{1}}\ldots\bigvee\limits_{f_{r}}\forall x_{1}\ldots\forall x_{k}\psi^{\prime}$ . Where the latter question can be solved by guessing an interpretation for each function symbol $f_{i}$ and $i\leq r$ . This requires $r\cdot|\mathcal{A}|^{k}$ guessing steps, and can be achieved in paraNP-time for a fixed structure $\mathcal{A}$ (as we consider expression complexity). Consequently, the membership in paraNP follows. Notice that the arity of function symbols in the paraNP-membership above is bounded by $k$ if $\Phi$ is a $\mathcal{D}$ -sentence. However, if $\Phi$ is a $\mathcal{D}$ -formulas with $m$ free variables then the arity of function symbols as well as the number of universal quantifiers in the reduction, both are bounded by $k+m$ where $k=\#\forall(\Phi)$ and $m=\#\mathsf{free\text{-}variables}(\Phi)$ . Nevertheless, recall that for $\mathsf{ec}$ , the team is also fixed. Moreover, due to Lemma 3.1 the collection of free variables in $\Phi$ has constant size. This implies that the reduction above provides an $\mathcal{ESO}$ -sentence with $k+m$ universal quantifiers as well as function symbols of arity $k+m$ at most. Finally, guessing the interpretation for functions still takes paraNP-steps (because $m$ is constant) and consequently, we get paraNP-membership for open formulas as well.

The following corollary immediately follows from the proof above.

Corollary 3.22.

${(\#\forall+\#\mathsf{free\text{-}variables})}\text{-}\mathsf{ec}$ is paraNP-complete.

Lemma 3.23.

${\#\forall}\text{-}\mathsf{cc}$ is paraNP-hard. Moreover, for sentences of $\mathcal{D}$ , ${\#\forall}\text{-}\mathsf{cc}$ is in XNP.

Proof 3.24.

The paraNP-lower bound follows due to the fact that the expression complexity of $\mathcal{D}$ is already paraNP-complete when parameterized by $\#\forall$ (Lemma 3.20).

For sentences, similar to the proof in Lemma 3.20, a $\mathcal{D}$ -sentence $\Phi$ can be translated to an equivalent $\mathcal{ESO}$ -sentence $\Psi$ in polynomial time. However, if the structure is not fixed as for expression complexity, then the computation of interpretations for functions can no longer be done in paraNP-time, but requires non-deterministic $|\mathcal{A}|^{k}$ -time for each guessed function, where $k=\#\forall$ . Consequently, we reach only membership in XNP for sentences.

For open formulas, we do not know if ${\#\forall}\text{-}\mathsf{cc}$ is also in XNP. Our proof technique does not immediately settle this case as the team is not fixed for $\mathsf{cc}$ .

Similar to the case of universal quantifiers, the arity as a parameter also reduces the complexity but not as much as the universal quantifiers. Moreover, the precise combined complexity when parameterized by the arity is also open.

Lemma 3.25.

${\mathsf{dep\text{-}arity}}\text{-}\mathsf{ec}$ is paraPSPACE-complete.

Proof 3.26.

Notice that a $\mathcal{D}$ -sentence $\Phi$ with $k$ -ary dependence atoms can be reduced in P-time to an $\mathcal{ESO}$ -sentence $\Psi$ of the form $\exists f_{1}\ldots\exists f_{r}\psi$ [5, Thm. 3.3], where $\psi$ is an $\mathcal{FO}$ -formula and each function symbol $f_{i}$ is at most $k$ -ary for $1\leq i\leq r$ . Finally, $\mathcal{A}\models\Phi\iff\mathcal{A}\models\bigvee\limits_{f_{1}}\ldots\bigvee\limits_{f_{r}}\psi^{\prime}$ . That is, one needs to guess the interpretation for each function symbol $f_{i}$ , which can be done in paraNP-time. Finally, evaluating an $\mathcal{FO}$ -formula $\psi^{\prime}$ for a fixed structure $\mathcal{A}$ can be done in PSPACE-time. This yields membership in paraPSPACE. Moreover, if $\Phi$ is an open $\mathcal{D}$ -formula then the result follows due to a similar discussion as in the prof of Lemma 3.20.

For hardness, notice that the expression complexity of $\mathcal{FO}$ is PSPACE-complete. This implies that already in the absence of any dependence atoms, the complexity remains PSPACE-hard, as a consequence, the $0$ -slice of ${\mathsf{dep\text{-}arity}}\text{-}\mathsf{ec}$ is PSPACE-hard.

This proves the desired result.

The combination ( $\mathsf{dep\text{-}arity}+\#\mathsf{free\text{-}variables}$ ) also does not lower the expression complexity as discussed before in the case of $\#\forall$ .

Corollary 3.27.

${(\mathsf{dep\text{-}arity}+\#\mathsf{free\text{-}variables})}\text{-}\mathsf{ec}$ is paraPSPACE-complete.

Lemma 3.28.

${\mathsf{dep\text{-}arity}}\text{-}\mathsf{cc}$ is paraPSPACE-hard.

Proof 3.29.

Consider the fragment of $\mathcal{D}$ with only dependence atoms of the form ${\mathsf{dep}}({};{x})$ , the so-called constancy logic. The combined complexity of constancy logic is PSPACE-complete [12, Theorem 5.3]. This implies that the $0$ -slice of ${\mathsf{dep\text{-}arity}}\text{-}\mathsf{cc}$ is PSPACE-hard, proving the result.

The combined complexity of model checking for constancy logic is PSPACE [12, Thm. 5.3]. Aiming for an paraPSPACE-upper bound via squeezing the fixed arity of dependence atoms (in some way) into constancy atoms is unlikely to happen as $\mathcal{D}$ captures $\mathcal{ESO}$ whereas constancy logic for sentences (and also open formulas) collapses to $\mathcal{FO}$ [10].

Notice that a similar reduction as in the proof of Lemma 3.20 holds from $\mathcal{PL}$ , in which both parameters ( $\#\forall$ and $\mathsf{dep\text{-}arity}$ ) are bounded. This implies that there is no hope for tractability even when both parameters are considered together. That is, the complexity of expression complexity remains paraNP-complete when parameterized by the combination of parameters ( $\#\forall$ , $\mathsf{dep\text{-}arity}$ ).

Corollary 3.30.

${(\#\forall+\mathsf{dep\text{-}arity})}\text{-}\mathsf{ec}$ is also paraNP-complete.

Finally, for the parameter total number of variables, the expression complexity drops to FPT whereas, the combined complexity drops to paraNP-completeness. The case of expression complexity is particularly interesting. This is due to the reason that it was posed as an open question in [28] whether the expression complexity of the fixed variable fragment of dependence logic ( $\mathcal{D}^{k}$ ) is NP-complete similar to the case of the combined complexity therein. We answer this negatively by stating FPT-membership for ${\#\mathsf{variables}}\text{-}\mathsf{ec}$ , which as a corollary proves that the expression complexity of $\mathcal{D}^{k}$ is in P for each $k\geq 1$ .

Lemma 3.31.

${\#\mathsf{variables}}\text{-}\mathsf{cc}$ is paraNP-complete.

Proof 3.32.

Notice that if the total number of variables in $\Phi$ is fixed, then the number of free variables in any subformula $\psi$ of $\Phi$ is also fixed. This implies the membership in paraNP due to [12, Theorem 5.1]. On the other hand, by [28, Theorem 3.9.6] we know that the combined complexity of $\mathcal{D}^{k}$ is NP-complete. This implies that for each $k$ , the $k$ -slice of the problem is NP-hard. This gives the desired lower bound.

Lemma 3.33.

${\#\mathsf{variables}}\text{-}\mathsf{ec}$ is FPT.

Proof 3.34.

Given a formula $\Phi$ of dependence logic with $k$ variables, we can construct an equivalent formula $\Psi$ of $\mathcal{ESO}^{k+1}$ in polynomial time [28, Theorem 3.3.17]. Moreover, since the structure $\mathcal{A}$ is fixed, there exists a reduction of $\Psi$ to an $\mathcal{FO}$ -formula $\psi$ with $k+1$ variables (big disjunction on the universe elements for each second order existential quantifier). Finally, the model checking for $\mathcal{FO}$ -formulas with $k$ variables is solvable in time $O(|\psi|\cdot|A|^{k})$ [17, Prop 6.6]. This implies the membership in FPT.

Corollary 3.35.

The expression complexity of $\mathcal{D}^{k}$ is in P for every $k\geq 1$ .

Proof 3.36.

Since both, the number of variables and the universe size is fixed. The runtime of the form $O(|\psi|\cdot|A|^{k})$ in Lemma 3.33 implies membership in P.

4 Conclusion

Figure 3: Complexity classification overview for model checking problem of dependence logic, that takes grouping of parameters (quantitative, size, structural) and complexity classes into account.

In this paper, we started the parameterized complexity classification of model checking for dependence logic $\mathcal{D}$ with respect to nine different parameters (see Table 2 for an overview of the results). In Fig. 3 we depict a different kind of presentation of our results that also takes the grouping of parameters into quantitative, size related, and structural into account. The data complexity of $\mathcal{D}$ shows a dichotomy (FPT vs./ paraNP-complete), where surprisingly there is only one case ( ${|\mathcal{A}|}$ ) where one can reach FPT. This is even more surprising in the light of the fact that the expression ( $\mathsf{ec}$ and the combined ( $\mathsf{cc}$ ) complexities under the same parameter are still highly intractable. Furthermore, there are parameters when $\mathsf{cc}$ and $\mathsf{ec}$ vary in the complexity ( $\#\mathsf{variables}$ ). The combined complexity of $\mathcal{D}$ stays intractable under any of the investigated parameterizations. It might be interesting to study combination of parameters and see their joint effect on the complexity (yet, Corollaries 3.22, 3.27, 3.30 tackle already some cases).

We want to close this presentation with some further questions:

•

What other parameters could be meaningful (e.g., number of conjunction, number of existential quantifiers, treewidth of the formula)?
•

What is the exact complexity of $\#\forall$ - $\mathsf{cc}$ , $\#\mathsf{splits}$ - $\mathsf{ec}$ /- $\mathsf{cc}$ , $\mathsf{dep\text{-}arity}$ - $\mathsf{cc}$ ?
•

The parameterized complexity analysis for other team-based logics, such as independence logic and inclusion logic.

References

[1] Stefan Arnborg, Derek G. Corneil, and Andrzej Proskurowski. Complexity of finding embeddings in a $k$ -tree. SIAM Journal on Algebraic Discrete Methods, 2(8):277––284, 1987. doi:10.1137/0608024.
[2] Hans L. Bodlaender. A tourist guide through treewidth. Acta Cybern., 11(1-2):1–21, 1993.
[3] Hans L. Bodlaender. Discovering treewidth. In SOFSEM, volume 3381 of Lecture Notes in Computer Science, pages 1–16. Springer, 2005.
[4] Rodney G. Downey and Michael R. Fellows. Fundamentals of Parameterized Complexity. Texts in Computer Science. Springer, 2013. doi:10.1007/978-1-4471-5559-1.
[5] Arnaud Durand and Juha Kontinen. Hierarchies in dependence logic. ACM Transactions on Computational Logic (TOCL), 13(4):31, 2012. doi:10.1145/2362355.2362359.
[6] Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995.
[7] Michael Elberfeld, Christoph Stockhusen, and Till Tantau. On the space and circuit complexity of parameterized problems: Classes and completeness. Algorithmica, 71(3):661–701, 2015.
[8] Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2006. doi:10.1007/3-540-29953-X.
[9] Pietro Galliani. Inclusion and exclusion dependencies in team semantics: On some logics of imperfect information. Annals of Pure and Applied Logic, 163(1):68 – 84, 2012. doi:10.1016/j.apal.2011.08.005.
[10] Pietro Galliani. On strongly first-order dependencies. In Dependence Logic, pages 53–71. Springer, 2016.
[11] Pietro Galliani and Lauri Hella. Inclusion Logic and Fixed Point Logic. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), volume 23 of Leibniz International Proceedings in Informatics (LIPIcs), pages 281–295, Dagstuhl, Germany, 2013. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: http://drops.dagstuhl.de/opus/volltexte/2013/4203, doi:10.4230/LIPIcs.CSL.2013.281.
[12] Erich Grädel. Model-checking games for logics of imperfect information. Theor. Comput. Sci., 493:2–14, 2013. doi:10.1016/j.tcs.2012.10.033.
[13] Erich Grädel and Jouko Väänänen. Dependence and independence. Studia Logica, 101(2):399–410, 2013. doi:10.1007/s11225-013-9479-2.
[14] Miika Hannula, Juha Kontinen, Jan Van den Bussche, and Jonni Virtema. Descriptive complexity of real computation and probabilistic independence logic. In LICS, pages 550–563. ACM, 2020.
[15] Miika Hannula, Juha Kontinen, Jonni Virtema, and Heribert Vollmer. Complexity of propositional logics in team semantic. ACM Trans. Comput. Log., 19(1):2:1–2:14, 2018.
[16] Jarmo Kontinen. Coherence and computational complexity of quantifier-free dependence logic formulas. Studia Logica, 101(2):267–291, 2013. doi:10.1007/s11225-013-9481-8.
[17] Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: http://www.cs.toronto.edu/%7Elibkin/fmt, doi:10.1007/978-3-662-07003-1.
[18] Peter Lohmann and Heribert Vollmer. Complexity results for modal dependence logic. Stud Logica, 101(2):343–366, 2013. doi:10.1007/s11225-013-9483-6.
[19] Martin Lück. Canonical models and the complexity of modal team logic. Log. Methods Comput. Sci., 15(2), 2019.
[20] Yasir Mahmood and Arne Meier. Parameterised complexity of model checking and satisfiability in propositional dependence logic. In Foundations of Information and Knowledge Systems - 11th International Symposium, FoIKS 2020, Dortmund, Germany, February 17-21, 2020, Proceedings, pages 157–174, 2020. doi:10.1007/978-3-030-39951-1\_10.
[21] Yasir Mahmood and Jonni Virtema. Parameterised complexity of propositional logic in team semantics. CoRR, abs/2105.14887, 2021.
[22] Barnaby Martin. First-order model checking problems parameterized by the model. In CiE, volume 5028 of Lecture Notes in Computer Science, pages 417–427. Springer, 2008.
[23] Arne Meier and Christian Reinbold. Enumeration complexity of poor man’s propositional dependence logic. In FoIKS, volume 10833 of Lecture Notes in Computer Science, pages 303–321. Springer, 2018.
[24] Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994.
[25] Neil Robertson and Paul D. Seymour. Graph minors. III. planar tree-width. J. Comb. Theory, Ser. B, 36(1):49–64, 1984.
[26] Marko Samer and Stefan Szeider. Fixed-parameter tractability. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 425–454. IOS Press, 2009.
[27] Jouko A. Väänänen. Dependence Logic - A New Approach to Independence Friendly Logic, volume 70 of London Mathematical Society student texts. Cambridge University Press, 2007. URL: http://www.cambridge.org/de/knowledge/isbn/item1164246/?site_locale=de_DE.
[28] Jonni Virtema. Approaches to Finite Variable Dependence: Expressiveness and Computational Complexity. PhD thesis, School of Information Sciences of the University of Tampere, 2014. Available online at https://trepo.tuni.fi/handle/10024/95328.