Why Does Prop. Quantification Make Logics on Trees Robustly Hard?]Why Does
Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?

B. Bednarczyk]bartosz Bednarczyk0000-0002-8267-7554[a]
Computational Logic Group, TU Dresden & Institute of Computer Science, University of Wrocław

S. Demri]Stéphane Demri0000-0002-3493-2610[b]
Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, 91190, Gif-sur-Yvette, France

Adding propositional quantification to the modal logics , $\mathsf{T}$ or is known to lead to undecidability
but with propositional quantification under the tree semantics () admits a non-elementary
-complete satisfiability problem.
We investigate the complexity of strict fragments of  as well as of the modal logic with propositional
quantification under the tree semantics.
More specifically, we show that  restricted to the temporal operator $\EX$ is already -hard,
which is unexpected as $\EX$ can only enforce local properties.
When  restricted to $\EX$ is interpreted on $N$-bounded trees for
some $N \geq 2$, we prove that the satisfiability problem is -complete;
-hardness is established by reduction from a recently introduced
tiling problem, instrumental for studying the model-checking problem for interval temporal logics.
As consequences of our proof method,
we prove -hardness of  restricted to  $\EF$ or to $\EX\EF$ and
of the well-known modal logics such as , , ,
and with propositional quantification under a semantics based on classes of trees.

§ INTRODUCTION

Propositional quantification in modal and temporal logics

A natural way to design logics that dynamically
update their models, consists in adding propositional quantification as done for example
to define QBF from SAT.
Propositional quantification is a very powerful feature to update models but this may have consequences
in terms of computability.
In the realm of modal logics [9], the paper [13] remains a quite early work adding
propositional quantification.
The undecidability of the propositional modal logic
(resp. $\mathsf{T}$, and ) augmented with propositional
quantification is first established in [24], and this is done thanks to a reduction
from  the second-order arithmetic. By contrast, the decidability of second-order versions of the
modal logic is first proved in <cit.> (see also [24, 30])
but two modalities and propositional quantification already lead to
undecidability [4, 34].

Many subsequent works have dealt with second-order modal logics,
see  [34, 33, 27, 57], but in the realm of
temporal logics, with propositional quantification (written ) is
introduced in Sistla's PhD thesis [53]
(see also [56]) and non-elementarity of the satisfiability
problem is a consequence of [42].
So, the satisfiability problem is decidable but with high complexity.
By contrast, with propositional
quantification (written ) already admits an undecidable satisfiability problem
by [24] (as captures the modal logic )
but its variant under the tree semantics (written )  admits a non-elementary -complete satisfiability
problem [37, 20] (the complexity class is introduced in [51]).
Having a tree semantics  means that the formulae of
are interpreted on computation trees obtained from the unfolding of
finite (total) Kripke structures, which allows us to regain decidability (see a
similar approach in [63] with a quantified version of the modal logic ).
This is a major observation from [37],
partly motivated by the design of decision procedures for with strategy
contexts [38]. The tree semantics, as far as
satisfiability is concerned, amounts to considering Kripke structures
that are finite-branching trees in which all the maximal branches are infinite.
This is an elegant way to regain decidability.
More generally, decidability in the presence of propositional quantification can be regained when
tree-like models are involved, see  [1, 6, 63, 37],
essentially by taking advantage of Rabin's Theorem [47].

The modal logic with propositional quantification from [24] is
interpreted under the structure semantics, as classified in [37],
but many variants of propositional quantification exist in the literature
(see  [45, 28, 16]
and [14, 15]
in the context of epistemic reasoning). Sometimes, propositional quantification
is syntactically restricted  in the temporal language, but its inclusion is
motivated by a gain of expressive power while preserving the decidability of the
reasoning tasks. By way of example, in [48], an extension
of the modal $\mu$-calculus with partial propositional quantification is
introduced to perform control synthesis, whereas an extension for model-checking
computer systems is also presented in [35].

Interestingly enough, propositional quantification can sometimes have a more hidden
presence. For instance, hybrid  logics with the down-arrow operator $\downarrow_{\anominal}$,
see e.g [2, 3, 41, 62, 31],
can be understood as a form of propositional quantification
since $\downarrow_{\anominal} \aformula$ enforces that the propositional variable
$\anominal$ holds true only at the current world (before evaluating the formula $\aformula$).
In such logics, the companion formula $@_{\anominal} \aformulabis$
expresses that
the unique world satisfying $\anominal$ also satisfied $\aformulabis$; $@_{\anominal}$ is a powerful
operator to navigate in the structure [41] (obviously, it is related
to the universal modality, see  [29]).

Our motivations

As recalled above, the modal logic augmented with propositional quantification
is undecidable [24] and a fortiori, undecidability holds for fragments
of with propositional quantification. Actually, these results hold under
the structure semantics but  (tree semantics) admits -complete
satisfiability and model-checking problems [37]. As
can express that every tree node has exactly one child, -hardness for the
satisfiability problem for , is a corollary of the -hardness of
the satisfiability problem for ,
see  [42, 56, 19].

Given the central position of the modal logic , surprisingly, the complexity
of the satisfiability problem for with propositional quantification under the
tree semantics has never been investigated
(closely related to  –  restricted to $\EX$–  as $\EX$ corresponds to $\Diamond$ in but with total models).

is a

natural and modest fragment of  and we aim at
characterising its

complexity. Furthermore, the model-checking problem for
is -hard even with input Kripke structures having at most two
successor worlds per world and -hardness of holds with linear
structures of length $\omega$, see  [56].
Thus, it is worth understanding what happens with the satisfiability problem
for  when the tree models are

(each node has at most $N$ children) for some fixed $N \geq 2$.

Our contributions

Given $\tQCTL{}$, the extension of with propositional quantification under
the tree semantics  (the models are  finite-branching trees where all the
maximal branches are infinite), let $\tQCTL{\leq N}$ be its variant in which the
models are $N$-bounded, for some $N \geq 2$. We write $\tQCTLEX{}$ and
$\tQCTLEX{,\leq N}$, to denote respectively the restriction to the operator $\EX$,
and $\tQCTLEF{}$ to denote the restriction of $\tQCTL{}$ to $\EF$.

We first present to the reader the toolkit of local nominals and explain the basic ideas behind the hardness results of this paper by proving, for all $N \geq 2$, that the satisfiability problem for $\tQCTLEX{,\leq N}$ is -complete (Section <ref>).

is the class of problems solvable by
exponential-time alternating Turing machines with a polynomial number of alternations.
By using a small model property and
the complexity of model-checking (with upper bound ), -easiness is established.
As far as -hardness is concerned,
the alternating multi-tiling problem introduced in [11]
is instrumental to establish that the model-checking
problem for the interval temporal logic
$B \bar{E}$ with regular expressions is -hard.
As a corollary, we get that the modal logic with propositional quantification
interpreted on finite trees of branching degree bounded by some fixed $N \geq 2$ is also

* More generally and despite the modest scope of $\EX$, the satisfiability problem
for $\tQCTLEX{}$ is shown to be -hard (Theorem <ref>), by
a uniform reduction from $\kNExpTime$-complete tiling problems (uniformity is
with respect to $k$). The corresponding upper bound is known
from [37] and it is worth noting that all the upper bound
results presented in this paper are based on translations into the satisfiability
problem for , sometimes via intermediate decision problems, which eventually
uses Rabin's Theorem [47] in some essential way.
The hardness proof is one of the main results of the paper and amounts first to
showing that one can enforce that a node has a number of children equal to some
tower of exponentials of height $k$ with a formula of size exponential in $k$.
By contrast, checking the satisfiability status of $\CTLStar$ formulae,
requires only to consider tree models with branching degree bounded by the size
of the formula, see  [21, 19].
Once this complex construction enforcing a  very high number of children is
performed, the reduction from the tiling problems can be done with the help of
other properties on the number of children. Hence, even though  under
the structure semantics is undecidable [24] and the variant of
under the tree semantics ($\tQCTL{}$) is decidable by [37],
the problem admits a high complexity despite the local range of $\EX$.
The lower bound for  crucially depends on the availability of very wide trees,
which contrasts with the upper bound for $\tQCTLEX{,\leq N}$ for which trees are $N$-bounded.

* By adapting our proof method, we show that  and
(a variant of  with the unique operator $\EX\EF$) are -hard too
(consult Section <ref>).

* As $\EX$, $\EF$ and $\EX\EF$ correspond to the modality $\Diamond$ in several
modal logics ($\EX\EF$ corresponds to $\Diamond$ in transitive frames), we
are able to establish -completeness for standard modal logics with
propositional quantification when interpreted on tree-like structures (see
Section <ref>). For instance, as the provability logic (after Gödel and Löb) is complete for the class of finite transitive trees,
the accessibility relation is the transitive closure of the child-relation
in the tree, see  [9], we also investigate
the satisfiability problem under the finite tree semantics.
We show that  and  (`$ft$' stands for 'finite tree
semantics') are -complete too. The satisfiability problem for (resp. ) with propositional quantification under the finite (resp. transitive)
tree semantics is shown to be -complete.
Similar results are shown for , and with propositional quantification
but interpreted on appropriate tree-like Kripke structures.
See Section <ref> for the details.

This work is a revised and complete version of our conference paper [7].

To keep the main body of the paper short we delegate all the proofs to the technical appendix.

§ PRELIMINARIES

§.§ Kripke structures and computation trees

Below, we recall standard definitions about Kripke structures.
Let $\AP = \set{\avarprop, \avarpropbis, \anominal, \anominalbis, \ldots}$
be a countably infinite set of propositional variables.
A Kripke structure $\kripkeK$ is a triple $\triple{W}{R}{l}$,
where $W$ is a set of worlds, $R \subseteq W \times W$ is a  transition relation
and $l : W \rightarrow 2^{\AP}$ is a labelling function.
A Kripke structure $\kripkeK$ is total whenever
for all $w \in W$, there is $w' \in W$ such that $\pair{w}{w'} \in R$.
Totality is a standard property for defining classes of models for temporal logics
such as . In the sequel, by a `Kripke structure' we mean a structure according
to the above definition, otherwise when arbitrary (or total, finite, etc.)
Kripke structures need to be considered, we  explicitly specify which classes of
structures we have in mind. For instance, a tree model (resp. finite tree model) $\atreemodel =
\triple{V}{E}{l}$  is an arbitrary Kripke structure where $\pair{V}{E}$ is a (resp. finite) rooted tree.
Standard definitions about trees are omitted herein. Such structures play an important role in the paper,
as the tree semantics involves specific tree models (those obtained as computation trees of
Kripke structures).

Given a Kripke structure $\kripkeK = \triple{W}{R}{l}$ and a world $w \in W$, a finite path
$\apath$ from $w$ is a finite sequence $w_0, \ldots, w_n$ such that
$w_0 = w$ and  for all
$i \in \interval{0}{n-1}$, we have $\pair{w_i}{w_{i+1}} \in R$.
An infinite path from $w$ is an infinite sequence $w_0, \ldots, w_n, \ldots$
such that $w_0 = w$ and  for all $i \geq 0$, we have  $\pair{w_i}{w_{i+1}} \in R$.
With $\Pi_{\kripkeK, w}$ we denote the set of all finite paths starting from a world
$w \in W$ on a Kripke structure $\kripkeK$.

For a Kripke structure $\kripkeK = \triple{W}{R}{l}$ and $w \in W$, the
computation tree unfolding $\kripkeK$ from $w$
is the tree model $\atreemodel_{\kripkeK,w} = \triple{V}{E}{l'}$ such that the following conditions are satisfied:

* $V \egdef \Pi_{\kripkeK, w}$,

* $\apath E \apath'$ $\equivdef$  $\apath = w_0, \ldots, w_n$, $\apath' = \apath, w_{n+1}$ for some $w_{n+1} \in W$ and $\pair{w_n}{w_{n+1}} \in R$,

* for all $\apath = w_0, \ldots, w_n \in V$, we have $l'(\apath) \egdef l(w_n)$.

Thus, when $\kripkeK$ is finite and total, $\atreemodel_{\kripkeK,w}$
is a finite-branching tree model in which all the maximal branches
are infinite and it is also a total Kripke structure. Below,
unless otherwise stated, the tree semantics involves such finite-branching trees with infinite
maximal branches.
In the sequel, tree-like Kripke structures are denoted by $\atreemodel = \triple{V}{E}{l}$
in order to emphasize the tree-like nature of such models.

§.§ The logics  sQCTL, tQCTL,
ftQCTL and gtQCTL

In this section, we define the logics sQCTL, tQCTL,
ftQCTL and gtQCTL
whose formulae are interpreted over different classes of Kripke structures.

The formulae of -like logics are defined from the grammar below
by extending the set of formulae from the computation tree logic
[17] with propositional quantification:

\[
\aformula ::=
\avarprop \mid  \neg \aformula \mid \aformula \wedge \aformula \mid
\EX \aformula \mid \E (\aformula \U \aformula) \mid \A (\aformula \U \aformula)
\mid \exists{\avarprop} \  \aformula,
\]

where $\avarprop \in \AP$. We use the standard abbreviations
$\vee, \rightarrow, \leftrightarrow, \bottom, \top$, as well as other
operators like $\AX$, $\EF$, $\AG$ and $\AF$:

* $\AX(\aformula) \egdef \neg \EX(\neg \aformula)$,

* $\EF(\aformula) \egdef \E (\top \U \aformula)$,
$\AG(\aformula) \egdef \neg \EF(\neg \aformula)$
and $\AF(\aformula) \egdef \A (\top \U \aformula)$.

* The universal quantifier $\forall{\avarprop} \  \aformula$ is used as
$\neg \exists{\avarprop} \  \neg \aformula$.

We denote by $\length{\aformula}$ the length of the formula $\aformula$
measured in a standard way, as the number of symbols used to write
$\aformula$. The modal/temporal depth of a formula $\aformula$,
written $\md{\aformula}$, is the maximal number of
nested temporal operators in $\aformula$.
We stress that  $\md{\aformula}$ is linear in $\length{\aformula}$.

By restricting the set of allowed temporal operators in to the only temporal operator $\EX$ (resp. $\EF$) we obtain the logic  (resp. ).
Note that $\AF$ does not occur in  but $\AX$ (resp. $\AG$) is allowed in  (resp. in ) as it is the dual operator of $\EX$ (resp. $\EF$).
The main object of study in the paper is the logic
under the tree semantics (below, written ). Moreover, we write
to denote the restriction of to the (combined) temporal operator $\EX \EF$, which provides a strict version of the future-time temporal operator $\EF$.
In the rest of the paper, we refer to (or to some of its fragments) to denote
a set of formulae and the notation $\QCTL^{\bullet}$ with a superscript `$\bullet$'
refers to a logic based on (or on some of its fragments) under a specific semantics and for
which the symbol `$\bullet$' is just a reminder of the semantics.

§.§ The logics  sQCTL, tQCTL,
ftQCTL and gtQCTL

The propositional quantifiers can be interpreted in various ways, see  [35, 27, 45, 48, 16].
Below, we provide a satisfaction relation $\models$
defined on total Kripke structures, providing
the so-called structure semantics for (and leading to the logic  ). However,
the version of with formulae interpreted
on  computation trees obtained from the unfoldings of  finite total Kripke structures
(in that case the satisfaction relation
operates on tree-like structures),
is known as $\QCTL$ under the
tree semantics  (written ) and is extensively studied in [37].
To define formally the semantics for propositional quantifiers,
we introduce the notion of $\aset$-equivalence between two Kripke structures, with $\aset$ being a set of propositional variables.
Intuitively, two Kripke structures are $\aset$-equivalent, whenever the only differences (if any) between them are  restricted
to the interpretation of the propositional variables not in $\aset$.
Formally, we say that two Kripke structures $\kripkeK = \triple{W}{R}{l}$ and
$\kripkeK' = \triple{W'}{R'}{l'}$ are $\aset$-equivalent
(written $\kripkeK \approx_{\aset} \kripkeK'$),
iff $W = W'$, $R = R'$ and $l(w) \cap \aset = l'(w) \cap \aset$ for all $w \in W$.

Given a Kripke structure $\kripkeK = \triple{W}{R}{l}$,

a world $w \in W$ and a formula
$\aformula$ in , the satisfaction relation
$\kripkeK, w \models \aformula$  is defined as follows:

\[
\begin{array}{lcl}
\kripkeK, w \models \avarprop &\text{iff}&  \avarprop \in l(w)\\
\kripkeK, w \models \neg \aformula  &\text{iff}& \kripkeK, w \not\models \aformula\\
\kripkeK, w  \models \aformula \wedge \aformulabis &\text{iff}&  \kripkeK, w \models \aformula \; \text{and} \;
\kripkeK, w \models_s \aformulabis \\
\kripkeK, w \models \EX \aformula &\text{iff}&  {\rm there \ is} \  w' \;
\text{such that} \;\pair{w}{w'} \in R \; \text{and} \; \kripkeK, w' \models \aformula \\
\kripkeK, w \models \E (\aformula \U \aformulabis) &\text{iff}& {\rm there \ is \ a \ path}  \  w_0, \ldots, w_n \;
\text{such that} \; w_0 = w, \\
&& \ \kripkeK, w_n \models \aformulabis \; \text{and} \; {\rm for \ all} \ i \in \interval{0}{n-1},  \ {\rm we \ have} \   \kripkeK, w_i \models \aformula \\
\kripkeK, w \models \A (\aformula \U \aformulabis) &\text{iff}&
{\rm for \ all \ infinite \ paths} \ w_0, \ldots, w_n, \ldots \; \text{such that} \; w_0 = w, {\rm there \ is} \\
&&  j \geq 0 \; \text{such that} \; \kripkeK, w_j \models \aformulabis \;  \text{and} \ {\rm for \ all} \ i \in \interval{0}{j-1},  \kripkeK, w_i \models \aformula \\
\kripkeK, w \models \exists{\avarprop} \; \aformula &\text{iff}& {\rm there \ is} \  \kripkeK'
\; {\rm such \ that}  \; \kripkeK \approx_{\AP \setminus \{\avarprop\}} \kripkeK' \;
{\rm and} \; \kripkeK', w \models \aformula
\end{array}
\]

Note that $\kripkeK, w \models \EF \aformula$ iff there is $w' \in R^*(w)$  (where $R^*$ is the reflexive transitive closure of $R$)
such that $\kripkeK, w' \models \aformula$. Stating that there is a unique successor of $w$ satisfying
the propositional variable $\anominal$ can be expressed by the formula
$\EX \ \anominal \wedge \neg (\exists \ \avarprop \
\EX(\anominal \wedge \avarprop) \wedge \EX(\anominal \wedge \neg \avarprop))$, where $\avarprop$ is
distinct from $\anominal$.

The satisfiability problem for the  logic  (under the structure semantics) takes as input a
formula $\aformula$ in and asks whether
there is a finite and total Kripke structure $\kripkeK$ and a world $w$ such that $\kripkeK, w \models \aformula$.

The tree semantics introduced in [37] is obtained by considering as only admissible models the computation trees of
finite and total Kripke structures.
As noted in <cit.>, an equivalent formulation can be provided:
the satisfiability problem for the logic  (under the tree semantics)
takes as input a formula in and asks whether
there is a finite-branching tree model $\atreemodel$ in which all the maximal branches are infinite
such that $\atreemodel, \aroot \models \aformula$
and $\aroot$ is the root of $\atreemodel$.
The equivalence is mainly due to the fact that  can be translated into Monadic Second-Order Logic (MSO)
over tree models with arbitrary finite branching (getting decidability by Rabin's Theorem [47]).
Indeed, as MSO over tree models with arbitrary finite branching is
decidable by  Rabin's Theorem [47], the satisfiability problem for  is decidable
too, by a standard translation internalising the tree semantics for .
As explained in <cit.>, the existence of a tree model implies also the existence of
a regular tree model, that can be precisely originated by a finite Kripke structure.
Hence,  has the finite model property. So, not only can every finite and total Kripke structure be unfolded
as a finite-branching tree in which all the maximal branches are infinite (a direct consequence of the
definition for computation trees) but the existence of a tree model with the above-mentioned properties
and  satisfying  $\aformula$
implies the existence of the computation tree of a finite and total Kripke structure satisfying  $\aformula$. Hence, satisfiability in
the computation tree of  a finite Kripke structure  is equivalent to satisfiability in  a finite-branching tree
in which all the maximal branches are infinite, and in the sequel, we shall operate with the latter definition.

We write $\alogic$ to denote the satisfiability problem for the logic $\alogic$.
The distinction between the tree semantics and the structure semantics is crucial
and affects the computational properties of the satisfiability problems.

$\sQCTL{}$ (under the structure semantics)
is undecidable <cit.>.

$\tQCTL{}$ (under the tree semantics)
is decidable and -complete <cit.>.

(III) The satisfiability problem for  is -hard even if restricted to $\omega$-sequences [42, 56].

All our forthcoming upper bound results are based on translations into the satisfiability problem for
, sometimes via intermediate decision problems, which eventually invokes Rabin's Theorem [47] in some essential way.
This is not  surprising, as considering tree-like models and propositional quantification naturally leads to
invoking the decidability of S$\omega$S [47] or its linear version,  the second-order logic of one successor S1S [12].
Decidability of other logics with propositional quantification is shown that way
in [1, 6, 63].

Apart from -like logics (see  [37] for a wealth of bibliographical references),
other logics with propositional quantification have been shown to be decidable that way.
Besides, in [1]  a fragment of is shown to be decidable by translation into
the weak monadic second-order logic of one  successor WS1S [12], and
a version of Gödel logic $\mathsf{LC}$ with propositional quantification is shown to be decidable by
translation into S1S [12, 6], see also [63] solving partially an open problem from <cit.>.

Let us recapitulate the different versions of quantified we have seen so far.

*  is interpreted over finite and total Kripke structures and
is undecidable, see  [37].

*  is interpreted over finite-branching trees in which all the maximal branches
are infinite and  is -complete, see  [37].

Let us introduce two additional versions that are closely related to modal logics with propositional
quantification on tree-like models introduced in the forthcoming Section <ref>.

*  is interpreted over finite trees,  can be shown to be in by a
logspace reduction into  and its restriction to $\EX$ will be shown to admit
a -hard satisfiability problem.

*  is interpreted over finite-branching trees (maximal branches may be finite),
can be shown to be in by logspace reduction into
and its restriction to $\EX \EF$ will be shown to admit
a -hard satisfiability problem.

To define formally the semantics for propositional quantifiers,
we introduce the notion of $\aset$-equivalence between two Kripke structures, with $\aset$ being a set of propositional variables.
Intuitively, two Kripke structures are $\aset$-equivalent, whenever the only differences (if any) between them are  restricted
to the interpretation of the propositional variables not in $\aset$.
Formally, we say that two Kripke structures $\kripkeK = \triple{W}{R}{l}$ and
$\kripkeK' = \triple{W'}{R'}{l'}$ are $\aset$-equivalent
(written $\kripkeK \approx_{\aset} \kripkeK'$),
iff $W = W'$, $R = R'$ and $l(w) \cap \aset = l'(w) \cap \aset$ for all $w \in W$.

Given a Kripke structure $\kripkeK = \triple{W}{R}{l}$,

a world $w \in W$ and a formula
$\aformula$ in , the satisfaction relation
$\kripkeK, w \models \aformula$  is defined as follows:

\[
\begin{array}{lcl}
\kripkeK, w \models \avarprop &\text{iff}&  \avarprop \in l(w)\\
\kripkeK, w \models \neg \aformula  &\text{iff}& \kripkeK, w \not\models \aformula\\
\kripkeK, w  \models \aformula \wedge \aformulabis &\text{iff}&  \kripkeK, w \models \aformula \; \text{and} \;
\kripkeK, w \models_s \aformulabis \\
\kripkeK, w \models \EX \aformula &\text{iff}&  {\rm there \ is} \  w' \;
\text{such that} \;\pair{w}{w'} \in R \; \text{and} \; \kripkeK, w' \models \aformula \\
\kripkeK, w \models \E (\aformula \U \aformulabis) &\text{iff}& {\rm there \ is \ a \ path}  \  w_0, \ldots, w_n \;
\text{such that} \; w_0 = w, \\
&& \ \kripkeK, w_n \models \aformulabis \; \text{and} \; {\rm for \ all} \ i \in \interval{0}{n-1},  \ {\rm we \ have} \   \kripkeK, w_i \models \aformula \\
\kripkeK, w \models \A (\aformula \U \aformulabis) &\text{iff}&
{\rm for \ all \ infinite \ paths} \ w_0, \ldots, w_n, \ldots \; \text{such that} \; w_0 = w, {\rm there \ is} \\
&&  j \geq 0 \; \text{such that} \; \kripkeK, w_j \models \aformulabis \;  \text{and} \ {\rm for \ all} \ i \in \interval{0}{j-1},  \kripkeK, w_i \models \aformula \\
\kripkeK, w \models \exists{\avarprop} \; \aformula &\text{iff}& {\rm there \ is} \  \kripkeK'
\; {\rm such \ that}  \; \kripkeK \approx_{\AP \setminus \{\avarprop\}} \kripkeK' \;
{\rm and} \; \kripkeK', w \models \aformula
\end{array}
\]

Note that $\kripkeK, w \models \EF \aformula$ iff there is $w' \in R^*(w)$  (where $R^*$ is the reflexive transitive closure of $R$)
such that $\kripkeK, w' \models \aformula$. Stating that there is a unique successor of $w$ satisfying
the propositional variable $\anominal$ can be expressed by the formula
$\EX \ \anominal \wedge \neg (\exists \ \avarprop \
\EX(\anominal \wedge \avarprop) \wedge \EX(\anominal \wedge \neg \avarprop))$, where $\avarprop$ is
distinct from $\anominal$.

The satisfiability problem for the  logic  (under the structure semantics) takes as input a
formula $\aformula$ in and asks whether
there is a finite and total Kripke structure $\kripkeK$ and a world $w$ such that $\kripkeK, w \models \aformula$.

The tree semantics introduced in [37] is obtained by considering as only admissible models the computation trees of
finite and total Kripke structures.
As noted in <cit.>, an equivalent formulation can be provided:
the satisfiability problem for the logic  (under the tree semantics)
takes as input a formula in and asks whether
there is a finite-branching tree model $\atreemodel$ in which all the maximal branches are infinite
such that $\atreemodel, \aroot \models \aformula$
and $\aroot$ is the root of $\atreemodel$.
This is the definition we adopt along the paper.

We write $\alogic$ to denote the satisfiability problem for the logic $\alogic$.
The distinction between the tree semantics and the structure semantics is crucial
and affects the computational properties of the satisfiability problems.

$\sQCTL{}$ (under the structure semantics)
is undecidable <cit.>.

$\tQCTL{}$ (under the tree semantics)
is decidable and -complete <cit.>.

(III) The satisfiability problem for  is -hard even if restricted to $\omega$-sequences [42, 56].

All our forthcoming upper bound results are based on translations into the satisfiability problem for
, sometimes via intermediate decision problems, which eventually invokes Rabin's Theorem [47] in some essential way.
This is not  surprising, as considering tree-like models and propositional quantification naturally leads to
invoking the decidability of S$\omega$S [47] or its linear version,  the second-order logic of one successor S1S [12].

Let us recapitulate the different versions of quantified we have seen so far.

*  is interpreted over finite and total Kripke structures and
is undecidable, see  [37].

*  is interpreted over finite-branching trees in which all the maximal branches
are infinite and  is -complete, see  [37].

Let us introduce two additional versions that are closely related to modal logics with propositional
quantification on tree-like models introduced in the forthcoming Section <ref>.

*  is interpreted over finite trees,  can be shown to be in by a
logspace reduction into  and its restriction to $\EX$ will be shown to admit
a -hard satisfiability problem (see Section <ref>).

*  is interpreted over finite-branching trees (maximal branches may be finite),
can be shown to be in by logspace reduction into
and its restriction to $\EX \EF$ will be shown to admit
a -hard satisfiability problem (see Section <ref>).

As a side remark, the equivalence between the two formulations of ,
is mainly due to the fact that  can be translated into Monadic Second-Order Logic (MSO)
over tree models with arbitrary finite branching (getting decidability by Rabin's Theorem [47]).
Indeed, as MSO over tree models with arbitrary finite branching is
decidable by  Rabin's Theorem [47], the satisfiability problem for  is decidable
too, by a standard translation internalising the tree semantics for .
As explained in <cit.>, the existence of a tree model implies also the existence of
a regular tree model, that can be precisely originated by a finite Kripke structure.
Hence,  has the finite model property. So, not only can every finite and total Kripke structure be unfolded
as a finite-branching tree in which all the maximal branches are infinite (a direct consequence of the
definition for computation trees) but the existence of a tree model with the above-mentioned properties
and  satisfying  $\aformula$
implies the existence of the computation tree of a finite and total Kripke structure satisfying  $\aformula$. Hence, satisfiability in
the computation tree of  a finite Kripke structure  is equivalent to satisfiability in  a finite-branching tree
in which all the maximal branches are infinite, and in the sequel, we shall operate with the latter definition.

Apart from -like logics (see  [37] for a wealth of bibliographical references),
other logics with propositional quantification have been shown to be decidable
by translation into S$\omega$S, see e.g. [1, 6, 63].
Besides, in [1]  a fragment of with propositional quantification
is shown to be decidable by translation into
the weak monadic second-order logic of one  successor WS1S [12], and
a version of Gödel logic $\mathsf{LC}$ with propositional quantification is shown to be decidable by
translation into S1S [12, 6], see also [63] solving partially an open problem from <cit.>.

§.§ Complexity classes and tiling problems

In this section, we introduce tiling problems that are mainly used in
Sections <ref> and <ref>.

Let $\tow : \Nat \times \Nat \to \Nat$ be a tetration function defined for integers $n,k \geq 0$,
inductively as $\tow(0,n) {=} n$ and $\tow(k{+}1,n) {=} 2^{\tow(k,n)}$.
Intuitively the function $\tow$ defines the tower of exponentials of
height $k$, we have $\tow(1, n) = 2^n$, $\tow(2, n) = 2^{2^n}$,
and so on.
By $\kNExpTime$ we denote the class of all problems decidable with a
nondeterministic Turing machines of working time in $\BigOh{\tow(k,p(n))}$ for some polynomial $p(\cdot)$,
on each input of length $n$. We define $\tower$ as the class of all problems
of time complexity bounded by a tower of exponentials, whose height is an
elementary function [51]. Thus, to show $\tower$-hardness (using elementary reductions [51]),
it is sufficient to prove $\kNExpTime$-hardness for all $k$ using uniform
reductions <cit.>. It is worth recalling that -hardness
is defined with the class of elementary reductions (i.e. those with time-complexity
bounded by a tower of exponentials of fixed height) [51]. Building a reduction from
instances of $\kNExpTime$-hard problems with time-complexity $\amap(n,k)$ where the size $n$ of the input
leads to an elementary reduction when  $\amap(n,k)$ itself is elementary in $n$ and $k$.
This is  what we mean by a uniform reduction in $k$ to establish -hardness.

For proving hardness results, we make extensive use of tiling problems, see  [61].

The tiling problem $\mathtt{Tiling}_k$ takes as inputs a triple $\triple{\cT}{\cH}{\cV}$
and $c \in \cT^{n}$ for some $n \geq 1$ such that $\cT$ is a finite set of tile types,
$\cH \subseteq \cT \times \cT$ (resp. $\cV \subseteq \cT \times \cT$)
represents the  horizontal (resp. vertical)  matching relation,
and  $c = t_0,t_1, \ldots, t_{n-1} \in \cT^{n}$

is the initial condition.
A solution for the instance $\triple{\cT}{\cH}{\cV}, c$ is a mapping
$\atiling : \interval{0}{\tow(k,n)-1} \times \interval{0}{\tow(k,n)-1} \to \cT$
such that:

0 cm

(init)tiling:init For all $i \in \interval{0}{n-1}$, $\atiling(0,i) = t_i$.

(hori)tiling:hori  For all $i, j \in \interval{0}{\tow(k,n)-1}$,
$i < \tow(k,n)-1$ implies $(\atiling(i,j), \atiling(i {+} 1, j)) \in \cH$.

(verti)tiling:verti For all $i, j \in \interval{0}{\tow(k,n)-1}$,
$j < \tow(k,n)-1$ implies $(\atiling(i,j),  \atiling(i, j {+} 1)) \in \cV$.

A mapping $\atiling$ satisfying <ref> and <ref> is called a tiling.

A $k$-tiling problem $\cP$ is a tuple $(\cT, \cH, \cV)$,
where $\cT$ is a finite set of tile types and
$\cH, \cV \subseteq \cT \times \cT$ represent the horizontal and
vertical matching conditions. Let $\cP$ be a tiling problem and let
$c = t_0,t_1, \ldots, t_{n-1} \in \cT^{n}$ be an initial condition.
A mapping $\tau : \{ 0,1, \ldots, \tow(k,n)-1 \} \times
\{ 0,1, \ldots, \tow(k,n)-1 \} \rightarrow \cT$ is a solution for
$\cP$ and $c$ if and only if, for all $i,j$ s.t., $i+1,j+1 \leq \tow(k,n)-1$,
the following holds $(\tau(i,j), \tau(i {+} 1, j)) \in \cH, (\tau(i,j),
\tau(i, j {+} 1)) \in \cV$ and $\tau(0,i) = t_i$ for all $i < n$.

The problem of checking if an instance of $\mathtt{Tiling}_k$
has a solution (note that $k$ does not appear in the instance and it governs
the size of the grid) is  $\kNExpTime$-complete [61].

Given $N \geq 2$,  let us consider the satisfiability problem for , ≤N in which the structures
are tree models where all the maximal branches are infinite but each node has at most $N$ children (and at least one child).
To characterise the complexity of , ≤N, we consider the
complexity class that
consists of all problems decidable by an alternating Turing machine (ATM) [18] working in
exponential-time and using only polynomially many alternations [11, 43]. We stress here that
allowing an unbounded number of alternations would give us the class $\ExpSpace$, and classes similar to have been considered in [10], typically  STA($\mathfrak{f}(n)$,$\mathfrak{g}(n)$,$\mathfrak{h}(n)$),
where $\mathfrak{f}(n)$ refers to the restriction on the Space,
$\mathfrak{g}(n)$ refers to the restriction on the Time,
and $\mathfrak{h}(n)$ refers to the restriction on the number of Alternations.
Consequently,  is the union of classes STA($\cdot$,$2^{\mathfrak{g}(n)}$,$\mathfrak{h}(n)$)
with polynomials $\mathfrak{g}(n)$, $\mathfrak{h}(n)$.
The complexity of several logical problems has been captured by the class , see  [26, 16, 11].

For proving -hardness, we use an elegant modification of
$\mathtt{Tiling}_1$, introduced in [11, 43].
The extension amounts to considering a stack of $n$ tilings,
with a matching relation between two consecutive tile types on
the same position of the grid, and quantifications over the tile types on
the first row (initial conditions). Details follow below.

The  alternating multi-tiling problem $\cPmulti$ takes as
inputs an even number $n$ (in unary), $\triple{\cT}{\cH}{\cV}$ (as for defining $\mathtt{Tiling}_1$),
$\cTzero \subseteq \cT$,
$\cTacc \subseteq \cT$ and  $\cTmulti \subseteq \cT \times \cT$.
Given an initial condition $c= (w_1, \ldots, w_n) \in (\cTzero^{2^n})^{n}$,
a solution for $c$ is a  multi-tiling $(\atiling_1, \ldots, \atiling_n)$ on the grid $\interval{0}{2^n-1} \times \interval{0}{2^n-1}$ such that:

0 cm

(m-init)amtp:m-init For all $\alpha \in \interval{1}{n}$, for all $j \in \interval{0}{2^n-1}$, $\atiling_{\alpha}(0,j) = w_{\alpha}(j)$
(the first row of $\atiling_{\alpha}$ is $w_{\alpha}$).

(m-tiling)amtp:m-tiling For  $\alpha \in \interval{1}{n}$, $\atiling_{\alpha}$ satisfies  <ref> and <ref>.

(m-multi)amtp:m-multi  For  $\alpha \in \interval{1}{n-1}$,
for all $i,j \in  \interval{0}{2^n-1}$, $\pair{\atiling_{\alpha}(i,j)}{\atiling_{\alpha+1}(i,j)} \in \cTmulti$.

(m-accept)amtp:m-accept For some $j \in \interval{0}{2^n-1}$, $\atiling_{n}(2^n-1,j) \in \cTacc$.

An instance $\mathcal{I}$ for $\cPmulti$ made of
$n$, $\triple{\cT}{\cH}{\cV}$, $\cTzero,\cTacc \subseteq \cT$,
$\cTmulti \subseteq \cT \times \cT$ is positive iff
for all $w_1 \in \cTzero^{2^n}$, there is $w_2 \in \cTzero^{2^n}$ such that $\ldots$
for all $w_{n-1} \in \cTzero^{2^n}$, there is $w_{n} \in \cTzero^{2^n}$ such that
there is a solution  $(\atiling_1, \ldots, \atiling_n)$
for $(w_1, \ldots, w_n)$.
Note that this sequence involves $n{-}1$ quantifier alternations.

The alternating multi-tiling problem is shown to be -complete in [11, 43].

§ WHAT HAPPENS WHEN TREES ARE BOUNDED?

In this section, we study the satisfiability problem for ,≤N with $N \geq 1$,
over trees, where the degree of each node is bounded by a fixed
natural number $N \geq 1$.

As we have already mentioned in the introduction, the goal of this section is two-fold.
First, we would like to make the reader familiar with our proof techniques applied to a simplified scenario.
Second, our results show that to get $\TOWER$-hardness of  we must focus on trees of arbitrarily large branching.

§ -HARDNESS OF THE SATISFIABILITY PROBLEM TQCTLEX

We are back to the (general) satisfiability problem for , with no further restrictions on the number of children per node.

§.§ Overview of the method

In order to show -hardness, we shall reduce the $k$--complete tiling problem $\mathtt{Tiling}_k$
introduced in Section <ref> to  and this should be
done in a uniform way so that -hardness can be concluded (see the discussion in <cit.> and
in Section <ref>).
Hence, we need to encode concisely a grid $\tow(k,n) \times \tow(k,n)$ and to do so, the main task consists in enforcing
that a node has $\tow(k,n)$ children, using a formula of elementary size in $k+n$ (bounded by a tower of exponentials of fixed height). Actually, our method produces
a formula of exponential size in $k+n$. Of course, this is not  the end of the story as we need to encode
the grid $\tow(k,n) \times \tow(k,n)$ and to express on it constraints about the tiling $\atiling$.
First, let us explain how to enforce that a node has exactly $\tow(k,n)$ children,
by partly taking  advantage of the proof technique of local nominals (see Section <ref>).

We recall that $\tow(1,n) {=} 2^n$ and $\tow(k+1,n) {=} 2^{\tow(k,n)}$ for $k > 0$.
For the forthcoming subsections, we assume that $n$ is fixed.
Below, we classify the nodes of a tree model by their type (a value in $\Nat$)
such that any node is of type 0, and if a node is of type $k > 0$, then it has exactly
$\tow(k,n)$ children and all the children are of type $k-1$. To be more precise, a node may have
two types (as one of them is always zero).
So, a node of type 1 has exactly $2^n$ children,  a node of type 2 has exactly $2^{2^n}$ children, etc.
Therefore if a node is of type $k>0$, then the value $k$ is unique.
Additional conditions apply for being of type $k > 0$ but we can already notice
that a node $\anode$ of type $k$ implicitly defines a balanced subtree of depth $k$ with root $\anode$.

[scale=.73,line cap=round]

(1,0) node[minirond, jaune] (AA) ;
(-2,-2) node[minirond, jaune] (AB1) ;
(-1,-2) node[minirond, bleu] (AB2) ;
(0,-2) node[minirond, vert] (AB3) ;
(0.75,-2) node[text=black] (AC1) ;
(1.5,-2) node[text=black] (AC2) $\ldots$;
(2.25,-2) node[text=black] (AC3) ;
(3,-2) node[minirond, rouge] (AB4) ;
(4,-2) node[minirond, vert] (AB5) ;
(5,-2) node[minirond, bleu] (AB6) ;

(-2,-2.5) node[text=black] (AD1) 0;
(-1,-2.5) node[text=black] (AD2) 1;
(0,-2.5) node[text=black] (AD3) 2;
(3,-2.5) node[text=black] (AD4) ;
(4,-2.5) node[text=black] (AD5) ;
(5.5,-2.5) node[text=black] (AD6) $\tow(k{-}1,n){-}1$;

(-2.7,-1.52) node[text=black] (AE1) type $k{-}1$;
(5.5,-1.52) node[text=black] (AE2) type $k{-}1$;

ı/ȷin AA/AB1, AA/AB2, AA/AB3, AA/AB4, AA/AB5, AA/AB6, AA/AC1, AA/AC3
[-latex'] (ı) – (ȷ);

(10+1,0) node[minirond, jaune] (BA) ;
(10+-2,-2) node[minirond, jaune] (BB1) ;
(10+-1,-2) node[minirond, bleu] (BB2) ;
(10+0,-2) node[minirond, vert] (BB3) ;
(10+0.75,-2) node[text=black] (BC1) ;
(10+1.5,-2) node[text=black] (BC2) $\ldots$;
(10+2.25,-2) node[text=black] (BC3) ;
(10+3,-2) node[minirond, rouge] (BB4) ;
(10+4,-2) node[minirond, vert] (BB5) ;
(10+5,-2) node[minirond, bleu] (BB6) ;

(10+-2,-2.5) node[text=black] (BD1) 0;
(10+-1,-2.5) node[text=black] (BD2) 1;
(10+0,-2.5) node[text=black] (BD3) 2;
(10+3,-2.5) node[text=black] (BD4) ;
(10+4,-2.5) node[text=black] (BD5) ;
(10+5.5,-2.5) node[text=black] (BD6) $\tow(k{-}1,n){-}1$;

(10+-2.25,-1.4) node[text=black] (BE1) type $k{-}1$;
(10+5,-1.52) node[text=black] (BE2) type $k{-}1$;

ı/ȷin BA/BB1, BA/BB2, BA/BB3, BA/BB4, BA/BB5, BA/BB6, BA/BC1, BA/BC3
[-latex'] (ı) – (ȷ);

(6.5,2) node[minirond, jaune] (C) ;
(6.5, 2.5) node[text=black] (AE2) type $k{+}1$;

(3,0) node[text=black] (X) ;

(4.75,0) node[text=black] (XX) $\ldots$;

(6,0) node[text=black] (Y) ;

(7.5,0) node[text=black] (YY) $\ldots$;

(9,0) node[text=black] (Z) ;

ı/ȷin C/AA, C/BA, C/X, C/Y, C/Z [-latex'] (ı) – (ȷ);

[use as bounding box]  (0,0);

In order to enforce that a node is of type $k  \geq 1$ (this is a trivial property for $k=0$),
and therefore has exactly $\tow(k,n)$ children,
with each node $\anode$ of type $k \geq 0$ is associated a number in $\interval{0}{\tow(k+1,n)-1}$.
Such a number is written $\semnumber{\atreemodel}{\anode}$.
The subscript `$\atreemodel$' may be omitted when the context is clear.
Similarly, when
$\atreemodel, \anode_0 \models \bindd{\anominal_1}{1} \wedge
\bigwedge_{i \in \interval{2}{d}}
\att{\anominal_1}{1} \att{\anominal_2}{1} \cdots \att{\anominal_{i-1}}{1} \bindd{\anominal_i}{1}$
the nodes  $\anode_1, \ldots, \anode_d$ are associated with $\anominal_1, \ldots \anominal_d$,
we write $\semnumber{\atreemodel}{\anominal_i}$ instead of $\semnumber{\atreemodel}{\anode_i}$
for all $i \in \interval{1}{d}$
(in general, by a slight abuse of notation, we may refer to a node
by its local nominal when it exists).

When the type of the node $\anode$ is zero, its number is defined as the unique $m$
such that the number represented by the truth values of
$\avarprop_{n-1}, \avarprop_{n-2}, \ldots \avarprop_0$ is equal to $m$.
As usual, the propositional variable $\avarprop_i$ is responsible for the $i$th bit of
the number $m$ and by convention, the least significant bit is encoded by the truth value of $\avarprop_0$.
We illustrate the encoding below:

[line cap=round]

(1,0.25) node[text=black] (XXX) type $1$;
(1,0) node[minirond, jaune] (A) ;
(-2,-2) node[minirond, jaune] (B1) ;
(-1,-2) node[minirond, bleu] (B2) ;
(0,-2) node[minirond, vert] (B3) ;
(0.75,-2) node[text=black] (C1) ;
(1.5,-2) node[text=black] (C2) $\ldots$;
(2.25,-2) node[text=black] (C3) ;
(3,-2) node[minirond, rouge] (B4) ;
(4,-2) node[minirond, vert] (B5) ;
(5,-2) node[minirond, bleu] (B6) ;

(-2,-2.25) node[text=black] (D1) 0;
(-1,-2.25) node[text=black] (D2) 1;
(0,-2.25) node[text=black] (D3) 2;
(3,-2.25) node[text=black] (D4) ;
(4,-2.25) node[text=black] (D5) ;
(5.5,-2.25) node[text=black] (D6) $2^n{-}1$;

(-2.8,-1.7) node[text=black] (E1) $\neg p_{n-1} \wedge \ldots \wedge \neg p_{0}$;
(5.85,-1.7) node[text=black] (E2) $p_{n-1} \wedge \ldots \wedge p_0$;

ı/ȷin A/B1, A/B2, A/B3, A/B4, A/B5, A/B6, A/C1,  A/C3
[-latex'] (ı) – (ȷ);

[use as bounding box]  (0,0);

Otherwise, when the type of $\anode$ is equal to some $k > 0$, its number is
represented by the binary encoding of
the propositional variable $\val{k-1}$ on its children assuming that there are $\tow(k,n)$ children
whose respective (bit) numbers span all over $\interval{0}{\tow(k,n)-1}$ and therefore all the children are implicitly ordered.
This principle makes sense conceptually but it remains to express it in , similarly
to the -hardness proof in [46] for the fluted fragment in which counters
with high values have to be enforced within a restricted language (see also [55]).
That is why, in Table <ref>,
we present a list of formulae to be defined.
All of them are interpreted on a node $\anode_0$ of type $k \geq 0$, $1 \leq d \leq k$.

Formulae to be defined     Intuitive meaning
$\phitype{k}$     $\anode_0$ is of type $k$
$\phifirst{k}$      $\semnumber{}{\anode_0} = 0$
$\philast{k}$      $\semnumber{}{\anode_0} = \tow(k+1,n)-1$
$\phiunique{k}$      $\forall \anode, \anode' \ ((\anode_0 E \anode) \ \& \  (\anode_0 E \anode') \ \& \
\anode \neq \anode') \ \rightarrow $

$\semnumber{}{\anode} \neq \semnumber{}{\anode'}$
$\phipopulate{k}$       $\forall \anode \ ((\anode_0 E \anode) \ \& \ \semnumber{}{\anode} < \tow(k,n)-1)
\ \rightarrow$

$\exists \ \anode'  \  (\anode_0 E \anode') \ \wedge \ \semnumber{}{\anode'} = \semnumber{}{\anode} + 1$
$\semnumber{}{\anode_d} = \semnumber{}{\anode_d'}$
$\semnumber{}{\anode_d'} = 1 + \semnumber{}{\anode_d}$
$\semnumber{}{\anode_d} < \semnumber{}{\anode_d'}$

Family of auxiliary formulae.

In the last 3 lines of the table, the subscript
`$k$' below `$=$' and `$<$' allows us
to remember that the formula is evaluated at a node of type $k$; as $\bar{\anominal}$ and  $\bar{\anominalbis}$
are of length $d$, the number comparison is done on nodes of type $k-d$ and the numbers can take
values in $\interval{0}{\tow(k-d+1,n)-1}$.  Though most of the intuitive meanings are straightforward,
let us notice that $\phiunique{k}$ is  intended to express that two distinct children of $\anode_0$ have
distinct numbers. Similarly, $\phipopulate{k}$ is intended to express that
if a child of $\anode_0$ has a number $n$ strictly less than
$\tow(k,n)-1$, then $\anode_0$ has also another child with number equal to $n+1$
(`compl' in $\phipopulate{k}$ stands for `complete').

In what follows we will also employ $\widehat{\bar{\anominal},\bar{\anominalbis}}$ to denote the formula

\[
\bindd{\anominal_1}{1} \wedge \bindd{\anominalbis_1}{1} \wedge \bigwedge_{i \in \interval{2}{d}}
(\att{\anominal_1}{1} \att{\anominal_2}{1} \cdots \att{\anominal_{i-1}}{1} \bindd{\anominal_i}{1}
\wedge
\att{\anominalbis_1}{1} \att{\anominalbis_2}{1} \cdots \att{\anominalbis_{i-1}}{1} \bindd{\anominalbis_i}{1}).
\]

Assuming that the nodes $\anode_1, \ldots, \anode_d$ are associated with $\bar{\anominal} = \anominal_1, \ldots, \anominal_d$
(resp.  $\anode_1', \ldots, \anode_d'$ are associated with $\bar{\anominalbis} = \anominalbis_1, \ldots, \anominalbis_d$),
$\anode_0, \anode_1, \ldots, \anode_d$ and $\anode_0, \anode_1', \ldots, \anode_d'$ can be understood
as two branches rooted at $\anode_0$ ending at the node $\anode_d$ and at the node $\anode_d'$ respectively.
The formula $\widehat{\bar{\anominal},\bar{\anominalbis}}$ uses subformulae introduced in Section <ref>
and the wide hat symbol in $\widehat{\bar{\anominal},\bar{\anominalbis}}$ above $\bar{\anominal}$ and  $\bar{\anominalbis}$
is a graphical reminder of these two branches.
By contrast, the specific  formula $\widehat{\bar{\anominal},\bar{\anominal}}$ states the existence of a single branch
with nodes $\anode_0, \ldots, \anode_d$.

In order to define $\phitype{k}$ ($k \geq 1$), we specify that every child is of type $k-1$,
there is a child with number equal to zero, and if a child has number $m < \tow(k,n)-1$, then
there is a child with number equal to $m+1$.
Moreover, two distinct children have distinct numbers in $\interval{0}{\tow(k,n)-1}$.
Satisfying these conditions  guarantees that
the number for the children span all over $\interval{0}{\tow(k,n)-1}$.
The formula $\phitype{k}$ (for $k \geq 1$) is defined as

\[ \phitype{k} \deff  \AX(\phitype{k-1}) \wedge \EX(\phifirst{k-1}) \wedge \phiunique{k} \wedge \phipopulate{k}. \]

Note that the above formula is intended to be built
over the propositional variables $\avarprop_0, \ldots, \avarprop_{n-1}, \val{}$ (only).

Let us first explain how we proceed to define all the mentioned formulae.
For successive values $N \in \Nat$, we define inductively the formulae:

* $\phitype{N}$, $\phifirst{N}$ and $\philast{N}$,

* $\eqk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$,

* $\gk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$,

* $\succk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$

for all $k-d = N-1$.
For $N = 0$, only the formulae  $\phitype{0}$, $\phifirst{0}$ and $\philast{0}$ make sense.
The case  $N = 1$ is not yet an instance of the general case.
We first treat the cases for $N \in \set{0,1}$ and then we proceed with the general case $N \geq 2$.

§.§ Formulae for types zero and one

When $k= 0$ (thus $k = N = 0$),  only the intended properties for the formulae
$\phitype{0}$, $\phifirst{0}$ and $\philast{0}$ are meaningful.
Let us define them, in the simplest way.

* $\phitype{0} \egdef \top$

* $\phifirst{0} \egdef \neg \avarprop_{n-1} \wedge \cdots \wedge \neg \avarprop_{0}$ and

* $\philast{0} \egdef \avarprop_{n-1} \wedge \cdots \wedge \avarprop_{0}$.

\phitype{0} \egdef \top \ \ \ \ \ \
\phifirst{0} \egdef \neg \avarprop_{n-1} \wedge \cdots \wedge \neg \avarprop_{0} \ \ \ \ \ \
\philast{0} \egdef \avarprop_{n-1} \wedge \cdots \wedge \avarprop_{0}.

It can be rapidly checked that $\atreemodel, \anode \models \phitype{0}$ iff $\anode$ is of type 0.
Moreover, assuming that $\anode$ is understood as a node of type $0$, we have  $\atreemodel, \anode \models \phifirst{0}$ iff $\semnumber{\atreemodel}{\anode} = 0$ and
$\atreemodel, \anode \models \philast{0}$ iff  $\semnumber{\atreemodel}{\anode} = \tow(1,n)-1 = 2^n-1$.

We next focus on the case when $N = 1$ and we define the formulae
$\phitype{k}$, $\phifirst{k}$ and $\philast{k}$
with $k {=} 1$ (when $k {=} N {=} 1$) as well as $\gk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$
and $\succk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$
with $k-d = 0$ (that is when $k{-}d = N{-}1$  with $N{=}1$).
We stress that $k$ and $d$ can be arbitrarily large as long as $k = d$.

To start with the formula $\eqk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$,
it can be easily defined in terms of $\gk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$ as:

\[\neg \left( \gk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d} \right)  \wedge \neg \left( \gk{k}{\anominalbis_1, \ldots, \anominalbis_d}{\anominal_1, \ldots, \anominal_d} \right). \]

Second, we turn our attention to the formula  $\phitype{1}$.
It states that there is a child with number equal to zero, if a child has number $m < 2^n-1$, then there is a child with number equal to $m+1$, all the children are of type $0$,
and  two distinct children have distinct numbers in $\interval{0}{2^n-1}$.
Remember that the number of each child (of type 0) is computed from the propositional variables in $\set{\avarprop_{n-1}, \ldots, \avarprop_0}$.
The arithmetical reasoning between children, leading to the fact that there are exactly $2^n$ children whose numbers
span all over $\interval{0}{2^n-1}$ takes advantage of standard arithmetical properties on numbers encoded by $n$ bits.
Here is the formula $\phitype{1}$:

\[ \phitype{1} \egdef \AX(\phitype{0}) \wedge \EX(\phifirst{0}) \wedge \phiunique{1} \wedge \phipopulate{1}. \]

It remains to specify what exactly the formulae $\phiunique{1}$ and $\phipopulate{1}$ are.
In order to define $\phiunique{1}$, responsible for enforcing the uniqueness among the children's numbering,
we simply state that there are no two distinct children (of type $0$) having the same number:

\[\forall{\anominal,\anominalbis} \ \distinctbindd{\anominal,\anominalbis}{1} \rightarrow
\neg (\eqk{1}{\anominal}{\anominalbis}).\]

Note that the formula $\distinctbindd{\anominal,\anominalbis}{1}$ guarantees that we pick two distinct children
and the nominals $\anominal$ and $\anominalbis$ allow us to access them (and check the values of the
propositional variables in $\set{\avarprop_{n-1}, \ldots, \avarprop_0}$). Consult Lemma <ref> for the correctness.

The formula $\phipopulate{1}$ below states that for each child $\anode$ (of type $0$) that is not the last one (does not have the highest possible number among all other nodes),
there is also a child $\anode'$ (also of type $0$)  such that $\semnumber{\atreemodel}{\anode'} = \semnumber{\atreemodel}{\anode} +1$.
Here is the formula $\phipopulate{1}$:

\[
\forall{\anominal} \ (\bindd{\anominal}{1} \wedge \att{\anominal}{1}(\neg \philast{0})) \rightarrow
\exists{\anominalbis} \ \bindd{\anominalbis}{1} \wedge \succk{1}{\anominal}{\anominalbis}. \]

Finally, it remains to define the formulae $\eqk{1}{\anominal}{\anominalbis}$ and $\succk{1}{\anominal}{\anominalbis}$
used respectively in $\phiunique{1}$ and in $\phipopulate{1}$.
Below, we treat the more general situation with $k = d$ ($k$ is not necessarily equal to 1), and
$\eqk{1}{\anominal}{\anominalbis}$ and $\succk{1}{\anominal}{\anominalbis}$ are  specific instances with $k=d=1$.
Let assume that $\bar{\anominal} = \anominal_1, \ldots, \anominal_k$ and $\bar{\anominalbis} =
\anominalbis_1, \ldots, \anominalbis_k$ (thus $d = k$).
The forthcoming definitions are standard and rely on elementary operations on binary encoding of natural numbers  with $n$ bits
(again, the least significant
bit is represented by the truth value of $\avarprop_0$):

0 cm

* $\succk{k}{\anominal_1, \ldots, \anominal_k}{\anominalbis_1, \ldots, \anominalbis_k}$
is defined as

\[
\bigvee_{i=0}^{n-1}
\left(
\underbrace{
\att{\bar{\anominal}}{}
\left(
(\neg \avarprop_i \wedge \bigwedge_{j=0}^{i-1} \avarprop_j)
\right)
}_{\text{look for the first zero bit}}
\wedge
\underbrace{
\att{\bar{\anominalbis}}{}
\left(
\bigwedge_{j=0}^{i-1} \neg \avarprop_j \wedge \avarprop_i
\right)
}_{\text{reset previous bits, set } \avarprop_i}
\wedge
\underbrace{
\left(
\bigwedge_{j=i+1}^{n-1}
\att{\bar{\anominal}}{} \avarprop_j \Iff  \att{\bar{\anominalbis}}{}
\avarprop_j
\right)
}_{\text{rewrite other bits}}
\right)
\]

* $\gk{k}{\anominal_1, \ldots, \anominal_k}{\anominalbis_1, \ldots, \anominalbis_k}$
is defined as

\[
\bigvee_{i=0}^{n-1}
\left(
\underbrace{\att{\bar{\anominalbis}}{} \avarprop_i \wedge
\att{\bar{\anominal}}{} \neg \avarprop_i \wedge}_{\text{find the first bit that differs}}
\underbrace{
\att{\bar{\anominal}}{} \avarprop_j \Iff \att{\bar{\anominalbis}}{} \avarprop_j)
}_{\text{equality of more significant bits}}
\right)
\]

For the sake of completeness, we define $\phifirst{1} \egdef \AX (\neg \val{0})$ and $\philast{1} \egdef \AX (\val{0})$.

The lemma below states that we have properly proceeded for the
binary encoding of numbers with the variables in $\avarprop_{n-1}, \ldots,
\avarprop_{0}$ (and Lemmas <ref>–<ref> need to be used).

Let $\atreemodel$ be a tree model and $\anode$ be one of its nodes such that $\anode$ satisfies $\widehat{\bar{\anominal},\bar{\anominalbis}}$ ($\bar{\anominal}$
and $\bar{\anominalbis}$ are both of length $k$) and, $\anode_k$ and $\anode_k'$ are  understood as nodes of type $0$.

(I) $\atreemodel, \anode \models \succk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ iff $\semnumber{\atreemodel}{\anode_k'} = 1 + \semnumber{\atreemodel}{\anode_k}$.

(II) $\atreemodel, \anode \models \gk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ iff $\semnumber{\atreemodel}{\anode_k} < \semnumber{\atreemodel}{\anode_k'}$.

(III) $\atreemodel, \anode \models \eqk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ iff $\semnumber{\atreemodel}{\anode_k} = \semnumber{\atreemodel}{\anode_k'}$.

By careful inspection of the presented formulae, Appendix <ref>.

We conclude by presenting the main lemma that gathers all established formulae.

Let $\atreemodel$ be a tree model and let $\anode$ be any of its nodes.
The following hold:

(I) $\atreemodel, \anode \models \phitype{1}$ iff $\anode$ is of type $1$,

(II) Assuming $\anode$ satisfies $\phitype{1}$, we have $\atreemodel, \anode \models \phifirst{1}$ iff $\semnumber{\atreemodel}{\anode} = 0$.

(III) Assuming $\anode$ satisfies $\phitype{1}$, we have $\atreemodel, \anode \models \philast{1}$ iff $\semnumber{\atreemodel}{\anode} = \tow(2,n)-1$.

The properties (II)–(III) follow immediately from the way we encode numbers.
Check Appendix <ref> for a more detailed explanation.

§.§ Formulae with arbitrary N >= 2

Let us consider the arbitrary case $N \geq 2$.
Below, we define the formulae  $\phitype{N}$, $\phifirst{N}$ and $\philast{N}$
as well as $\gk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$,
and $\succk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$ with $k{-}d = N{-}1$.
We also consider the formula $\eqk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$, that is defined as follows:

\[\neg (\gk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}) \wedge
\neg (\gk{k}{\anominalbis_1, \ldots, \anominalbis_d}{\anominal_1, \ldots, \anominal_d}).\]

We assume that for all $k < N$, the formulae $\phitype{k}$, $\philast{k}$ and $\phifirst{k}$
are already defined and for  $k-d \leq N-2$,
the formulae $\gk{k}{\bar{\anominal}}{\bar{\anominalbis}}$,  $\eqk{k}{\bar{\anominal}}{\bar{\anominalbis}}$
and  $\succk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ are already defined too ($\bar{\anominal}$ and
$\bar{\anominalbis}$ are of length $d$). This can be understood as an implicit induction hypothesis
when proving the correctness of the formulae built for $N$.

As for the case $N=1$, the formula $\phitype{N}$ follows the general schema:
it states that there is a child with number equal to zero,
if a child has number $m < \tow(N,n)-1$, then there is a child with number equal to $m+1$,
and two distinct children have distinct numbers in $\interval{0}{\tow(N,n)-1}$.
Of course, all the children are enforced to be of type $N-1$.
We present the claimed formula $\phitype{N}$ below.

\[
\phitype{N} \deff \AX(\phitype{N-1}) \wedge
\EX(\phifirst{N-1}) \wedge \phiunique{N} \wedge \phipopulate{N}.
\]

Again, it remains to specify what $\phiunique{N}$ and $\phipopulate{N}$ are.
In order to define $\phiunique{N}$, we simply  state that there are no
two distinct children (of type $N-1$) with the same number:

\[
\phiunique{N} \deff
\forall{\anominal,\anominalbis} \ \distinctbindd{\anominal,\anominalbis}{1} \rightarrow \neg  (\eqk{N}{\anominal}{\anominalbis}).
\]

Again, the formula $\distinctbindd{\anominal,\anominalbis}{1}$ allows us to select two distinct children (of type $N-1$).
The formula $\phipopulate{N}$ below states that for each  child $\anode$ (of type $N-1$) that is not the last one,
there is also a child $\anode'$ (of type $N-1$ too) such that $\semnumber{\atreemodel}{\anode'} = \semnumber{\atreemodel}{\anode} +1$.
Here it is:

\[
\phipopulate{N} \egdef
\forall{\anominal} \ (\bindd{\anominal}{1} \wedge \att{\anominal}{1}(\neg \philast{N-1})) \rightarrow
\exists{\anominalbis} \ \bindd{\anominalbis}{1} \wedge \succk{N}{\anominal}{\anominalbis}.
\]

It remains to define $\eqk{N}{\anominal}{\anominalbis}$ and $\succk{N}{\anominal}{\anominalbis}$
used respectively in $\phiunique{N}$ and in $\phipopulate{N}$. This time, this requires
much lengthier developments, apart from using the properties of the formulae constructed for $N-1$ and for smaller values
(implicit induction hypothesis).
Below, we treat the more general situation with $k-d = N-1$, and
$\eqk{N}{\anominal}{\anominalbis}$ and $\succk{N}{\anominal}{\anominalbis}$ are just particular instances with $k=N$ and $d = 1$.
Thus, let $\bar{\anominal} = \anominal_1, \ldots, \anominal_d$ and $\bar{\anominalbis} =
\anominalbis_1, \ldots, \anominalbis_d$.

For defining $\succk{k}{\anominal_1, \ldots, \anominal_k}{\anominalbis_1, \ldots, \anominalbis_k}$
(see Section <ref>), we have compared the respective truth values of
the propositional variables $\avarprop_{n-1}, \ldots, \avarprop_{0}$
for the node $\anode_k$ (the interpretation of  $\anominal_k$) and for the node $\anode'_k$
(the interpretation of $\anominalbis_k$).
The same principle applied for defining $\eqk{k}{\anominal_1, \ldots, \anominal_k}{\anominalbis_1, \ldots, \anominalbis_k}$.
Typically, $\succk{k}{\anominal_1, \ldots, \anominal_k}{\anominalbis_1, \ldots, \anominalbis_k}$ holds iff
there is an index $i \in \interval{0}{n-1}$, such that

0 cm

* for every $j \in \interval{i+1}{n-1}$, $\anode_k$ and $\anode_k'$ agree on $\avarprop_j$,

* $\anode_k$ does not satisfy $\avarprop_i$ and  $\anode_k'$  satisfies $\avarprop_i$,

* for $j \in \interval{0}{i-1}$, $\anode_k$  satisfies $\avarprop_j$, $\anode_k'$  does not satisfy $\avarprop_j$.

Thus, we needed to define a partition $\set{\interval{i+1}{n-1}, \set{i}, \interval{0}{i-1}}$
of $\interval{0}{n-1}$ (understood as the set of bit numbers to encode a value in $\interval{0}{2^n-1}$).
The same   principle  applies when the bit numbers are among $\interval{0}{\tow(k{-}d,n) - 1}$ to encode a value in
$\interval{0}{\tow(k{-}d{+}1,n) - 1}$. This needs to be done concisely as we cannot go through all the $\tow(k{-}d,n)$ bit numbers
because the whole reduction has to be of elementary complexity.

Now, when attempting to define  $\succk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$,
the nodes $\anode_d$ and $\anode_d'$ are of type $k-d > 0$ with $\tow(k-d,n)$ children each. The truth values of $\val{}$ on their
respective children determine precisely the numbers $\semnumber{}{\anode_d}$ and $\semnumber{}{\anode_d'}$.
Below, we describe what $\anode_d$'s children look like.

[scale=.9,line cap=round]

(1,0) node[minirond, jaune] (AA) ;
(-2,-2) node[minirond, jaune] (AB1) ;
(-1,-2) node[minirond, bleu] (AB2) ;
(0,-2) node[minirond, vert] (AB3) ;
(0.75,-2) node[text=black] (AC1) ;
(1.5,-2) node[text=black] (AC2) $\ldots$;
(2.25,-2) node[text=black] (AC3) ;
(3,-2) node[minirond, rouge] (AB4) ;
(4,-2) node[minirond, vert] (AB5) ;
(5,-2) node[minirond, bleu] (AB6) ;

(-2,-2.5) node[text=black] (AD1) 0;
(-2,-3) node[text=black] (Text1) val;

(-1,-2.5) node[text=black] (AD2) 1;
(-1,-3) node[text=black] (Text1) $\neg$val;

(0,-2.5) node[text=black] (AD3) 2;
(0,-3) node[text=black] (Text1) $\neg$val;

(3,-2.5) node[text=black] (AD4) ;
(3,-3) node[text=black] (Text1) $\ldots$;

(4,-2.5) node[text=black] (AD5) ;
(4,-3) node[text=black] (Text1) val;

(5.5,-2.5) node[text=black] (AD6) $\tow(k{-}d,n){-}1$;
(5.5,-3) node[text=black] (Text1) val;

(-2.7,-1.52) node[text=black] (AE1) type $k{-}d{-}1$;
(5.5,-1.52) node[text=black] (AE2) type $k{-}d{-}1$;

ı/ȷin AA/AB1, AA/AB2, AA/AB3, AA/AB4, AA/AB5, AA/AB6, AA/AC1, AA/AC3
[-latex'] (ı) – (ȷ);

[use as bounding box]  (0,0);

Let $\anodebis_{\tow(k-d,n)-1}, \ldots, \anodebis_0$ be the children of $\anode_d$ such that $\semnumber{}{\anodebis_j} = j$ for all $j$.
Similarly, let $\anodebis_{\tow(k-d,n)-1}', \ldots, \anodebis_0'$ be the children of $\anode_k'$ such that
$\semnumber{}{\anodebis_j'} = j$ for all $j$. Hence, $\succk{k}{\anominal_1, \ldots, \anominal_d}{\anominalbis_1, \ldots, \anominalbis_d}$ holds iff there is a position $i \in \interval{0}{\tow(k-d,n)-1}$ satisfying

* for  $j \in \interval{i+1}{\tow(k-d,n)-1}$, $\anodebis_j$ and $\anodebis_j'$ agree on $\val{}$,

* $\anodebis_i$ does not satisfy $\val{}$ and  $\anodebis_i'$  satisfies $\val{}$,

* for every  $j \in \interval{0}{i-1}$, $\anodebis_j$  satisfies $\val{}$ and $\anodebis_j'$  does not satisfy $\val{}$.

We have to define a partition $\set{\anodebis_{i+1}, \ldots, \anodebis_{\tow(k-d,n)-1}}, \set{\anodebis_i}, \set{\anodebis_0, \ldots, \anodebis_{i-1}}$ of  $\set{\anodebis_{\tow(k-d,n)-1}, \ldots, \anodebis_0}$ (and similarly for the children
of $\anode_d'$). To do so, we employ the existential quantification
on the fresh propositional variables $\mathsf{l}$ (left), $\mathsf{s}$ (selected bit), $\mathsf{r}$ (right) such that

0 cm

(a) for every child of $\anode_d$ (resp. $\anode_d'$), exactly one propositional
variable among $\set{\mathsf{l},\mathsf{s},\mathsf{r}}$ holds true,

(b) exactly one child of $\anode_d$ (resp. $\anode_d'$) satisfies $\mathsf{s}$,

(c) if $\anode$ is a child of $\anode_d$  satisfying $\mathsf{l}$ (resp. $\mathsf{s}$)
and $\anode'$ is child of $\anode_d$  satisfying $\mathsf{s}$ (resp. $\mathsf{r}$), then $\semnumber{\atreemodel}{\anode} <
\semnumber{\atreemodel}{\anode'}$. The same condition holds with $\anode_d'$.

Below, we illustrate how the propositional variables
$\mathsf{l}$, $\mathsf{s}$ and $\mathsf{r}$ are distributed.

[scale=.9,line cap=round]

(5,1) node[minirond, vert] (Root) ;

(1,0) node[minirond, jaune] (AA) ;
(-2,-2) node[minirond, jaune] (AB1) ;
(-1,-2) node[minirond, bleu] (AB2) ;

(0,-2) node[text=black] (AC1) $\ldots$;

(1.5,-2) node[minirond, vert]  (AC2) ;
(1.4,-2) node[]  (AC2l) ;
(1.6,-2) node[]  (AC2r) ;

(3,-2) node[text=black] (AC3) $\ldots$;

(4,-2) node[minirond, jaune] (AB5) ;
(5,-2) node[minirond, bleu] (AB6) ;

(-2,-2.3) node[text=black] (AD1) $\small{\mathsf{l}}$;
(-1,-2.3) node[text=black] (AD2) $\small{\mathsf{l}}$;
(1.5,-2.3) node[text=black] (AD3) $\small{\mathsf{s}}$;
(4,-2.3) node[text=black] (AD4) $\small{\mathsf{r}}$;
(5,-2.3) node[text=black] (AD5) $\small{\mathsf{r}}$;

ı/ȷin AA/AB1, AA/AB2, AA/AB3, AA/AB4, AA/AB5, AA/AB6, AA/AC2
[-latex'] (ı) – (ȷ);

[on background layer] [blue!10, line width=2.1em, line join=round,] (AB1.center) – (AC1.center) – cycle;
[on background layer] [vert!10, line width=2.1em, line join=round,] (AC2l.center) – (AC2r.center) – cycle;
[on background layer] [rouge!10, line width=2.1em, line join=round,] (AC3.center) – (AB6.center) – cycle;

(9,0) node[minirond, jaune] (BB) ;
(6,-2) node[minirond, jaune] (BB1) ;
(7,-2) node[minirond, bleu] (BB2) ;

(8,-2) node[text=black] (BC1) $\ldots$;
(9.5,-2) node[minirond, vert]  (BC2) ;
(9.4,-2) node[]  (BC2l) ;
(9.6,-2) node[]  (BC2r) ;
(11,-2) node[text=black] (BC3) $\ldots$;

(12,-2) node[minirond, jaune] (BB5) ;
(13,-2) node[minirond, bleu] (BB6) ;

(6,-2.3) node[text=black] (BD1) $\small{\mathsf{l}}$;
(7,-2.3) node[text=black] (BD2) $\small{\mathsf{l}}$;
(9.5,-2.3) node[text=black] (BD3) $\small{\mathsf{s}}$;
(12,-2.3) node[text=black] (BD4) $\small{\mathsf{r}}$;
(13,-2.3) node[text=black] (BD5) $\small{\mathsf{r}}$;

ı/ȷin BB/BB1, BB/BB2, BB/BB3, BB/BB4, BB/BB5, BB/BB6, BB/BC2
[-latex'] (ı) – (ȷ);

[-latex'] (Root) – (AA);
[-latex'] (Root) – (BB);

[on background layer] [blue!10, line width=2.1em, line join=round,] (BB1.center) – (BC1.center) – cycle;
[on background layer] [vert!10, line width=2.1em, line join=round,] (BC2l.center) – (BC2r.center) – cycle;
[on background layer] [rouge!10, line width=2.1em, line join=round,] (BC3.center) – (BB6.center) – cycle;

[use as bounding box]  (0,0);

Additional arithmetical constraints are needed to relate the partition
of $\bar{\anominal}$ with the partition of $\bar{\anominalbis}$ (see below the details)
but in a way, it is independent of the partition itself.
For instance, the unique child of $\anode_d$ satisfying $\mathsf{s}$ and the  unique child of $\anode_d'$ satisfying $\mathsf{s}$
should have the same (bit) number.
Nevertheless, it is clear that we need, at least,
to be able
to state in  the existence of a partition satisfying the conditions (a), (b) and (c).
In the sequel, such partitions are called $\mathsf{l}\mathsf{s}\mathsf{r}$-partitions.
The forthcoming formula $\lsr{k}{\bar{\anominal}}$ does the job for $\anode_d$ (then use $\lsr{k}{\bar{\anominalbis}}$ for $\anode_d'$).

Take $\bar{\anominal} = \anominal_1, \ldots, \anominal_d$.
In the context of the definition of $\lsr{k}{\bar{\anominal}}$,
we allow the limit case $d=0$, with empty sequence $\varepsilon$, assuming that $\att{\varepsilon}{} \aformulabis \egdef \aformulabis$
and $\widehat{\varepsilon,\varepsilon} \egdef \top$.
Below $0 \leq d < k$ and the formula $\lsr{k}{\bar{\anominal}}$  is defined as the conjunction $\lsrone{k}{\bar{\anominal}} \wedge
\lsrtwo{k}{\bar{\anominal}} \wedge \lsrthree{k}{\bar{\anominal}}$ and
is  interpreted on a node $\anode_0$ of type $k$ satisfying
$\widehat{\bar{\anominal},\bar{\anominal}}$, and therefore this satisfaction is witnessed by the branch $\anode_0, \ldots, \anode_d$
(notations for developments below).

First, $\lsrtwo{k}{\bar{\anominal}} \egdef \att{\bar{\anominal}}{}(\EXOne(\mathsf{s}))$,
$\EXOne(\aformulabis)$ defined as  $\EX \aformulabis \wedge \neg \exists \ \avarprop \
(\EX(\aformulabis  \wedge \avarprop) \wedge  \EX(\aformulabis  \wedge \neg \avarprop))$ for a fresh $\avarprop$.
Note that the formula $\lsrtwo{k}{\bar{\anominal}}$ simply states that there is a unique child of $\anode_d$ satisfying $\mathsf{s}$.
Next, let $\lsrone{k}{\bar{\anominal}}$ be defined below, stating that for every child of $\anode_d$, exactly one
propositional variable among $\set{\mathsf{l},\mathsf{s},\mathsf{r}}$ holds true:

\[
\lsrone{k}{\bar{\anominal}} \egdef
\att{\bar{\anominal}}{}
\left( \AX((\mathsf{s} \vee \mathsf{l} \vee \mathsf{r})  \wedge
\neg (\mathsf{s} \wedge \mathsf{l}) \wedge
\neg (\mathsf{s} \wedge \mathsf{r}) \wedge \neg (\mathsf{l} \wedge \mathsf{r}))
\right).
\]

Finally, $\lsrthree{k}{\bar{\anominal}}$ is defined as follows.

\[
\att{\bar{\anominal}}{}
\forall{w} \forall{w'} \ \distinctbindd{w,w'}{1} \wedge ((\att{w}{1}(\mathsf{s}) \wedge
\att{w'}{1}(\mathsf{r})) \vee
(\att{w}{1}(\mathsf{l}) \wedge \att{w'}{1}(\mathsf{s}))) \rightarrow
\gk{k-d}{w'}{w}
\]

The formula $\lsrthree{k}{\bar{\anominal}}$ states if $\anode$ is a child of $\anode_d$ satisfying $\mathsf{l}$ (resp. $\mathsf{s}$)
and $\anode'$ is another child of $\anode_d$ satisfying $\mathsf{s}$ (resp. $\mathsf{r}$), then $\semnumber{\atreemodel}{\anode} <
\semnumber{\atreemodel}{\anode'}$. The nodes $\anode$ and $\anode'$ are obviously of type $k-d-1$ and their respective
numbers belong to $\interval{0}{\tow(k-d,n)-1}$. It is important to observe that $\gk{k-d}{w'}{w}$ is well-defined recursively as soon as
$k-d \leq N-2$.

Let $\atreemodel$ be a tree model, $\anode_0$ be a node of type $k \geq 0$, and
$\bar{\anominal}$ be a (possibly empty) sequence of nominals $\anominal_1, \ldots, \anominal_d$ for some $d \in \interval{0}{k-1}$
such that  $k-d \leq N-1$, $\atreemodel, \anode_0 \models \widehat{\bar{\anominal},\bar{\anominal}}$, and its witness branch is $\anode_0, \ldots, \anode_d$.
Then $\atreemodel, \anode_0 \models \lsr{k}{\bar{\anominal}}$ iff the conditions below hold:

0 cm

(a) For every child of $\anode_d$, exactly one propositional
variable among $\set{\mathsf{l},\mathsf{s},\mathsf{r}}$ holds true.

(b) Exactly one child of $\anode_d$ satisfies $\mathsf{s}$.

(c) If $\anode$ is a child of $\anode_d$ satisfying $\mathsf{l}$ (resp. $\mathsf{s}$)
and $\anode'$ is a child of $\anode_d$ satisfying $\mathsf{s}$ (resp. $\mathsf{r}$), then $\semnumber{\atreemodel}{\anode} <
\semnumber{\atreemodel}{\anode'}$.

By careful inspection of the presented formulae, Appendix <ref>.

We come back to the question of defining formulae expressing number comparisons.
The formula $\succk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ (remember $k-d=N-1$) is defined as the expression

\[
\exists \  \mathsf{l}, \mathsf{s}, \mathsf{r} \
\lsr{k}{\bar{\anominal}} \wedge \lsr{k}{\bar{\anominalbis}} \wedge
\aformula_{{\tiny \rm left}}(k) \wedge \aformula_{{\tiny \rm select}}(k) \wedge \aformula_{{\tiny \rm right}}(k).
\]

The conjunction $\aformula_{{\tiny \rm left}}(k) \wedge \aformula_{{\tiny \rm select}}(k) \wedge \aformula_{{\tiny \rm right}}(k)$ takes care of the arithmetical constraints.
The formula $\aformula_{{\tiny \rm select}}(k)$ states that the $\anode_d$'s unique child  satisfying $\mathsf{s}$ (whose
number is the pivot bit $i$) does not satisfy $\val{}$, and the $\anode_d'$'s unique child  satisfying $\mathsf{s}$ (whose number is also the pivot bit $i$) satisfies $\val{}$:

\[
\aformula_{{\tiny \rm select}}(k)  \egdef
\att{\bar{\anominal}}{} \left( \AX(\mathsf{s} \rightarrow \neg \val{k-d-1}) \right) \wedge
\att{\bar{\anominalbis}}{} \left( \AX(\mathsf{s} \rightarrow  \val{k-d-1}) \right).
\]

The formula $\aformula_{{\tiny \rm right}}(k)$ states that for all the children of $\anode_d$ satisfying $\mathsf{r}$ (and therefore with bit number strictly smaller than $i$), the bit value is 1, and  for all the children of $\anode_d'$ satisfying
$\mathsf{r}$ (and therefore with bit number strictly smaller than $i$), the bit value is $0$.

\[
\aformula_{{\tiny \rm right}}(k)  \egdef \att{\bar{\anominal}}{} \left( \AX(\mathsf{r} \rightarrow  \val{k-d-1}) \right) \wedge
\att{\bar{\anominalbis}}{} \left( \AX(\mathsf{r} \rightarrow  \neg \val{k-d-1}) \right).
\]

The formula $\aformula_{{\tiny \rm left}}(k)$ states that the children of $\anode_d$ satisfying $\mathsf{l}$ induce a set of
bit numbers equal to the set of bit numbers induced by the children of $\anode_d'$ satisfying  $\mathsf{l}$.
This entails also that the unique respective children of $\anode_d$ and $\anode_d'$ satisfying $\mathsf{s}$ have the same (bit) number.
Moreover, we require that children with the same bit number satisfying $\mathsf{l}$ (taken from $\anode_d$ and from $\anode_d'$) have the same bit value witnessed by the truth value of $\val{}$.
The formula $\aformula_{{\tiny \rm left}}(k)$ is equal to $\aformula_{{\tiny \rm left}}^{\bar{\anominal}, \bar{\anominalbis}}(k)
\wedge \aformula_{{\tiny \rm left}}^{\bar{\anominalbis}, \bar{\anominal}}(k)$  with $\aformula_{{\tiny \rm left}}^{\bar{\anominal}, \bar{\anominalbis}}(k)$
defined below:

\[
\aformula_{{\tiny \rm left}}^{\bar{\anominal}, \bar{\anominalbis}}(k) \egdef
\forall{w} \; \att{\bar{\anominal}}{}(\bindd{w}{1} \wedge \att{w}{1} (\mathsf{l})) \rightarrow
\]

\[
\big(\exists{w'} \;
\att{\bar{\anominalbis}}{}(\bindd{w'}{1} \wedge \att{w'}{1} (\mathsf{l})) \wedge
\eqk{k}{\bar{\anominal},w}{\bar{\anominalbis},w'} \wedge (\att{\bar{\anominal},w}{} \val{k-d-1} \leftrightarrow
\att{\bar{\anominalbis},w'}{} \val{k-d-1})\big).
\]

Note that $\eqk{k}{\bar{\anominal},w}{\bar{\anominalbis},w'}$ is well-defined as $k-(d+1) \leq N-2$.

Below, we define the formula $\gk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ with $k-d=N-1$, $\bar{\anominal} = \anominal_1, \ldots,\anominal_d$ and $\bar{\anominalbis} = \anominalbis_1, \ldots,\anominalbis_d$.
Based on previous developments and on standard arithmetical properties of numbers encoded in binary with $k-d$ bits, we define the formula $\gk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ as the expression

\[
\gk{k}{\bar{\anominal}}{\bar{\anominalbis}} \egdef
\exists \ \mathsf{s}, \mathsf{l}, \mathsf{r} \
\lsr{k}{\bar{\anominal}} \wedge \lsr{k}{\bar{\anominalbis}} \wedge
\aformula_{{\tiny \rm left}}(k) \wedge \aformula_{{\tiny \rm select}}(k).
\]

As previously, the formula $\eqk{k}{\bar{\anominal}}{\bar{\anominalbis}}$  is defined as follows:

\[
\eqk{k}{\bar{\anominal}}{\bar{\anominalbis}}
\egdef
\neg (\gk{k}{\bar{\anominal}}{\bar{\anominalbis}})
\wedge
\neg (\gk{k}{\bar{\anominalbis}}{\bar{\anominal}}).
\]

Let $\atreemodel$ be a tree model, $\anode$ be a node satisfying $\widehat{\bar{\anominal},\bar{\anominalbis}}$ and, $\anode_{d}$, $\anode'_{d}$ are of type $k - d$.

(I) We have $\atreemodel, \anode \models \succk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ iff $\semnumber{\atreemodel}{\anode_d'} = 1+ \semnumber{\atreemodel}{\anode_d}$.

(II) We have $\atreemodel, \anode \models \gk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ iff $\semnumber{\atreemodel}{\anode_d} < \semnumber{\atreemodel}{\anode_d'}$.

(III) We have $\atreemodel, \anode \models \eqk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ iff $\semnumber{\atreemodel}{\anode_d} = \semnumber{\atreemodel}{\anode_d'}$.

By careful inspection of the presented formulae, Appendix <ref>.

Mainly, this allows us to prove Lemma <ref>(I).

Let $N \geq 2$, $\atreemodel$ be a tree model and $\anode$ be one of its nodes.

(I) $\atreemodel, \anode \models \phitype{N}$ iff $\anode$ is of type $N$,

(II) Assuming that $\anode$ satisfies $\phitype{N}$, we have $\atreemodel, \anode \models \phifirst{N}$ iff $\semnumber{\atreemodel}{\anode} = 0$.

(III) Assuming that $\anode$ satisfies $\phitype{N}$, we have $\atreemodel, \anode \models \philast{N}$ iff $\semnumber{\atreemodel}{\anode} = \tow(N+1,n)-1$.

Similar to the proof of Lemma <ref>, see Appendix <ref> for more details.

Consequently, for all $k \geq 0$, $\phitype{k}$, $\phifirst{k}$ and $\philast{k}$
characterise exactly the discussed properties, and similarly for the formulae
of form $\succk{k}{\bar{\anominal}}{\bar{\anominalbis}}$,
where $\bar{\anominal}$ and $\bar{\anominalbis}$ are of length $d$ in $\interval{1}{k}$ and $k \geq 1$.
It is natural to wonder what is the size of $\phitype{k}$, using a reasonably succinct encoding for formulae.
As the definition of $\phitype{k}$ requires the subformulae $\phitype{k-1}$,
$\eqk{k}{\bar{\anominal}}{\bar{\anominalbis}}$ and $\succk{k}{\bar{\anominal}}{\bar{\anominalbis}}$
(the other subformulae  are of constant size), and the formula $\phitype{1}$ is quadratic in $n$, one can show that $\phitype{k}$ is of size $2^{\mathcal{O}(k+n)}$.
This is sufficient for our purposes.

§.§ Uniform reduction leading to -hardness

Let $(\cP, c)$, where $\cP = (\cT, \cH, \cV)$ and $c = t_0,t_1, \ldots, t_{n-1}$
be an instance of  $\mathtt{Tiling}_k$ known to be $\kNExpTime$-complete
(see also <cit.>). We reduce the existence of a tiling $\tau: \interval{0}{\tow(k,n)-1} \times
\interval{0}{\tow(k,n)-1} \rightarrow \cT$, respecting the initial condition
and the horizontal and vertical matching conditions,
to the satisfiability of a formula $\aformula$ in .

To encode the grid  $\interval{0}{\tow(k,n)-1} \times \interval{0}{\tow(k,n)-1}$, we consider a root node $\aroot$ of type $k+1$, and we distinguish $\tow(k,n)$ children among all of its $\tow(k+1,n)$ children.
Each child of $\aroot$ has itself exactly $\tow(k,n)$ children as it is a node of type $k$.
In order to identify the $\tow(k,n)$ first children of $\aroot$, we use an $\mathsf{l} \mathsf{s} \mathsf{r}$-partition
so that the unique child satisfying $\mathsf{s}$ has precisely the number $\tow(k,n)$.
This guarantees that exactly the children of $\aroot$ whose numbers are in $\interval{0}{\tow(k,n)-1}$
satisfy $\mathsf{r}$.  So, the $\mathsf{l} \mathsf{s} \mathsf{r}$-partition is used in a new context.

Below, we define the new formula $\anothereqk{k}$  that expresses that
a node of type $k$ has number $\tow(k,n)$ ($k \geq 1$).
We recall that a node of type $k$ takes its values in $\interval{0}{\tow(k+1,n)-1}$.
Let us provide an inductive definition for $\anothereqk{k}$ with the base case  $k = 1$.

* $\anothereqk{0} \; \egdef \neg \avarprop_{n-1} \wedge \cdots \wedge \neg \avarprop_0$.

* $\anothereqk{1} \egdef \AX (\val{0} \leftrightarrow \aset_n = n)$, where $\aset_n = n$ is an abbreviation for the formula
stating that the truth values for $\avarprop_{n-1}, \ldots, \avarprop_0$ encode $n$ in binary.

* For $k \geq 2$,  $(\anothereqk{k}) \egdef \AX (\val{k-1} \leftrightarrow (\anothereqk{k-1}))$.

Assume that $\atreemodel, \anode \models \phitype{k}$. Then
$\semnumber{\atreemodel}{\anode} = \tow(k,n)$ iff $\atreemodel, \anode \models (\anothereqk{k})$.

By careful inspection of the semantics, Appendix <ref>.

Let $\aformula_\cP$ be the formula built from the instance $(\cP = (\cT, \cH, \cV),c)$ as follows:

\[
\phitype{k+1} \wedge \exists \ \mathsf{l}, \mathsf{s}, \mathsf{r} \
\lsr{k+1}{\varepsilon} \wedge
\EX(\mathsf{s} \wedge (\anothereqk{k})) \wedge
\aformula_{\rm cov} \wedge
\aformula_{\rm init}   \wedge
\aformula_{\cH} \wedge
\aformula_{\cV}.
\]

Definitions and explanations for $\aformula_{\rm cov}$, $\aformula_{\rm init}$, $\aformula_{\cH}$
and $\aformula_{\cV}$ follow but observe that an $\mathsf{l}\mathsf{s}\mathsf{r}$-partition
is performed for a node of type $k+1$ and exactly $\tow(k,n)$ children satisfy $\mathsf{r}$ thanks
to the satisfaction of the subformula $\EX(\mathsf{s} \wedge (\anothereqk{k}))$.
The formula $\aformula_{\rm cov}$ states that every position in $\interval{0}{\tow(k,n)-1} \times \interval{0}{\tow(k,n)-1}$ has a unique tile:

\[
\forall \ \anominal, \anominalbis \
\bindd{\anominal}{1} \wedge \att{\anominal}{1} \mathsf{r} \wedge
\att{\anominal}{1} \bindd{\anominalbis}{1}
\rightarrow
\att{\anominal, \anominalbis}{} (\bigvee_{t \in \cT} t \wedge \bigwedge_{t \neq t' \in \cT} \neg (t \wedge t')).
\]

The tile types in $\cT$ are understood as propositional variables.
In order to access the root node $\aroot$ to a node  encoding a position of the grid,
one needs first to access a child $\anode$ of $\aroot$ satisfying $\mathsf{r}$ (and this is done
with the help of the local nominal $\anominal$) and then to access any child $\anode'$ of $\anode$
(done  with  the local nominal $\anominalbis$). Then, to reason propositionally on $\anode'$, it is sufficient
to consider subformulae of the form $\att{\anominal, \anominalbis}{}  \aformulabis$. This principle
is applied to all the formulae below.

The formula $\aformula_{\cH}$ defined below encodes the horizontal matching constraints.

\[
\forall \ \anominal, \anominal', \anominalbis, \anominalbis' \
(\bindd{\anominal}{1} \wedge \att{\anominal}{1} \mathsf{r} \wedge
\bindd{\anominal'}{1} \wedge \att{\anominal'}{1} \mathsf{r} \wedge
\att{\anominal}{1} \bindd{\anominalbis}{1} \wedge \att{\anominal'}{1} \bindd{\anominalbis'}{1}
\wedge
\]

\[
\succk{k+1}{\anominal}{\anominal'} \wedge
\eqk{k+1}{\anominal,\anominalbis}{\anominal,\anominalbis'})
\rightarrow
\bigvee_{\pair{t}{t'} \in \mathcal{H}} \att{\anominal,\anominalbis}{} t \wedge \att{\anominal',\anominalbis'}{} t'
\]

Similarly, the following formula $\aformula_{\cV}$ encodes the vertical matching constraints.

\[
\forall \ \anominal, \anominal', \anominalbis, \anominalbis' \
\bindd{\anominal}{1} \wedge \att{\anominal}{1} \mathsf{r} \wedge
\bindd{\anominal'}{1} \wedge \att{\anominal'}{1} \mathsf{r} \wedge
\att{\anominal}{1} \bindd{\anominalbis}{1} \wedge \att{\anominal'}{1} \bindd{\anominalbis'}{1}
\wedge
\]

\[
\eqk{k+1}{\anominal}{\anominal'} \wedge  \succk{k+1}{\anominal,\anominalbis}{\anominal,\anominalbis'}
\rightarrow
\bigvee_{\pair{t}{t'} \in \mathcal{V}} \att{\anominal,\anominalbis}{} t \wedge \att{\anominal',\anominalbis'}{} t'
\]

It remains to express the initial conditions. It is sufficient to identify the $n$ first children
of the first child of $\aroot$ (identified by the satisfaction of $\phifirst{k}$).
For example, to express that the $j$th child of the first child of $\aroot$ (say $\anode$ is this first child
of $\aroot$) satisfies $t_j$,
perform an $\mathsf{l} \mathsf{s} \mathsf{r}$-partition on $\anode$,
enforce that the unique child satisfying $\mathsf{s}$ also satisfies $t_j$
and express that there are exactly $j-1$ children of  $\anode$  satisfying $\mathsf{r}$.
This is a condition from graded modal logic that is easy to express.
Let $\EX_{=i} \ \aformulabis$ be the formula below stating that exactly $i \geq 1$ children satisfy

\[
\exists \ \avarpropbis_1, \ldots, \avarpropbis_i \
\distinctbindd{\avarpropbis_1, \ldots, \avarpropbis_i}{1} \wedge
\AX ((\avarpropbis_1 \vee \cdots \vee \avarpropbis_i) \leftrightarrow \aformulabis),
\]

where $\avarpropbis_1, \ldots, \avarpropbis_i$ are fresh
By convention $\EX_{=0} \ \aformulabis$ is defined as $\AX \neg \aformulabis$.
The formula $\aformula_{\rm init}$ is defined as

\[
\forall \ \anominal \  ( \bindd{\anominal}{1} \wedge \att{\anominal}{1} (\phifirst{k}))
\rightarrow \att{\anominal}{1} (
\bigwedge_{i \in \interval{0}{n-1}} \exists \ \mathsf{l}, \mathsf{s}, \mathsf{r} \
\lsr{k}{\varepsilon} \wedge \EX_{=i} \ \mathsf{r} \wedge \EX(\mathsf{s} \wedge t_i)
\]

The correctness of the reduction is stated below.

$\cP = (\cT, \cH, \cV)$, $c = t_0,t_1, \ldots, t_{n-1}$  is a positive instance
of $\mathtt{Tiling}_k$
iff $\aformula_\cP$ is satisfiable in .

Given an instance $\cP = (\cT, \cH, \cV)$, $c = t_0,t_1, \ldots, t_{n-1}$
of the tiling problem $\mathtt{Tiling}_k$, let  $\tau: \interval{0}{\tow(k,n)-1} \times
\interval{0}{\tow(k,n)-1} \rightarrow \cT$ be a tiling respecting all the constraints <ref>, <ref> and <ref>.
Below, we build a tree model $\atreemodel = \triple{V}{E}{l}$ such that
$\atreemodel, \aroot \models \aformula_{\cP}$ where $\aroot$ is the root node of $\atreemodel$.
Let $V$ be the following subset of $\Nat^*$ (set of finite sequences over $\Nat$):

* $\aroot$ is the empty string and it belongs to $V$,

* For all $j \in \interval{1}{k+1}$,
$\interval{0}{\tow(k+1,n)-1} \times \cdots \times \interval{0}{\tow(j,n)-1} \subseteq V$.

* $\interval{0}{\tow(k+1,n)-1} \times \cdots \times \interval{0}{\tow(1,n)-1} \times 0^+ \subseteq V$.

The binary relation $E$ is simply defined as: $\anode E \anode'$ $\equivdef$ $\anode$ is a prefix of $\anode'$, and $\anode \cdot \alpha
= \anode'$ for some $\alpha \in \Nat$. So, $\pair{V}{E}$ is a finite-branching tree such that all the maximal branches are infinite.
The labelling map $l$ is defined in  a way so that $\atreemodel, \aroot \models \phitype{k+1}$.
For instance, any node $m_{k+1}, \ldots, m_{2} \in V \cap \Nat^{k-1}$ has $2^n$ children, and their numbers should span
over $\interval{0}{2^n-1}$. This is easy to realise by setting properly the truth values for $\avarprop_{n-1}, \ldots, \avarprop_0$.
Similarly, any node $m_{k+1}, \ldots, m_{3} \in V \cap \Nat^{k-2}$ has $\tow(2,n)$ children, and their numbers should span
over $\interval{0}{\tow(2,n)-1}$. Again, this is easy to realise by setting properly the truth values of $\val{}$
on the nodes in $\interval{0}{\tow(k+1,n)-1} \times \cdots \times \interval{0}{\tow(1,n)-1}$.
So, it remains to take care of the propositional variables dedicated to the tile types.

* For all $\pair{i}{j} \in \interval{0}{\tow(k,n)-1} \times \interval{0}{\tow(k,n)-1}$,
$l(\pair{i}{j}) \cap \cT$ is equal to $\set{\tau(i,j)}$ by definition.
In particular, this means that for all $\pair{i}{j} \in \interval{0}{\tow(k,n)-1} \times \interval{0}{\tow(k,n)-1}$,
there is exactly one tile type (understood as a propositional variable) satisfied by $\pair{i}{j}$.

* For all $\anode \in V \setminus \interval{0}{\tow(k,n)-1} \times \interval{0}{\tow(k,n)-1}$,
the value of the set $l(\anode) \cap \cT$ is irrelevant.

It remains to check that

\[
\atreemodel, \aroot \models \phitype{k+1} \wedge \exists \ \mathsf{l}, \textit{s}, \mathsf{r} \
\lsr{k+1}{\varepsilon} \wedge
\EX(\mathsf{s}\wedge \anothereqk{k}) \wedge
\aformula_{\rm cov} \wedge
\aformula_{\rm init}   \wedge
\aformula_{\cH} \wedge
\aformula_{\cV},
\]

which is routine and done in Appendix <ref>.

We are ready to conclude the main theorem of this paper.

is -complete.

Theorem <ref> significantly
improves  the lower bound from <cit.>
by considering as only temporal operator, the (local) modality $\EX$.
-hardness can be also obtained with arbitrary countable trees.
In Section <ref> below, we show that
this entails more -hardness results for other fragments of  and for modal logics
with propositional quantification under appropriate tree semantics.

§ A HARVEST OF -COMPLETE MODAL AND TEMPORAL LOGICS

We capitalise on the -hardness of the satisfiability problem for ,
by showing -hardness of other fragments of  that involve only $\EF$ or its strict
variant $\EX \EF$ (Section <ref>).
-hardness is obtained by reduction from  by introducing propositional variables that enforce layers from the root in the tree model and therefore this allows us to simulate $\EX$.
In Section <ref>, we consider well-known modal logics that are complete
for classes of tree-like Kripke structures, and we show that their extension with propositional
quantification for such classes of tree-like Kripke structures
is decidable in , but more importantly -hard.
Some of such classes involve finite trees and therefore, we also take the opportunity to
study  and  that happen, for instance, to be closely related
to the  modal logics and , respectively.

§.§ The satisfiability problems for tQCTLEF and tQCTLEFplus are -hard!

The fragment  of  is defined according to the following grammar

\[
\aformula ::= \avarprop \ | \ \neg \aformula \
| \  \aformula \wedge \aformula \
| \ \EF \aformula \
|  \ \ \exists{\avarprop} \; \aformula.
\]

We recall the standard semantics for $\EF$-formulae:
$\atreemodel, \anode \models \EF \aformula$ $\equivdef$
there is $j \geq 0$ such that $\anode E^j \anode'$ and  $\atreemodel, \anode' \models \aformula$, and
as usual, $\AG \aformula \egdef \neg \EF \neg \aformula$.

In order to show that  is -hard,
we design a logarithmic-space many-one reduction from .

A more sophisticated analysis is also possible to establish -hardness for even smaller fragments, see
the recent work [39].

Let $\aformula$ be a formula in  with modal depth $\md{\aformula} = k$.
Without loss of generality, we assume that $\aformula$ may contain occurrences
of $\EX$ and no occurrences of $\AX$. Let us define
the formula $\aformula' = \textit{trans}(k,\aformula) \wedge {\rm shape}(k)$
in ,  where the formula ${\rm shape}(k)$ enforces a discipline for layers (explained below)
and $ \textit{trans}(k,\aformula)$ admits a recursive definition, by relativising the occurrences of $\EX$.
We consider the set of propositional variables
$\asetbis_{k} = \set{\layer{-1}, \layer{0}, \ldots, \layer{k}}$
with the intended meaning that a node satisfying $\layer{i}$ is of “layer $i$”, the root node being of layer $k$.
Indeed, there is a need for such propositional variables, as unlike with
the formulae in , we have to enforce that moving with $\EF$ leads
to a lower layer.

The formula ${\rm shape}(k)$ is defined as the conjunction of the following formulae.

0 cm

* Every node satisfies exactly one propositional variable from $\asetbis_k$ (layer unicity):

\[
\AG \left( (\layer{-1} \vee \layer{0} \vee \cdots \vee \layer{k} )
\wedge \bigwedge_{-1 \leq i\neq j \leq k} \neg (\layer{i} \wedge \layer{j}) \right)
\]

* When a node satisfies $\layer{i}$ with $-1 \leq i \leq k$, none of its
descendants satisfies $\layer{j}$ with $j > i$ (monotonicity of layer numbers):

\[
\bigwedge_{-1 \leq i \leq k} \AG(\layer{i} \rightarrow
\AG (\layer{-1} \vee \layer{0} \vee \cdots \vee \layer{i}))
\]

* When a node satisfies $\layer{i}$ with $0 \leq i \leq k$,  there is a descendant
satisfying $\layer{i-1}$ (weak progress):

\[
\bigwedge_{0 \leq i \leq k} \AG(\layer{i} \rightarrow \EF \ \layer{i-1})
\]

* When a node satisfies $\layer{i}$ with $0 \leq i \leq k$, it has no (strict) descendant satisfying $\layer{i}$ (no stuttering). This type of constraints does not apply to $\layer{-1}$.

\[
\bigwedge_{0 \leq i \leq k}
\AG(\layer{i} \rightarrow \neg \exists{\avarprop} \ (\avarprop  \wedge \EF(\layer{i} \wedge \neg \avarprop)))\]

* The root node is at layer $k$: $\layer{k}$.

A tree model $\atreemodel = \triple{V}{E}{l}$ for  with root $\aroot$
is $k$-layered iff the conditions below hold:

0 cm

(a) For every node $\anode \in V$, $\card{l(\anode) \cap \asetbis_{k}} = 1$.

(b) For all $\anode \in V$ such that $\layer{j} \in l(\anode)$ for some $j \in \interval{-1}{k}$,

* if $j \geq 0$, then there is $\anode'$ such that $\anode E \anode'$ and $\layer{j-1} \in l(\anode')$ and,

* for all $\anode'$ such that $\anode E^+ \anode'$ and $\layer{j'} \in l(\anode')$, we have $j' \leq j$.

(c) For all $j \in \interval{0}{k}$, there are no distinct nodes $\anode$  and $\anode'$
such that $\anode E^+ \anode'$ and $\layer{j} \in l(\anode) \cap l(\anode')$.

(d) $\layer{k} \in l(\aroot)$, where $\aroot$ is the root of the tree model.

This means that the only propositional variable from $\asetbis_k$
satisfied by a node reachable in $j \in \interval{1}{k}$ steps from $\aroot$ is
$\layer{m}$ for some $m \leq k-j$, and the only propositional variable from $\asetbis_k$
satisfied by a node reachable in strictly more than $k$ steps
from $\aroot$  is $\layer{-1}$. Moreover, once $\layer{-1}$ holds true,
it holds for all its descendants.
Actually, the formula ${\rm shape}(k)$ characterises $k$-layered structures.

Let $\atreemodel = \triple{V}{E}{l}$ be a tree model for  with the root node $\aroot$.
We have $\atreemodel, \aroot \models {\rm shape}(k)$ holds if and only if $\atreemodel$ is $k$-layered.

By careful inspection of the semantics, Appendix <ref>.

To define $\textit{trans}(k,\aformula)$, we define
$\textit{trans}(i,\aformulabis)$ where
$\aformulabis$ is a subformula of $\aformula$ and $\md{\aformulabis} \leq i$.

0 cm

* $ \textit{trans}(i, \avarprop) \egdef \avarprop$ for all propositional variables $\avarprop$,

* $ \textit{trans}$ is homomorphic for Boolean connectives and  $ \textit{trans}(i, \exists \ \avarprop \ \aformulabis) \egdef \exists \ \avarprop \ \textit{trans}(i, \aformulabis)$,

* $ \textit{trans}(i, \EX \aformulabis) \egdef \EF \left(\layer{i{-}1} \wedge  \textit{trans}(i{-}1, \aformulabis)\right)$.

Note that $ \textit{trans}(k,\aformula)$ has no occurrence of $\layer{-1}$
since $\md{\aformula}=k$ and that translating an $\EX$-formula decreases
the index of the layer by exactly one.
The correctness of the reduction can be now stated as follows.

A formula $\aformula$ is satisfiable for  iff
$\textit{trans}(k,\aformula) \wedge {\rm shape}(k)$
is satisfiable for .

By induction. Consult Appendix <ref>.

Hence we conclude yet another important result.

The satisfiability problem for  is -complete.

The upper bound  is established for
the full logic  in [37]
and in particular for . Theorem <ref> also admits a variant in which we only allow
to move to proper descendants. It amounts to replacing $\EF$ by $\EX \EF$ (treated here as a single modality) in  $\tQCTLEF{}$, leading to
the variant  , with formulae obtained from

\[
\aformula ::= \avarprop \ | \ \neg \aformula \
| \  \aformula \wedge \aformula \
| \ \EX \EF \aformula \
|  \ \ \exists{\avarprop} \; \aformula
\]

As usual, we  write $\AX \AG \; \aformulabis$ as an abbreviation of $\neg \EX \EF \neg \aformula$.

The satisfiability problem for  is -complete.

As above, the upper bound for  is inherited from  [37].
Note that in , the formula $\EF \avarprop$ is logically equivalent to $\avarprop \vee \EX \EF \avarprop$. Thus, we get a (possibly exponential, which is sufficient for us) reduction from  to ,
whence the -hardness of .  Recall that -hardness is defined with respect
to elementary reductions and therefore an exponential-time reduction is fine to establish -hardness,
see e.g. [51] and Section <ref>.

§.§ Modal logics with propositional quantification on trees

Numerous well-known  modal logics are complete (a.k.a. determined) for classes of tree-like structures.

A modal logic $\alogic$ (defined from the Hilbert-style system $\mathcal{H}\alogic$)
is complete for a class of Kripke structures $\mathcal{C}$ iff
the theoremhood of $\aformula$ in $\mathcal{H}\alogic$ is equivalent
to the validity of $\aformula$ in $\mathcal{C}$ (i.e. for all $\kripkeK \in \mathcal{C}$,
for all $w$, we have $\kripkeK, w \models \aformula$).
For instance, the  (propositional) modal logic is complete for the class of finite
trees [52, 9].
It is worth noting that a given modal logic can be complete for different classes of Kripke models
(is complete for the class of all the Kripke models, but also complete for the class of finite Kripke models)
and their extension to propositional quantification may lead to distinct logics.
Typically, with propositional
quantification under the structure semantics is undecidable [24] whereas it is shown below to be
-complete under the finite tree semantics.

Below, for the propositional modal logics  $\alogic$ in ,  , , and we define
an extension $\mathsf{Q}\alogic^t$ with propositional quantification under a class of tree-like models
that is complete  for the logic $\alogic$.

In order to avoid too many notations, the modalities for each logic $\mathsf{Q}\alogic^t$
are $\EX$ and $\AX$ (instead of the more standard modal operators $\Diamond$ and $\Box$)
and therefore $\mathsf{Q}\alogic^t$ formulae are built from the grammar below:
\aformula ::=
\avarprop \mid  \neg \aformula \mid \aformula \wedge \aformula \mid
\EX \aformula \mid \AX \aformula
\mid \exists{\avarprop} \  \aformula

* The propositional modal logic is complete for the class of finite trees and we define as the modal logic
with propositional quantification over the class of finite trees.

* The propositional modal logic (with seriality, a.k.a. totality) is known to be complete for the class
of finite-branching trees for which all the maximal branches are infinite.
Indeed, is complete for the class of finite total Kripke models.
Therefore by using the unfolding
construction, completeness applies also for
the class
of finite-branching trees for which all the maximal branches are infinite, the models for .
Let be the modal logic
with propositional quantification over the class
of finite-branching trees for which all the maximal branches are infinite.
The satisfiability problem for is exactly the problem for .

* The modal logic is known to be complete for the class of finite transitive trees
(is complete with respect to finite irreflexive transitive Kripke models [54]), the class
of Kripke structures $\triple{V}{E^+}{l}$ such that $\triple{V}{E}{l}$ is a finite tree model, see  [9].
Let be the modal logic with propositional quantification over the
class of finite transitive trees, which is precisely .
It is worth noting that adding propositional quantification to is studied in [1],
where a fragment is shown to be decidable by translation into the weak monadic second-order logic of one successor
WS1S [12].

* The modal logic is complete for the class of Kripke structures
$\triple{V}{E^+}{l}$ such that $\triple{V}{E}{l}$ is a finite-branching tree
model (some branches may be infinite, some others not).
Let be the modal logic with propositional quantification over the
class of finite-branching trees.

* The modal logic is complete for the class of finite Kripke structures such that
the accessibility relation is reflexive and transitive, and therefore complete
for the class of structures
$\triple{V}{E^*}{l}$ such that $\triple{V}{E}{l}$ is a finite-branching tree
model in which all the  branches are infinite (by unfolding).
Let be the modal logic with propositional quantification over the
class of finite-branching trees in which all the  branches are infinite (precisely
the class of models for ). The satisfiability problem for happens to be exactly the problem
for , modulo the fact that $\EX$ in corresponds to $\EF$ in .

In this section, we show that the satisfiability problem for
the logics , , , and and whose models are tree-like Kripke structures is -complete.
For instance, corresponds to the modal logic interpreted on finite trees
with propositional quantification, which is precisely ,
restricted to the $\EX$ operator.

is -complete.

The satisfiability problem in Theorem <ref> is exactly . An easy translation can be found in Appendix <ref>.

As a corollary of Theorem <ref>,
for all $N \geq 2$, the satisfiability problem for $\QKt_{\leq N}$
is -complete too where $\QKt_{\leq N}$ is interpreted on finite trees whose
branching degree is at most $N$. The lower bound can be obtained using the same
reduction as for , ≤N whereas the upper bound uses also the same arguments
as for , ≤N.

We have seen that is actually defined
as  (is characterised by total and finite Kripke structures whose
unfoldings generate finite-branching trees in which all the branches are infinite).

is -complete.

Recall that the modal logic is known to be complete for the class of finite transitive trees.
The logic extends it with propositional quantification. We obtain the following:

is -complete.

The logic can be shown to be precisely  when $\EX$ is translated into
$\EX\EF$, whence we get a upper bound.
For the -hardness proof, it is very similar to the one for  (actually, it is a bit simpler).
Consult Appendix <ref>.

is defined as the modal logic with propositional quantification over the
class of finite-branching trees. Our next theorem is as follows.

is -complete.

Full proof is in Appendix <ref>.
We first show  and
are identical modulo the rewriting of $\EX$ into $\EX \EF$.
This yields the upper bound.
As far as -hardness is concerned, for any formula $\aformula$ in
, one can show that $\aformula$ is satisfiable for
iff $\aformula \wedge \EX \ \EF \ \top \wedge \AX \AG \ \EX  \EF \ \top$ is satisfiable
in .

Finally, by noting that is equal to  modulo that $\EX$ is rewritten into $\EF$,
using Theorem <ref>, we get the following complexity characterisation.

is -complete.

§ CONCLUSION

In the paper, we have developed a relatively simple proof method to show that the satisfiability problems for
,  and  are -complete, see also similar methods in [55, 46].
Our contribution is to establish -hardness, which could be also
shown for several modal logics with propositional quantification
whose respective classes of models are tree-like structures.

Moreover, in the case of fixed degree, we have shown that for all $N \geq 2$,
the satisfiability problem for the variant $\tQCTLEX{,\leq N}$ is -complete.
Whereas -hardness is established by reducing the alternating multi-tiling problem
recently introduced in [11], the -hardness of
is essentially based on the fact that one can enforce concisely that a node has a number
of children equal to some tower of exponentials.

Section <ref> deals with the -completeness of
and , as well as -completeness for
the well-known modal logics , , , and
extended with propositional quantification
but with adequate classes of tree-like structures.
Though the upper bound  for decision problems on trees should not come as a real surprise,
all our -hardness results significantly improve the current state-of-the-art

regarding the fragments of  and for the above-mentioned modal logics.
In particular, our proof technique for -hardness of
(and therefore for on finite trees)
is simple enough so that it could be further reused or adapted, see a recent refinement of the proof in [8].

This work can be continued in several directions.
For instance, -hardness of  is recently refined
in [40, 39] by establishing that already
restricted to formulae of modal/temporal depth two is also
Among the several directions, one of them would be to characterise the expressiveness
of  or  along the lines of [20] or [36], see
also [5].

More generally, we believe that standard modal logics with propositional quantification, but under the
tree semantics, deserve to be much better understood.

§ ACKNOWLEDGEMENTS

We would like to thank the reviewers for the numerous suggestions that help
us to improve the quality of the document.
Bartosz Bednarczyk was supported by the Polish Ministry of Science and
Higher Education programme “Diamentowy Grant” no. DI2017 006447.
Stéphane Demri is supported by the Centre National de la Recherche
Scientifique (CNRS). Furthermore, we would like to thank Raul Fervari
(University of Cordoba) and Alessio Mansutti (University of Oxford)
for many insightful discussions about modal logics with propositional
quantification, modal separation logics and related topics.

[1]
S. Artëmov and L. Beklemishev.
On propositional quantifiers in provability logic.
Notre Dame Journal of Formal Logic, 34(3):401–419, 1993.

[2]
C. Areces, P. Blackburn, and M. Marx.
Complexity of hybrid temporal logics.
Logic Journal of the IGPL, 8(5):653–679, 2000.

[3]
C. Areces, P. Blackburn, and M. Marx.
Hybrid logics: characterization, interpolation and complexity.
The Journal of Symbolic Logic, 66(3):977–1010, 2001.

[4]
G.A. Antonelli and R.H. Thomason.
Representability in second-order propositional poly-modal logic.
The Journal of Symbolic Logic, 67(3):1039–1054, 2002.

[5]
G. Aucher, J. van Benthem, and D. Grossi.
Modal logics of sabotage revisited.
Journal of Logic and Computation, 28(2):269–303, 2018.

[6]
M. Baaz, A. Ciabattoni, and R. Zach.
Quantified propositional Gödel logics.
In LPAR'00, volume 1955 of Lecture Notes in Computer
Science, pages 240–256. Springer, 2000.

[7]
B. Bednarczyk and S. Demri.
Why propositional quantification makes modal logics on trees robustly
In LiCS'19, pages 1–13. IEEE, 2019.

[8]
B. Bednarczyk, S. Demri, R. Fervari, and A. Mansutti.
Modal Logics with Composition on Finite Forests:
Expressivity and Complexity.
In LiCS'20, pages 167–180. ACM, 2020.

[9]
P. Blackburn, M. de Rijke, and Y. Venema.
Modal Logic.
Cambridge University Press, 2001.

[10]
L. Berman.
The complexity of logical theories.
Theoretical Computer Science, 11:71–77, 1980.

[11]
L. Bozzelli, A. Molinari, A. Montanari, and A. Peron.
On the complexity of model checking for syntactically maximal
fragments of the interval temporal logic HS with regular expressions.
In GandALF'17, volume 256 of EPTCS, pages 31–45, 2017.

[12]
J.R. Büchi.
On a decision method in restricted second-order arithmetic.
In Logic, Methodology, and Philosophy of Science, pages 1–11,

[13]
R. Bull.
On modal logic with propositional quantifiers.
The Journal of Symbolic Logic, 34(2):257–263, 1969.

[14]
F. Belardinelli and W. van der Hoek.
A semantical analysis of second-order propositional modal logic.
In AAAI'16, pages 886–892. AAAI Press, 2016.

[15]
F. Belardinelli, W. van der Hoek, and L.B. Kuijer.
Second-order propositional modal logic: Expressiveness and
completeness results.
Artificial Intelligence, 263:3–45, 2018.

[16]
L. Bozzelli, H. van Ditmarsch, and S. Pinchinat.
The complexity of one-agent refinement modal logic.
Theoretical Computer Science, 603:58–83, 2015.

[17]
E. Clarke and A. Emerson.
Design and synthesis of synchronization skeletons using branching
time temporal logic.
In Worshop on Logic of Programs, volume 131 of Lecture
Notes in Computer Science, pages 52–71. Springer, 1981.

[18]
A.K. Chandra, D. Kozen, and L.J. Stockmeyer.
Journal of the ACM, 28(1):114–133, 1981.

[19]
S. Demri, V. Goranko, and M. Lange.
Temporal Logics in Computer Science.
Cambridge University Press, 2016.

[20]
A. David, F. Laroussinie, and N. Markey.
On the expressiveness of QCTL.
In CONCUR'16, volume 59 of LIPIcs, pages 28:1–28:15.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.

[21]
A. Emerson and P. Sistla.
Deciding full branching time logic.
Information and Control, 61:175–201, 1984.

[22]
M. Fattorosi Barnaba and F. De Caro.
Graded modalities.
Studia Logica, 44(2):197–221, 1985.

[23]
K. Fine.
For some proposition and so many possible worlds.
PhD thesis, University of Warwick, 1969.

[24]
K. Fine.
Propositional quantifiers in modal logic.
Theoria, 36:336–346, 1970.

[25]
K. Fine.
In so many possible worlds.
Notre Dame Journal of Formal Logic, 13(4):516–520, 1972.

[26]
J. Ferrante and Ch. Rackoff.
A decision procedure for the first order theory of real addition with
SIAM Journal of Computing, 4(1):69–76, 1975.

[27]
T. French.
Decidability of quantifed propositional branching time logics.
In 14th Australian Joint Conference on Artificial Intelligence,
volume 2256 of Lecture Notes in Computer Science, pages 165–176.
Springer, 2001.

[28]
T. French.
Quantified propositional temporal logic with repeating states.
In TIME-ICTL'03, pages 155–165. IEEE Computer Society, 2003.

[29]
V. Goranko and S. Passy.
Using the universal modality: gains and questions.
Journal of Logic and Computation, 2(1):5–30, 1992.

[30]
D. Kaplan.
S5 with quantifiable propositional variables.
The Journal of Symbolic Logic, 35(2):355, 1970.

[31]
D. Kernberger.
Hybrid Branching-Time Logics.
PhD thesis, University of Kassel, Germany, 2019.
URL: <https://kobra.uni-kassel.de/handle/123456789/11380>.

[32]
Ph. Kremer.
On the complexity of propositional quantification in intuitionistic
The Journal of Symbolic Logic, 62(2):529–544, 1997.

[33]
Ph. Kremer.
Propositional quantification in the topological semantics for S4.
Notre Dame Journal of Formal Logic, 38(2):295–313, 1997.

[34]
M. Kaminski and M. Tiomkin.
The expressive power of second order propositional modal logic.
Notre Dame Journal of Formal Logic, 37(1):35–43, 1996.

[35]
O. Kupferman.
Augmenting branching temporal logics with existential quantification
over atomic propositions.
Journal of Logic and Computation, 9(2):135–147, 1999.

[36]
A. Kuusisto.
Second-order propositional modal logic and monadic alternation
Annals of Pure and Applied Logic, 166(1):1–28, 2015.

[37]
F. Laroussinie and N. Markey.
Quantified CTL: expressiveness and complexity.
Logical Methods in Computer Science, 10(4), 2014.

[38]
F. Laroussinie and N. Markey.
Augmenting ATL with strategy contexts.
Information and Computation, 245:98–123, 2015.

[39]
A. Mansutti.
An Auxiliary Logic on Trees: on the Tower-Hardness of
Logics Featuring Reachability and Submodel Reasoning.
In FoSSaCS'20, volume 12077 of Lecture Notes in Computer
Science, pages 462–481. Springer, 2020.

[40]
A. Mansutti.
Reasoning with Separation Logics: Complexity, Expressive
Power, Proof Systems.
PhD thesis, Université Paris-Saclay, December 2020.

[41]
M. Marx.
Narcissists, stepmothers and spies.
In Workshop on Description Logics (DL'02), volume 53 of CEUR Workshop Proceedings, 2002.

[42]
A.R. Meyer.
Weak second order theory of successor is not elementary-recursive.
Technical Report MAC TM-38, MIT, 1973.
26 pages.

[43]
A. Molinari.
Model Checking: The Interval Way.
PhD thesis, University of Udine, Italy, February 2019.

[44]
A. Meyer and L. Stockmeyer.
Word problems requiring exponential time.
In STOC'73, pages 1–9, 1973.

[45]
A.C. Patthak, I. Bhattacharya, A. Dasgupta, P. Dasgupta, and P.P. Chakrabarti.
Quantified computation tree logic.
Information Processing Letters, 82(3):123–129, 2002.

[46]
I. Pratt-Hartmann, W. Szwast, and L. Tendera.
The fluted fragment revisited.
The Journal of Symbolic Logic, 84(3):1020–1048, 2019.

[47]
M. Rabin.
Decidability of second-order theories and automata on infinite trees.
Transactions of the American Mathematical Society, 41:1–35,

[48]
S. Riedweg and S. Pinchinat.
Quantified mu-calculus for control synthesis.
In MFCS'03, volume 2747 of Lecture Notes in Computer
Science, pages 642–651. Springer, 2003.

[49]
W.J. Savitch.
Relationships between nondeterministic and deterministic tape
JCSS, 4(2):177–192, 1970.

[50]
Ph. Schnoebelen.
The complexity of temporal logic model checking.
In AiML'02, pages 437–459. College Publications, 2003.

[51]
S. Schmitz.
Complexity hierarchies beyond elementary.
ACM Transactions on Computation Theory, 8(1):3:1–3:36, 2016.

[52]
K. Segerberg.
An essay in classical modal logic (three vols.).
Technical Report Filosofiska Studier nr 13, Uppsala Universitet,

[53]
A.P. Sistla.
Theoretical issues in the design and verification of distributed
PhD thesis, Harvard University, 1983.

[54]
C. Smoryński.
Self-reference and Modal Logic.
Springer-Verlag, 1985.

[55]
L. Stockmeyer.
The complexity of decision problems in automata theory and
PhD thesis, Department of Electrical Engineering, MIT, 1974.

[56]
A. Sistla, M. Vardi, and P. Wolper.
The complementation problem for Büchi automata with applications
to temporal logic.
Theoretical Computer Science, 49:217–237, 1987.

[57]
B. ten Cate.
Expressivity of second order propositional modal logic.
Journal of Philosophical Logic, 35(2):209–223, 2006.

[58]
W. Thomas.
Languages, automata, and logic.
In G. Rozenberg and A. Salomaa, editors, Handbook of Formal
Languages, Vol. 3: Beyond Words, pages 389–455. Springer, 1997.

[59]
S. Tobies.
PSPACE reasoning for graded modal logics.
Journal of Logic and Computation, 11:85–106, 2001.

[60]
M. Vardi.
The complexity of relational query languages.
In STOC'82, pages 137–146, 1982.

[61]
P. van Emde Boas.
The convenience of tilings.
In A. Sorbi, editor, Complexity, Logic, and recursion Theory,
volume 187 of Lecture Notes in Pure and Applied Logic, pages 331–363.
Marcel Dekker, Inc., 1997.

[62]
V. Weber.
Hybrid branching-time logics.
CoRR, abs/0708.1723, 2007.

[63]
R. Zach.
Decidability of quantified propositional intuitionistic logic and
S4 on trees of height and arity \(\leq\)\(\omega\).
Journal of Philosophical Logic, 33(2):155–164, 2004.

§ PROOFS  FROM SECTION <REF>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§ PROOFS  FROM SECTION <REF>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ More details on the proof of Lemma <ref>

§ PROOFS  FROM SECTION <REF>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>

§.§ Proof of Lemma <ref>