Bartosz Bednarczyk

Stéphane Demri

Raul Fervari

Modal Logics with Composition on Finite Forests: Expressivity and Complexity

Keywords: CCS Concepts:, Theory of computation → Modal and temporal logics modal logic on trees, separation logic, static ambient logic, graded modal logic, expressive power, complexity

We study the expressivity and complexity of two modal logics interpreted on finite forests and equipped with standard modalities to reason on submodels. The logic ML( ) extends the modal logic K with the composition operator from ambient logic, whereas ML( * ) features the separating conjunction * from separation logic. Both operators are second-order in nature. We show that ML( ) is as expressive as the graded modal logic GML (on trees) whereas ML( * ) is strictly less expressive than GML. Moreover, we establish that the satisfiability problem is Tower-complete for ML( * ), whereas it is (only) AExp Pol -complete for ML( ), a result which is surprising given their relative expressivity. As by-products, we solve open problems related to sister logics such as static ambient logic and modal separation logic.

Introduction

The ability to quantify over substructures to express properties of a model is often instrumental to perform modular and local reasoning. Two well-known examples are provided by separation logics [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF][START_REF] O'hearn | Local Reasoning about Programs that Alter Data Structures[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF], dedicated to reasoning on pointer programs, and ambient (or more generally, spatial) logics [START_REF] Boneva | Expressiveness of a Spatial Logic for Trees[END_REF][START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF][START_REF] Calcagno | Context logic and tree update[END_REF][START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF], dedicated to reasoning on disjoint data structures. In the realm of modal logics dedicated to knowledge representation, submodel reasoning remains a key ingredient to express the dynamics of knowledge and belief, as done in the logics of public announcement [START_REF] Ph | Knowable' as 'known after an announcement[END_REF][START_REF] Lutz | Complexity and succinctness of public announcement logic[END_REF][START_REF] Plaza | Logics of public communication[END_REF], sabotage modal logics [START_REF] Aucher | Modal logics of sabotage revisited[END_REF], refinement modal logics [START_REF] Bozzelli | The complexity of one-agent refinement modal logic[END_REF] and relation-changing logics [START_REF] Areces | Moving Arrows and Four Model Checking Results[END_REF][START_REF] Areces | Relation-changing modal operators[END_REF][START_REF] Aucher | Global and Local Graph Modifiers[END_REF]. Though the models may be of different nature (e.g. memory states for separation logics, epistemic models for logics of public announcement or finite edge-labelled trees for ambient logics), all those logics feature composition operators that enable to compose or decompose substructures in a very natural way.

From a technical point of view, reasoning about submodels requires a global analysis, unlike the local approach for classical modal and temporal logics (typically based on automata techniques [START_REF] Vardi | Automata-theoretic techniques for modal logics of programs[END_REF][START_REF] Vardi | Reasoning about Infinite Computations[END_REF]). This makes the comparison between those formalisms quite challenging and often limited to a superficial analysis on the different classes of models and composition operators. For instance, the composition operator in ambient logics decomposes a tree into two disjoint pieces such that once a node has been assigned to one submodel, all its descendants belong to the same submodel. Instead, the separating conjunction * from separation logic decomposes the memory states into two disjoint memory states. Obviously, these and other well-known operators are closely related but no uniform framework investigates exhaustively their relationships in terms of expressive power.

Most of these logics can be easily encoded in monadic second-order logic MSO (or in second-order modal logics [START_REF] Fine | Propositional quantifiers in modal logic[END_REF][START_REF] Laroussinie | Quantified CTL: Expressiveness and Complexity[END_REF]). Complexity-wise, if models are tree-like structures, we can then infer decidability thanks to the celebrated Rabin's theorem [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. However, most likely, this does not produce the best decision procedures when it comes to solving simple reasoning tasks (e.g. the satisfiability problem of MSO is Tower-complete [START_REF] Schmitz | Complexity Hierarchies beyond Elementary[END_REF]). Thus, relying on MSO as a common umbrella to capture and understand the differences between those logical formalisms is often not satisfactory.

Our motivations. Our intention in this work is to provide an in-depth comparison between the composition operator from static ambient logic [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF] and the separating conjunction * from separation logics [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF] by identifying a common ground in terms of logical languages and models. As a consequence, we are able to study the effects of having these operators as far as expressivity and complexity are concerned. We aim at defining two logics whose only differences rest on their use of and * syntactically and semantically (by considering the adequate composition operation). To do so, we pick as our common class of models, the Kripke-style finite trees (actually finite forests, so that the class is closed under taking submodels), which provides an ubiquitous class of structures, extremely well-studied in computer science. For the underlying logical language (i.e. apart from or * ), we advocate the use of the standard modal logic K (i.e. to have Boolean connectives and the standard modality 3) so that the main operations on the models amount to quantify over submodels or to move along the edges. This framework is sufficiently fundamental to give us the possibility to take advantage of model theoretical tools from modal logics [START_REF] Barnaba | Graded Modalities[END_REF][START_REF] Blackburn | Modal Logic[END_REF][START_REF] De Rijke | A Note on Graded Modal Logic[END_REF]. The benefits of settling a common ground for comparison may lead to further comparisons with other logics and new results.

Our contributions. We introduce ML( ) and ML( * ), two logics interpreted on Kripke-style forest models, equipped with the standard modality 3, and respectively with the composition operator from static ambient logic [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF] and with the separating conjunction * from separation logic [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]. Both logical formalisms can state non-trivial properties about submodels, but the binary modalities and * operate differently: whereas * is able to decompose the models at any depth, is much less permissive as the decomposition is completely determined by what happens at the level of the children of the current node. We study their expressive power and complexity, obtaining surprising results. We show that ML( ) is as expressive as the graded modal logic GML [START_REF] Barnaba | Graded Modalities[END_REF][START_REF] Tobies | PSPACE Reasoning for Graded Modal Logics[END_REF] whereas ML( * ) is strictly less expressive than GML. Interestingly, this latter development partially reuses the result for ML( ), hence showing how our framework allows us to transpose results between the two logics. To show that GML is strictly more expressive than ML( * ), we define Ehrenfeucht-Fraïssé games for ML( * ). In terms of complexity, the satisfiability problem for ML( ) is shown AExp Pol -complete 1 , interestingly the same complexity as for the refinement modal logic RML [START_REF] Bozzelli | The complexity of one-agent refinement modal logic[END_REF] handling a quantifier over refinements (generalising the submodel construction). The AExp Pol upper bound follows from an exponential-size model property, whereas the lower bound is by reducing the satisfiability problem for an AExp Pol -complete team logic [START_REF] Hannula | Complexity of Propositional Logics in Team Semantic[END_REF]. Much more surprisingly, although ML( * ) is strictly less expressive than ML( ), its complexity is much higher (not even elementary). Precisely, we show that the satisfiability problem for ML( * ) is Tower-complete. The Tower upper bound is a consequence of [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF], whereas hardness is shown by reduction from a Tower-complete tiling problem, adapting substantially the 1 Problems in AExp Pol are decidable by an alternating Turing machine working in exponential-time and using polynomially many alternations [START_REF] Bozzelli | On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions[END_REF].

Tower-hardness proof from [START_REF] Bednarczyk | Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?[END_REF] for second-order modal logic K on finite trees. To conclude, we get the best of our results on ML( ) and ML( * ) to solve several open problems. We relate ML( ) with an intensional fragment of static ambient logic SAL( ) from [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF] by providing polynomial-time reductions between their satisfiability problems. Consequently, we establish AExp Pol -completeness of SAL( ), refuting hints from [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF]Section 6]. Similarly, we show that the modal separation logic MSL(3 -1 , * ) from [START_REF] Demri | The power of modal separation logics[END_REF] is Tower-complete. Omitted proofs can be found in the technical report on ArXiv.

Preliminaries

In this section, we introduce the logics ML( ) and ML( * ) interpreted on tree-like structures equipped with operators to split the structure into disjoint pieces. Due to the presence of such operators, we are required to consider a class of models that is closed under submodels, which we call Kripkestyle finite forests (or finite forests for short).

Let AP be a countably infinite set of atomic propositions. A (Kripke-style) finite forest is a triple M = (W ,R,V ) where W is a non-empty finite set of worlds, V : AP → P (W ) is a valuation and R ⊆ W ×W is a binary relation whose inverse R -1 is functional and acyclic. Then, in particular the graph described by (W ,R) is a finite collection of disjoint finite trees (where R encodes the child relation).

We define R(w

) def = {w ′ ∈ W | (w,w ′ ) ∈ R}. Worlds in R(w ) are understood as children of w. We inductively define R n : R 0 def = {(w,w ) | w ∈ W }; R n+1 def = {(w,w ′′ ) | ∃w ′ (w,w ′ ) ∈ R n and (w ′ ,w ′′ ) ∈ R }. R + denotes the transitive closure of R.
We define operators that chop a finite forest. It should be noted that these operators, as well as the resulting logics, can be cast under the umbrella of the logic of bunched implications BI [START_REF] Galmiche | The Semantics of BI and Resource Tableaux[END_REF][START_REF] Pym | The semantics and proof theory of the logic of bunched implications[END_REF], with the exception that we do not explicitly require them to have an identity element (as enforced on the multiplicative operators of BI, see [START_REF] Galmiche | The Semantics of BI and Resource Tableaux[END_REF]). Let M = (W ,R,V ) and M i = (W i ,R i ,V i ) (for i ∈ {1, 2}) be three finite forests.

The separation logic composition. We introduce the binary operator + that performs the disjoint union at the level of parent-child relation. Formally,

M = M 1 + M 2 def ⇔ R 1 ⊎ R 2 = R, W 1 = W 2 = W , V 1 = V 2 = V.
This is the composition used in separation logic [START_REF] Demri | The power of modal separation logics[END_REF][START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]. The figure below depicts possible instances for M, M 1 and M 2 .

= +

The ambient logic composition. We introduce the operator + w , where w ∈ W , that constraints further +:

M = M 1 + w M 2 def ⇔ M = M 1 + M 2 and R + i (w ′ ) = R + (w ′ ) holds for all i ∈ {1, 2} and w ′ ∈ R i (w ).
M is a disjoint union between M 1 and M 2 except that, as soon as w ′ ∈ R i (w ), the whole subtree of w ′ in R belongs to M i , like the composition in ambient logic [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF]. Below, we illustrate a model decomposed with + w .

w = w + w w We say that M 1 is a submodel of M, written M 1 ⊑ M if there is M 2 such that M = M 1 + M 2 .
Modal logics on trees. The logic ML( ) enriches the modal logic K (a.k.a. ML) with a binary connective , called composition operator, that admits submodel reasoning via the operator + w . Similarly, ML( * ) enriches ML with the connective * , called separating conjunction (or star) that admits submodel reasoning via the operator +. Both connectives and * are understood as binary modalities. As we show throughout the paper, ML( ) and ML( * ) are strongly related to the graded modal logic GML [START_REF] De Rijke | A Note on Graded Modal Logic[END_REF]. For conciseness, let us define all these logics by considering formulae that contain all of their ingredients. These formulae are built from

φ := ⊤ | p | φ ∧ φ | ¬φ | 3φ | 3 ≥k φ | φ * φ | φ φ,
where p ∈ AP and k ∈ N (encoded in binary). A pointed forest (M,w ) is a finite forest M = (W ,R,V ) together with a world w ∈ W . The satisfaction relation |= is defined as follows (standard clauses for ∧, ¬ and ⊤ are omitted):

M,w |= p ⇔ w ∈ V (p); M,w |= 3φ ⇔ there is w ′ ∈ R(w ) s.t. M,w ′ |= φ; M,w |= 3 ≥k φ ⇔ |{w ′ ∈ R(w ) | M,w ′ |= φ}| ≥ k; M,w |= φ 1 * φ 2 ⇔ there are M 1 , M 2 s.t. M = M 1 + M 2 , M 1 ,w |= φ 1 and M 2 ,w |= φ 2 ; M,w |= φ 1 φ 2 ⇔ there are M 1 , M 2 s.t. M = M 1 + w M 2 , M 1 ,w |= φ 1 and M 2 ,w |= φ 2 .
The formulae φ ⇒ ψ , φ ∨ ψ and ⊥ are defined as usual. We use the following standard abbreviations: 2φ def = ¬3¬φ, 3 ≤k φ def = ¬3 ≥k +1 φ and 3 =k φ def = 3 ≥k φ ∧ 3 ≤k φ. We write size(φ) to denote the size of φ with a tree representation of formulae and with a reasonably succinct encoding of atomic formulae. Besides, we write md(φ) to denote the modal degree of φ understood as the maximal number of nested unary modalities (i.e. 3 or 3 ≥k ) in φ. Similarly, the graded rank gr(φ) of φ is defined as max({k | 3 ≥k ψ ∈ subf(φ)} ∪ {0}), where subf(φ) is the set of all the subformulae of φ.

Given the formulae φ and ψ , φ ≡ ψ denotes that φ and ψ are logically equivalent; i.e., for every pointed forest (M,w ), M,w |= φ iff M,w |= ψ . For instance (k ≥ 1 and p ∈ AP):

1. 3φ ≡ 3 ≥1 φ; 2. (22⊥ 22⊥) (22⊥ * 22⊥); 3. 3 ≥k p ≡ 3p * • • • * 3p k times ; 4. 3 ≥k φ ≡ 3φ • • • 3φ k times .
The modal logic ML is the logic restricted to formulae with the unique modality 3 [START_REF] Blackburn | Modal Logic[END_REF]. Similarly, the graded modal logic GML is restricted to the graded modalities 3 ≥k [START_REF] De Rijke | A Note on Graded Modal Logic[END_REF]. We introduce the modal logics ML( ) and ML( * ), which are restricted to the suites of modalities (3, ) and (3, * ), respectively. The two equivalences (3) and ( 4) already shed some light on ML( ) and ML( * ): the two logics are similar when it comes to their formulae of modal degree one.

Lemma 2.1. Let φ be a formula in ML( ) with md(φ) ≤ 1.

Then, φ ≡ φ[ ← * ] where φ[ ← * ] is the formula in ML( * ) obtained from φ by replacing every occurrence of by * .

However, as shown by the non-equivalence (2), it is unclear how the two logics compare when it comes to formulae of modal degree greater than one. Indeed, since M = M 1 + w M 2 implies M = M 1 + M 2 , but not vice-versa, the separating conjunction * is more permissive than the operator . However, further connections between the two operators can be easily established. Let us introduce the auxiliary operator defined as

φ def = φ * 2⊥. Formally, (W ,R,V ),w |= φ ⇔ there is R ′ ⊆ R s.t. R ′ (w ) = R(w )
and (W ,R ′ ,V ),w |= φ. Similar operators are studied in [START_REF] Areces | Relation-changing modal operators[END_REF][START_REF] Aucher | Modal logics of sabotage revisited[END_REF][START_REF] Bozzelli | The complexity of one-agent refinement modal logic[END_REF]. We show that and are sufficient to capture * (essential property for Section 5). Lemma 2.2. Let φ,ψ ∈ GML. We have φ * ψ ≡ (φ ψ ).

Unlike , when * splits a finite forest M into M 1 and M 2 , it may disconnect in both submodels worlds that are otherwise reachable, from the current world, in M. Applying before allows us to imitate this behaviour. Indeed, even though preserves reachability in either M 1 or M 2 , deletes part of M, making some world inaccessible. This way of expressing the separating conjunction allows us to reuse some methods developed for ML( ) in order to study ML( * ).

The logic QK t . Both ML( ) and ML( * ) can be seen as fragments of the logic QK t , which in turn is known to be a fragment of monadic second-order logic on trees [START_REF] Bednarczyk | Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?[END_REF]. The logic QK t extends ML with second-order quantification and is interpreted on finite trees. Its formulae are defined according to the following grammar:

φ := p | 3φ | φ ∧ φ | ¬φ | ∃p φ. Given M = (W ,R,V ) and w ∈ W , the satisfaction relation |= of ML is extended as follows: M,w |= ∃p φ iff ∃W ′ ⊆ W s.t. (W ,R,V [p ← W ′ ]),w |= φ.
One can show logspace reductions from ML( ) and ML( * ) to QK t , by simply reinterpreting the operators * and as restrictive forms of second-order quantification, and by relativising 3 to appropriate propositional symbols in order to capture the notion of submodel (details are omitted).

Satisfiability problem. The satisfiability problem for a logic L, written Sat(L), takes as input a formula φ in L and checks whether there is a pointed forest (M,w ) such that M,w |= φ.

Note that any L among ML, GML, ML( ) or ML( * ) has the tree model property, i.e. any satisfiable formula is also satisfied in some tree structure. The problems Sat(ML) and Sat(GML) are known to be PSpace-complete, see e.g. [START_REF] Blackburn | Modal Logic[END_REF][START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF][START_REF] Schröder | PSPACE bounds for rank-1 modal logics[END_REF][START_REF] Tobies | PSPACE Reasoning for Graded Modal Logics[END_REF], and therefore Sat(ML( )) and Sat(ML( * )) are PSpacehard. As an upper bound, by Rabin's theorem [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF], the satisfiability problem for QK t is decidable in Tower, which transfers directly to Sat(ML( )) and Sat(ML( * )).

Expressive power. Given two logics L 1 and L 2 , we say that L 2 is at least as expressive as L 1 (written L 1 ⪯ L 2 ) whenever for every formula φ of L 1 , there is a formula ψ of L 2 such that φ ≡ ψ . L 1 ≈ L 2 denotes that L 1 and L 2 are equally expressive, i.e. L 1 ⪯ L 2 and L 2 ⪯ L 1 . Lastly, L 1 ≺ L 2 denotes that L 2 is strictly more expressive than L 1 , i.e. L 1 ⪯ L 2 and L 1 L 2 . The equivalence (1) recalls us that ML ≺ GML [START_REF] De Rijke | A Note on Graded Modal Logic[END_REF]. From the equivalence (4), we get GML ⪯ ML( ).

ML( ): Expressiveness and Complexity

In this section, we study the expressive power of ML( ) and the complexity of Sat(ML( )). We show constructively that ML( ) ⪯ GML, hence proving ML( ) ≈ GML. Next, we show that Sat(ML( )) is AExp Pol -complete. The upper bound is achieved by proving an exponential-size model property. The lower bound is by reduction from the satisfiability problem for propositional team logic [27, Thm. 4.9].

3.1 ML( ) is not more expressive than GML Establishing ML( ) ⪯ GML amounts to show that given φ 1 , φ 2 in GML, one can construct ψ in GML such that φ 1 φ 2 ≡ ψ . For instance, a simple case analysis yields the equivalence (p ∨ 3 ≥3 r ) (q ∨ 3 ≤5 q) ≡ (p ∨ 3 ≥3 r ). With this property, the general algorithm consists in iteratively replacing innermost subformulae of the form φ 1 φ 2 by a counterpart in GML, allowing us to eliminate all the occurrences of and obtain an equivalent formula in GML. The base case involves subformulae φ 1 and φ 2 in ML (a fragment of GML).

Let us provide a few definitions. Let φ be a formula in GML. We write max PC (φ) to denote the set of subformulae ψ of φ that are maximal and modality-free, i.e.

1. ψ is modality-free: it does not contain modalities 3 ≥k and one of its occurrences is not in the scope of 3 ≥k ; 2. ψ is maximal: one of its occurrences does not belong to a larger modality-free subformula of φ.

For instance, max PC ((p∨3 ≥3 r )∧(q∨p)) = {p,q∨p}. Similarly, max GM (φ) denotes the set of subformulae ψ of φ such that ψ is of the form 3 ≥k ψ ′ and one of its occurrences in φ is not in the scope of graded modalities 3 ≥k . For instance,

max GM ((p ∨ 3 ≥3 r ) ∧ (q ∨ 3 ≥5 3 ≥2 q)) = {3 ≥3 r , 3 ≥5 3 ≥2 q}.
Every formula φ in GML is a Boolean combination of formulae from max PC (φ) ∪ max GM (φ). Lastly, φ is in good shape if the properties (1) and (2) below hold:

1. max PC (φ) ⊆ {⊥, ⊤}. Consequently, every propositional variable in φ occurs in the scope of a graded modality; 2. For all 3 ≥k ψ , 3 ≥k ′ ψ ′ in max GM (φ) with ψ ψ ′ , the conjunction ψ ∧ ψ ′ is unsatisfiable.

Let φ 1 and φ 2 be GML formulae. First, we show that when φ 1 ∧ φ 2 is in good shape, there is a GML formula ψ such that φ 1 φ 2 ≡ ψ . To do so, we take a slight detour through Presburger arithmetic (PA), see e.g. [START_REF] Ch | A survival guide to Presburger arithmetic[END_REF][START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF]. Given two formulae φ 1 ,φ 2 in GML, we will characterise the formula φ 1 φ 2 by using arithmetical constraints for the number of successors. Then, we will take advantage of basic properties of PA in order to eliminate quantifiers, and obtain a GML formula. Below, the variables x, y, z, . . ., possibly decorated and occurring in formulae, are from PA and therefore they are interpreted by natural numbers.

Let φ be in GML s.t. max PC (φ) ⊆ {⊤, ⊥} and {ψ 1 , . . . ,ψ n } contains the set {ψ | 3 ≥k ψ ∈ max GM (φ)}. We define formulae in PA that state constraints about the number of children satisfying a formula ψ j . The variable x j is intended to be interpreted as the number of children satisfying ψ j . We write φ PA (x 1 , . . . , x n ) to denote the arithmetical formula obtained from φ by replacing with x j ≥ k every occurrence of 3 ≥k ψ j that it is not in the scope of a graded modality. For instance, assuming that φ = 3 ≥5 (p ∧ q) ∨ ¬3 ≥4 ¬p, the expression

φ PA (x 1 , x 2 ) denotes the formula x 1 ≥ 5 ∨ ¬(x 2 ≥ 4). Let φ 1 ,φ 2 be GML formulae such that φ 1 ∧ φ 2 is in good shape and {ψ 1 , . . . ,ψ n } = {ψ | 3 ≥k ψ ∈ max GM (φ 1 ∧ φ 2 )}. We consider the formula [φ 1 ,φ 2 ] PA in PA defined below: [φ 1 ,φ 2 ] PA def = ∃ y 1 1 , y 2 1 , . . . , y 1 n , y 2 n ( n j=1 x j = y 1 j + y 2 j )∧ φ PA 1 (y 1 1 , . . . , y 1 n ) ∧ φ PA 2 (y 2 1 , . . . , y 2 n ). The formula [φ 1 ,φ 2 ]
PA states that there is a way to divide the children in two distinct sets and each set allows to satisfy φ PA 1 or φ PA 2 , respectively. As PA admits quantifier elimination [START_REF] Cooper | Theorem proving in arithmetic without multiplication[END_REF][START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF][START_REF] Reddy | Presburger arithmetic with bounded quantifier alternation[END_REF], there is a quantifier-free formula χ equivalent to [φ 1 ,φ 2 ] PA and its free variables are among x 1 , . . . , x n . A priori, the atomic formulae of χ may not be of the simple form x j ≥ k (e.g. 'modulo constraints' or constraints of the form a i x j ≥ k may be involved). However, if the atomic formulae of χ are restricted to expressions of the form x j ≥ k, then we write χ GML to denote the GML formula obtained from χ by replacing every occurrence of x j ≥ k by 3 ≥k ψ j .

Lemma 3.1. Let φ 1 , φ 2 be in GML such that φ 1 ∧ φ 2 is in good shape. [φ 1 ,φ 2 ]
PA is equivalent to a quantifier-free PA formula χ whose atomic formulae are only of the form x j ≥ k. Moreover, φ 1 φ 2 ≡ χ GML and gr(χ GML ) ≤ gr(φ 1 ) + gr(φ 2 ).

The bound on gr(χ GML ) stated in this key lemma is essential to obtain an exponential bound on the smallest model satisfying a formula in ML( ) (see Section 3.2). Thanks to Lemma 3.1, we can show that GML is closed under the operator by reducing the occurrences of this operator to formulae in good shape. In particular, we show that given two arbitrary formulae φ 1 and φ 2 in GML, φ 1 φ 2 is equivalent to a disjunction of formulae of the form (ψ 1 ψ 2 ) ∧ χ , where χ is a Boolean combination of atomic propositions and ψ 1 ∧ψ 2 is in good shape (hence ψ 1 ψ 2 is equivalent to a formula in GML by Lemma 3.1). This is shown syntactically: atomic propositions are dealt with by propositional reasoning, whereas to produce ψ 1 and ψ 2 we use axioms from GML [START_REF] Barnaba | Graded Modalities[END_REF] and rely on the following equivalences:

(guess) 3 ≥k φ ≡ 3 ≥k (φ ∧ ψ ) ∨ (φ ∧ ¬ψ ) ; (3 ≥k dist) if φ ∧ψ unsat., 3 ≥k (φ∨ψ ) ≡ k =k1+k2 (3 ≥k1 φ ∧ 3 ≥k2 ψ ); ( dist) (φ ∨ ψ ) χ ≡ (φ χ ) ∨ (ψ χ ).
Notice that the conjunction of φ ∧ψ and φ ∧ ¬ψ from (guess) is trivially unsatisfiable, allowing us to use (3 ≥k dist). As GML is shown to be closed under the operator , we conclude. Theorem 3.2. ML( ) ⪯ GML. Therefore, ML( ) ≈ GML.

To prove ML( ) ⪯ GML, we iteratively put subformulae in good shape and apply Lemma 3.1. This is done several times, potentially causing an exponential blow-up each time a formula is transformed. To provide an optimal complexity upper bound, we need to tame this combinatorial explosion.

AExp Pol -completeness

In order to show that Sat(ML( )) is in AExp Pol , the main ingredient is to show that given φ in ML( ), we build φ ′ in GML such that φ ′ ≡ φ and the models for φ ′ (if any) do not require a number of children per node more than exponential in size(φ). The proof of Theorem 3.2 needs to be refined to improve the way φ ′ is computed. In particular, this requires a strategy for the application of the equivalences used to put a formula in good shape.

We need to introduce a few more simple notions. Let φ be a GML formula with max GM (φ) = {3 ≥k 1 ψ 1 , . . . , 3 ≥k n ψ n }. We define bd(0,φ

) def = k 1 + • • • + k n . For all m ≥ 0, we define bd(m + 1,φ) def = max{bd(m,ψ ) | 3 ≥k ψ ∈ max GM (φ)}.
Hence, bd(m,φ) can be understood as the maximal bd(0,ψ ) for some subformula ψ occurring at the modal depth m within φ. We write max bd (φ) for the value max{bd(m,φ) | m ∈ [0, md(φ)]}. If φ is satisfiable, we can use max bd (φ) to obtain a bound on the smallest model satisfying it, as stated in Lemma 3.3 below. Lemma 3.3. Every satisfiable φ in GML is satisfied by a pointed forest with at most max bd (φ) md(φ )+1 worlds.

To show that ML( ) has the exponential-size model property, we establish that given φ in ML( ), there is φ ′ in GML such that φ ′ ≡ φ, md(φ ′ ) ≤ md(φ) and max bd (φ ′ ) is exponential in size(φ). First, we consider the fragment F of ML( ):

φ ::= 3 ≥k ψ | p | φ φ | φ ∧ φ | ¬φ,
where p ∈ AP and 3 ≥k ψ is a formula in GML (abusively assumed in ML( ) but we know GML ⪯ ML( )). Given φ in ML( ) or in F, we write cd(φ) to denote its composition degree, i.e. the maximal number of imbrications of in φ. We extend the notion of bd to formulae in F, so that bd(m,φ) = bd(m,φ[ ← ∧]), where φ[ ← ∧] is the formula obtained from φ by replacing every occurrence of by ∧. Similarly, max GM (φ

) def = max GM (φ[ ← ∧]).
Let φ be in F such that max GM (φ) = {3 ≥k 1 χ 1 , . . . , 3 ≥k n χ n }. The key step to show the exponential-size model property essentially manipulates the formulae in max GM (φ) in order to produce equivalent formulae ψ 1 , . . . ,ψ n , so that for all distinct i and j, ψ i ∧ψ j is in good shape. Moreover, by replacing in φ every 3 ≥k i χ i with the equivalent formula ψ i , we only witness an exponential blow-up on bd(0,φ), whereas for every m > 1, bd(m,φ) remains polynomially bounded by the bd of the original formula. With the bound on the graded rank found in Lemma 3.1, we derive Lemma 3.4. Lemma 3.4. Let φ be a formula of the fragment F such that max GM (φ) = {3 ≥k 1 χ 1 , . . . ,3 ≥k n χ n } and k = max{k 1 , . . . ,k n }. There is a GML formula ψ such that φ ≡ ψ and,

1. md(ψ ) ≤ md(φ); 2. bd(0,ψ ) ≤ k × 2 n+cd(φ ) ; 3. bd(1,ψ ) ≤ n × bd(1,φ); 4. ∀m ≥ 2, bd(m,ψ ) = bd(m,φ).
In the proof of Lemma 3.4, a first step essentially consists in applying multiple times (guess) in order to derive, for every i ∈ [1,n], an equivalence

3 ≥k i χ i ≡ ψ ′ i where ψ ′ i def = 3 ≥k i f:[1,n]→{⊤,⊥} χ i ∧ [χ 1 ] f(1) ∧ • • • ∧ [χ n ] f(n) .
Here, [χ j ] ⊤ def = χ j and [χ j ] ⊥ def = ¬χ j . Roughly speaking, in this step, we expand χ i by considering all the possible truth values for the formulae χ 1 , . . . , χ n (the disjuncts where χ i is negated can be simply discharged from the disjunction, as they are unsatisfiable). Substituting every Lemma 3.4) and for every m 1, bd(m,φ ′ ) = bd(m,φ). Afterwards, we repeatedly apply (3 ≥k dist) to ψ ′ i and obtain the formula ψ i satisfying the aforementioned property, i.e. for all distinct i and j, ψ i ∧ ψ j is in good shape. With ( dist), this allows us to apply Lemma 3.1 until all the operators are removed. Besides, replacing every ψ ′ i by ψ i in φ ′ leads to a formula having the same bd as the formula ψ in Lemma 3.4.

3 ≥k i χ i by ψ ′ i in φ leads to a formula φ ′ such that bd(1,φ ′ ) ≤ n × bd(1,φ) (as in
Applying adequately the transformation from Lemma 3.4 to a formula in ML( ), i.e. by considering maximal subformulae of the fragment F, allows us to get a logically equivalent GML formula having small models. Lemma 3.5. Every satisfiable φ in ML( ) is satisfied by a pointed forest of size at most exponential in size(φ).

The proof of Lemma 3.5 (relying on Lemma 3.4) consists in showing that for all φ in ML( ), there is φ ′ in GML such that φ ′ ≡ φ and max bd (φ ′ ) is exponential in size(φ), which is sufficient by Lemma 3.3 to get the exponential-size model property, whence the upper bound AExp Pol .

Theorem 3.6. Sat(ML( )) is in AExp Pol .
The (standard) proof consists in observing that to check the satisfiability status of φ in ML( ), first guess a pointed forest of exponential-size (thanks to Lemma 3.5) and check whether it satisfies φ. This can be done in exponential-time using an alternating Turing machine with a linear amount of alternations (between universal states and existential states) by viewing ML( ) as a fragment of MSO.

It remains to establish AExp Pol -hardness. We provide a logspace reduction from the satisfiability problem for the team logic PL [~] shown AExp Pol -complete in [START_REF] Hannula | Complexity of Propositional Logics in Team Semantic[END_REF]Thm. 4.9]. PL[~] formulae are defined by the following grammar:

φ := p | ¬p | φ ∧ φ | ~φ | φ ∨φ ,
where p ∈ AP and the connectives ¬ and ∨ are dotted to avoid confusion with those of ML( ). PL[~] is interpreted on sets of (Boolean) propositional valuations over a finite subset of AP. They are called teams and are denoted by T, T 1 , . . . . A model for φ is a team T over a set of propositional variables including those occurring in φ and such that T |= φ with:

T |= p ⇔ for all v ∈ T, we have v(p) = ⊤; T |= ¬p ⇔ for all v ∈ T, we have v(p) = ⊥; T |= φ 1 ∨φ 2 ⇔ ∃ T 1 , T 2 s.t. T = T 1 ∪ T 2 , T 1 |=φ 1 , T 2 |=φ 2 .
The connectives ~and ∧ are interpreted as the classical negation and conjunction, respectively. Notice that, in the clause for ∨, the teams T 1 and T 2 are not necessarily disjoint.

Let us discuss the reduction from Sat(PL[~]) to Sat(ML( )). A direct encoding of a team T into a pointed forest (M,w ) consists in having a correspondence between the propositional valuations in T and the propositional valuations of the children of w. This would work fine if there were no mismatch between the semantics for (disjointness of the children) and the one for ∨ (disjointness not required). To handle this, when checking the satisfaction of φ in PL [~] with n occurrences of ∨, we impose that if a propositional valuation occurs among the children of w, then it occurs in least n + 1 children. This property must be maintained after applying ∨ several times, always with respect to the number of occurrences of ∨ in the subformula of φ that is evaluated. Non-disjointness of the teams is encoded by carefully separating the children of w having identical valuations.

We now formalise the reduction. Assume that we wish to translate φ from PL[~], written with atomic propositions in P = {p 1 , . . . ,p m } and containing at most n occurrences of the operator ∨. We introduce a set Q = {q 1 , . . . ,q n+1 } of auxiliary propositions disjoint from P. The elements of Q are used to distinguish different copies of the same propositional valuation of a team. Thus, with respect to a pointed forest (M,w ), we require each child of w to satisfy exactly one element of Q. This can be done with the formula

uni(Q) def = 2( i i ′ ∈[1,n+1] ¬(q i ∧ q i ′ ) ∧ i ∈[1,n+1] q i ).
We require that if a child of w satisfies a propositional valuation over (elements in) P, then there are n + 1 children satisfying that valuation over P, each of them satisfying a distinct symbol in Q. So, every valuation over P occurring in some child of w, occurs at least in n + 1 children of w. However, as the translation of the operator ∨ modifies the set of copies of a propositional valuation, this property must be extended to arbitrary subsets of Q. Given ∅ X ⊆ [1,n + 1], we require that for all k k ′ ∈ X , if a children of w satisfies q k , then there is a child satisfying q k ′ with the same valuation over P. The formula cp(X ) below does the job:

k k ′ ∈X ¬ 2q k (3 =1 q k ∧ ¬(⊤ 3 =1 q k ∧ 3 =1 q k ′ ∧ j ∈[1,m] 3p j ⇒ 2p j )) .
Lastly, before defining the translation map τ , we describe how different copies of the same propositional valuation are split. We introduce two auxiliary choice functions c 1 and c 2 that take as arguments X ⊆ [1,n + 1], and

n 1 ,n 2 ∈ N with |X | ≥ n 1 + n 2 such that for each i ∈ {1, 2}, we have c i (X ,n 1 ,n 2 ) ⊆ X , |c i (X ,n 1 ,n 2 )| ≥ n i . Moreover c 1 (X ,n 1 ,n 2 )⊎ c 2 (X ,n 1 ,n 2 ) = X .
The maps c 1 and c 2 are instrumental to decide how to split X into two disjoint subsets respecting basic cardinality constraints. The translation map τ is designed as follows

(∅ X ⊆ [1,n + 1]): τ (p,X ) def = 2(( j ∈X q j ) ⇒ p); τ ( ¬p,X ) def = 2(( j ∈X q j ) ⇒ ¬p); τ (φ 1 ∧ φ 2 ,X ) def = τ (φ 1 ,X ) ∧ τ (φ 2 ,X ); τ (~φ,X ) def = ¬τ (φ,X ); τ (φ 1 ∨φ 2 ,X ) def = (τ (φ 1 ,X 1 ) ∧ cp(X 1 )) (τ (φ 2 ,X 2 ) ∧ cp(X 2 )),
where (i) |X | is greater or equal to the number of occurrences of ∨ in φ 1 ∨φ 2 plus one; (ii) given n 1 ,n 2 such that n 1 (resp. n 2 ) is the number of occurrences of ∨ in φ 1 (resp. φ 2 ) plus one, for each i ∈ {1, 2} we have c i (X ,n 1 ,n 2 ) = X i .

Lemma 3.7 below guarantees that starting with a linear number of children with the same propositional valuation is sufficient to encode ∨ within ML( ). Lemma 3.7. Let φ be in PL [~] with n occurrences of ∨ and built upon p 1 , . . . , p m . Then, φ is satisfiable iff so is uni(q 1 , . . . ,

q n+1 ) ∧ cp([1,n + 1]) ∧ τ (φ, [1,n + 1]).
The ML( ) formula involved in Lemma 3.7 has modal depth one. By Theorem 3.6, Sat(ML( )) is AExp Pol -complete even restricted to formulae of modal depth at most one.

Corollary 3.8. Sat(ML( )) is AExp Pol -complete.

As we show in the next section, the complexity of ML( * ) does not collapse to modal depth one: Sat(ML( * )) restricted to formulae of modal depth k is exponentially easier than Sat(ML( * )) restricted to formulae of modal depth k + 1.

ML( * ) is Tower-complete

We show that Sat(ML( * )) is Tower-complete, i.e. complete for the class of all problems of time complexity bounded by a tower of exponentials whose height is an elementary function [START_REF] Schmitz | Complexity Hierarchies beyond Elementary[END_REF]. Given k,n ≥ 0, we inductively define the tetration function t as t(0,n) def = n and t(k

+ 1,n) = 2 t(k,n) .
Intuitively, t(k,n) defines a tower of exponentials of height k. By k-NExpTime, we denote the class of all problems decidable with a nondeterministic Turing machine (NTM) of working time O (t(k,p(n))) for some polynomial p(.), on each input of length n. To show Tower-hardness, we design a uniform elementary reduction allowing us to get k-NExpTimehardness for all k greater than a certain (fixed) integer. In our case, we achieve an exponential-space reduction from the k-NExpTime variant of the tiling problem, for all k ≥ 2.

The tiling problem Tile k takes as input a triple T T = (T , H , V ) where T is a finite set of tile types, H ⊆ T × T (resp. V ⊆ T × T ) represents the horizontal (resp. vertical) matching relation, and an initial tile type c ∈ T . A solution for the instance

(T T ,c) is a mapping τ : [0, t(k,n) -1] × [0, t(k,n) -1] → T such that (first) τ (0, 0) = c, and (hor&vert) for all i ∈ [0, t(k,n) -1] and j ∈ [0, t(k,n) -2],
(τ (j,i),τ (j + 1,i)) ∈ H and (τ (i, j),τ (i, j + 1)) ∈ V.

The problem of checking whether an instance of Tile k has a solution is known to be k-NExpTime-complete (see [START_REF] Papadimitriou | Computational complexity[END_REF]). The reduction below from Tile k to Sat(ML( * )) recycles ideas from [START_REF] Bednarczyk | Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?[END_REF] to reduce Tile k to Sat(QK t ). To provide the adequate adaptation for ML( * ), we need to solve two major issues. First, QK t admits second-order quantification, whereas in ML( * ), the second-order features are limited to the separating conjunction * . Second, the second-order quantification of QK t essentially colours the nodes in Kripke-style structures without changing the frame (W ,R). By contrast, the operator * modifies the accessibility relation, possibly making worlds that were reachable from the current world, unreachable in submodels. The Tower-hardness proof for Sat(ML( * )) becomes then much more challenging: we would like to characterise the position on the grid encoded by a world w by exploiting properties of its descendants (as done for QK t ), but at the same time, we need to be careful and only consider submodels where w keeps encoding the same position. In a sense, our encoding is robust: when the operator * is used to reason on submodels, we can enforce that no world changes the position of the grid that it encodes.

Enforcing t(j,n) children.

Let M = (W ,R,V ) be a finite forest. We consider two disjoint sets of atomic propositions P = {p 1 , . . . ,p n , val} and Aux = {x, y, l, s, r} (whose respective role is later defined). Elements from Aux are understood as auxiliary propositions. We call ax-node (resp. Aux-node) a world satisfying the proposition ax ∈ Aux (resp. satisfying some proposition in Aux). We call t-node a world that satisfies the formula t def = ax∈Aux ¬ax. Every world of M is either a t-node or an Aux-node. We say that w ′ is a t-child of w ∈W if w ′ ∈ R(w ) and w ′ is a t-node. We define the concepts of Aux-child and ax-child similarly.

The key development of our reduction is given by the definition of a formula, of exponential size in j ≥ 1 and polynomial size in n ≥ 1, that when satisfied by (M,w ) forces every t-node in R i (w ), where 0 ≤ i < j, to have exactly t(j-i,n) t-children, each of them encoding a different number in [0, t(j -i,n) -1]. As we impose that w is a t-node, it must have t(j,n) t-children. We assume n to be fixed throughout the section and denote this formula by type(j). From the property above, if M,w |= type(j) then for all i ∈ [1, j-1] and all t-nodes w ′ ∈ R i (w ) we have M,w ′ |= type(j-i).

First, let us informally describe how numbers are encoded in the model (M,w ) satisfying type(j). Let i ∈ [1, j]. Given a t-node w ′ ∈ R i (w ), n i (w ′ ) denotes the number encoded by w ′ . We omit the subscript i when it is clear from the context. When i = j, we represent n(w ′ ) by using the truth values of the atomic propositions p 1 , . . . ,p n . The proposition p b is responsible for the b-th bit of the number, with the least significant bit being encoded by p 1 . For example, for n = 3, we have M,w ′ |= p 3 ∧ p 2 ∧ ¬p 1 whenever n(w ′ ) = 6. The formula type(1) forces the parent of w ′ (i.e. is a t-node in R j-1 (w )) to have exactly 2 n t-children by requiring one tchild for each possible valuation upon p 1 , . . . ,p n . Otherwise, for i < j (and therefore j ≥ 2), the number n i (w ′ ) is represented by the binary encoding of the truth values of val on the t-children of w ′ which, since (M,w ′ ) |= type(j -i), are t(j -i,n) children implicitly ordered by the number they, in turn, encode. The essential property of type(j) is therefore the following: the numbers encoded by the t-children of a t-node w ′′ ∈ R i (w ), represent positions in the binary representation of the number n i (w ′′ ). Thanks to this property, the formula type(j) forces w to have exactly t(j,n) children, all encoding different numbers in [0, t(j,n) -1]. This is roughly represented in the picture below, where "1" stands for val being true whereas "0" stands for val being false.

. w . . . . . . < < . . . < < . . . < < 1 1 1 0 0 1 0 0 0 type(j), has t(j,n) children type(j-1) type(j-2)
To characterise these trees in ML( * ), we simulate secondorder quantification by using Aux-nodes. Informally, we require a pointed forest (M,w ) satisfying type(j) to be such that (i) every t-node w ′ ∈ R(w ) has exactly one x-child, and one (different) y-child. These nodes do not satisfy any other auxiliary proposition; (ii) for every i ≥ 2, every tnode w ′ ∈ R i (w ) has exactly five Aux-children, one for each ax ∈ Aux. We can simulate second-order existential quantification on t-nodes with respect to the symbol ax ∈ Aux by using the operator * in order to remove edges leading to ax-nodes. Then, we evaluate whether a property holds on the resulting model where a t-node "satisfies" ax ∈ Aux if it has a child satisfying ax. To better emphasise the need to move along t-nodes, given a formula φ, we write ⟨t⟩φ for the formula 3(t ∧ φ). Dually, [t]φ def = 2(t ⇒ φ). ⟨t⟩ i and [t] i are also defined, as expected.

Let us start to formalise this encoding. Let j ≥ 1. First, we restrict ourselves to models where every t-node reachable in at most j steps does not have two Aux-children satisfying the same proposition. Moreover, these Aux-nodes have no children and only satisfy exactly one ax ∈ Aux. We express this condition with the formula init(j) below:

⊞ j ax∈Aux t ⇒ ¬(3ax * 3ax) ∧ 2 ax ⇒ 2⊥ ∧ bx∈Aux\{ax} ¬bx ,
where ⊞ 0 φ def = φ and ⊞ m+1 φ def = φ ∧ 2 ⊞ m (φ). Notice that if M,w |= init(j) and M ′ ⊑ M, then M ′ ,w |= init(j).

Among the models ((W ,R,V ),w ) satisfying init(j), we define the ones satisfying type(j) described below (see similar conditions in [7, Section IV]):

(sub j ) every t-node in R(w ) satisfies type(j -1); (zero j ) there is a t-node w ∈ R(w ) such that n( w ) = 0; (uniq j ) distinct t-nodes in R(w ) encode different numbers; (compl j ) for every t-node w 1 ∈ R(w ), if n(w 1 ) < t(j,n) -1 then n(w 2 ) = n(w 1 ) + 1 for some t-node w 2 ∈ R(w ); (aux) w is a t-node, every t-node in R(w ) has one x-child and one y-child, and every t-node in R 2 (w ) has three children satisfying l, r and s, respectively.

We define type(0) def = ⊤, and for j ≥ 1, type(j) is defined as type(j) def = sub(j) ∧ zero(j) ∧ uniq(j) ∧ compl(j) ∧ aux, where each conjunct expresses its homonymous property. The formulae for sub(j), aux and zero(j) can be defined as sub(j) def = [t]type(j -1);

aux def = t ∧ [t](3x * 3y) ∧ [t] 2 (3l * 3s * 3r); zero(1) def = ⟨t⟩ b ∈[1,n] ¬p b ; zero(j + 1) def = ⟨t⟩[t]¬val.
The challenge is therefore how to express uniq(j) and compl(j), to guarantee that the numbers of children of w span all over [0, t(j,n) -1]. The structural properties expressed by type(j) lead to strong constraints, which permits to control the effects of * when submodels are constructed. This is a key point in designing type(j) as it helps us to control which edges are lost when considering a submodel.

Nominals, forks and number comparisons. In order to define uniq(j) and compl(j) (completing the definition of type(j)), we introduce auxiliary formulae, characterising classes of models that emerge naturally when trying to capture the semantics of (uniq j ) and (compl j ).

Let us consider a finite forest M = (W ,R,V ) and w ∈ W . A first ingredient is given by the concept of local nominals, borrowed from [START_REF] Bednarczyk | Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?[END_REF]. We say that ax ∈ Aux is a (local) nominal for the depth i ≥ 1 if there is exactly one t-node w ′ ∈ R i (w ) having an ax-child. In this case, w ′ is said to be the world that corresponds to the local nominal ax. The following formula states that ax is a local nominal for the depth i:

nom i (ax) def = ⟨t⟩ i 3ax ∧ k ∈[0,i-1] [t] k ¬ ⟨t⟩ i-k 3ax * ⟨t⟩ i-k 3ax .
We define the formula @ i ax φ def = ⟨t⟩ i (3ax∧φ) which, under the hypothesis that ax is a local nominal for the depth i, states that φ holds on the t-node that corresponds to ax. Moreover, we define nom i (ax bx) def = nom i (ax) ∧ nom i (bx) ∧ ¬@ i ax 3bx, which states that ax and bx are two nominals for the depth i with respect to two distinct t-nodes.

As a second ingredient, we introduce the notion of fork that is a specific type of models naturally emerging when trying to compare the numbers n(w 1 ) and n(w 2 ) of two worlds w 1 ,w 2 ∈ R i (w ) (e.g. when checking whether n(w 1 ) = n(w 2 ) or n(w 2 ) = n(w 1 ) + 1 holds). Given j ≥ i ≥ 1 we introduce the formula fork i j (ax, bx) that is satisfied by (M,w ) iff: • ax and bx are nominals for the depth i.

• w has exactly two t-children, say w U and w D .

• For every k ∈ [1,i -1], both R k (w U ) and R k (w D )
contain exactly one t-child. • The only t-node in R i-1 (w U ), say w ax , corresponds to the nominal ax. The only t-node in R i-1 (w D ), say w bx , corresponds to the nominal bx. • If i < j, then (M,w ax ) and (M,w bx ) satisfy type lsr (j -i) def = type(j -i) ∧ [t](3l ∧ 3s ∧ 3r). It should be noted that, whenever (M,w ) satisfies the formula fork i j (ax, bx), we witness two paths of length i, both starting at w and leading to w ax and w bx , respectively. Worlds in this path may have Aux-children. Below, we schematise a model satisfying fork i j (ax, bx):

.

fork i j (ax, bx) w type lsr (j-i) type lsr (j-i) ax bx i
Since the definition of fork i j (ax, bx) is recursive on i and j (due to type(j -i)), we postpone its formal definition to the next two sections where we treat the base cases for i = j and the inductive case for j > i separately.

The last auxiliary formulae are [ax < bx] i j and [bx = ax+1] j . Under the hypothesis that (M,w ) satisfies fork i j (ax, bx), the formula [ax < bx] i j is satisfied whenever the two (distinct) worlds w ax ,w bx ∈ R i (w ) corresponding to the nominals ax and bx are such that n(w ax ) < n(w bx ). Similarly, under the hypothesis that (M,w ) satisfies fork 1 j (ax, bx), the formula [bx = ax+1] j is satisfied whenever n(w bx ) = n(w ax ) + 1 holds. Both formulae are recursively defined, with base cases for i = j and j = 1, respectively.

For the base case, we define the formulae fork j j (ax, bx) and [ax < bx] j j (for arbitrary j), as well as [bx = ax+1] 1 . From these formulae, we are then able to define uniq(1) and compl [START_REF] Areces | Moving Arrows and Four Model Checking Results[END_REF], which completes the characterisation of type(1) and type lsr [START_REF] Areces | Moving Arrows and Four Model Checking Results[END_REF]. Afterwards, we consider the case 1 ≤ i < j and j ≥ 2, and define fork i j (ax, bx), [ax < bx] i j , [bx = ax+1] j , as well as uniq(j) and compl(j), by only relying on formulae that are already defined (by inductive reasoning).

Base cases: i = j or j = 1. In what follows, we consider a finite forest M = (W ,R,V ) and a world w. Following its informal description, we have

fork j j (ax, bx) def = 3 =2 t ∧ [t] ⊞ j-2 (t⇒3 =1 t) ∧ nom j (ax bx)
, where ⊞ j φ def = ⊤ for j < 0. As previously explained, in the base case, the number n(w ′ ) encoded by a t-node w ′ ∈ R j (w ) is represented by the truth values of p 1 , . . . ,p n . Then, the formula [ax < bx] j j is defined as

[ax < bx] j j def = u ∈[1,n] @ j ax ¬p u ∧ @ j bx p u ∧ v ∈[u+1,n] (@ j ax p v ⇔ @ j bx p v ) .
The satisfaction of (M,w ) |= fork j j (ax, bx) enforces that the distinct t-nodes w ax ,w bx ∈ R j (w ) corresponding to ax and bx satisfy n(w ax ) < n(w bx ), which can be shown by using standard properties about bit vectors.

The formula [bx = ax+1] 1 is similarly defined:

u ∈[1,n] @ 1 ax (¬p u ∧ v ∈[1,u-1] p v ) ∧ @ 1 bx (p u ∧ v ∈[1,u-1] ¬p v )∧ v ∈[u+1,n] (@ 1 ax p v ⇔@ 1 bx p v ) .
Assuming (M,w ) |= fork 1 1 (ax, bx), this formula states that the two distinct t-nodes w ax ,w bx ∈ R(w ) corresponding to ax and bx are such that n(w bx ) = n(w ax ) + 1. Again, correctness is guaranteed by standard analysis on bit vectors.

To define uniq(1), we recall that a model satisfying type(1) satisfies the formula aux and hence every t-node in R(w ) has two auxiliary children, one x-node and one y-node. The idea is to use these two Aux-children and rely on * to state that it is not possible to find a submodel of M such that w has only two distinct children w x and w y corresponding to the nominals x and y, respectively, and such that n(w x ) = n(w y ). In a sense, the operator * simulates a second-order quantification on x and y.

Let [x = y] 1 1 def = ¬([x < y] 1 1 ∨ [y < x] 1 1
). We define uniq(1) def = ¬ ⊤ * (fork 1 1 (x, y) ∧ [x = y] 1 1 ) . To capture compl(1) we state that it is not possible to find a submodel of M that looses x-nodes from R 2 (w ), keeps all y-nodes, and is such that (i) x is a local nominal for the depth 1, corresponding to a world w x encoding n(w x ) < 2 n -1; (ii) there is no submodel where w has two t-children, w x and a second world w y , such that w y corresponds to the nominal y and n(w y ) = n(w x )+1. Thus, compl(1) is defined as:

¬ 2⊥ * [t]3y∧@ 1 x ¬1 1 ∧¬(⊤ * (fork 1 1 (x, y)∧[y = x+1] 1 )
) . The subscript "1" in the formula 1 1 refers to the fact that we are treating the base case of compl(j) with j = 1. We have

1 1 def = i ∈[1,n] p i , reflecting the encoding of 2 n -1.
This concludes the definition of type(1) (and type lsr (1)), which is established correct with respect to its specification. Lemma 4.1. Let M,w |= init [START_REF] Areces | Moving Arrows and Four Model Checking Results[END_REF]. We have M,w |= type( 1) iff (M,w ) satisfies (sub 1 ), (zero 1 ), (uniq 1 ), (compl 1 ) and (aux).

Inductive case: 1 ≤ i < j. As an implicit inductive hypothesis used to prove that the formulae are well-defined, we assume that [bx = ax+1] j ′ and type(j ′ ) are already defined for every j ′ < j, whereas fork i ′ j ′ (ax, bx), and [ax < bx] i ′ j ′ are already defined for every 1 ≤ i ′ ≤ j ′ such that j ′ -i ′ < ji. Therefore, we define:

fork i j (ax, bx) def = fork i i (ax, bx) ∧ [t] i type lsr (j -i).
It is easy to see that this formula is well-defined: fork i i (ax, bx) is from the base case, whereas type lsr (j-i) is defined by inductive hypothesis, since we have ji < j.

Consider now [ax < bx] i j . Assuming M,w |= fork i j (ax, bx), we wish to express n(w ax ) < n(w bx ) for the two distinct worlds w ax ,w bx ∈ R i (w ) corresponding to the nominals ax and bx, respectively. As i < j, n(w ax ) (resp. n(w bx )) is encoded using the truth value of val on the t-children of w ax (resp. w bx ). To rely on arithmetical properties of binary numbers used to define [ax < bx] j j , we need to find two partitions P ax = {L ax ,S ax ,R ax } and P bx = {L bx ,S bx ,R bx }, one for the t-children of w ax and another one for those of w bx s.t.: (LSR): Given b ∈ {ax, bx}, P b splits the t-children as follows:

• there is a t-child s b of w b such that S b = {s b };

• n(r ) < n(s b ) < n(l ), for every r ∈ R b and l ∈ L b . (LESS): P ax and P bx have constraints to satisfy <:

• n(s ax ) = n(s bx ), M,s ax |= ¬val and M,s bx |= val;

• for every l ax ∈ L ax and

l bx ∈ L bx , if n(l ax ) = n(l bx ) then M,l ax |= val iff M,l bx |= val.
It is important to notice that these conditions essentially revolve around the numbers encoded by t-children, which will be compared using the already defined (by inductive reasoning) formulae [ax < bx] i ′ j ′ , where j ′ -i ′ < ji. Since the semantics of [ax < bx] i j is given under the hypothesis that M,w |= fork i j (ax, bx), we can assume that every child of w ax and w bx has all the possible Aux-children. Then, we rely on the auxiliary propositions in {l, s, r} in order to mimic the reasoning done in (LSR) and (LESS).

We start by considering the constraints involved in (LSR) and express them with the formula lsr(j), which is satisfied by a pointed forest (M = (W ,R,V ),w ) whenever:

• (M,w ) satisfies type(j). • Every t-child of w has exactly one {l, s, r}-child, and only one of these t-children (say w ′ ) has an s-child. • Every t-child of w that has an l-child (resp. r-child) encodes a number greater (resp. smaller) than n(w ′ ). Despite this formula being defined in terms of type(j), we only rely on lsr(j -i) (which is defined by inductive reasoning) in order to define [ax < bx] i j . The picture below schematises a model satisfying lsr(j). The definition of lsr(j) follows closely its specification:

lsr(j) def = type(j) ∧ nom 1 (s) ∧¬(⊤ * (fork 1 j (s, l) ∧¬[s < l] 1 j )) ∧¬(⊤ * (fork 1 j (s, r) ∧¬[r < s] 1 j )) ∧ [t]3 =1 (l ∨ s ∨ r).
We define the formula [ax < bx] i j as follows: ⊤ * nom i (ax bx) ∧ [t] i lsr(j -i) ∧ S i j (ax, bx) ∧ L i j (ax, bx) , where S i j (ax, bx) and L i j (ax, bx) check the first and second condition in (LESS), respectively. In particular, by defining

[ax = bx] i j def = ¬([ax < bx] i j ∨ [bx < ax] i j ), we have S i j (ax, bx) def = ⊤ * fork i+1 j (x, y) ∧ @ i ax ⟨t⟩(3s ∧ 3x) ∧ @ i bx ⟨t⟩(3s ∧ 3y) ∧ [x = y] i+1 j ∧ @ i+1 x ¬val ∧ @ i+1 y val L i j (ax, bx) def = ¬ ⊤ * fork i+1 j (x, y) ∧ @ i ax ⟨t⟩(3l ∧ 3x) ∧ @ i bx ⟨t⟩(3l ∧ 3y) ∧ [x = y] i+1 j ∧¬(@ i+1
x val ⇔ @ i+1 y val) . Both fork i+1 j (x, y) and [x = y] i+1 j used in these formulae are defined recursively. The formula S i j (ax, bx) states that there is a submodel M ′ ⊑ M such that I.

M ′ ,w |= fork i+1 j (x, y); II.

s ax corresponds to the nominal x at depth i + 1; III.

s bx corresponds to the nominal y at depth i + 1; IV-VI. n(s ax ) = n(s bx ), M,s ax ̸ |= val and M,s bx |= val.

(The enumeration I-VI refers to the conjuncts in the formula) S i j (ax, bx) correctly models the first condition of (LESS). Regarding L i j (ax, bx) and (LESS), a similar analysis can be performed. We define LS i j (ax, bx) def = L i j (ax, bx) ∧ S i j (ax, bx). Let us consider [bx = ax+1] j . Under the hypothesis that M,w |= fork i j (ax, bx), this formula must express n(w bx ) = n(w ax ) + 1 for the two (distinct) worlds w ax ,w bx ∈ R i (w ). Then, as done for defining [ax < bx] i j , we take advantage of arithmetical properties on binary numbers and we search for two partitions P ax = {L ax ,S ax ,R ax } and P bx = {L bx ,S bx ,R bx } of the t-children of w ax and w bx , respectively, such that P ax and P bx satisfy (LSR) as well as the condition below:

(PLUS): P ax and P bx have the properties of +1 :

• P ax and P bx satisfy (LESS);

• for every r ax ∈ R ax , we have M,r ax |= val;

• for every r bx ∈ R bx , we have M,r ax ̸ |= val,

where S ax = {s ax } and S bx = {s bx }, as required by (LSR).

The definition of [bx

= ax+1] j is similar to [ax < bx] i j : ⊤ * nom 1 (ax bx) ∧ [t]lsr(j -1) ∧ LS 1 j (ax, bx) ∧ R(ax, bx) , where R(ax, bx) def = @ 1 ax [t](3r ⇒ val)∧@ 1 bx [t](3r ⇒ ¬val) captures the last two conditions of (PLUS).
To define uniq(j) and compl(j), we rely on fork i j (ax, bx),

[ax < bx] i j and [bx = ax+1] j . uniq(j) def = ¬ ⊤ * (fork 1 j (x, y) ∧ [x = y] 1 j ) compl(j) def = ¬ 2⊥ * [t](type lsr (j -1) ∧ 3y) ∧ nom 1 (x)∧ @ 1 x ¬1 j ∧ ¬ ⊤ * (fork 1 j (x, y) ∧ [y = x+1] j )
, where 1 j def = [t]val reflects the encoding of t(j,n) -1 for j > 1. The main difference between compl(1) and compl(j) (j > 1) is that the conjunct [t]3y of compl( 1) is replaced by [t](type lsr (j -1) ∧ 3y) in compl(j), as needed to correctly evaluate fork 1 j (x, y). Indeed, the difference between fork 1 1 (x, y) and fork 1 j (x, y) is precisely that the latter requires [t]type lsr (j -1). The definition of type(j) is now complete. We can state its correctness. Lemma 4.2. Let M,w |= init(j). We have M,w |= type(j) iff (M,w ) satisfies (sub j ), (zero j ), (uniq j ), (compl j ) and (aux).

The size of type(j) is exponential in j > 1 and polynomial in n ≥ 1. As its size is elementary, we can use this formula as a starting point to reduce Tile k .

Tiling a grid

[0, t(k,n) -1] × [0, t(k,n) -1]
Below, we briefly explain how to use previous developments to define a uniform reduction from Tile k , for every k ≥ 2. Several adaptations are needed to encode smoothly the grid but the hardest part was the design of type(j). Let k ≥ 2 and (T T , c) be an instance of Tile k . We can construct a formula tiling T T ,c (k ) that is satisfiable if and only if (T T , c) as a solution. To represent [0, t(k,n) -1] 2 in some pointed forest (M,w ), where M = (W ,R,V ), we recycle the ideas for defining type(k ). From Lemma 4.2, we know that if M,w |= init(k ) ∧ type(k ) then the t-children of w encode the interval [0, t(k,n) -1]. A position in the grid is however a pair of numbers, hence the crux of our encoding rests on the fact that each w ′ ∈ R(w ) encodes two numbers n H (w ′ ) and n V (w ′ ). Similarly to type(k ), these numbers are represented by the truth values on the t-children of w ′ , with the help of new propositions val H and val V . We are in luck: since both numbers are from [0, t(k,n) -1], w ′ just needs as many children as when encoding a single number, and therefore if M,w |= tiling T T ,c (k ) then M,w ′ |= type(k-1). In fact, the portion of tiling T T ,c (k ) that encodes the grid can be described quite naturally by slightly updating the characterisation of type(k ). For example, (uniq j ) becomes

(uniq T T ,k ) for all distinct t-nodes w 1 ,w 2 ∈ R(w ) n H (w 1 ) n H (w 2 ) or n V (w 1 ) n V (w 2 ).
The formula uniq(k ) has to be updated accordingly, but without major differences or complications. Of course, more is required as tiling T T ,c (k ) must also encode the tiling conditions (first) and (hor&vert). Fortunately, the kit of formulae defined for type(k ) allows us to have access to n H (w ′ ) and n V (w ′ ) in such a way that both conditions can be expressed rather easily. For example, to express vertical constraints, we design a formula stating that for all t-nodes

w 1 ,w 2 ∈ R(w ), if n V (w 2 ) = n V (w 1 )+1 and n H (w 2 ) = n H (w 1 ) then there is (c 1 , c 2 ) ∈ V such that w 1 ∈ V (c 1 ) and w 2 ∈ V (c 2 )
. Further details are omitted by lack of space.

Theorem 4.3. Sat(ML( * )) is Tower-complete.

ML( * ) Strictly Less Expressive Than GML

Below, we focus on the expressivity of ML( * ). We first show ML( * ) ⪯ GML and then we prove the strictness of the inclusion. The former result takes advantage of the notion of gbisimulation, i.e. the underlying structural indistinguishability relation of GML, studied in [START_REF] De Rijke | A Note on Graded Modal Logic[END_REF]. To show ML( * ) ≺ GML, we define an ad hoc notion of Ehrenfeucht-Fraïssé games for ML( * ), see e.g. classical definitions in [START_REF] Libkin | Elements of Finite Model Theory[END_REF] and similar approaches in [START_REF] Calcagno | Adjunct elimination in Context Logic for trees[END_REF][START_REF] Dawar | Adjunct Elimination Through Games in Static Ambient Logic[END_REF]. Then, we design a simple formula in GML that cannot be expressed in ML( * ).

5.1 ML( * ) is not more expressive than GML To establish that ML( * ) ⪯ GML, we proceed as in Section 3.1.

In fact, by Lemma 2.2, given φ 1 , φ 2 in GML, the formula φ 1 * φ 2 is equivalent to (φ 1 φ 2 ). Moreover, we know that given φ 1 , φ 2 in GML, φ 1 φ 2 is equivalent to some formula in GML, as shown in Section 3. So, to prove that ML( * ) ⪯ GML by applying the proof schema of Theorem 3.2, it is sufficient to show that given φ in GML, there is ψ in GML such that φ ≡ ψ . To do so, we rely on the indistinguishability relation of GML, called g-bisimulation [START_REF] De Rijke | A Note on Graded Modal Logic[END_REF].

A g-bisimulation is a refinement of the classical backand-forth conditions of a bisimulation (see e.g. [START_REF] Blackburn | Modal Logic[END_REF]), tailored towards capturing graded modalities. It relates models with similar structural properties, but up to parameters m,k ∈ N responsible for the modal degree and the graded rank, respectively. The following invariance result holds: g-bisimilar models are modally equivalent in GML (up to formulae of modal degree m and graded rank at most k). For simplicity, we present the construction of the above-mentioned formula ψ by directly using the notion of model equivalence, without going explicitly through g-bisimulations.

Given m,k ∈ N and P ⊆ fin AP, we write GML[m,k, P] to denote the set of GML formulae ψ having md(ψ ) ≤ m, gr(ψ ) ≤ k and propositional variables from P. GML[m,k, P] is finite up to logical equivalence [START_REF] De Rijke | A Note on Graded Modal Logic[END_REF]. Given pointed forests (M,w ) and (M ′ ,w ′ ), we write (M,w ) ≡ P m,k (M ′ ,w ′ ) whenever (M,w ) and (M ′ ,w ′ ) are GML[m,k, P]-indistinguishable, i.e. for every ψ in GML[m,k, P], M,w |= ψ iff M ′ ,w ′ |= ψ . We write T P (m,k ) to denote the quotient set induced by the equivalence relation ≡ P m,k . As GML[m,k, P] is finite up to logical equivalence, we get that T P (m,k ) is finite.

To establish that GML is closed under , we show that there is a function f : N 2 → N such that for all m,k ∈ N and P ⊆ fin AP, if two models are in the same equivalence class of ≡ P m,f(m,k ) , then they satisfy the same formulae of the form φ, where φ is in GML[m,k, P]. By standard arguments and using the fact that GML[m, f(m,k ), P] is finite up to logical equivalence, we then conclude that φ is equivalent to a formula in GML[m, f(m,k ), P]. Similar approaches are followed in [START_REF] Demri | Axiomatising Logics with Separating Conjunction and Modalities[END_REF][START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF][START_REF] Mansutti | Extending Propositional Separation Logic for Robustness Properties[END_REF]. As we are not interested in the size of the equivalent formula, we can simply use the cardinality of T P (m,k ) in order to inductively define a suitable function:

f(0,k ) def = k, f(m + 1,k ) def = k × (|T P (m, f(m,k ))| + 1
). In conformity with the results in Section 4, the map f can be shown to be a non-elementary function. To prove that f satisfies the required properties, we start by showing a technical lemma which essentially formalises a simulation argument on the relation ≡ P m,f(m,k ) with respect to the submodel relation. By taking submodels as with the operator, equivalence in GML is preserved.

Lemma 5.1. Let (M,w ) ≡ P m,f(m,k ) (M ′ ,w ′ ) where m,k ∈ N, P ⊆ fin AP, M = (W ,R,V ) and M ′ = (W ′ ,R ′ ,V ′ ). Let R 1 ⊆ R. There is R ′ 1 ⊆ R ′ s.t. ((W ,R 1 ,V ),w ) ≡ P m,k ((W ′ ,R ′ 1 ,V ′ ),w ′ ) and if R 1 (w ) = R(w ), then R ′ 1 (w ′ ) = R ′ (w ′
). The proof of Lemma 5.1 is by induction on m. The last condition about R 1 (w ) = R(w ) will serve in the proof of Lemma 5.2, as it allows us to capture the semantics of , by preserving the children of the world w ′ . In the proof, we rely on the properties of g-bisimulations [START_REF] De Rijke | A Note on Graded Modal Logic[END_REF] to define a binary relation ↔ between worlds of R(w ) and R ′ (w ′ ). Every

w 1 ↔ w ′ 1 is such that (M,w 1 ) ≡ P m-1,f(m-1,k ) (M ′ ,w ′ 1 )
. The operator does not necessarily preserve the children of w 1 and w ′ 1 , so that the induction hypothesis, naturally defined from the statement of Lemma 5.1, is applied on models where the condition R 1 (w 1 ) = R(w 1 ) may not hold. We show that for all R 1 ⊆ R, it is possible to construct R ′ 1 ⊆ R ′ such that, for all w 1 ↔ w ′ 1 , ((W ,R 1 ,V ),w 1 )

≡ P m-1,k ((W ′ ,R ′ 1 ,V ′ ),w ′ 1 )
. The result is then lifted to ((W ,R 1 ,V ),w ) ≡ P m,k ((W ′ ,R ′ 1 ,V ′ ),w ′ ), again thanks to the properties of the g-bisimulation.

Intuitively, Lemma 5.1 states that given two models satisfying the same formulae up to the parameters m and f(m,k ), we can extract submodels satisfying the same formulae up to m and k (reduced graded rank). This allows us to conclude that if φ is in GML, there is some GML formula equivalent to φ (Lemma 5.2). In other words, the operator can be eliminated to obtain a GML formula. This, together with Lemma 2.2 and Theorem 3.2 entail ML( * ) ⪯ GML. Lemma 5.2. For every φ ∈ GML[m,k, P] there is a formula ψ ∈ GML[m, f(m,k ), P] such that φ ≡ ψ .

Showing ML( * ) ≺ GML with EF games for ML( * )

We tackle the problem of showing that ML( * ) is strictly less expressive than GML. To do so, we adapt the notion of Ehrenfeucht-Fraïssé games (EF games, in short) [START_REF] Libkin | Elements of Finite Model Theory[END_REF] to ML( * ), and use it to design a GML formula that is not expressible in ML( * ). We write ML( * )[m,s, P] for the set of formulae φ of ML( * ) having md(φ) ≤ m, at most s nested * , and atomic propositions from P ⊆ fin AP. It is easy to see that ML( * )[m,s, P] is finite up to logical equivalence.

We introduce the EF games for ML( * ). A game is played between two players: the spoiler and the duplicator. A game

Game on [(M 1 =(W 1 , R 1 , V 1 ), w 1 ), (M 2 =(W 2 , R 2 , V 2 ), w 2 ), (m, s, P)].
if there is p ∈ P s.t. w 1 ∈ V 1 (p ) iff w 2 V 2 (p ) then the spoiler wins. else the spoiler chooses i ∈ {1, 2} and plays on M i . The duplicator replies on M j where j i. The spoiler must choose one of the following moves, otherwise the duplicator wins: modal move: if m ≥ 1 and R i (w i ) ∅ then the spoiler can choose to play a modal move by selecting an element w ′ i ∈ R i (w i ). Then, • the duplicator must reply with a w ′ j ∈ R j (w j ) (else, the spoiler wins); state is a triple made of two pointed forests (M,w ) and (M ′ ,w ′ ) and a rank (m,s, P), where m,s ∈ N and P ⊆ fin AP. The goal of the spoiler is to show that the two models are different. The goal of the duplicator is to counter the spoiler and to show that the two models are similar. Two models are different whenever there is φ ∈ ML( * )[m,s, P] that is satisfied by only one of the two models. The EF games for ML( * ) are formally defined in Figure 1. The exact correspondence between the game and the logic is formalised in Lemma 5.3.

Using the standard definitions in [START_REF] Libkin | Elements of Finite Model Theory[END_REF], the duplicator has a winning strategy for the game ((M,w ), (M ′ ,w ′ ), (m,s, P)) if she can play in a way that guarantees her to win regardless how the spoiler plays. When this is the case, we write (M,w ) ≈ P m,s (M ′ ,w ′ ). Similarly, the spoiler has a winning strategy, written (M,w ) P m,s (M ′ ,w ′ ), if he can play in a way that guarantees him to win, regardless how the duplicator plays. Lemma 5.3 guarantees that the games are well-defined.

Lemma 5.3. (M,w ) P m,s (M ′ ,w ′ ) iff there is a formula φ in ML( * )[m,s, P] such that M,w |= φ and M ′ ,w ′ ̸ |= φ. Lemma 5.3 is proven with standard arguments from [START_REF] Libkin | Elements of Finite Model Theory[END_REF], for instance the left-to-right direction, i.e. the completeness of the game, is by induction on the rank (m,s, P). Thanks to the EF games, we are able to find a GML formula φ that is not expressible in ML( * ). By Lemma 2.1 and as ML( ) ≈ GML, such a formula is necessarily of modal degree at least 2. Happily, φ = 3 =2 3 =1 ⊤ does the job and cannot be expressed in ML( * ). For the proof, we show that for every rank (m,s, P), there are two structures (M,w ) and (M ′ ,w ′ ) such that (M,w ) ≈ P m,s (M ′ ,w ′ ), M,w |= φ and M ′ ,w ′ ̸ |= φ. The inexpressibility of φ then stems from Lemma 5.3. The two structures are represented below ((M,w ) on the left).

. . . . . . ≥ 2 s + 1 ≥ 2 s-1 (s + 1)(s + 2) + 1 ≈ P m,s w ′ . . . . . . ≥ 2 s + 1 ≥ 2 s-1 (s + 1)(s + 2) + 1
In the following, we say that a world has type i if it has i children. As one can see in the figure above, children of the current worlds w and w ′ are of three types: 0, 1 or 2. When the spoiler performs a spatial move in the game, a world of type i can take, in the submodels, a type between 0 and i. That is, the number of children of a world weakly monotonically decreases when taking submodels. This monotonicity, together with the finiteness of the game, lead to bounds on the number of children of each type, over which the duplicator is guaranteed to win. For instance, the bound for worlds of type 2 is given by the value 2 s (s + 1)(s + 2), where s is the number of spatial moves in the game. In the two presented pointed forests, one child of type 0 and one of type 2 are added with respect to these bounds, so that the duplicator can make up for the different numbers of children of type 1.

Lemma 5.4. ML( * ) cannot characterise the class of models satisfying the GML formula 3 =2 3 =1 ⊤. Notice that ML( * ) is more expressive than ML. Indeed, the formula 3⊤ * 3⊤ distinguishes the two models on the right, which are bisimilar and hence indistinguishable in ML [START_REF] Van Benthem | Modal Correspondence Theory[END_REF]. By ML( * ) ⪯ GML, Lemma 5.4 and Theorem 3.2, we conclude. Theorem 5.5. ML ≺ ML( * ) ≺ GML ≈ ML( ).

ML( ), ML( * ) and Sister Logics

Below, we show how our new results on ML( ) and ML( * ) allow us to make substantial contributions for sister logics.

Static ambient logic

Static ambient logic (SAL) is a formalism proposed to reason about spatial properties of concurrent processes specified in the ambient calculus [START_REF] Cardelli | Formal Methods for Distributed Processing[END_REF]. In [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF], the satisfiability and validity problems for a very expressive fragment of SAL are shown to be decidable and conjectured to be in PSpace (see [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF]Section 6]). We invalidate this conjecture by showing that the intensional fragment of SAL (see [START_REF] Lozes | Adjuncts elimination in the static ambient logic[END_REF]), herein denoted SAL( ), is already AExp Pol -complete. More precisely, we design semantically faithful reductions between Sat(ML( )) and Sat(SAL( )) (in both directions), leading to the abovementioned result by Corollary 3.8. SAL( ) formulae are from

φ := ⊤ | 0 | n[φ] | φ ∧ φ | ¬φ | φ φ,
where n ∈ AP is an ambient name. Historically, the semantics of SAL is given on a class of syntactically defined finite trees. However, this class of models is isomorphic to the class of finite trees M = (W ,R,V ), such that each world in W satisfies exactly one atomic proposition (its ambient name). Then, the satisfaction relation |= for SAL( ) is standard for ⊤ and Boolean connectives, φ 1 φ 2 is as in ML( ), and otherwise

M,w |= 0 ⇔ R(w ) = ∅; M,w |= n[φ] ⇔ there is w ′ ∈ W such that R(w ) = {w ′ }, w ′ ∈ V (n) and M,w ′ |= φ.
With such a presentation, SAL( ) is a fragment of ML( ), where 0 and n[φ] correspond to 2⊥ and 3 =1 ⊤∧3(n∧φ), respectively. However, to reduce Sat(SAL( )) to Sat(ML( )), we must deal with the constraint on V (uniqueness of the ambient name). Let φ be in SAL( ) written with the ambient names in N = {n 1 , . . . , n m }. It is known (see [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF]Lemma 8]) that if φ is satisfiable, then it can be satisfied by a tree having ambient names from N ∪ {n}, where n is a fresh name. Thus, we can show that φ is satisfiable iff so is the ML( ) formula φ ∧ ⊞ md(φ ) ( n∈N∪{n} (n ∧ n ′ ∈(N∪{n})\{n} ¬n ′ )),

where the right conjunct states that V , restricted to the propositions in N ∪ {n}, forms a partition of the worlds reachable from the current one in at most md(φ) steps.

Reducing Sat(ML( )) to Sat(SAL( )) requires a bit more work. Let M = (W ,R,V ) be a finite forest and w ∈ W . Assume we want to check the satisfiability status of φ in ML( ) having atomic propositions from P = {p 1 , . . . ,p m } and with n occurrences of . We encode (M,w ) into a model (M ′ = (W ′ ,R ′ ,V ′ ),w ) of SAL( ) as follows. Let rel and ap be two ambient names not in P. The ambient name rel encodes the relation R whereas ap can be seen as a container for propositional variables holding on the current world. (i) We require W ⊆ W ′ , R ⊆ R ′ and i ∈[0,md(φ )] R i (w ) ⊆ V ′ (rel), i.e., every world reachable from w in at most md(φ) steps has the ambient name rel. Let w ′ be one of these worlds and suppose that {p | w ′ ∈ V (p)} ∩ P = {q 1 , . . . ,q l }. (ii) We require W ′ to contain n + 1 worlds w ′ 1 , . . . ,w ′ n+1 ∈ R ′ (w ′ ) \ R(w ′ ), all having ambient name ap. These worlds encode copies of w ′ 's valuation, similarly to what is done in Section 3.2 to encode teams from PL[~]. (iii) For all j ∈ [1,n + 1], R ′ (w ′ j ) contains l worlds, all satisfying 0 and a distinct ambient name from {q 1 , . . . ,q l }. Below we schematise the encoding (w.r.t. w ′ ). Lastly, we define the translation of φ, written τ (φ), into SAL( ). It is homomorphic for Boolean connectives and ⊤, τ (p) def = ⟨ap⟩⟨p⟩⊤ and otherwise it is inductively defined: τ (3ψ ) def = ⟨rel⟩τ (ψ ); τ (ψ 1 ψ 2 ) def = τ (ψ 1 ) ∧ ⟨ap⟩ ≥j ⊤ τ (ψ 2 ) ∧ ⟨ap⟩ ≥k ⊤ , where in τ (ψ 1 ψ 2 ), j (resp. k) is the number of occurrences of in ψ 1 (resp. ψ 2 ) plus one and ⟨ap⟩ ≥α ⊤ def = (∀[ap] ∧ [# = α]) ⊤.

We show that φ is satisfiable in ML( ) iff C φ ∧ τ (φ) is satisfiable in SAL( ), leading to the following results about the complexity of static ambient logics. Corollary 6.1. Sat(SAL( )) is AExp Pol -complete. Sat(SAL) with SAL from [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF] is AExp Pol -hard.

Modal separation logic

The family of modal separation logics (MSL), combining separating and modal connectives, has been recently introduced in [START_REF] Demri | The power of modal separation logics[END_REF]. Its models, inspired from the memory states used in separation logic (see also [START_REF] Courtault | A modal separation logic for resource dynamics[END_REF]), are Kripke-style structures M = (W ,R,V ), where W = N and R ⊆ W × W is finite and functional. Hence, unlike finite forests, M may have loops.

Among the fragments studied in [START_REF] Demri | The power of modal separation logics[END_REF], the modal separation logic MSL( * , 3 -1 ) was left with a huge complexity gap (between PSpace and Tower). Then, assume we want to check the satisfiability of φ in ML( * ) by relying on an algorithm for Sat(MSL( * , 3 -1 )). We simply need to consider the formula φ[3 ← 3 -1 ] obtained from φ by replacing every occurrence of 3 by 3 -1 , and check if it can be satisfied by a locally acyclic model (M,w ) of MSL, i.e. one where w does not belong to a loop of length ≤ md(φ). Local acyclicity can be enforced by the formula locacycl def = r ∧ i ∈[1,md(φ )] (2 -1 ) i ¬r , where r ∈ AP is fresh. Then, φ in ML( * ) is satisfiable iff φ[3 ← 3 -1 ]∧locacycl in MSL( * , 3 -1 ) is satisfiable. Hence, the results in Section 4 allow us to close the complexity gap. Corollary 6.2. Sat(MSL( * , 3 -1 )) is Tower-complete.

Conclusion

We have studied and compared ML( ) and ML( * ), two modal logics interpreted on finite forests and featuring composition operators. We have not only characterised the expressive power and the complexity for both logics, but also identified remarkable differences and export our results to other logics. ML( ) is shown as expressive as GML, and its satisfiability problem is found to be AExp Pol -complete. Besides the obvious similarities between ML( ) and ML( * ), these results are counter-intuitive: though the logic ML( * ) is strictly less expressive than GML (and consequently, than ML( )), Sat(ML( * )) is Tower-complete. We also recalled that there are logspace reductions from ML( * ) and ML( ) to the secondorder modal logic QK t from [START_REF] Bednarczyk | Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?[END_REF].

Our proof techniques go beyond what is known in the literature. For instance, to design the Tower-hardness proof we needed substantial modifications from the proof introduced in [START_REF] Bednarczyk | Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?[END_REF] for QK t . On the other hand, to show the expressivity inclusion of ML( * ) within GML, we provided a novel definition of Ehrenfeucht-Fraïssé games for ML( * ).

Lastly, our framework led to the characterisation of the satisfiability problems for two sister logics . We proved that the satisfiability problem for the modal separation logic MSL( * , 3 -1 ) is Tower-complete [START_REF] Demri | The power of modal separation logics[END_REF]. Moreover, the satisfiability problem for the static ambient logic SAL( ) is AExp Polcomplete, solving open problems from [START_REF] Calcagno | Deciding validity in a spatial logic for trees[END_REF][START_REF] Demri | The power of modal separation logics[END_REF] and paving the way to study the complexity of the full SAL.

.

Figure 1 .

 1 Figure 1. Ehrenfeucht-Fraïssé games for ML( * )

  w

  Let n ∈ AP. We define the modality⟨n⟩φ def = n[φ] ⊤ and its dual [n]φ def = ¬⟨n⟩¬φ. We write ∀[n] for ¬((¬0 ∧ ¬n[⊤]) ⊤), so that (M,w ) |= ∀[n] whenever every child of w has the ambient name n. Moreover, [# ≥ 0] def = ⊤ and [# ≥ β+1] def = ¬0 [# ≥ β], so that (M,w ) |= [# ≥ β] whenever w has at least β children. Lastly, [# = β] def = [# ≥ β]∧¬[# ≥ β+1].The models of SAL( ) encoding models of ML( ) are characterised byC φ def = j ∈[0,md(φ )] [rel] j ∀[rel] ∀[ap] ∧ [# = n+1] ∧ [ap] (p 1 [0]∨0) . . . (p m [0]∨0) ∧ i ∈[1,m] (⟨ap⟩⟨p i ⟩⊤ ⇒ [ap]⟨p i ⟩⊤) .

  Its formulae are defined fromφ := p | 3 -1 φ | φ ∧ φ | ¬φ | φ * φ . The satisfaction relation is as in ML( * ) for p ∈ AP, Boolean connectives and φ 1 * φ 2 , otherwise M,w |= 3 -1 φ ⇔ ∃w ′ s.t. (w ′ ,w ) ∈ R and M,w ′ |= φ.Since MSL( * , 3 -1 ) is interpreted over a finite and functional relation, 3 -1 effectively works as the 3 modality of ML( * ).

Acknowledgements

We would like to thank the anonymous reviewers for their comments and suggestions that helped us to improve the quality of the document. B. Bednarczyk is supported by the Polish Ministry of Science and Higher Education program "Diamentowy Grant" no. DI2017 006447. S. Demri and A. Mansutti are supported by the Centre National de la Recherche Scientifique (CNRS). R. Fervari is supported by ANPCyT-PICTs-2017-1130 and 2016-0215, and by the Laboratoire International Associé SINFIN.