Michael Benedikt

Pierre Bourhis

Michael Vanden Boom

A step up in expressiveness of decidable fixpoint logics

Guardedness restrictions are one of the principal means to obtain decidable logics -operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic.

Introduction

We are interested in expressive logics for which static analysis problems such as satisfiability are decidable. One way to achieve decidability is via guardedness restrictions. The Guarded Fragment (GF) [START_REF] Andréka | Modal languages and bounded fragments of predicate logic[END_REF] is a fragment of first-order logic obtained by requiring in existential quantification 9x. (x) that be of the form R(x)^ 0 (x), where R(x) is an atom containing all free variables of 0 , and requiring in universal quantification that be of the form R(x) ! 0 (x), where R is as above. The Guarded Negation Fragment (GNF) [START_REF] Bárány | Guarded negation[END_REF] is an even more expressive decidable language, allowing unrestricted existential quantification but restricting negation to be of the form R(x) ^¬ 0 (x), with R as above.

Of course, there are other paradigms for decidability within first-order logic, such as restricting to two variables [START_REF] Scott | A decision method for validity of sentences in two variables[END_REF]. A particularly attractive feature of guarded logics is that, unlike with the two variable fragment [START_REF] Grädel | Undecidability results on twovariable logics[END_REF], decidability can be extended to give decidable fragments of least fixpoint logic (LFP). LFP is the natural extension of first-order logic with a fixpoint constructor. Given a formula (x 1 . . . x m , y 1 . . . y n ) over some signature in which an m-ary second-order variable X occurs freely and positively in , and given a -structure A and some fixed valuation ⇢ for y, we can define a new m-ary relation: the relation is defined as the limit of a monotone sequence X 0 . . ., starting with X 0 = ; and then setting X i+1 to be the set of a such that holds when extending ⇢ with the interpretation of X as X i and x as a. Emphasizing the distinction between x and y, we call x the fixpoint variables and y the param-[Copyright notice will appear here once 'preprint' option is removed.] eter variables. Informally, during the fixpoint process, the fixpoint variables change in each iteration, while the parameter variables stay the same. Formulas in LFP can use relations defined using a fixpoint constructor like this, in addition to relations in .

Guarded Fixpoint Logic (denoted GFP or µGF) [START_REF] Grädel | Guarded fixed point logic[END_REF] extends GF with a fixpoint operator while maintaining decidability. The fixpoint constructor is restricted in two ways: the parameter variables y must be empty, and the fixpoint relation itself cannot be used as a guard. Guarded Negation Fixpoint Logic (GNFP) [START_REF] Bárány | Guarded negation[END_REF] adds fixpoint constructors to GNF with similar restrictions.

It is known that the second restriction on these fixpoint logics is essential for decidability [START_REF] Grädel | Guarded fixed point logic[END_REF]. But what about the first? It certainly seemed important to the proofs of decidability; [START_REF] Grädel | Back and forth between guarded and modal logics[END_REF] states It should be stressed that the presence of extra first-order parameters in fixed-point operations as well as the use of second-order variables and fixed points as guards is disallowed in µGF. These restrictions are essential for keeping the semantics invariant under guarded bisimulation. For instance, with the use of a first-order parameter ... one can define the transitive closure of a binary relation ... However, the transitive closure query is not invariant under guarded bisimulation and it is known that adding transitive closure to GF produces an undecidable logic [START_REF] Grädel | On the restraining power of guards[END_REF].

In this paper we show that the parameter restriction can indeed be loosened. We introduce a variation of GNFP, denoted GNFP-UP, where the fixpoint variables of any fixpoint need to be guarded, but the fixpoint can carry additional unguarded parameters. One can write a GNFP-UP formula holding on the transitive closure of a binary relation. But such a formula cannot be used as a guard, and thus assertions that a binary relation is transitive (the key to undecidability in [START_REF] Grädel | On the restraining power of guards[END_REF]) cannot be expressed. GNFP-UP can express many properties related to transitivity, such as assertions of paths with certain properties (see the discussion of conjunctive regular path queries with inverse in Section 3).

The decidability of GFP is proven using an elegant high-level argument [START_REF] Grädel | Guarded fixed point logics and the monadic theory of countable trees[END_REF]: one shows that satisfiable formulas must have treelike models, and thus satisfiability can be reduced to satisfiability of a Monadic Second Order Logic sentence over trees, decidable via Rabin's theorem [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. A finer argument shows that from a GFP formula one can e↵ectively create a tree automaton A which is non-empty exactly when is satisfiable. By analyzing the complexity of this automaton construction, Grädel and Walukiewicz derived a 2-ExpTime bound on satisfiability [START_REF] Grädel | Guarded fixed point logic[END_REF].

We begin by showing that the high-level argument easily extends to give decidability of GNFP-UP. The finer analysis of the complexity of GNFP-UP satisfiability requires more work. Because of negation and quantification in our logic, one might expect that the complexity would be a tower of exponentials based on the quantifier alternation. However, we show that the complexity is controlled by the parameter depth of the formula: informally, this is a number that measures the number of times we change parameters while passing from a formula to a subformula. We give elementary bounds for each parameter depth, while proving that the complexity is non-elementary (but still primitive recursive) when the depth is not restricted. Each parameter depth includes formulas of arbitrary quantifier alternation; we avoid unnecessary exponential blowups by identifying pieces of the GNFP-UP formulas that behave like GNFP. We also show that some interesting logics fit within low parameter depth.

Finally, we describe how our translation to automata can be modified to show decidability of the boundedness problem, a quantitative analog of satisfiability that asks if a fixpoint can be replaced by a fixed number of unfoldings. Our solution to the boundedness problem can be applied to decide whether certain GNFP-UPexpressible formulas can be rewritten in first-order logic.

Preliminaries

We consider signatures with a finite set of relations and constants. We write const( ) for the set of constants in the signature .

Least fixed point logic (LFP) over is the extension of firstorder logic over with the following formation rule: if (y, z, Y, Z) is a formula in which Y is a free second-order variable of arity |y| that appears only positively, and t is a tuple of variables and constants of length |y|, then [lfp Y,y . ](t) is also a formula. Informally, it asserts that t is in the least fixpoint induced by . The parameter variables of this formula are z -the free variables of other than y. In this paper, we emphasize the parameters by writing [lfp z Y,y . ], and reserve [lfp Y,y . ] for the case when there are no parameters.

The semantics are standard: since (y, z, Y, Z) is positive in Y, it induces a monotone operator U 7 ! O A,v,V (U) := {u : A, u, v, U, V | = (y, z, Y, Z)} on every structure A with valuation v for z and V for Z. Hence, this operator has a unique least fixpoint, denoted 1 (A, v, V), and this can be obtained as the union of its fixpoint approximants (A, v, V) over all ordinals , where 0 (A, v, V) := ;

+1 (A, v, V) := O A,v,V ( (A, v, V)) (A, v, V) := S 0 < 0 (A, v, V)
where is a limit ordinal.

The semantics of the least fixpoint formulas is defined such that

A, v, V | = [lfp z Y,y . ](t) i↵ t 2 1 (A, v, V) = S 2Ord (A, v, V).
Free and bound variables The notion of free vs. bound secondorder variables is standard. In particular, Y is free in (y, z, Y, Z) but bound in [lfp z Y,y . ](t). We assume no second-order variable Y is bound by more than one fixpoint operator, so each bound second-order variable Y identifies a unique fixpoint. If Y identifies a fixpoint with parameters z, then params(Y) := z, the parameters associated with the second-order variable Y.

We use free( ) to denote the free first-order variables in . It is defined recursively. For atoms Rt with R 2 and t a tuple consisting of constants and variables, the free first-order variables are just the variables in t. For Y t with Y a second-order variable, free(Y t) is the union of the variables in t and params(Y). For boolean connectives, free( 1 ^ 2 ) = free( 1 _ 2 ) = free( 1 ) [ free( 2 ), and free(¬ ) = free( ). For quantification, free(9x. ) = free( ) \ {x}. Finally, for [lfp z Y,y . ](t), the free first-order variables consist of the parameter variables z together with the variables in t.

The parameters in consists of the union of params(Y) for all second-order variables Y occurring in ; we let params( ) denote the subset of these parameters that occur free in .

GNFP-UP Guarded negation fixpoint logic with unguarded parameters (GNFP-UP) is the fragment of LFP that allows unguarded parameter variables in fixpoint definitions, but requires fixpoint variables and negation to be guarded. Formally, a GNFP-UP[ ] formula is generated recursively from the following grammar:

::= R t | Y t | ^ | _ | 9y. | ↵ ^¬ where free( ) ✓ free(↵) | [lfp z
Y,y . gdd(y) ^ (y, z, Y, Z)](t) for positive in Y where t is a tuple of variables or constants, Rt and ↵ are atoms using a relation in or =, and gdd(y) is defined below.

Guardedness The guardedness predicate gdd(y) asserts y is guarded by an atom in or =. It can be understood as an abbreviation for the disjunction of existentially quantified atoms that use a relation from or = and involve all of the variables in y. Because of this, only guarded relations can be defined using fixpoints in GNFP-UP: i.e. any tuple of elements in the relation defined by the fixpoint formula must already be guarded by an atom in the base signature . Note that the relations defined using a fixpoint operator cannot be used as guards.

The parameters z are not required to be guarded in the fixpoint definition. However, for the purposes of negation, parameters are treated like other variables and must be guarded. For example, if ↵(x) is an atomic formula over , and Y identifies a fixpoint with parameters z, then ↵(x) ^¬Y x is not permitted since Y implicitly uses parameters z and these parameters are not guarded by ↵ (since the free variables in Y x are really x and z).

A formula that includes free first-order variables x is xguarded if it is logically equivalent to gdd(x) ^ . If free( ) = x and is x-guarded, then we say it is answer-guarded. Sentences or formulas with one free variable are always answer-guarded since we can use a trivial guard like x = x. For readability purposes, we often omit such trivial guards.

Simultaneous fixpoints We will also allow simultaneous fixpoints [lfp z Y i ,y i .S ](t) where S = 8 > > < > > : Y 1 , y 1 := gdd(y 1 ) ^ 1 (y 1 , z, Y 1 , . . . , Y j , Z) . . . Y j , y j := gdd(y j ) ^ j (y j , z, Y 1 , . . . , Y j , Z) is a system of mutually defined equations Y i , y i := i such that i 2 GNFP-UP, and Y 1 , . . . , Y j occur only positively in i . Each i utilizes the same parameters z, but di↵erent fixpoint variables y i . Such a system defines a monotone operation on vectors of relations, and [lfp z Y i ,y i .S ](t) expresses that t is a tuple in the i-th component of the least fixpoint defined by this operation; Y i is the distinguished goal predicate in [lfp z Y i ,y i .S ](t). Allowing simultaneous fixpoints does not change the expressivity of the logic, since they can be eliminated in favor of traditional fixpoints [START_REF] Arnold | Rudiments of mu-calculus[END_REF], with a possible exponential blow-up in size. However, it is often more convenient to work directly with these simultaneous fixpoints (see Example 4).

GNFP-UP vs. GNFP A good example to keep in mind is that GNFP-UP can express the transitive closure of a binary relation R. Y,y . R yz _ 9y 0 .(Ryy 0 ^Yy 0 )](x) . Observe that has two free variables, the variable x being tested in the fixpoint and the parameter variable z. The formula (x, z) expresses that there is some R-path from element x to z, i.e. (x, z) is in the transitive closure of R.

We can express that x participates in an R-cycle by using the formula (x, x).

We cannot express that the structure is strongly R-connected, since this would require unguarded negation, but we can say every pair of guarded elements is R-connected: ¬9xz.(gdd(x, z) ¬ (x, z)) 2 GNFP-UP.

The sentence ¬9xz.( (x, z) ^¬Rxz) _ (Rxz ^¬ (x, z)) that says R is transitively closed is not in GNFP-UP, since we cannot use the fixpoint relation defined by as a guard for ¬Rxz.

In LFP, it is always possible to eliminate the use of parameters by increasing the arity of the defined fixpoint predicates and passing the parameters explicitly in the fixpoint. This is not usually possible in our context, because the fixpoint variables are required to be guarded. Indeed, it can be shown that the transitive closure of a binary relation R cannot be expressed in GNFP (the fragment of GNFP-UP in which fixpoints do not use any parameters). Proposition 2. GNFP-UP is strictly more expressive than GNFP, even over finite structures.

Normal form A conjunctive query (CQ) is 9y. for a conjunction of atoms. A union of conjunctive queries (UCQ) is a disjunction of CQs. Such queries are expressible in GNF. It is helpful to work with GNFP-UP in a normal form that highlights the fact that GNFP-UP formulas can be built up from UCQ-shaped formulas using guarded negation and guarded fixpoints with parameters.

Formally, A normal form GNFP-UP[ ] formula or is generated recursively from the following grammars:

::= W i 9y i . V j i j ::= R t | Y t | ↵ ^¬ where free( ) ✓ free(↵) | [lfp z
Ym,y m .S ](t) where t is a tuple of variables or constants, Rt and ↵ are atoms using a relation in or =, and S is a system with equations of the form Y, y := gdd(y) ^ (y, z, Y, Z), as described earlier.

Any GNFP-UP formula can be converted into normal form in a canonical way. The width of a GNFP-UP formula is the maximum number of free variables used in any subformula after the formula is converted into normal form. We write (GNFP-UP) k [ ] for GNFP-UP formulas of width k.

Other guarded logics with parameters We could consider variants of other guarded logics with parameters. The unary negation fixpoint logic with unguarded parameters (UNFP-UP) is the fragment of GNFP-UP where only formulas with at most one free variable are negated, and the fixpoint predicates are monadic but may still carry any number of unguarded parameters. The formula (x, z) in Example 1 is in UNFP-UP.

We could also consider GFP-UP, the variant of GFP with parameters in the fixpoints, but where these parameters still need to be guarded if appearing under a quantification (this mimics the way we have added parameters to GNFP). The formula in Example 1 is not in GFP-UP since the quantification in 9y 0 .(Ryy 0 ^Yy 0 ) is not correctly guarded: GFP-UP would require something like 9y 0 .(Gzy 0 ^Yy 0 ), which includes a guard that covers not only y 0 but also the parameter z implicit in the fixpoint predicate Y. However, adding parameters to GFP in this way does not increase expressivity: Proposition 3. For every answer-guarded GFP-UP formula , we can construct in linear time an equivalent GFP formula 0 using fixpoint predicates of higher arity.

This may explain why parameters were not considered further in [START_REF] Grädel | Guarded fixed point logic[END_REF][START_REF] Grädel | Back and forth between guarded and modal logics[END_REF]: when they are introduced to GFP in their full power, it leads to undecidability, and when they are introduced in this more restrictive way, they do not add any expressive power. This is in contrast to GNFP, where we can add parameters in a way that strictly increases expressivity while still retaining decidability.

Organization In Section 3, we give some examples illustrating the expressive power of GNFP-UP. We also define the parameter depth, a key measure of how complicated a GNFP-UP formula is. We then argue in Section 4 that GNFP-UP has tree-like models, which makes satisfiability and boundedness amenable to tree automata techniques. The main technical work is described in Sections 5 and 6 where we describe the automata tools needed for GNFP-UP. Finally, in Sections 7 and 8, we use this automata machinery to study static analysis problems like satisfiability and boundedness.

Expressivity examples

In this section, we give some examples showing that GNFP-UP subsumes and extends a wide range of logics. This provides evidence of its power, and explains some of the good properties of these previously-studied logics.

In order to help study the power of GNFP-UP, we first define a way to measure how the parameters are used. Roughly speaking, the parameter depth is the maximum number of nested parameter changes. We define pdepth z (⌘) inductively as follows:

pdepth z (R t) = pdepth z (Y t) := 0 pdepth z (↵ ^¬ ) := pdepth z\free( ) ( ) pdepth z ( W i 9x i . V j i j ) := max i p i s.t. p i := 8 > > < > > : 1 + max j pdepth params( i j ) ( i j ) if 9 j. params( i j ) * z max j pdepth z ( i j ) otherwise pdepth z ([lfp z 0 Xm,xm .S ](t)) := 8 > > < > > : 1 + max j 2S pdepth params( j ) ( j ) if 9 j. params( j ) * z max j 2S pdepth z ( j ) otherwise .
The parameter depth pdepth( ) for normal form 2 GNFP-UP is just pdepth free( ) ( ). For not necessarily in normal form, we define it to be the pdepth after converting to normal form.

Observe that a formula that does not use any parameters has pdepth 0. Even a formula that does use parameters can have pdepth 0 if all of its parameters actually come from free variables of the formula. This is because parameters like this can be viewed as constants, since they have a fixed interpretation in any structure. Because of this, if 2 GNFP-UP[ ] with pdepth( ) = 0 and params( ) = z, then we can view as a GNFP formula without parameters, over the signature extended with extra constants z.

In general, the pdepth increases when we pass through a subformula that introduces more parameters. This can happen when passing through existential quantification that introduces a variable that is later used as a parameter (see the third case in the pdepth definition), or it can happen when passing through a fixpoint definition that introduces a fixpoint variable that is later used as a parameter (see the fourth case).

Later, we will see that the parameter depth is the major factor impacting the complexity of satisfiability testing.

We now give some examples to illustrate the expressivity of GNFP-UP, and this notion of parameter depth. These examples are drawn mostly from query languages used in databases and knowledge representation. Understanding these di↵erent logics and query languages is not important for understanding the main results about GNFP-UP (e.g., Theorem 20 and Theorem 24). However, for readers familiar with some of these previously-studied logics, they may give some insight into the sort of properties that can be expressed in GNFP-UP. Indeed, it is interesting to note that many of the previously-studied logics described below are low in this parameter depth hierarchy.

Traditional guarded logics GNFP-UP subsumes all of the previously mentioned guarded logics (and their fixpoint extensions), including GFP sentences, UNFP formulas, and GNFP formulas. Unsurprisingly, these traditional guarded logics without parameters can be expressed as GNFP-UP formulas of pdepth 0. Navigational queries There are a number of languages for navigational queries in graph databases, where the signature consists only of binary and unary relations. For these languages, a regular expression E over symbols R, R coming from binary relations R 2 can be seen as defining a navigation relation that holds for (x, y) exactly when there is some path between x and y matching E. A conjunctive 2-way regular path query (C2RPQ) [START_REF] Calvanese | Containment of conjunctive regular path queries with inverse[END_REF] is just a CQ over such expressions. Example 4. Consider some C2RPQ over signature . Let ⌃ := {R, R : R is a binary relation in }.

Given a regular expression E over ⌃, we can capture the navigation relation defined by it using a GNFP-UP formula E 0 . We start with a finite state automaton A = h⌃, Q, q 0 , , Fi for E and write a GNFP-UP[ ] formula with simultaneous fixpoints E 0 (x, y) := [lfp y X 0 ,x . S ](x) which has a second-order variable X i for each state q i 2 Q, and the equation for the i-th component X i , x i in S captures the possible transitions from state q i : _

(q i ,T,q j )2 9z.( T (x i , z) ^Xj z) _ ( x i = y if i 2 F ? if i < F where T (x i , z) is Rx i z if T = R and Rzx i if T = R .
Once we have E 0 in GNFP-UP for each regular expression E appearing in the C2RPQ, it is easy to translate into GNFP-UP by replacing each E(x, y) in the C2RPQ by E 0 (x, y). These GNFP-UP formulas have parameter depth 1: the GNFP-UP formula E 0 (x, y) for each regular expression predicate E(x, y) has pdepth 0; when these are substituted in the CQ, the resulting formula has pdepth at most 1 since the existential quantification may be introducing variables that are used as parameters in the inner formulas. GNFP-UP can also express unions of C2RPQs.

We can in fact replace regular expressions in C2RPQs by a variant of propositional dynamic logic (PDL). PDL consists of programs (defining binary relations within a labeled graph) and tests (defining unary relations within a graph) defined by mutual recursion. Programs contain all binary relation symbols and are closed under concatenation, union, and Kleene star. Tests contain all unary relation symbols and are closed under boolean operations. Given a test t, we can define a program t? that returns pairs (x, x) such that x is in the unary relation defined by t, and given a program P we can form a test hPi, defining a relation consisting of pairs (u, u) such that there exists v with (u, v) in the language described by P. We let CQPDL denote the language of conjunctive queries where binary relations can be PDL programs. Clearly this subsumes C2RPQs, and it also subsumes extensions defined in the description logic literature [START_REF] Bienvenu | Nested regular path queries in description logics[END_REF]. If P is restricted to be a traditional regular expression, then the corresponding GNFP-UP formula for hPi has pdepth at most 1. By writing expressions with more complicated nesting of these tests, however, these formulas can reach higher parameter depth levels. Fragments of Datalog Datalog is a syntax for expressing the negation-free fragment of least fixpoint logic. It is heavily used to express database queries that involve some form of recursion. We argue that all the previously-defined fragments of Datalog that have decidable static analysis problems are contained in GNFP-UP.

Formally, a Datalog query is specified by

⇧ = hEDB ⇧ , IDB ⇧ , Rules ⇧ , goali
where the extensional predicates EDB ⇧ and intensional predicates IDB ⇧ are disjoint sets, Rules ⇧ consists of formulas of the form R(x 1 . . . x n ) (xy) where R is an IDB predicate and is a conjunction of atoms, and goal is a distinguished member of IDB ⇧ . Given some structure A we can evaluate goal in the structure obtained from A by firing the rules of ⇧ until a fixpoint has been reached. For a structure A and query ⇧ we let ⇧(A) be the value of the predicate goal so obtained. A boolean Datalog query is one where the goal predicate is 0-ary, and hence the query defines a boolean function on input structures.

Monadic Datalog restricts the IDBs to have arity 1. In this case, it is possible to express the query using a UNFP formula with simultaneous fixpoints without parameters. Frontier-guarded Datalog allows the use of intensional predicates with unrestricted arities, but for each rule R(x 1 . . . x n ) (xy), the variables x 1 . . . x n in the head of the rule, must appear in a single EDB atom appearing in the body . This subsumes monadic Datalog, since the single head variable in the monadic Datalog rules can be trivially guarded. Frontier-guarded Datalog can be expressed in GNFP. No parameters are necessary, so the parameter depth is 0.

The flag and check queries introduced in [START_REF] Bourhis | Reasonable highly expressive query languages[END_REF][START_REF] Rudolph | Flag & check: data access with monadically defined queries[END_REF] are based on fragments of Datalog queries that have been shown to have decidable analysis problems.

One family consists of the monadically defined queries (MQs). These are of the form 9y.⇧ where ⇧ is a Monadic Datalog query, the goal predicate is nullary, and the rules use special symbols z. The answers to the query are (projections of) assignments to the special symbols for which the corresponding Monadic Datalog query evaluates to true. The idea is that the special symbols serve as flags for potential answers to the query, and the Datalog query checks if the flags mark actual answers. Example 5 (based on [START_REF] Bourhis | Reasonable highly expressive query languages[END_REF]). The transitive closure of a binary relation R can be expressed by the MQ ⇧ with special symbols z 1 , z 2 where ⇧ is

U(y) R z 1 y U(y) U x ^R xy hit() Uz 2 .
The answer to the query would consist of all pairs (a 1 , a 2 ) for which the rules imply hit under the standard Datalog semantics, when interpreting z 1 as a 1 and z 2 as a 2 .

In UNFP-UP, this is (z 1 , z 2 ) := [lfp z We can translate an arbitrary MQ 9y.⇧ with special symbols z using a similar method: the monadic Datalog query becomes a simultaneous fixpoint 0 in GNFP-UP, with the special symbols z as parameters, and the special nullary hit predicate as the goal predicate. The MQ itself can then be written in GNFP-UP as 9y. 0 (z). The resulting formula has pdepth at most 1, since 0 (z) has pdepth 0, and 9y. 0 (z) may project some of the parameters (the previous example only has pdepth 0 because there is no such projection).

In [START_REF] Rudolph | Flag & check: data access with monadically defined queries[END_REF], they also consider a nested version of these flag and check queries. An m-nested MQ is one where the monadic Datalog query is allowed to use predicates defined by (m 1)-nested MQs in the rule bodies (but these predicates cannot be used as guards); a 1-nested MQ is just the MQ defined above. In general, we can translate an m-nested MQ query into a GNFP-UP formula of pdepth at most m. [START_REF] Bourhis | Reasonable highly expressive query languages[END_REF] defines other variants of flag and check queries; all of them can be similarly captured in GNFP-UP.

A Datalog query ⇧ 1 is contained in a Datalog query ⇧ 2 if for all input structures A, ⇧ 1 (A) ✓ ⇧ 2 (A). Similarly given a sentence in some logic, we say Datalog query ⇧ 1 is contained in ⇧ 2 relative to if ⇧ 1 (A) ✓ ⇧ 2 (A) for all A satisfying . GNFP-UP can express the Datalog queries in the fragments above. Moreover, since it is closed under boolean combinations for sentences, it can also express containment of two boolean queries within each fragment, and containment relative to sentences that are expressible in GNFP-UP.

Transitive closure logic The extension of FO with a transitive closure operator (rather than a full fixpoint operator) was introduced in [START_REF] Immerman | Relational queries computable in polynomial time[END_REF] and has been studied extensively. In a similar vein, we can consider GNF extended with a (guarded) transitive closure operator which we denote GNF(TC). The idea is to add to GNF the following formula building rule: if (x, y) 2 GNF(TC) for m-tuples x and y, then [TC x,y . gdd(x) ^ (x, y)](u, v) is a formula in GNF(TC). The intended meaning is that u and v are guarded (in the original signature) and (u, v) is in the reflexive transitive closure of the binary relation on m-tuples defined by gdd(x) ^ (x, y).

Example 1 is 9x 0 .(Rxx 0 ^[TC y,y 0 . Ryy 0 ](x 0 , z)) (the guardedness predicate is omitted since singletons are trivially guarded). CQPDL, and hence C2RPQs, can also be expressed in GNF(TC).

It is straightforward to check that every GNF(TC) formula can be translated in polynomial time to an equivalent GNFP-UP formula, and that such formulas can reach arbitrary pdepth levels.

Why GNFP-UP? The previous examples serve to illustrate the variety of logics that GNFP-UP subsumes. GNFP-UP is useful because it serves as a unifying logic for all of these di↵erent formalisms that have some recursive nature.

A major advantage of GNFP-UP over the Datalog-based languages is that the logic has some form of negation. Not only does the presence of negation increase the expressivity of the queries that can be written in this language, but it also means that we can express directly query containment problems in this language, which was not possible in many of these earlier formalisms.

Despite the increased expressivity, we will show that GNFP-UP still has many useful model theoretic and computational properties, including decidable satisfiability and boundedness.

Tree-like models and tree encodings

Although GNFP-UP fails to have the finite model property (since it embeds the 2-way µ-calculus), it does have the tree-like model property. This says that if there is a model, then there is a model with a tree decomposition of some bounded tree width. A tree decomposition of a structure A is a tree labelled with atomic facts of A such that every atom is present in some label, and for each a 2 dom(A), the set of nodes (often called bags) that mention a form a connected part of the tree. The decomposition has tree-width w 1 if the number of elements represented in each bag is at most w. Proposition 6. Every satisfiable (GNFP-UP) k [ ] sentence has a model of tree-width at most k + |const( )| 1.

The proof uses a standard technique, involving an unravelling based on a notion of guarded negation bisimulation.

The first route to deciding satisfiability relies on the tree-like model property of Proposition 6 along with the fact that GNFP-UP can be expressed in a fragment of second-order logic called guarded second-order logic (GSO) in which second-order quantification is interpreted only over guarded relations, i.e. relations where every tuple is guarded by some atom in the base signature. Proposition 7. Given 2 GNFP-UP[ ], we can construct an equivalent 0 2 GSO[ ] in linear time. Corollary 8. Satisfiability for GNFP-UP is decidable.

Proof. GNFP-UP embeds in GSO by Proposition 7 and has bounded tree-width by Proposition 6. Using [START_REF] Grädel | Back and forth between guarded and modal logics[END_REF], GSO can be translated into an equivalent MSO formula (over encodings of the tree-like models) which is decidable by [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. ⇤ This is the easiest route to showing decidability of GNFP-UP, but it is not good for extracting complexity bounds. We next show how to make direct use of the tree-like model property and a translation taking a formula in the logic to tree automata that represent tree-like models of the formula, to determine more precisely the complexity of satisfiability and boundedness for GNFP-UP. Coding structures Structures of bounded tree-width can be encoded as trees over a finite alphabet that depends only on the signature and the tree-width. Fix some signature and some width k 2 N. Let U k be a set of size 2(k + |const( )|). We refer to these as "names", as they name elements coded in a node. The signature ˜ k for the encodings is defined as follows.

• For all a 2 U k , there is a unary relation D a 2 ˜ k which indicates that a is a name for an element in the bag. • For every relation R 2 of arity n and every n-tuple a 2 U n k , there is a unary relation R a 2 ˜ k , which indicates that R holds for the tuple of elements indexed by a.

• For every constant z 2 and c 2 U k , there are unary relations V c/z which indicate that z is interpreted by the element named by c in the given bag. Tree decompositions and the corresponding encodings can generally have unbounded (possibly infinite) degree. We apply the firstchild, next-sibling transformation (based on an arbitrary ordering of the children) to the standard encoding, so that we can use binary trees for our encodings. This transformation takes a tree with arbitrary branching degree and constructs a binary tree as follows: it maps the root of the original tree to the root of a new binary tree; then, starting from the root, each node's leftmost child in the original tree is mapped to its left child in the binary tree, and its next sibling to the right in the original tree is mapped to its right child.

Hence, for our binary tree encodings, a node u can be identified by a word in {0, 1} ⇤ , and the biological children of u are the nodes u01 ⇤ (these are the nodes that would have been children of u in the tree decomposition before the first-child next-sibling transformation). The biological parent of v , ✏ is the unique u such that v 2 u01 ⇤ . A biological neighbor is a biological child or biological parent. For these binary tree encodings, we also add to ˜ k unary predicates P i for i 2 {0, 1} which indicate the node is the i-th child of its parent.

This transformation to a binary tree encoding is essential in certain automaton constructions (e.g. Theorem 13) when the automaton needs to record in its state the direction it came from. From now on, we use ˜ k -tree to refer to an infinite full binary tree over ˜ k . Decoding structures If a ˜ k -tree satisfies certain consistency properties, then it can be decoded into a -structure that has tree-

width k + |const( )| 1. Let names(v) := {a 2 U k : D a v} denote the set of names used for elements in bag v. A consistent ˜ k -tree is a ˜ k -tree such that every node v satisfies • |names(v)|  k + |const( )|; • for all R a 2 ˜ k , if R a v then a ✓ names(v); • P i v holds i↵ v is the i-th child of its parent;
• for all constants z 2 , there is exactly one node w and one c 2 names(w) such that V c/z w. Given a consistent tree T , we say nodes u and v are a-connected if there is a sequence of nodes u = w 0 , w 1 , . . . , w j = v such that w i+1 is a biological neighbor of w i , and a 2 names(w i ) for all i 2 {0, . . . , j}. We write [v, a] for the equivalence class of aconnected nodes of v. For a = a 1 . . . a n , we often abuse notation and write [v, a]

for the tuple [v, a 1 ], . . . , [v, a n ]
The decoding of T is the -structure D(T ) with universe {[v, a] : v 2 dom(T ) and a 2 names(v)} such that for each constant z, we have z D(T ) := [v, c] for the unique v, c such that V c/z v holds, and for each relation R,

we have R D(T ) ([v 1 , a 1 ], . . . , [v j , a j ]) i↵ there is w 2 dom(T ) such that R a w holds and [w, a i ] = [v i , a i ] for all i.
Free variables For formulas with free variables, the trees are extended with additional information about the valuations for these free variables. These trees use an extended signature where for each free first-order variable z and each c 2 U k , we introduce a predicate V c/z , and for each second-order variable Z of arity n and each a 2 U n k , we introduce a predicate Z a . We refer to these as free variable markers or encodings of valuations for free variables.

We write z ! for the sets of predicates associated with z. For a set of free variables z = {z 1 . . . z n }, we write

z ! for z 1 ! [ • • • [ z n ! .
We sometimes abuse notation and write z ! for both the predicates and the valuation of those predicates. Similar conventions apply to the free second-order variables.

Given a ˜ k -tree T , we write (T , z ! , Z ! ) for a tree over the signature ˜ k [z ! [Z ! . We abuse the terminology and say (T , z ! , Z ! ) is a consistent ˜ k -tree if T is a consistent ˜ k -tree, and for each z 2 z ! , there is exactly one v and one c 2 names(v) such that V c/z v holds, and for each Z a 2 Z ! , if Z a v then a ✓ names(v).

Automata tools

We make use of automata running on infinite binary trees. In this section, we briefly recall some definitions and properties (please consult, e.g., [START_REF] Löding | Automata on infinite trees[END_REF][START_REF] Thomas | Languages, Automata, and Logic[END_REF] for more information). We will need to use 2-way automata that can move both up and down as they process the tree, so we highlight some less familiar properties about the relationship between 2-way and 1-way versions of these automata.

Trees The input structures are infinite full binary trees T over a finite set of propositions ⌃. In other words, these are structures over a signature with binary relations for the left and right child relation, and unary relations for the propositions. We also assume there are propositions indicating whether each node is a left child, right child, or the root. We write T (v) for the set of propositions that hold at node v.

Tree automata An alternating parity tree automaton A is a tuple h⌃, Q, q 0 , , ⌦i where ⌃ is a finite set of propositions, Q is a finite set of states, q 0 2 Q is the initial state, :

Q ⇥ P(⌃) ! B + (Dir ⇥ Q)
is the transition function with directions Dir ✓ {l, r, "}, and ⌦ : Q ! P is the priority function with a finite set of priorities P ✓ N.

The transition function maps a state and input letter to a positive boolean formula over propositions Dir ⇥ Q, denoted B + (Dir ⇥ Q). This formula indicates possible next moves for the automaton. We can assume that these formulas are written in disjunctive normal form. Running the automaton A on some input tree T is best thought of in terms of an acceptance game. Positions in the game are of the form (q, v) 2 Q ⇥ dom(T ). In position (q, v), Eve chooses a disjunct ✓ in (q, T (v)). Then Adam chooses a conjunct (d, q 0 ) in ✓ and the game continues from position (q 0 , v 0 ), where v 0 is the node in direction d from v. In other words, the disjunct ✓ chosen by Eve specifies the possible copies of the automaton that could be launched by Adam from v or a neighbor of v.

A play (q 0 , v 0 )(q 1 , v 1 ) . . . in the game is winning for Eve if it satisfies the parity condition: the maximum priority occurring infinitely often in ⌦(q 0 )⌦(q 1 ) . . . is even. A strategy for Eve is a function that given the history of the play and the current position in the game, determines Eve's choice in the game. Note that we allow the automaton to be started from arbitrary positions v 0 in the tree, rather than just the root; we will often indicate this by saying that the automaton is launched from v 0 . We say that A accepts T starting from v 0 if Eve has a strategy such that all plays consistent with the strategy starting from (q 0 , v 0 ) are winning. L(A) denotes the language of trees accepted by A starting from the root.

A 1-way alternating automaton is an automaton that uses only directions l and r. A (1-way) nondeterministic automaton is a 1-way alternating automaton such that every transition function formula is of the form W i (l, q i l ) ^(r, q i r ). Closure properties We recall some closure properties of these automata (omitting the standard proofs).

First, the automata that we are using are closed under union and intersection (of their languages). Proposition 9. 2-way alternating parity tree automata and 1-way nondeterministic parity tree automata are closed under union and intersection, with only a polynomial blow-up in the number of states and overall size.

For example, this means that if we are given 2-way alternating parity tree automata A 1 and A 2 , then we can construct in PTime a 2-way alternating parity tree automaton A such that L(A) = L(A 1 ) \ L(A 2 ). In automaton constructions, when we say, e.g., "take the intersection of A 1 and A 2 ", we mean take this automaton

A such that L(A) = L(A 1 ) \ L(A 2 ).
Another important language operation is projection. Let L 0 be a language of trees over propositions ⌃ [ {P}. The projection of L 0 with respect to P is the language of trees T over ⌃ such that there is some T 0 2 L 0 such that T and T 0 agree on all propositions in ⌃. Projection is easy for nondeterministic automata since the valuation for the projected proposition can be guessed by Eve. Proposition 10. 1-way nondeterministic parity tree automata are closed under projection, with no change in the number of states and overall size.

Finally, complementation is easy for alternating automata by taking the dual automaton, obtained by switching conjunctions and disjunctions in the transition function, and incrementing all of the priorities by one. Proposition 11. 2-way alternating parity tree automata are closed under complementation, with no change in the number of states and overall size.

Connections between 2-way and 1-way automata It was shown by Vardi [START_REF] Vardi | Reasoning about the past with two-way automata[END_REF] that 2-way alternating parity tree automata can be converted to equivalent 1-way nondeterministic automata, with an exponential blow-up. Theorem 12 ([31]). Let A be a 2-way alternating parity tree automaton. We can construct a 1-way nondeterministic parity tree automaton A 0 such that L(A) = L(A 0 ). The number of states of A 0 is exponential in the number of states of A, but the number of priorities of A 0 is linear in the number of priorities of A.

1-way nondeterministic tree automata can be seen as a special case of 2-way alternating automata, so the previous theorem shows that 1-way nondeterministic and 2-way alternating parity automata are equivalent, in terms of their ability to recognize trees starting from the root.

We need another conversion from 1-way nondeterministic to 2way alternating automata that we call localization. This is the process by which a 1-way nondeterministic automaton that is running on trees with extra information about some predicate annotated on the tree is converted to an equivalent 2-way alternating automaton that operates on trees without these annotations, but under the assumption that these predicates hold only locally at the position the 2-way automaton is launched from. A similar localization idea is present in prior work (see, e.g., [START_REF] Blumensath | Two-way cost automata and cost logics over infinite trees[END_REF][START_REF] Bourhis | Reasonable highly expressive query languages[END_REF]). Theorem 13. Let ⌃ 0 := ⌃ [ {P 1 , . . . , P j }. Let A 0 be a 1-way nondeterministic parity automaton on ⌃ 0 -trees. We can construct a 2-way alternating parity automaton A on ⌃-trees such that for all ⌃-trees T and v 2 dom(T ),

A 0 accepts T 0 from the root i↵ A accepts T from v, where T 0 is the ⌃ 0 -tree obtained from T by setting P

T 0 1 = • • • = P T 0 j = {v}.
The number of states of A is linear in the number of states of A 0 , and the overall size is linear in the size of A 0 . Proof sketch. A simulates A 0 by guessing in a backwards fashion an initial part of a run of A 0 on the path from v to the root and then processing the rest of the tree in a normal downwards fashion. The subtlety is that the automaton A is reading a tree without valuations for P 1 , . . . , P j so once the automaton leaves node v, if it were to cross this position again, it would be unable to correctly simulate A 0 . To avoid this, we only send downwards copies of the automaton in directions that are not on the path from the root to v. ⇤

We remark that this construction can be adapted for an alternating parity automaton as input, but A is exponential in the size of the input automaton A 0 , rather than linear.

Emptiness testing Finally, we make use of the well-known fact that language emptiness of tree automata is decidable. Theorem 14 ([16], [START_REF] Vardi | Reasoning about the past with two-way automata[END_REF]). For 1-way nondeterministic parity tree automata, emptiness is decidable in time polynomial in the number of states and exponential in the number of priorities. For 2-way alternating parity automata, it is decidable in time exponential in the number of states and priorities.

Automata for GNFP-UP

In this section, we construct automata for ✓ in GNFP-UP[ ]. Before we give some details of the construction, it is helpful to consider how automata can be used to analyze fixpoints.

Using localized automata for fixpoints Testing whether some tuple t is in the least fixpoint [lfp z Y,y . ] in some structure A and for some fixed valuation of the parameters (and any other free variables) can be viewed as a game. Positions in this game consist of the current tuple y being tested in the fixpoint, with the initial position being t. In general, in position y, one round of the game consists of the following:

• Eve chooses some valuation for Y such that (y, Y) holds (if it is not possible, she loses), then • Adam chooses tuple y 0 2 Y (if it is not possible, he loses), and the game proceeds to the next round in position y 0 . Adam wins if the game continues forever.

The idea is that if t is really in the least fixpoint, then it must be added in some fixpoint approximant. This gives Eve a strategy for choosing Y at each stage in the game, in such a way that after finitely many challenges by Adam, she should be able to guess the empty valuation.

When the fixpoint can consist of only guarded tuples, there is a version of this game on a tree encoding T of a structure, that can be implemented using tree automata. We start with an automaton A for the body of the fixpoint. In fact, we start with localized versions of this automaton because we need to launch di↵erent versions based on Adam's challenges. A local assignment b/y for b = b 1 . . . b n 2 U n k and y = y 1 . . . y n is a mapping such that y i 7 ! b i . A node v in T with b ✓ names(v) and a local assignment b/y, specifies a valuation for y ! . We say it is local since the free variable markers for y would all appear locally in v. If we have an automaton A running on trees with free variable markers for y, we say that we localize A to b/y if we apply the localization theorem (Theorem 13) to the predicates V b i /y i , and then eliminate the dependence on any other V c/y i for c , b i by always assuming these predicates do not hold. This results in an automaton that simulates A under the assumption that the free variables y correspond to the elements [v, b], but it no longer relies on free variable markers for y. These localized automata are important because they can be launched to test that a tuple of elements that appear together in a node satisfy some property -without having the markers for this tuple explicitly written on the tree.

We now describe the version of the fixpoint game using localized automata. Initially, Eve navigates to a node in T carrying t, and launches the appropriate localized A from there. In general, the game proceeds as follows:

• Eve and Adam simulate some localized version of A . During the simulation Eve can guess a valuation for Y (recall that A runs on trees with an annotation describing the valuation for the second-order variable Y, and that information is missing from T ). Because Y can only contain guarded tuples, this amounts to guessing an annotation of the tree with this valuation. • When Eve guesses some y 0 2 Y, Adam can either continue the simulation, or challenge her on this assertion. A challenge corresponds to launching a new localized copy of A from the node carrying y 0 (again, we know that y 0 must be present locally in a node, since any tuple in the fixpoint must be guarded). After each challenge, the game continues as before (with the new copy of A being simulated, Eve guessing a new valuation for Y, etc.). Adam wins if he challenges infinitely often, or if the game stabilizes in some simulation of A where he wins.

Assuming we have localized automata for , we can implement this game using a 2-way alternating parity automaton. We assign a large odd priority (larger than the priorities in A ) to the states where Adam challenges, so that he wins if he is able to challenge infinitely many times; the other priorities are just inherited from A . Simultaneous fixpoints can be handled in a similar way.

In order to analyze the fixpoints like this, our inductive automaton construction must produce 2-way localized automata at each stage -if we did not, then each time we reached a fixpoint and needed localized automata for the body of the fixpoint, we would get an exponential blow-up. For GFP and GNFP, we can define directly the localized versions of the automata using a state set of size at most singly exponential in the size of the input formula. However, by adding parameters in GNFP-UP, this direct definition of a localized version becomes more challenging. We are forced to construct non-localized automata at some points -namely, for subformulas that introduce new parameters -and then apply Theorems 12 and 13, resulting in an exponential blow-up. The parameter depth is a measure of how many of these blow-ups occur. Construction We now describe more details of the construction of an automaton for normal form ✓ 2 GNFP-UP[ ]. First, it is straightforward to construct an automaton that checks consistency: Proposition 15. There is a 2-way alternating parity tree automaton C that checks whether or not a ˜ k -tree (possibly extended with additional free variable markers for z and Z) is consistent. The size of C is at most exponential in

(| | + |z| + |Z|) • |U k | k .
Hence, we can concentrate on defining an automaton for ✓ that runs on consistent trees and accepts i↵ the decoding of the consistent input tree actually satisfies ✓.

The main theorem states that the size of the automaton for ✓ is a tower of exponentials whose height depends on the pdepth. Given a function f , we write exp n f (m) for a tower of exponentials of height n based on f , i.e. exp 0

f (m) = m and exp n f (m) = 2 f (exp n 1 f (m)) . Theorem 16. For normal form ✓ 2 (GNFP-UP) k [ ] with pdepth(✓)
1, we can construct a 2-way alternating parity tree automaton A ✓ such that for all consistent ˜ k -trees T , D(T ) | = ✓ i↵ T 2 L(A ✓ ), and the size of A ✓ is at most (pdepth(✓)+1)-exponential in |✓|.

More precisely, there is a polynomial function f independent of ✓ such that the size is at most exp pdepth(✓) f ( f (m)•2 f (klr) ) where m = |✓|, l = |const( )|, and r = rank CQ ( ) (see definitions below).

For brevity, in this theorem and in the remainder of the paper, we usually give only bounds on the output size, not the running time of the algorithms. However the proofs will show that the worstcase running time is bounded by a polynomial in the output size, i.e. the running time of Theorem 16 is (pdepth(✓) + 1)-ExpTime. We emphasize that this means that for fixed pdepth, the construction can be done in elementary time.

The main factor a↵ecting the output size is the pdepth, since this determines the height of the tower of exponentials. However, for more precise bounds, the other factors a↵ecting the size are the size of the formula ✓, the width k, the number of constants in , and the CQ-rank (the maximum number of conjuncts i in any CQ-shaped subformula 9x.

V i i for non-empty x). The proof of Theorem 16 is by induction on |✓|, and constructs localized 2-way automata for subformulas of ✓. For GNFP subformulas, it is known from [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF] how to construct 2-way automata: 1Lemma 17 ([8]). Let (y, Z) 2 GNFP k [ 0 ] in normal form. Then for every local assignment b/y, we can construct a 2-way alternating parity tree automaton A b/y such that for all consistent ˜ 0 k -trees (T , Z ! ) and for all nodes w 2 dom(T ) with b ✓ names(w),

D(T ), [w, b], Z | = i↵ A b/y accepts (T , Z ! ) from w.
There is a polynomial function f independent of such that the number of states for all such localized automata is at most

N := f (m) • 2 f (klr) where m = | |, l = |const( 0 )|, and r = rank CQ ( ). The number of priorities in each automaton is linear in | |. The overall size is at most exponential in | 0 | • N.
We use these automata for GNFP as building blocks for our GNFP-UP construction. Recall that pdepth 0 formulas can always be viewed as GNFP formulas. We can also transform parts of the formula into GNFP formulas over a slightly di↵erent signature.

For this purpose, given 2 (GNFP-UP) k [ ] with params( ) ✓ z, define the augmented signature z, to be the signature together with additional constants z 2 z and subformula predicates F ⌘ for subformulas ⌘ with params(⌘) ✓ z. For such ⌘, the arity of F ⌘ is usually |free(⌘) \ params(⌘)|; in the special case that ⌘ is a fixpoint formula, then the arity of F ⌘ is the arity of this fixpoint predicate. Then we can transform the outer part of a GNFP-UP formula to a GNFP formula over this augmented signature. We can only perform this transformation on the outer part of the formula that uses the same set of parameters. Consider ⌘ 2 (GNFP-UP) k [ ] with free(⌘) ✓ yz and params(⌘) ✓ z. We define transform z (⌘)

2 GNFP k [ z,⌘ ] inductively as follows: transform z (R t) := R t transform z (Y t) := Y t transform z (↵ ^¬ ) := ↵ ^¬transform z\free( ) ( ) transform z ([lfp z 0 X,x .S ](t)) := 8 > > < > > : F [lfp z 0 X,x .S ](t) t if there is j 2 S with params( j ) * z [lfp X,x .S 0 ](t) o.w.
where S 0 is the result of applying transform z to each j 2 S transform z ( W i 9x i .

V j i j ) := ( F W i 9x i . V j i j y if there is i, j such that params( i j ) * z W i 9x i . V j transform z\free( i j ) ( i j ) o.w.
The GNFP formula obtained using this transformation is "equivalent" to the GNFP-UP formula, under the assumption that the additional predicates in the augmented signature are interpreted in the expected way. It does not increase the width, CQ-rank, or the size of the formula.

If the transformation applied to ⌘ only introduces F ⌘ 0 for strict subformulas ⌘ 0 of ⌘, then we say the transformation is helpful. In a helpful transformation, all occurrences of these new predicates F ⌘ 0 appear under a guard of free(⌘ 0 ) \ params(⌘ 0 ). Another way to understand the parameter depth is to say that the parameter depth measures the number of unhelpful breakpoints we reach as we try to transform the entire formula using this operation.

The main idea in the construction, described in Lemma 18 below, is to transform the outer part of the formula into a GNFP formula. If the transformation is helpful, we can then use the GNFP automaton for the outer part of the formula, and plug in inductively defined automata checking the subformulas. When this is not possible, we must use di↵erent techniques which result in an exponential blow-up at these stages. Lemma 18. Let (y, z, Z) be a subformula of ✓ 2 (GNFP-UP) k [ ] with params( ) ✓ z. For each local assignment b/y, we can construct a 2-way alternating parity tree automaton B b/y such that for all consistent ˜ k -trees (T , z ! , Z ! ) and for all nodes w 2 dom(T ) with b ✓ names(w),

D(T ), [w, b], z, Z | = i↵ B b/y accepts (T , z ! , Z ! ) from w.
For pdepth z ( ) 1, there is a polynomial function f independent of such that the size of all such localized automata is at most exp Assume 0 := transform z ( ) is helpful. This always holds for the smallest (atomic) formulas, so this covers the base of the induction. We construct B b/y to simulate the automaton A b/y 0 from Lemma 17, while allowing Eve to guess valuations for the F ⌘ relations from 0 . Since 0 is helpful, we know that every F ⌘ relation in 0 is for some formula ⌘ that is strictly smaller than , and hence the inductive hypothesis ensures there is a corresponding automaton for every suitable local assignment. During the simulation of A b/y 0 , if Eve asserts F ⌘(x) a at w for some a ✓ names(w), then Adam can challenge this by launching the localized automaton for the intersection of B a/x ⌘(x) and B a/x gdd(x) from w; likewise, if Eve does not assert F ⌘(x) a at w for some a ✓ names(w), then Adam can challenge this by launching the localized automaton for the dual of the intersection of B a/x ⌘(x) and B a/x gdd(x) from w. Correctness follows from Lemma 17, and the fact that the inductive hypothesis ensures the subautomata for F ⌘ in 0 are correct. There is no exponential blowup in this case.

pdepth z ( ) f ( f (mn) • 2 f (klr) ) where m = | |, n = | |, l = |const( )|,
Next, assume that 0 := transform z ( ) is unhelpful. There are two possible cases.

The first case is when is a UCQ-shaped formula W i 9x i .

V j i j
where variables from some x i are used as parameters in V j i j . To start, we consider each CQ-shaped formula separately, so fix some 9x i .

V j i j . We use the inductive hypothesis to obtain 2-way alternating automata for each conjunct i j , using the empty local assignment. This is possible since the size of these conjuncts must be strictly less than the size of . Because we are using the empty local assignment, these automata operate on trees with markers for all of the free variables: x i [ y [ z. Take the intersection of these automata using Proposition 9. Then take the intersection with the automaton from Proposition 15 checking consistency. This yields a 2-way alternating automaton corresponding to V j i j . We then convert this automaton to a nondeterministic version using Theorem 12 and project away the information about x i using Proposition 10. This yields an equivalent (1-way) nondeterministic parity automaton for the CQ. Next, we localize this automaton to the desired variables y using Theorem 13. Finally, to construct the automaton B b/y , we take the union of the individual CQ automata using Proposition 9.

The conversion from a 2-way alternating automaton to a nondeterministic automaton is the costly step in this process, resulting in an exponential blow-up. This matches the claimed size bound since pdepth( i j ) < pdepth z ( ).

The second case is when is a fixpoint formula where fixpoint variables are used as parameters in the body of the fixpoint. Suppose it is of the form [lfp z 0 X,x . gdd(x) ^ (xz 0 , XZ)](t) where params( )\ x , ;, so params( ) * z; the construction is similar for a simultaneous fixpoint. The formula in the body of the fixpoint is strictly smaller, so we can apply the inductive hypothesis to get an automaton for this part. We want this automaton to be localized to x so we can test for tuples in the fixpoint by launching copies of the automaton for some local assignment. However, the inductive hypothesis does not directly yield this, since some variables from x are used as parameters. Hence, we must use the inductive hypothesis to get a 2-way automaton for B ;/; 0 , apply Theorem 12 to get an equivalent 1-way nondeterministic automaton (resulting in an exponential blow-up), and then localize to some a/x using Theorem 13. Once we have these localized automata B a/x for the body of the fixpoint, we can construct an automaton that captures the fixpoint game described at the beginning of this section. ⇤ Theorem 16 easily follows from this lemma. Using exactly the same conversion rules from [START_REF] Bárány | Guarded negation[END_REF], it can be shown that an arbitrary GNFP-UP sentence ✓ 0 can be converted to an equivalent normal form ✓ with size exponential in |✓|, but width and CQ-rank linear in |✓|. Hence, we have the following corollary. Corollary 19. For ✓ 0 2 GNFP-UP[ ] (not necessarily in normal form), we can construct an automaton A ✓ 0 of (pdepth(✓ 0 ) + 1)exponential size.

Satisfiability and containment

Because of the tree-like model property for GNFP-UP, we can use the automaton construction and ExpTime emptiness testing (Theorem 14) to decide satisfiability of GNFP-UP. Theorem 20. Satisfiability for ✓ 2 GNFP-UP is decidable in (pdepth(✓) + 2)-ExpTime.

Applications We can apply Theorem 20 to obtain results about the query languages described in Section 3: e.g., containment of mnested MQs is in (m + 2)-ExpTime. This result was known already from [START_REF] Bourhis | Reasonable highly expressive query languages[END_REF]. However, an advantage of this GNFP-UP framework is that we can introduce additional features such as relativizing the results to sentences in our logics, without a↵ecting the complexity. Corollary 21. Containment of m-nested MQs relative to boolean frontier-guarded Datalog queries (or any boolean queries translatable to GNFP in PTime) is decidable in (m + 2)-ExpTime.

We can extend our approach to even allow some unguarded logics on the left-hand side of the containment (as is done in [START_REF] Bourhis | Reasonable highly expressive query languages[END_REF], which considers only unrelativized containment). Corollary 22. Containment of a Datalog query in an m-nested MQ is in (m + 2)-ExpTime, even relative to a boolean frontier-guarded Datalog query or a GNFP sentence.

We can also derive results about satisfiability of CQPDL with respect to GNFP sentences. Although CQPDL can reach arbitrary pdepth levels, we can construct an equi-satisfiable formula of low pdepth. This yields the following new result, extending results about (nested) C2RPQs from [START_REF] Bienvenu | Nested regular path queries in description logics[END_REF]. Corollary 23. Satisfiability of CQPDL sentences (or boolean combinations of CQPDL sentences and GNFP sentences) is decidable in 2-ExpTime.

Lower bounds This connection with flag and check queries also demonstrates that our general (m + 2)-ExpTime bound on satisfiability for GNFP-UP formulas of pdepth m is optimal, since containment of boolean Datalog queries in m-nested MQs is actually (m + 2)-ExpTime hard [START_REF] Bourhis | Reasonable highly expressive query languages[END_REF].

Extending to boundedness

Thus far, we have concentrated on showing that satisfiability is decidable for GNFP-UP, using techniques based on automata. In this section, we point out that we can extend this automata machinery to help answer additional questions like boundedness.

The boundedness problem for a logic L over asks:

Given a formula (x, X) 2 L[ ] positive in some secondorder variable X of arity |x|, is there a natural number n such that for all -structures A, n (A) = n+1 (A)?

In other words, the boundedness problem asks whether there is a uniform natural number bound on the number of iterations needed to reach the least fixpoint induced by (x, X). For formulas (x, z, X) with some designated set of parameters z, it is also natural to ask the following variant of the boundedness problem: is there a natural number n such that for all -structures A and for all valuations z 7 ! c, does n (A, c) = n+1 (A, c)?

There is a large body of work studying boundedness for various logics, particularly Datalog queries (see [START_REF] Abiteboul | Boundedness is undecidable for datalog programs with a single recursive rule[END_REF][START_REF] Cosmadakis | Decidable optimization problems for database logic programs[END_REF][START_REF] Hillebrand | Undecidable boundedness problems for datalog programs[END_REF]). Boundedness is undecidable when is a negation-free first-order formula. However, for many guarded logics, boundedness has been shown to be decidable [START_REF] Bárány | Queries with guarded negation[END_REF][START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF][START_REF] Blumensath | Decidability results for the boundedness problem[END_REF] (some of the decidability results rely on unpublished work due to Colcombet, referred to as ILT in [START_REF] Bárány | Queries with guarded negation[END_REF]).

Using similar techniques, we can analyze boundedness for GNFP-UP. As was the case for our analysis of satisfiability, the key is to take advantage of the fact that we can restrict to structures of bounded tree-width, and then use tree automata to help solve the problem. For boundedness a variant of the prior construction (with the same bounds) can generate a special type of tree automaton with counters called a cost automaton (see [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF][START_REF] Colcombet | Regular cost functions over finite trees[END_REF] for more information). This cost automaton defines a function that maps a consistent tree T to the least n 2 N [ {1} such that every tuple in 1 (D(T )) is in n (D(T )) -there is a single counter that is incremented each time the fixpoint is unfolded. The range of the function defined by this cost automaton is bounded by a natural number across all consistent trees i↵ is bounded.

In general, it is not known how to decide if the range of the function defined by a cost automaton over infinite trees is bounded. However, for special types of cost automata -like the automata that come from analyzing boundedness for guarded logics -this is known to be decidable [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF] (in cases where there is a reliance on cost automaton results that have been claimed before but not published, we mark this with ILT as in [START_REF] Bárány | Queries with guarded negation[END_REF]). 2 Hence, by combining our automaton construction with results from [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF] and ILT, we can show: Theorem 24. Assuming ILT, the boundedness problem is decidable for x-guarded (x, X) 2 GNFP-UP[ ] in non-elementary time (elementary time for fixed pdepth).

In the special case of x-guarded (x, z, X) 2 GNF[ ], boundedness is decidable in elementary time (without assuming ILT).

FO definability For certain logics, boundedness coincides with FO definability; e.g., we have the following corollary of Theorem 24. Corollary 25. It is decidable whether [lfp z X,x . ] can be written in

FO for x-guarded (x, z, X) 2 GNF[ ].
Furthermore, whenever this holds the fixpoint [lfp z X,x . ] can in fact be written in GNF.

Proof. If 2 GNF is bounded, then the fixpoint is equivalent to the n-th approximant, for some n 2 N. We can write out the formula n for this approximant, where 0 := ?, and n := [ n 1 (y)/Xy]. This is in GNF, and witnesses the FO definability of [lfp z X,x . ]. The other direction follows from the Barwise-Moschovakis theorem [START_REF] Barwise | Global inductive definability[END_REF]. ⇤ A similar result is not known for 2 GNFP-UP[ ], because of the presence of additional fixpoints in -the boundedness problem only concerns the elimination of the outermost fixpoint.

As another application, we can combine automata techniques from this paper with other cost automata results in [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF][START_REF] Blumensath | Two-way cost automata and cost logics over infinite trees[END_REF] to prove the following result about negation-free CQPDL and FO definability. Theorem 26. It is decidable whether or not a negation-free CQPDL sentence relative to a GNF sentence can be expressed in FO.

In particular, we can decide whether a conjunctive regular path query can be expressed in FO, and similarly for their nested and two-way variants (e.g. C2RPQs).

The ability to reduce C2RPQ querying to first-order querying is interesting, since when this occurs we can use standard database techniques to evaluate graph queries with recursion.

Conclusion

We have explained how fixpoint logics can be increased in expressivity while retaining decidability, by allowing unguarded parameters. We have also undertaken a fine-grained analysis of the complexity of static analysis problems for the resulting logics.

A limitation of our analysis is that it restricts to reasoning over all structures, both finite and infinite. In contrast, [START_REF] Bárány | Finite satisfiability for guarded fixpoint logic[END_REF][START_REF] Segoufin | Unary negation[END_REF] have shown that unparameterized guarded fixpoint logics have decidable satisfiability problems over finite structures. It is not clear if the technique of [START_REF] Bárány | Finite satisfiability for guarded fixpoint logic[END_REF] extends to deal with unguarded parameters.

The results about testing first-order definability of fixpoint logics and recursive queries (e.g. Theorem 26) do not include complexity bounds. We conjecture that the cost automaton results could be analyzed and refined further (as was done in [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF]) to extract at least an elementary bound (and, ideally, a 2-ExpTime bound). For cases without negation, like FO definability of C2RPQs, it may well be possible to extend the more elementary automata-theoretic approach used to decide boundedness for monadic Datalog [START_REF] Cosmadakis | Decidable optimization problems for database logic programs[END_REF], avoiding the use of cost automata altogether.

A. Missing proofs from Section 2

A.1 Proof of Proposition 2 (GNFP-UP strictly more expressive than GNFP)

We prove:

GNFP-UP is strictly more expressive than GNFP, even over finite structures. In particular, it cannot express the transitive closure of a binary relation R. We claim this cannot be expressed in GNFP, and hence the transitive closure of R is not expressible in GNFP.

Assume there were a GNFP sentence of width k (when in normal form) equivalent to . Let A be the structure with a single R-loop of length k + 1, with every element in the loop satisfying Q. Let B be the structure built by starting from an R-chain of three elements, and then adding an R-loop of length k + 1 to the first and third elements, and labelling all elements with Q. In other words, B has two lassos, one terminating at the second element, and the other starting from the second element. Notice that A satisfies , but B does not because the second element is not part of an R-cycle.

We now define a winning strategy for Duplicator in the k-width all-at-once game between A and B. This is the bisimulation game associated with normal form GNFP k from [START_REF] Bárány | Guarded negation[END_REF]. It is an infinite game played on a pair of structures A, B by two players: Spoiler and Duplicator. The game has two kinds of positions: i) pairs of guarded tuples (m, n), such that m 7 ! n is a partial isomorphism from A to B; and ii) partial homomorphisms h :

A X ! B Y or g : B Y ! A X ,
where X ⇢ A and Y ⇢ B, both finite and |X|, |Y|  k. From a position (m, n) Spoiler must choose a finite subset X ⇢ A or a finite subset Y ⇢ B , in either case of size at most k, upon which Duplicator must respond by a homomorphism with domain X or Y accordingly, mapping it into the other structure in a manner consistent with m 7 ! n. From a position h : X ! Y Spoiler chooses a guarded tuple m inside X taking the play to the position (m, h(m)). Similarly, from a position g : Y ! X Spoiler chooses a guarded tuple n in Y taking the play to the position (g(n), n). Spoiler wins if he can force the play into a position from which Duplicator cannot respond, and Duplicator wins if she can continue to play indefinitely.

A winning strategy for Duplicator implies agreement between the structures on GNFP k sentences, so proving the existence of a winning strategy for Duplicator in the game between the structures A and B defined above will yield the desired contradiction.

Duplicator's winning strategy will maintain the property that any group of R-connected elements that Spoiler selects in the active structure are R-connected in the other structure, and any elements that are R-connected to the starting position in the active structure are R-connected to the starting position in the other structure. Notice that any position in the game consists of at most two R-connected elements.

If the active structure is A, then when Spoiler selects his set of elements, there must be at least one element in the loop that is not selected. For pebbles that are forward (respectively, backward) connected to the starting position, we place these in the corresponding forward (respectively, backward) connected positions in B. Any other blocks of pebbles that are not connected to the starting position can be placed arbitrarily (as long as R-connected blocks stay together).

If the active structure is B, then the most interesting case is when Spoiler plays pebbles both inside a lasso and outside of it. For instance, if the starting position is the first element in the chain, and Spoiler selects both R-successors of this position (i.e. the second element in the chain and the first element in the R-loop starting from the first element), then Duplicator maps both of these pebbles to the same element in A (the single successor of the starting position in A). This is acceptable, because it is not possible for Spoiler to select all of the elements in a single lasso, which would be needed to distinguish between these two di↵erent successors. Using this sort of strategy, Duplicator can always choose her pebble positions in A so that R-connected blocks of elements are preserved. ⇤

A.2 Proof of Proposition 3 (GFP-UP is not more expressive than GFP)

Recall the statement:

For every answer-guarded GFP-UP[ ] formula , we can construct an equivalent GFP[ ] formula 0 using fixpoint predicates of higher arity such that

| 0 | is linear in | |.
Proof. Consider an answer-guarded GFP-UP formula gdd(xz) ^[lfp z Y,y . gdd(y) ^ (yz)](x). We claim that we can replace this with

gdd(xz) ^[lfp Y 0 ,yz . gdd(yz) ^ 0 (yz)](xz)
where 0 is the result of replacing Y w with Y 0 wz in .

Fix some structure A, and a valuation z 7 ! c. We need to argue that although there may be tuples b in the fixpoint such that bc is not guarded, for any a in the fixpoint for such that ac is guarded, we can witness this in the fixpoint only using other tuples that are also guarded with c. We define an alternative fixpoint semantics ˆ based on this idea: ˆ 0 (A) := ;

ˆ +1 (A) := ˆ A ( ˆ (A)) ˆ (A) := [ 0 <
ˆ 0 (A) for a limit ordinal where ˆ A (V) := a : ac is guarded and A, V | = (ac, Y) . We can prove by induction on the fixpoint approximant , that for all a such that ac is guarded, a 2 (A) i↵ a 2 ˆ (A). The base and limit ordinal cases of the induction are trivial. For a successor ordinal + 1, consider some a 2 +1 (A) such that ac is guarded.

Then A | = (ac, (A)). Consider occurrences of Yw in . If w contains only variables from xz, then this tuple must be guarded by assumption on ac, so we can replace Yw with gdd(wz) ^Yw in and still have a logically equivalent formula. If w contains variables outside of xz, then Yw must occur under some quantification that guards wz, so we can replace Yw with gdd(wz) ^Yw and still have a logically equivalent formula. In other words, a being in the ( + 1)-approximant of the fixpoint only depends on tuples in the -approximant that are guarded with c. Overall, this means that A | = (ac, ˆ (A)), so a 2 ˆ +1 (A) as desired. The other direction is trivial. This argument justifies the substitution described in the first paragraph.

In an answer-guarded GFP-UP formula, all fixpoints must be answer-guarded. Hence, we can apply the substitution described in the first paragraph to all fixpoints to yield an equivalent GFP formula, with fixpoints of possibly higher arity. ⇤

B. Missing proofs from Section 4 B.1 Proof of Proposition 6 (Tree-like model property for GNFP-UP)

We prove:

Every satisfiable (GNFP-UP) k [ ] sentence has a model of tree-width at most k + |const( )| 1.

Bisimulation game

In order to prove the tree-like model property, we begin by defining a GN-bisimulation game between structures A and B, that captures when two structures agree on certain guarded negation formulas. We write f : a 7 ! b to indicate a partial map f from A to B with domain set(a), range set(b), and f (a i ) = b i , where set(c) denotes the set of elements in the tuple a.

A position in the GN k [ ] bisimulation game between A and B (relative to some signature , possibly with constants) is a partial map f :

a 7 ! b or f : b 7 ! a such that |dom( f )|  k + |const( )|.
dom( f ) must include the interpretation of the constants in . Moreover, we require that f is a partial rigid homomorphism: that is, f is a partial homomorphism and for any guarded tuple c in dom( f ), f c (the restriction of f to set(c)) is a partial isomorphism. The structure containing dom( f ) is called the active structure.

Starting in position f , one round of the game consists of the following:

Restrict Spoiler can choose some tuple c such that set(c) ✓ dom( f ) contains the interpretation of all constants, and then the game proceeds from position f c ; or Switch if dom( f ) is a guarded set, then Spoiler can choose to switch structures, and the game proceeds from position f 1 ; or Infinitary logic A winning strategy for Duplicator implies agreement between A and B on certain guarded negation formulas in GNF 1 . Formulas in GNF 1 are built up from atoms using conjunction, guarded negation, and infinitary disjunction W (for a possibly infinite set of formulas). This is like GNFP-UP, except the least fixpoint case is replaced by infinitary disjunction. We write GNF k 1 for the k-width fragment (i.e. the maximum number of free variables in any subformula is at most k). Proposition 27. Assume Duplicator has a winning strategy in the GN k [ ]-bisimulation game between A and B starting from position a 7 ! b.

Add if |dom( f )| < k + |const( )|,
If (x) 2 GNF k 1 [ ] and A, a | = (x), then B, b | = (x).
Proof. The proof is a straightforward induction on the structure of (x). Let f : a 7 ! b be the initial position. The base case is trivial, since the position a 7 ! b is a partial rigid homomorphism.

Suppose is an infinitary disjunction of the form W . Since A, a | = (x), there is some 2 such that A, a 0 | = , where a 0 ✓ a are the elements corresponding to free( ) ✓ x. Consider the move where Spoiler restricts to a 0 . Since this is a valid move in the game, we know that Duplicator still has a winning strategy from f 0 := f a 0 , so the inductive hypothesis implies that B, f 0 (a 0 ) | = , and hence B, f (a) | = . The argument is similar for with the outermost connective a conjunction.

Suppose is of the form 9y. (xy). Since the width of is at most k, we know that |x [ {y}|  k, and hence it is possible for Spoiler to add an element in the game. Consider the move in the game corresponding to Spoiler adding the witness c such that A, ac | = (xy). Since Duplicator has a winning strategy, there is some d in B such that Over structures of some fixed cardinality, GNFP-UP can be expressed in GNF 1 . Proposition 28. For all 2 (GNFP-UP) k [ ] and for all cardinals , there is

f 0 := f [c 7 ! d]
0 2 GNF k 1 [ ] such that for all structures A of cardinality at most , A | = i↵ A | = 0 . Proof. Consider := [lfp z Y,y . gdd(y) ^ 0 ](x) for 0 2 GNF k 1 [ ].
Then for each ordinal , the -approximant to the fixpoint defined by can be expressed in GNF 1 , while preserving the width. This is easily shown by transfinite induction on . Now given 2 (GNFP-UP) k [ ] and , we work from the inside out, replacing each fixpoint definition with its  + 1 approximant, an upper bound on the closure ordinal where the fixpoint is reached in structures of cardinality at most . ⇤

Unravelling The tree-like models for GNFP-UP (and indeed, for GNF and GNFP) can be obtained using an unravelling construction based on the GN bisimulation game. Fix a structure A. Consider the set ⇧ of sequences of the form X 0 X 1 . . . X n , where X 0 = const( ) A , X i ✓ dom(A) with |X i |  k, and X i+1 = X i [ {a} for some a 2 dom(A) \ X i , or X i+1 ✓ X i . We can arrange these sequences in a tree based on the prefix order. Each sequence ⇡ = X 0 X 1 . . . X n identifies a unique node in the tree; we say a 2 dom(A) is represented at node ⇡ if a 2 X n . For a 2 dom(A), we say ⇡ and ⇡ 0 are a-equivalent if a is represented at every node on the unique minimal path between ⇡ and ⇡ 0 in this tree. For a represented at ⇡, we write [⇡, a] for the a-equivalence class.

The GN k [ ]-unravelling of A is the structure A k with universe [⇡, a] : ⇡ 2 ⇧, a represented at ⇡ and such that e A k := [X 0 , e A ] for X 0 := const( ) A and R A k ([⇡ 1 , a 1 ], . . . , [⇡ j , a j ]) i↵ R A a 1 . . . a j and there is some ⇡ 2 ⇧ such that for all i, [⇡, a i ] = [⇡ i , a i ].
There is a natural tree decomposition of width k + |const( )| 1 for A k induced by the tree of sequences from ⇧. Note that this tree may have unbounded, infinite degree.

Proposition 29. The GN k [ ]-unravelling A k of A is GN k [ ]- bisimilar to A.
Proof. We distinguish safe positions f in the GN k [ ]-bisimulation game between A and

A k : if the active structure is A k , then f is safe if for all [⇡, a] 2 dom( f ), f ([⇡, a]) = a; if the active structure is A, then f is safe if there is some ⇡ such that f (a) = [⇡, a] for all a 2 dom( f ).
We now argue that starting from a safe position f , Duplicator has a strategy to move to a new safe position f 0 . This is enough to conclude that Duplicator has a winning strategy in the GN k [ ]bisimulation game between A and A k starting from any safe position.

First, assume that the active structure is A k .

• If Spoiler restricts to some subset, then the restriction of f is clearly still safe. • If Spoiler adds an element [⇡ 0 , a 0 ], then Duplicator should choose a 0 in A to maintain safety. This new map

f 0 = f [[⇡ 0 , a 0 ] 7 ! a 0
] is still a partial homomorphism since any relation holding for a tuple of elements [⇡ 1 , a 1 ], . . . , [⇡ n , a n ] from dom( f 0 ) must hold for the tuple of elements a 1 , . . . , a n in A by definition of A k . It is possible that there is some [⇡, a 0 ] in dom( f 0 ) with [⇡, a 0 ] , [⇡ 0 , a 0 ]; however, [⇡, a 0 ] and [⇡ 0 , a 0 ] are not guarded in A k . Hence rigidity of f implies that any restriction f 00 of f 0 to a guarded set of elements is a bijection. Moreover, such an f 00 is a partial isomorphism: consider some a 1 , . . . , a n 2 rng( f 00 ) for which some relation R holds in A; since ( f 00 ) 1 (a 1 ), . . . , ( f 00 ) 1 (a n ) must be guarded, we know that there is some ⇡ such that [⇡, a 1 ] = ( f 00 ) 1 (a 1 ),. . . , [⇡, a n ] = ( f 00 ) 1 (a n ), so by definition of A k , R holds of ( f 00 ) 1 (a 1 ), . . . , ( f 00 ) 1 (a n ) as desired. Hence, f 0 is a safe rigid partial homomorphism. • If Spoiler switches structures, then we know that dom( f ) is guarded by some relation R, so there is some ⇡ with f (a) = [⇡, a] for all a 2 dom( f ) by construction of A k . Hence, f 0 = f 1 is still safe. Now assume that the active structure is A. Since f is safe, there is some ⇡ such that f (a) = [⇡, a] for all a 2 dom( f ). Let X be the set of elements represented at ⇡.

• If Spoiler restricts to some subset, then the restriction of f is still safe. • If Spoiler adds an element a 0 , then Duplicator should choose [⇡ 0 , a 0 ], where ⇡ 0 = ⇡(X [ {a} 0 ). By construction of the unravelling, ⇡ 0 2 ⇧ and the resulting partial mapping f 0 still satisfies the safety property with ⇡ 0 as witness. Now consider some tuple a = a 1 . . . a n of elements from dom( f 0 ) that are in some relation R. We know that f (a i ) = [⇡ 0 , a i ], hence R must hold for f (a) in A k . Moreover, for any guarded set a = {a 1 , . . . , a n } of distinct elements from dom( f 0 ), we know that f (a) yields a set of distinct elements { f (a 1 ), . . . , f (a n )}, and these elements can only participate in some fact in A k if the underlying elements from a participate in the same fact in A. Hence, f 0 is a safe partial rigid homomorphism.

• If Spoiler switches structures, then f 0 = f 1 is still safe. This is enough to conclude that Duplicator has a winning strategy starting from any safe position (in particular, the empty position), so A k and A are GN k [ ]-bisimilar. ⇤

We can now conclude the proof of Proposition 6. Assume that A is a model of 2 (GNFP-UP) k [ ], and let  be the cardinality of A k . By Proposition 28, there is an equivalent 0 2 GNF k 1 [ ], at least on structures of cardinality at most . By Propositions 27 and 29, this means that A k is also a model of 0 . Hence, we can conclude that the unravelling A k is the desired tree-like model of .

B.2 Proof of Proposition 7 (GNFP-UP to GSO)

We prove:

Given 2 GNFP-UP[ ], we can construct an equivalent 0 2 GSO[ ].
Proof. By structural induction on . The interesting case is for the least fixpoint. If (yz) = [lfp z X,x . gdd(x) ^ (X, x, z)](y) then 0 (yz) := 8X.[(8x.((gdd(x) ^ 0 (X, x, z)) ! Xx)) ! Xy] where second-order quantifiers range over guarded relations. This uses the characterization of the least fixpoint as the intersection of all prefixpoints. Although the body of the fixpoint may use parameters z, the tuples in the fixpoint are all guarded, so it su ces to range only over prefixpoints that are guarded relations (i.e. only contain tuples that are guarded by relations in ). ⇤

C. Missing proofs from Section 5

C.1 Proof of Theorem 13 (Localization)

Recall the statement:

Let ⌃ 0 := ⌃ [ {P 1 , .
. . , P j }. Let A 0 be a 1-way nondeterministic parity automaton on ⌃ 0 -trees. We can construct a 2-way alternating parity automaton A on ⌃-trees such that for all ⌃-trees T and v 2 dom(T ), A 0 accepts T 0 from the root i↵ A accepts T from v, where T 0 is the ⌃ 0 -tree obtained from T by setting

P T 0 1 = • • • = P T 0 j = {v}.
The number of states of A is linear in the number of states of A 0 , and the overall size is linear in the size of A 0 .

Proof. Roughly speaking, A simulates A 0 by guessing in a backwards fashion an initial part of a run of A 0 on the path from v to the root and then processing the rest of the tree in the normal downwards fashion. The subtlety is that the automaton A is reading a tree without the valuation for P 1 , . . . , P j so once the automaton leaves node v, if it were to cross this position again, it would be unable to correctly simulate A 0 . To avoid this problem, we only send downwards copies of the automaton in directions that are not on the path from the root to v.

The state set of

A is {q 0 } [ Q A 0 [ ({l, r} ⇥ Q A 0
) consisting of initial state q 0 , downwards mode states of the form q 2 Q A 0 and upwards mode states of the form (d, q) 2 ({l, r} ⇥ Q A 0 ).

We describe the acceptance game of A on some ⌃-tree T starting in node v 2 dom(T ); the actual transition function for the automaton can be extracted from this.

Initially, in state q 0 at node v, Eve guesses some state q 2 Q A 0 and some (d 1 , r 1 ) ^(d 2 , r 2 ) in A 0 (q, T 0 (v)), where T 0 is the tree obtained from T by taking

P T 0 1 = • • • = P T 0 j = {v}.
If v is the root, then q must be q 0 A 0 . Adam can either challenge some (d i , r i ) and move in direction d i to downward state r i , or (if v is not the root) he can move to the parent and switch to upward mode state (d, q), where v is the d-child of its parent.

In downwards mode state r at node w, the original automaton A 0 is simulated, i.e. Eve guesses some (d 1 , r 1 )^(d 2 , r 2 ) in A 0 (r, T (w)), and then Adam chooses some i and moves in direction d i to state r i .

In upwards mode state (d, r) at node w, Eve guesses some state q and some (d, r) ^(d 0 , r 0 ) or (d 0 , r 0 ) ^(d, r) that is a disjunct in (q, T (w)). If w is the root, then q must be q 0 A 0 . Adam can either move in direction d 0 to downward state r 0 , or (if w is not the root) he can move to the parent of w in upward mode state (d 00 , q), where w is the d 00 -child of its parent. Note that Adam is not allowed to move in direction d, since this where the automaton came from.

The priority assignment is given by ⌦ A (q 0 ) := 1, ⌦ A (r) := ⌦ A 0 (r), and ⌦ A ((d, r)) := ⌦ A 0 (r).

If there is an accepting run ⇢ 0 of A 0 on T 0 , then it is not hard to see that this induces a winning strategy ⇢ for Eve in the game G(A, T , v): Eve guesses in a backwards fashion the part of the run ⇢ 0 on the path from v to the root, and then processes the rest of the tree in a normal downwards fashion, using ⇢ 0 to drive her choices. Using this strategy, any play is infinite and a su x of this play (namely, once the play has switched to downward mode) corresponds directly to a su x of a play in ⇢ 0 . Since the priorities in these su xes are identical, the parity condition must be satisfied, so ⇢ is winning, and A accepts T starting from v.

Now suppose Eve has a winning strategy ⇢ in the acceptance game G(A, T , v). Using ⇢, we stitch together an accepting run ⇢ 0 of A 0 on T 0 . Recall that such an accepting run can be viewed as a labelling of T 0 with states consistent with A 0 and T 0 such that the maximum priority occurring infinitely often on each branch is even. We construct this labelling starting at v, based on Eve's guess of the state in the initial state. The labelling of the subtree rooted at v is then induced by the plays in ⇢ that switch immediately to downward mode at v. We can then proceed to label the parent u of v, by considering Eve's choice when Adam stays in upward mode and moves to the parent u of v. If v is the d-child of u, then the subtree in direction d from u is already labelled; the subtree in the other direction can be labelled by considering the plays when Adam switches to downward mode at u. Continuing in this fashion, we obtain a labelling of the entire tree with states such that q 0 A 0 is the label at the root and the other labels are consistent with A 0 on T 0 (it is consistent with T 0 and not T , because in the initial state, Eve's choice of state and disjunct is under the assumption of the extra predicates present at v). Every branch in this run tree satisfies the parity condition, since a su x of the branch corresponds to a su x of a play in ⇢ that satisfies the parity condition. Hence, A 0 accepts T 0 from the root. ⇤

D. Missing proofs from Section 6 D.1 Proof of Proposition 15 (Automaton checking consistency)

Recall the statement:

There is a 2-way alternating parity tree automaton C that checks whether or not a ˜ k -tree (possibly extended with additional free variable markers for z and Z) is consistent. The size of C is at most exponential in

(| | + |z| + |Z|) • |U k | k .
Proof. We can construct a 2-way alternating parity tree automaton for each consistency condition, and then take the product of these automata using Proposition 9. The constructions are straightforward, but we give one example, for the automaton checking the condition for all constants z 2 , there is exactly one node w and one c 2 names(w) such that V c/z v.

The automaton can be launched from any position in the tree. First, Eve navigates to a node v where some V c/z holds. While she is doing this, the automaton is in a state with priority 1. If she finds a node like this, then the automaton switches to a state with priority 0. In this state, Adam tries to navigate to a di↵erent node v 0 , v where V d/z holds. He does this by choosing at each stage a direction to move in, with the restriction that he cannot move in the direction he came from (to ensure that he does not return to v). Hence, the automaton must record in its state whether the previous node was in direction l, r, or ". If he finds some V d/z at v 0 , v, then the automaton enters a sink state with priority 1, and Adam wins. There are a constant number of states, and the overall size is linear in the size of the alphabet, which is exponential in

(| |+|z|+|Z|)•|U k | k . ⇤ D.

Proof of Lemma 17 (Automata for GNFP)

We prove the following result about automata for GNFP: Let (y, Z) 2 GNFP k [ 0 ] in normal form. Then for every local assignment b/y, we can construct a 2-way alternating parity tree automaton A b/y such that for all consistent ˜ 0 ktrees (T , Z ! ) and for all nodes w 2 dom(T ) with b ✓ names(w),

D(T ), [w, b], Z | = i↵ A b/y accepts (T , Z ! ) from w.
There is a polynomial function f independent of such that the number of states for all such localized automata is at most A similar result was already known from [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF]. We cannot directly use this previous result, since this earlier work used a slightly di↵erent encoding of the tree-like models: we use a binary encoding here rather than working with trees with arbitrary branching degree; and we mark a free variable or constant in one node only rather than the entire connected part of the tree containing this element.

N := f (m) • 2 f
We present a construction here designed for our encodings. It is similar to the construction in [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF], but it utilizes the localization theorem (Theorem 13). and deals directly with equality (whereas the construction in [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF] treats equality separately).

We are now ready to give the automaton construction for GNFP.

Proof of Lemma 17. We describe the construction of A b/y , which proceeds by induction on the structure of . Instead of formally specifying the transition function of the automaton, we describe the operation of A b/y in terms of the roles of Adam and Eve. Let z denote the constants in 0 .

• Assume is an atomic formula R t for R 2 0 and t = t 1 . . . t j . We first construct a 2-way alternating automaton running on trees with markers for free( ). Eve navigates to a node w 0 with some R a . If she is able to do this, Adam can then challenge Eve to show that t corresponds to a. Say he challenges her on a i 2 a.

Then Eve must navigate from w 0 to the node w 00 carrying the marker for t i and check that this marker is a i . However, she must do this by passing through a series of biological neighbors that also contain a i (the intermediate nodes in between biological neighbors might not contain a i ), to ensure that the a i in w 0 corresponds to the same element in w 00 . If she is able to do this, she wins (the automaton enters a sink state with priority 0). The other states are assigned priority 1.

The number of states of the automaton is linear in kl (indeed, linear in |U k |), since the automaton must store the name a i that Adam is challenging. We can convert this into an equivalent nondeterministic parity tree automaton with a state set of size exponential kl. We can localize this nondeterministic automaton to get localized 2-way alternating parity tree automata with a combined state set exponential in kl.

The construction is similar for of the form Z t for Z 2 Z, or for the guardedness predicate gdd(y). • Assume is an equality of the form t 1 = t 2 . Again, we first construct an automaton running on trees with the free variable markers. Eve navigates to the node carrying the marker for t 1 , with some name a. Then she must navigate to the node carrying t 2 , by navigating along biological neighbors that also carry a.

If she is able to do this, she wins (the automaton enters a sink state with priority 0). The other states are assigned priority 1.

The number of states of the automaton is linear in kl, since the automaton must store the name a for t 1 . We can convert this into an equivalent nondeterministic parity tree automaton with a state set of size exponential kl. We can localize this nondeterministic automaton to get localized 2-way alternating parity tree automata with a combined state set exponential in kl.

• Assume is a CQ

9x.(↵ 1 (xy) ^• • • ^↵ j (xy)).
This case is helpful for handling the general CQ-shaped formulas below. Again, we start by defining an automaton that runs on trees with the free variable markers. Take the intersection of the automata for each ↵ i (running on trees with markers for the free variables), together with an automaton checking that the free variable markers for x are unique. This results in a 2-way alternating automaton C of size linear in kl j  klr. Using Theorem 12, we can then construct an equivalent nondeterministic tree automaton B with an exponential blow up in the number of states. The desired automaton is the projection of B on the free variable markers: it simulates B while guessing the markers for the free variables x. Even after localization, the number of states is still at most exponential in klr.

• Assume is a CQ-shaped formula 9x.( 1 (xy) ^• • • ^ j (xy)).
We know that each i is either an atom, or is a guarded subformula (i.e., the free variables in i are guarded). We first construct an automaton N for the CQ obtained from by replacing each non-atomic guarded subformula i with a new predicate Y i . Examining this case above, we see that this automaton is of size at most exponential in klr. Note that this automaton runs on trees with a valuation for these guarded subformula predicates marked on the tree. The desired automaton starts by simulating N, but with Eve guessing valuations for the guarded subformula predicates Y i . Adam can either accept Eve's guesses of the valuation and continue the simulation of N, or can challenge one of Eve's assertions for some Y i by launching the localized version of i . The number of states is linear in the sum of the number of states of N and the automata for the i , which is at most exponential in klr but polynomial in | |.

• Assume is of the from W i i . Then Eve chooses some i and launches A b i /y i i from w.

• Assume is of the form ↵ ^¬ 0 . Let A b/y be the automaton where Adam chooses whether to simulate A b/y ↵ or the dual of A b/y 0 . • Assume is of the form gdd(y) ^ 0 . Let A b/y be the automaton where Adam chooses whether to simulate A b/y gdd(y) or

A b/y 0 . • Assume is a fixpoint [lfp X,x . 0 (x, X, Z)](t).
Let A b/y be the automaton in which Eve navigates to a node w 0 with t

0 = t[b/y, c/z] such that [w 0 , b] = [w, b] and [w 0 , c i ] = [w i , c i ]
where w i is the node with the marking V c i /z i (she immediately loses if she does not navigate to such a node). Eve then simulates A t 0 /x 0 while guessing a valuation for X ! . During this simulation, if Eve guesses that X a holds at u, then Adam can challenge this choice by launching another copy of A a/x 0 from u; the priority in this case is some odd priority larger than the priorities in A t 0 /x 0 . The simulation continues in a similar fashion (with Eve guessing a valuation and Adam allowed to challenge these guesses). The number of states is linear in the the sum of the sizes of the state sets for the localized versions of 0 , which meets the desired bound.

• Assume is a simultaneous fixpoint of the form [lfp X i ,x i .S ](t).

We proceed as in the previous case, starting with automata for the formulas in the equations in S , and allowing Eve to guess a valuation for X ! j for each second-order variable X j in the system. Adam can challenge these guesses by launching the appropriate automata for formulas in S as described before.

⇤ D.3 Proof of Lemma 18 (Automata for GNFP-UP)

We prove the following result about automata for GNFP-UP:

Let (y, z, Z) be a subformula of ✓ 2 (GNFP-UP) k [ ] with params( ) ✓ z. For each local assignment b/y, we can construct a 2-way alternating parity tree automaton B b/y such that for all consistent ˜ k -trees (T , z ! , Z ! ) and for all nodes w 2 dom(T ) with b ✓ names(w),

D(T ), [w, b], z, Z | = i↵ B b/y accepts (T , z ! , Z ! ) from w.
For pdepth z ( ) 1, there is a polynomial function f independent of such that the size of all such localized automata is at most exp Assume 0 := transform z ( ) is helpful. Note that this always holds for the smallest (atomic) formulas, so this covers the base of the induction. We construct B b/y to simulate the automaton A b/y 0 from Lemma 17, while allowing Eve to guess valuations for the F ⌘ relations from 0 . Constants and free variables are encoded in the same way, so it makes no di↵erence that we are viewing z as free variables in the automaton for and as constants in the automaton for 0 . Since 0 is helpful, we know that every F ⌘ relation in 0 is for some formula ⌘ that is strictly smaller than , and hence the inductive hypothesis ensures there is a corresponding automaton for every suitable local assignment. During the simulation of A b/y 0 , if Eve asserts F ⌘(x) a at w for some a ✓ names(w), then Adam can challenge this by launching the automaton for the intersection of B a/x ⌘(x) and B a/x gdd(x) from w; likewise, if Eve does not assert F ⌘(x) a at w for some a ✓ names(w), then Adam can challenge this by launching the automaton for the dual of the intersection of B a/x ⌘(x) and B a/x gdd(x) from w. Correctness follows from Lemma 17, Lemma 30 (see below), and the fact that the inductive hypothesis ensures that the subautomata for F ⌘ in 0 are correct. Observe that the size of A b/y 0 is at most exp(g(mn) • 2 g(klr) ) for some polynomial function g, since | z, |  m+n. The size of the subautomata for each F ⌘ relation appearing in 0 is at most exp pdepth z (⌘) f ( f (|⌘|n) • 2 f (klr) ). Moreover, the sum of the sizes of these subformulas ⌘ is strictly less than the size of . Assuming f su ciently dominates g, this ensures that the size of the automaton for is at most exp

pdepth z ( ) f ( f (| |n) • 2 f (klr) ).
Next, assume that 0 := transform z ( ) is unhelpful. Then we need to consider two possible cases. Throughout these arguments we make use of the closure properties described in Section 5.

• The first case is that is a UCQ-shaped subformula

_ i 9x i . ĵ i j
where variables from some x i are used as parameters in V j i j . To start, we consider each CQ-shaped formula separately, so fix some 9x i .

V j i j . We use the inductive hypothesis to obtain 2way alternating automata for each conjunct i j , using the empty local assignment. This is possible since the size of these conjuncts must be strictly less than the size of . Because we are using the empty local assignment, these automata operate on trees with markers for all of the free variables: x i [ y [ z. Take the intersection of these automata using Proposition 9. Then take the intersection with the automaton from Proposition 15 checking consistency. This yields a 2-way alternating automaton corresponding to V j i j . We then convert this automaton to a nondeterministic version using Theorem 12 and project away the information about x i using Proposition 10. This yields an equivalent (1-way) nondeterministic parity automaton for the CQ. Next, we localize this automaton to the desired variables y using Theorem 13. Finally, to construct the automaton B b/y , we take the union of the individual CQ automata using Proposition 9. The conversion from a 2-way alternating automaton to a nondeterministic automaton is the costly step in this process, resulting in an exponential blow-up. Observe that pdepth( i j ) < pdepth z ( ) for each conjunct i j in the CQs. If pdepth z ( ) 2, then the size of each B ;/;

i j is at most exp

pdepth z ( ) 1 f ( f (| i j |n) • 2 f (klr)
), so we can absorb the exponential blow-up. Likewise, if pdepth z ( ) = 1, then the size of each B ;/;

i j is at most exp(g(| i j |n) • 2 g(klr) ) but the number of states is at most g(| i j |) • 2 g(klr) for some polynomial function g. Because the conversion to a 1-way nondeterministic automaton is actually exponential only in the size of the state set, this means that we can absorb the blow-up here too. In either case, it can be checked that the size of B b/y is at most exp

pdepth z ( ) f ( f (mn) • 2 f (klr) ).
• The second case is when is a fixpoint formula where fixpoint variables are used as parameters in the body of the fixpoint. Suppose is of the form [lfp z 0 X,x . gdd(x) ^ (xz 0 , XZ)](t) where params( ) \ x , ;, so params( ) * z. The formula in the body of the fixpoint is strictly smaller, so we can apply the inductive hypothesis to get an automaton for this part. We want this automaton to be localized to x so we can test for tuples in the fixpoint by launching copies of the automaton for some local assignment. However, the inductive hypothesis does not directly yield this, since some variables from x are used as parameters. Hence, we must use the inductive hypothesis to get a 2-way automaton for B ;/; 0 , apply Theorem 12 to get an equivalent 1-way nondeterministic automaton, and then localize to some assignment a/x using Theorem 13. Once we have these localized automata B a/x for the body of the fixpoint, we can proceed as we did for the fixpoint case in the GNFP automaton construction. The conversion between 2-way and 1-way nondeterministic automata results in an exponential blow-up, but pdepth z ( ) = pdepth z ( ) + 1, so the size of the fully localized automata for are at most exp klr) ). Hence, the overall size of the automaton is at most exp

pdepth z ( ) f ( f (| |n) • 2 f (
pdepth z ( ) f ( f (mn) • 2 f (klr) ).
The argument is similar if is a simultaneous fixpoint.

⇤

In the previous proof, we made use of the following straightforward lemma, which just says that the GNFP formula obtained using the transformation operation is "equivalent" to the GNFP-UP formula, under the assumption that the additional predicates in the augmented signature used by the GNFP formula are interpreted in the expected way. Proof. We proceed by induction on the structure of . For notational simplicity, we omit the second-order variables Z in the parts of the argument where these do not play a role.

• If is atomic, then the result is immediate since z M 0 := c.

• Assume is of the form ↵^¬ . Then 0 := ↵^¬transform z\free( ) ( ). Otherwise, consider the case when 0 = [lfp X,x . gdd(x) transform z ( (x, XZ))](t). We can prove by a straightforward induction on the fixpoint approximant (an ordinal) that for all -guarded tuples a, a 2 M i↵ a 2 (transform z ( )) M 0 . The result follows by noting that the least fixpoint is the union over these approximants, and t[b/y, c/z] must be -guarded to be in either of the fixpoints defined by and 0 .

• Assume is W i 9x i . V j i j . Consider the case when 0 is F ⌘ y. Since b is -guarded by assumption, M | = [b/y, c/z] i↵ M 0 | = (F ⌘ y)[b/y] by definition of S M 0 . On the other hand, if 0 is W i 9x i .
V j transform z\free( i j ) ( i j ), then the result follows by a straightforward application of the inductive hypothesis.

⇤

This completes the proof of Lemma 18.

E. Missing proofs from Section 7 E.1 Proof of Theorem 20 (Satisfiability for GNFP-UP)

We prove: Satisfiability for ✓ 2 GNFP-UP is decidable in (pdepth(✓) + 2)-ExpTime.

Proof. Let k be the width of ✓. We first consider the case when pdepth(✓)

1. Given ✓ 2 GNFP-UP with signature , we can construct a 2-way alternating parity tree automaton B ;/; ✓ using Theorem 16 or Corollary 19 of (pdepth(✓) + 1)-exponential size, since the width, CQ-rank, and number of constants are at most |✓|. Take the product of B ;/;

✓ with the automaton C from Proposition 15 that checks that a tree is a consistent ˜ k -tree. Call the resulting automaton A ✓ . The size of A ✓ is still of (pdepth(✓) + 1)-exponential size. By the tree-like model property in Proposition 6, we know that there is a model for ✓ i↵ there is a tree-like model of tree-width k + |const(✓)| 1. Hence, ✓ is satisfiable i↵ L(A ✓ ) is empty. We can decide emptiness for a 2-way alternating parity tree automaton in ExpTime hence satisfiability ✓ can be decided in (pdepth(✓) + 2)-ExpTime.

For pdepth(✓) = 0, we can view ✓ as a GNFP formula (with any free variables viewed as constants) and apply Lemma 17 instead of Theorem 16 to start. Although the overall size of this automaton is doubly exponential in |✓|, the number of states is only single exponential and the number of priorities is linear. Moreover, emptiness for 2-way alternating parity tree automata is exponential only in the number of states and number of priorities, so the satisfiability test can be done in 2-ExpTime as desired. ⇤ E.2 Proof of Corollary 23 (Satisfiability for CQPDL)

We prove:

Satisfiability of CQPDLs (or boolean combinations of CQPDL sentences and GNFP sentences) is decidable in 2-ExpTime.

We first prove the following lemma about the translation of PDL programs and formulas into GNFP-UP: Lemma 31. For each PDL program P we can construct in PTime an equi-satisfiable GNFP-UP formula translate(P)(x, y) ^ P in normal form such that translate(P) has pdepth 0 and CQ-rank at most 3 and P has pdepth 1 and CQ-rank at most 3.

Likewise, for each PDL test t, we construct in PTime an equisatisfiable GNFP-UP formula in normal form translate(t)(x) ^ t such that translate(t) has pdepth 0 and CQ-rank at most 3 and t has pdepth 1 and CQ-rank at most 3.

Proof. The proof is by induction.

An atomic program P is a binary relation R (or its inverse R ); in this case, we set translate(P)(x, y) := Rxy (respectively, translate(P)(x, y) := Ryx). We set P := > in either case. Atomic tests are similar.

Consider an arbitrary program P. We start by flattening P into some P 0 such that every t? at the outer level in P is replaced with a new unary relation U t? . The resulting P 0 is a traditional regular expression over the original binary relations and the special unary relations U t? . We can then define translate(P) to be the normal form GNFP-UP formula that describes the operation of the finite state automaton A for P 0 . This is similar to Example 4, but for technical reasons, we describe the backwards operation of the automaton. In more detail: we start with a finite state automaton A for P 0 (obtained from P 0 in PTime), with states Q, initial state q 0 , and accepting states F. We write a GNFP-UP formula with simultaneous fixpoints [lfp x Y,y . S ](y) which has a second-order variable Y i for each state q i 2 Q, together with an additional variable Y. The equation for the j-th component Y j , y j in S captures the possible backwards transitions from state q j :

_ (q i ,T,q j )2 9z.( T (z, y j ) ^Yi z) _ ( y j = x if j = 0 ? if j , 0
where T (z, y j ) is Rzy j if T = R, Ry j z if T = R , and y j = z ^Ut? (z) if T = U t? . The equation for the goal predicate Y, y captures the acceptance condition: W q i 2F Y i y. This simultaneous fixpoint has parameters x, pdepth 0, and CQ-rank at most 3. We set P to be the conjunction of t for each U t? in P 0 , together with 8x.(U t? (x) $ translate(t)(x)) that describes the meaning of U t? ; this can be expressed in GNFP-UP since it uses only unary negation. Now consider an arbitrary test t. We can translate atomic tests using the inductive hypothesis. We replace any test of the form hPi in t with the GNFP-UP formula 9y.translate(P)(x, y), which still has pdepth 0 since translate(P)(x, y) has pdepth 0 and the quantified variable y is not used as a parameter in translate(P)(x, y). Since only unary negation is used, all boolean operations in t can also be expressed in GNFP-UP. Moreover, this boolean combination can always be written in normal form with only a polynomial blowup in size, and no change to the CQ-rank (since it is composed of only unary formulas, and the quantification comes only from the translation of hPi). Finally, t is obtained by taking the conjunction of P for all hPi appearing in t. ⇤ Now given some input CQPDL formula 9x.(P

1 (x 1 ) ^• • • ^Pn (x n ))
we can construct in PTime an equi-satisfiable GNFP-UP formula 9x.(translate(P

1 )(x 1 ) ^• • • ^translate(P n )(x n )) ^ P 1 ^• • • ^ Pn
of pdepth 1 using Lemma 31. Using Theorem 20, we can then get a 3-ExpTime bound on satisfiability for CQPDL. We can do better by noting that the formulas produced by Lemma 31 have a fixed width, fixed CQ-rank, and no constants. Hence, the size of the 2-way alternating automaton for P 1 ^• • •^ Pn is only exponential in the size of the input by Lemma 18. Moreover, the automaton for each translate(P i )(x i ) is only exponential in the size of the input, with state set of size only polynomial in the size of the input by Lemma 17. Thus, by taking the intersection of the 2-way alternating automata for the translate(P i )(x i ), converting to a nondeterministic version, and then projecting, we have an automaton for 9x.(translate(P 1 )(x 1 ) ^• • • ^translate(P n )(x n )) that is only exponential in the size of the input.

Using Lemma 17, the state set and priorities of automata for GNFP sentences is also only at most exponential in the size of the input using (although the overall size may be doubly exponential).

Hence, an automaton for a boolean combination of CQPDL sentences and GNFP sentences can be constructed in at most doubly exponential time, and has at most exponentially many states and priorities. Using Theorem 14, this means we can test satisfiability in doubly exponential time as desired in Corollary 23.

F. Missing proofs from Section 8

F.1 Proof sketch of Theorem 24 (Boundedness for GNFP-UP)

In this section, we sketch the proof of Theorem 24:

Assuming ILT, the boundedness problem is decidable for x-guarded (x, X) 2 GNFP-UP[ ] in non-elementary time (elementary time for fixed pdepth). In the special case of x-guarded (x, z, X) 2 GNF[ ], boundedness is decidable in elementary time (without assuming ILT).

We start with the first part of the theorem, about answer-guarded (x, X) 2 GNFP-UP. Like we did for satisfiability, we first observe that we can restrict to considering structures of bounded tree-width. Proposition 32. Let (x, X) 2 (GNFP-UP) k [ ] be positive in X (of arity |x|) and answer-guarded. Then (x, X) is bounded over allstructures i↵ it is bounded over tree-like -structures of tree-width at most k + |const( )| 1. This is a straightforward consequence of the tree-like model property of (GNFP-UP) k (Proposition 6), and the fact that the fixpoint approximants for natural numbers n are expressible in (GNFP-UP) k . It opens up the ability to use automata for boundedness, like we did earlier for the question of satisfiability. However, we must shift to using a type of automaton that can carry some quantitative information about the number of fixpoint unfoldings that are used.

In particular, we reduce the question of boundedness for (x, X) 2 (GNFP-UP) k [ ] to a question of boundedness for a cost automaton, a traditional automaton enriched with a finite set of counters that are initially zero and that can be incremented, reset, or left unchanged on each transition. A cost automaton B naturally defines a function ~B that maps an input to the least n 2 N [ {1} such that Eve has a winning strategy in the acceptance game that keeps the counter values below the threshold n. The boundedness problem for cost automata is: Given a cost automaton ~A over -trees, is there some n such that on all -trees T , ~A(T )  n? This is the target problem for our reduction.

The following theorem describes the automata that we construct. The idea is to adapt the automata we constructed in Theorem 16 to count the outermost fixpoint unfolding. This construction actually produces a special type of cost automaton called a distance ^parity automaton: it has only a single counter that is incremented or left unchanged on each transition (never reset). We only need a single counter like this, since we only have to count the unfolding of the single outermost fixpoint. Theorem 33. Let (x, X) 2 (GNFP-UP) k [ ] such that it is positive in X of arity |x| and answer-guarded, and pdepth( ) 1. There is a 2-way alternating cost automaton B on ˜ k -trees such that (x, X) is bounded over all -structures i↵ ~B is bounded over all ˜ k -trees. Moreover, B is a distance ^parity automaton of (pdepth( ) + 1)-size. The number of priorities is linear in | |.

Proof sketch. For a fixed structure A, what we want to measure is the threshold n such that for all guarded tuples of elements a in dom(A), if a is in the least fixpoint induced by , then a is in the n-unfolding of .

There is a cost automaton that computes this threshold for encodings of tree-like structures. The idea is to take the automata we constructed in Section 6 and add a single counter which is incremented exactly when the fixpoint is unfolded.

Claim 34. There is a 2-way alternating cost parity tree automaton B such that for all consistent ˜ k -trees T , ~B(T )  n i↵ for all tuples a 2 dom(D(T )), if a is in in the least fixpoint induced by in D(T ), then a is in the n-unfolding of in D(T ) 3 Moreover, B is a distance ^parity automaton of (pdepth( ) + 1)-size, and the number of priorities is linear in | |.

Proof of claim. Using Lemma 18, we can construct for each localization b/y a localized 2-way alternating parity tree automaton A b/y such that when launched from some node v in a consistent ˜ k -tree T , the automaton accepts just if D(T ), [v, b] | = [lfp X,x . gdd(x) ^ (x, X)](y). We can create a cost automaton based on this that actually counts the number of fixpoint unfoldings that are needed. Let B b/y be the result of taking A b/y and adding a single counter. This counter is never touched, except for the transitions when a fixpoint is unfolded: namely, the transitions where Adam challenges Eve's choice of valuation for X ! . The value of B b/y when it starts from v in a consistent ˜ k -tree T is n 2 N i↵ D(T ), [v, b] satisfies the n-unfolding of the fixpoint (but does not satisfy the n 0 -unfolding for any n 0 < n).

The automaton B operates as follows. First, Adam is allowed to navigate to some node in the tree, and pick out some guarded tuple (i.e. some node v and localization b/y). Eve can then choose whether to launch the dual of A b/y or the cost automaton B b/y . Note that Adam cannot force a high value by choosing tuples outside of the fixpoint, since in that case Eve can simply run the dual of A b/y , which will yield value 0. For actual guarded tuples in the fixpoint, however, Eve must simulate B b/y in order to win, so the value in this case will be the number of unfoldings required to witness that this tuple is in the fixpoint.

Overall, this ensures that ~B(T )  n i↵ for all tuples a 2 dom(D(T )), if a is in in the least fixpoint induced by , then a is in the n-unfolding of .

Due to the size bounds in Lemma 18, the size of B is at most (pdepth( ) + 1)-exponential in the size of . ⇤

The automaton guaranteed by this claim has the property that it is bounded over all consistent ˜ k -trees i↵ is bounded over all tree-like -structures of width k + |const( )| 1. However, the boundedness problem for cost automata talks about the values over all ˜ k -trees, not just consistent ˜ k -trees. Hence, the desired automaton B is just the union of B and the dual of the automaton C from Proposition 15 that checks that the input ˜ k -tree is consistent. This automaton B is bounded over all ˜ k -trees i↵ is bounded over all tree-like -structures of width k + |const( )| 1 i↵ (by Proposition 32) is bounded over all -structures. This concludes the proof sketch of Theorem 33. ⇤

It is not known in general whether boundedness is decidable for cost automata over infinite trees. However, boundedness for 2-way distance ^parity automata was shown to be decidable in [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF]Theorem 12], subject to the unpublished result of Colcombet (called ILT or Dual-Inf) Theorem 35 ([8, Theorem 12]). Boundedness for 2-way distance ^parity automata is decidable in elementary time, assuming ILT.

If only priorities {0, 1} are used, then boundedness is decidable in elementary time.

Together, Proposition 32, Theorem 33, and Theorem 35 imply the first part of Theorem 24. The complexity is non-elementary in general (because of the size of the automata), but elementary for fixed pdepth.

For the second part of the theorem, we are given x-guarded (x, z, X) positive in X of arity |x| but with extra parameters z, is there a natural number n such that for all -structures A and for all valuations z 7 ! c, does n (A, c) = n+1 (A, c)? This situation can be handled by the argument above by treating z as constants, i.e. by viewing as a formula over the signature 0 extending with constants for each z 2 z. However, it can be shown that the automaton B constructed in this case uses only priorities {0, 1}, so we can use an optimized result from [START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF]Theorem 12] which says that boundedness can be decided in elementary time (this is not subject to any unpublished results). This means that boundedness for x-guarded (x, z, X) 2 GNF[ ] is decidable in elementary time.

F.2 Proof sketch of Theorem 26 (FO definability of negation-free CQPDL)

The goal is to prove:

It is decidable whether or not a negation-free CQPDL sentence relative to a GNF sentence can be expressed in FO.

We start by considering a C2RPQ relative to GNF sentence ✓. The argument consists of two main steps:

1. show that expressibility of ^✓ in FO can be reduced to a boundedness question;

2. show that this boundedness question is decidable.

Step 1. Reduce to boundedness question The Barwise-Moschovakis theorem [START_REF] Barwise | Global inductive definability[END_REF] states that an FO formula (x, X) is bounded i↵ [lfp X,x . ] can be expressed in FO. It is easy to see that this result extends to simultaneous fixpoints, but for completeness (and because we could not find an explicit statement of this in the literature), we formalize the argument here.

If we have a system S of equations A 1 , x 1 := 1 , . . . , A n , x n := n for a simultaneous fixpoint, we say that (x 1 ) defines the projection of the fixpoint on A 1 if in any structure A, the set A 1 (A) := {a 1 : A, a 1 | = } agrees with {a 1 : 9a 2 . . . a n such that a 1 a 2 . . . a n is in the least fixpoint of the equations on A}. If the simultaneous fixpoint is bounded by some j with respect to A 1 we will say, S , A 1 is bounded. If S , A 1 is bounded (by j) then [lfp A 1 ,x 1 .S ] is clearly FO definable, since we can express the projection of the fixpoint on A 1 by the FO formula that describes the j-th approximant of the fixpoint. For the other direction: Lemma 36. If we have a system S of equations A 1 , x 1 := 1 , . . ., A n , x n := n and there is a first-order (x 1 ) that defines the projection of the fixpoint on A 1 , then there is j 2 N such that in any structure A, A 1 (A) is {a 1 : 9a 1 . . . a n such that a 1 a 2 . . . a n is in the j th iteration of the equations on A}. In this case, we say that S , A 1 is bounded.

Proof. This is proven via a slight variation of the proof of the Barwise-Moschovakis theorem (see the outline in [START_REF] Otto | The boundedness problem for monadic universal first-order logic[END_REF]). First it is shown that in a saturated model, every tuple that is in the projection of the fixpoint is in the projection of some finite iteration of the equations. This follows from the fact that the closure ordinal of a first-order operator is at most ! in a saturated model. Second, we note that if the projection of fixpoint does not collapse to the projection of some fixed number of iterations, we can get a tuple that does not enter the projection of the fixpoint in any finite stage, contradicting the result above. ⇤ Thus, it su ces to show that ^✓ can be written as a single least fixpoint of a system S of equations using FO formulas and some goal predicate goal, since this will imply that ^✓ is FO definable i↵ S , goal is bounded.

Each E(x, y) in the body of can be translated into an LFP formula using a simultaneous fixpoint and no parameters. This is similar to Example 4, but we include both variables explicitly in the fixpoint as fixpoint variables, rather than as parameters. We write S E for the system of equations coming from E, and write X E for its designated goal predicate.

We now rewrite ^✓ as a simultaneous least fixpoint of the form [lfp goal,; .S ]() (that is, the distinguished goal predicate is a nullary predicate called goal) where S is a system of the following equations:

• the equations from S E for each E(x, y) in the body of ;

• Q, ; := 0 , where Q is a fresh 0-ary variable and 0 is the result of replacing each E(x, y) in with X E (x, y); • goal, ; := Q ^✓.

(Note that it would not have been possible to combine the definitions of the E(x, y) and the CQ 0 in a single fixpoint like this if we were using x or y as parameters in S E and these variables were quantified in .)

Since [lfp goal,;

.S ]() is equivalent to ^✓, by (the extension of) Barwise-Moschovakis, definability in FO corresponds to this fixpoint being bounded.

Step 2. Show that this boundedness question is decidable Unfortunately, we cannot decide boundedness directly for S , goal since [lfp goal,; .S ]() is not in GNFP-UP.

However, we know that there is a GNFP-UP formula 0 equivalent to that we can relate this to. Lemma 37. S , goal is bounded i↵ there is some natural number n such that ( 0 ) n ^✓ is equivalent to 0 ^✓, where ( 0 ) n denotes the result of replacing every fixpoint in 0 with its n-th approximant.

Proof. Suppose that S , goal is unbounded. Then for all n 2 N, there is a structure A n satisfying the fixpoint, but requiring at least n iterations to reach the fixpoint. Consider the fixpoint game for [lfp goal,; .S ]() on A n (the fixpoint game is similar to the game described in Section 6, but is adapted to simultaneous fixpoints). Since A n requires at least n iterations to reach the fixpoint, Adam must have a strategy to enforce at least n rounds in the fixpoint game. This means that regardless of the S E valuations Eve chooses to witness 0 , Adam has a strategy to challenge some (a 1 , a 2 ) 2 S E , to enforce a further n 1 rounds. But once Adam challenges her on some (a 1 , a 2 ) 2 S E , then we are in the fixpoint game for S E . Hence, this implies that the fixpoint related to the conjunct E(x, y) in requires at least n 1 unfoldings: A n 6 | = (E 0 ) n 2 (a 1 , a 2 ) where (E 0 ) n 2 is the n 2-approximant of the GNFP-UP formula E 0 equivalent to E. That means that ( 0 ) n 2 ^✓ is not equivalent to 0 ^✓ on A n . Since this is true for all n, this means that the family of structures A n witnesses the fact that there is no N such that for all structures, ( 0 ) N ^✓ is equivalent to 0 ^✓.

Similar reasoning shows that if S , goal is bounded, then the uniform bound N for this fixpoint implies that ( 0 ) N ^✓ is equivalent to 0 ^✓. ⇤ Hence, we have a new (but equivalent) boundedness question that we can try to answer: is there some natural number n such that ( 0 ) n ^✓ is equivalent to 0 ^✓. Because this involves GNFP-UP formulas, we can tackle these with the automata machinery developed in this paper, and some previous cost automata results. As before, we can restrict to tree-like models, and construct cost automata related to this question.

The cost automaton that we construct has a nice property: it is counter-weak (or quasi-weak), which means that in any cycle in the automaton that visits states with both odd and even priorities, there is a counter which is incremented but not reset. This is a generalization of weak automata which satisfy the stronger condition that there is no cycle that visits states with both odd and even priorities. Lemma 38. There is a 2-way alternating counter-weak cost parity tree automaton B such that ~B is bounded i↵ there is some n such that ( 0 ) n ^✓ is equivalent to 0 ^✓ over all structures.

Proof sketch. There are counter-weak cost automata for each conjunct in 0 : we take the automaton from Lemma 18, and just add a counter that is incremented each time the fixpoint is unfolded. They are weak (and hence counter-weak) because these automata start in states with odd priorities and once they switch to an even priority, they remain there forever (since the only states with even priorities are sink states).

Counter-weak cost automata are closed under maximum (respectively, minimum) simply by giving Adam (respectively, Eve) the choice of which conjunct automaton to simulate. These are the closure operations needed to capture conjunction and disjunction in the logic.

The operation corresponding to projection is more challenging. Without counters, we would convert to a nondeterministic automaton, and then allow Eve to guess the free variable markers. In general, it is not known how to convert alternating cost automata to an equivalent nondeterministic version and do this projection. However, counter-weak automata are closed under a special form of weak projection where the set being projected is finite [START_REF] Blumensath | Two-way cost automata and cost logics over infinite trees[END_REF] (it is called weak inf-projection there). This is all we need, since we only need to project the finite number of free variable markers. So there is a counter-weak automaton B 0 that (roughly speaking) computes the minimum number of unfoldings required for the fixpoints in 0 .

On input T , the overall automaton B works by giving Eve a choice to (a) show T is inconsistent, or (b) show that D(T ) does not satisfy 0 ^✓, or (c) run B 0 . This automaton is bounded over all trees i↵ there is some n such that ( 0 ) n ^✓ is equivalent to 0 ^✓ over all structures. Because the automata checking (a) and (b) are also weak (and hence counter-weak), the overall automaton is counterweak as desired. ⇤

Unlike general cost automata over infinite trees, these counterweak automata are another special class of cost automata for which boundedness is known to be decidable. Theorem 39 ([10, Corollary 3]). Boundedness for 2-way counterweak cost automata is decidable.

Overall, putting these lemmas together gives us a method to construct a 2-way counter-weak cost automaton that is bounded i↵ S , goal is bounded, which we can decide using the previous theorem. Extension to negation-free CQPDL In Step 1, we proceed by induction on the number of nested programs/tests in the CQPDL. The base case is exactly the C2RPQ case from before. For the inductive case, the idea is to flatten the CQPDL in a similar way as in Corollary 23. For each E(x, y) in the CQPDL, we translate to a C2RPQ translate(E)(x, y) as in Corollary 23. This C2RPQ has new predicates U t? for t? occurring in E. We add equations in the simultaneous fixpoint based on the automaton for translate(E)(x, y), and add equations describing the meaning of each new predicate U t? based on the inductively defined formulas. The rest of step 1 is similar.

In Step 2, we again construct a 2-way counter-weak automaton for which boundedness is decidable. The construction of the automaton relies on the closure properties of 2-way counterweak automata described in [START_REF] Blumensath | Two-way cost automata and cost logics over infinite trees[END_REF], including closure under (weak) projection, min/max, localization, etc.

It is important for both of these steps that we are in negationfree CQPDL: the flattening to a single least fixpoint in step 1 only works because all of the U t? occur positively, and the reduction to cost automata boundedness in step 2 only works because we are trying to minimize the unfoldings of least fixpoints.

Example 1 .

 1 Suppose R is a binary relation in . Consider the following GNFP-UP[ ]-formula: (x, z) := [lfp z

  and r = rank CQ ( ). The number of priorities is linear in | |. For pdepth z ( ) = 0, the bounds match Lemma 17. Proof sketch. The proof is by induction on | |.

Proof.

  Let = {Q, R}. Consider the UNFP-UP[ ] sentence := ¬9x. ⇣ Qx ^¬[lfp x Y,y .Ryx _ 9y 0 .(Ryy 0 ^Yy 0 )](x) ⌘ which expresses that there is an R-loop from every Q-labelled element. Note that [lfp x Y,y .Ryx _ 9y 0 .(Ryy 0 ^Yy 0 )] defines the transitive closure of the binary relation R.

  Spoiler can select an element c such that c is in the active structure, Duplicator must choose d in the inactive structure such that f [c 7 ! d] is a partial rigid homomorphism, and then the game proceeds from position f [c 7 ! d]. In the special case that c 2 dom( f ), then d must be f (c). Spoiler wins if Duplicator gets stuck (i.e. Spoiler chooses some c but Duplicator is unable to select d such that f [c 7 ! d] is a partial rigid homomorphism). If the game continues forever, then Duplicator wins. We say A and B are GN k [ ] bisimilar if Duplicator has a winning strategy in the GN k [ ] bisimulation game starting from the empty position.

  is a partial rigid homomorphism. Hence by the inductive hypothesis, B, f 0 (ad) | = (xy), and B, f (a) | = . Finally, suppose is of the form ↵(x) ^¬ . We have A, a | = ↵ and and hence B, b | = ↵ since a 7 ! b is a partial rigid homomorphism. This ensures that a is guarded in A, so it is possible for Spoiler to switch structures (and possibly restrict further to the elements corresponding to free( )), and move to position b 7 ! a (or some restriction of this). Hence, the inductive hypothesis shows that B, b | = implies A, a | = . Since A, a | = ¬ , this means that it must be the case that B, b | = ¬ . Hence, B, b | = as desired.⇤

  (klr) where m = | |, l = |const( 0 )|, and r = rank CQ ( ). The number of priorities in each automaton is linear in | |. The overall size is exponential in | 0 | • N.

  pdepth z ( ) f ( f (mn) • 2 f (klr) ) where m = | |, n = | |, l = |const( )|, and r = rank CQ ( ). The number of priorities is linear in | |. For pdepth z ( ) = 0, the bounds match Lemma 17.

  Proof. We proceed by induction on | |, with params( ) ✓ z. Let m = | |, n = | |, l = |const( )|, and r = rank CQ ( ).

Lemma 30 .

 30 Let (yz, Z) 2 (GNFP-UP) k [ ] in normal form with params( ) ✓ z. If 0 (y) := transform z ( ) 2 GNFP k [ z, ] then for all -structures M, for all -guarded relations J for Z, for allguarded b for y and all c for z, M, bc, J | = (yz, Z) i↵ M 0 , b, J | = 0 (y, Z) where M 0 is the z, -structure obtained from M by taking z M 0 := c, and F M 0 ⌘(x) := {a : a is -guarded in M and M | = ⌘[a/x, c/z]} .

  Since z M 0 := c, M | = ↵[b/y, c/z] i↵ M 0 | = ↵[b/y]. By the inductive hypothesis, M | = [b/y, c/z] i↵ M 0 | = [b/y]. This implies the desired result. • Assume is [lfp z 0 X,x . gdd(x) ^ (xz 0 , XZ)](t). Consider the case when 0 = F t. If M 0 | = (F t)[b/y], then M | = [b/y, c/z] by definition of F M 0 . Likewise, if M | = [b/y, c/z],t[b/y, c/z] must be -guarded since any tuple in the fixpoint is guarded. Hence, t[b/y, c/z] 2 F M 0 and M 0 | = (F t)[b/y].

2016/4/29

2016/4/29

2016/4/29

2016/4/29

2016/4/29

2016/4/29

2016/4/29

[START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF] used a di↵erent encoding of the tree-like models, but the adaptation to the encoding here requires only minor technical changes.

2016/4/29

ILT stands for "infinite limitedness theorem", a statement about cost automata on infinite trees. More details can be found in[START_REF] Benedikt | The complexity of boundedness for guarded logics[END_REF].

2016/4/29

2016/4/29

2016/4/29

2016/4/29

2016/4/29

2016/4/29

2016/4/29

2016/4/29

If n = 1, then by the n-unfolding we mean the fixpoint itself, so the statement is vacuous.

2016/4/29

2016/4/29

2016/4/29

Acknowledgments

Benedikt's work was sponsored by the Engineering and Physical Sciences Research Council of the United Kingdom (EPSRC), grants EP/M005852/1 and EP/L012138/1. Vanden Boom was partially supported by EPSRC grant EP/L012138/1. Bourhis was supported by CPER Nord-Pas de Calais/FEDER DATA Advanced Data Science and Technologies 2015-2020 and the ANR Aggreg Project ANR-14-CE25-0017, INRIA Northern European Associate Team Integrated Linked Data.