# Strategy Logic with Imperfect Information

Raphaël Berthon  École Normale Supérieure de RennesComputer Science and
TelecommunicationRennesFrance<EMAIL_ADDRESS>,  Bastien Maubert
0000-0002-9081-2920 Università degli Studi di Napoli “Federico
II”DIETINaplesItaly<EMAIL_ADDRESS>,  Aniello Murano  Università
degli Studi di Napoli “Federico II”DIETINaplesItaly<EMAIL_ADDRESS>,  Sasha
Rubin  Università degli Studi di Napoli “Federico II”DIETINaplesItaly
<EMAIL_ADDRESS>and  Moshe Y. Vardi  Rice UniversityHoustonTexasUSA
<EMAIL_ADDRESS>
(September 2018)

###### Abstract.

We introduce an extension of Strategy Logic for the imperfect-information
setting, called $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$, and study
its model-checking problem. As this logic naturally captures multi-player
games with imperfect information, this problem is undecidable; but we
introduce a syntactical class of “hierarchical instances” for which,
intuitively, as one goes down the syntactic tree of the formula, strategy
quantifications are concerned with finer observations of the model, and we
prove that model-checking $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$
restricted to hierarchical instances is decidable. This result, because it
allows for complex patterns of existential and universal quantification on
strategies, greatly generalises the decidability of distributed synthesis for
systems with hierarchical information. It allows us to easily derive new
decidability results concerning strategic problems under imperfect information
such as the existence of Nash equilibria, or rational synthesis.

To establish this result we go through an intermediary, “low-level” logic much
more adapted to automata techniques. $\textnormal{{QCTL}}^{*}$ is an extension
of $\textnormal{{CTL}}^{*}$ with second-order quantification over atomic
propositions that has been used to study strategic logics with perfect
information. We extend it to the imperfect information setting by
parameterising second-order quantifiers with observations. The simple syntax
of the resulting logic, $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$, allows us to provide a conceptually neat reduction of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ to
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ that separates
concerns, allowing one to forget about strategies and players and focus solely
on second-order quantification. While the model-checking problem of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is, in general,
undecidable, we identify a syntactic fragment of hierarchical formulas and
prove, using an automata-theoretic approach, that it is decidable.

We apply our result to solve complex strategic problems in the imperfect-
information setting. We first show that the existence of Nash equilibria for
deterministic strategies is decidable in games with hierarchical information.
We also introduce distributed rational synthesis, a generalisation of rational
synthesis to the imperfect-information setting. Because it can easily be
expressed in our logic, our main result provides a solution to this problem in
the case of hierarchical information.

strategic reasoning, imperfect information, perfect recall, distributed
synthesis, hierarchical information, Nash equilibria, rational synthesis

††journal: TOCL††copyright: acmlicensed††doi: 0000001.0000001††ccs: Theory of
computation Logic and verification††ccs: Theory of computation Modal and
temporal logics††ccs: Theory of computation Automata over infinite objects

##  1\. Introduction

Temporal logics such as LTL (Pnueli, 1977) or $\textnormal{{CTL}}^{*}$
(Emerson and Halpern, 1986) are extremely successful logics that have been
studied in great detail and extended in many directions along the past
decades, notably in relation with the development of the model-checking
approach to program verification (Clarke et al., 1999). When considering
systems with multiple components such as multi-agent systems or distributed
programs, popular extensions of temporal logics are the family of so-called
_logics for strategic reasoning_ , or _strategic logics_ , which introduce
operators that can express the existence of strategies for components to
ensure that the system’s executions satisfy certain temporal properties.

A fundational logic in this family is Alternating-time Temporal Logic (ATL)
(Alur et al., 2002). It extends $\textnormal{{CTL}}^{*}$ with a coalition
operator $\langle A\rangle\varphi$, where $A$ is a subset of components/agents
of the system, which reads as “coalition $A$ has a strategy to enforce
property $\varphi$ no matter what the other components/agents do”. This logic
is thus quite expressive, as it allows for instance to express the existence
of winning strategies in games played on graphs. However it is not well suited
to reason about other important solution concepts in game theory, such as Nash
equilibria. To address this problem Strategy Logic (SL) was introduced
(Chatterjee et al., 2010a; Mogavero et al., 2014). In SL strategies are
treated as first-order objects, thanks to strategy variables $x$ that can be
quantified upon and bound to players: $\langle\\!\langle x\rangle\\!\rangle$
reads as “there exists a strategy $x$”, and $(a,x)$ reads as “strategy $x$ is
assigned to player $a$”. This leads to a very expressive logic that can
express many solution concepts from game-theory such as best response,
existence of Nash equilibria or subgame-perfect equilibria.

Imperfect information. An essential property of realistic multi-player games
is that players often have a limited view of the system. Such imperfect
information, or partial observation, is usually captured by equipping the
models with equivalence relations $o$ (called _observations_) over the state
space, that specify indistinguishable states. Strategies are then required to
be _uniform_ , i.e., they cannot assign different moves to indistinguishable
situations. Imperfect information is known to make games computationally
harder to solve. For two-player reachability games, Reif showed in (Reif,
1984) that deciding the existence of winning strategies is Exptime -complete
for imperfect information, while it is in Ptime for perfect information. This
result has later been generalised to omega-regular objectives (Berwanger et
al., 2010; Doyen and Raskin, 2011), and adapted to the setting of program
synthesis from temporal specifications (Pnueli and Rosner, 1989; Kupferman and
Vardi, 1999). In the case of multiple players/components/agents, which
interests us here, the situation is even worse: the existence of distributed
winning strategies is undecidable already for two players with incomparable
observation trying to enforce some reachability objective in the presence of
an adversarial third player (Peterson and Reif, 1979), and a similar result
was also proved in the framework of distributed synthesis (Pnueli and Rosner,
1990). Since then, the formal-methods community has spent much effort finding
restrictions and variations that ensure decidability (Kupferman and Vardi,
2001; Pnueli and Rosner, 1990; Gastin et al., 2009; Peterson et al., 2002;
Finkbeiner and Schewe, 2005; Pinchinat and Riedweg, 2005; Schewe and
Finkbeiner, 2007; Berwanger et al., 2018). The common thread in these
approaches is hierarchical information: players can be totally ordered
according to how well they observe the game. Another line of works establishes
that decidability can be retained by forbidding private communication, i.e.,
by considering variants around the idea that all new information should be
public (van der Meyden and Vardi, 1998; van der Meyden and Wilke, 2005;
Ramanujam and Simon, 2010; Belardinelli et al., 2017b, a; Bouyer, 2018).

Strategy Logic with imperfect information. We propose an extension of Strategy
Logic to the imperfect-information setting, which we call
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$. The first step is to choose
how to introduce imperfect information in the logic. In the formal-methods
literature it is typical to associate observations to players. In
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$, instead, we associate
observations to strategies: the strategy quantifier $\langle\\!\langle
x\rangle\\!\rangle{}$ from SL is now parameterised by observation $o$, written
$\langle\\!\langle x\rangle\\!\rangle^{o}$. This novelty allows one to
express, in the logic, that a player’s observation changes over time, to
capture for instance the loss of a sensor resulting in a diminished
observation power. We also add to our logic
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ the outcome quantifier ${\bf
A}$ from Branching-time Strategy Logic (BSL) (Knight and Maubert, 2019), which
quantifies on outcomes of strategies currently used by the agents, and the
unbinding operator $(a,\operatorname{?})$, which frees an agent from her
current strategy. This does not increase the expressivity of the logic but
presents advantages that we discuss in Section 2.2. For instance it allows us
to naturally consider nondeterministic strategies (Strategy Logic only
considers deterministic ones), which in turn allows us to capture module
checking, the extension of model checking to open systems (Kupferman et al.,
2001; Jamroga and Murano, 2014, 2015).

The logic $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ is very powerful:
it is an extension of SL (which considers perfect information), and of the
imperfect-information strategic logics
$\textnormal{{ATL}}^{*}_{\textnormal{\scriptsize i,R}}$ (Bulling and Jamroga,
2014) and $\textnormal{{ATL}}^{*}_{\textnormal{\scriptsize sc,i}}$
(Laroussinie et al., 2015). As already mentioned,
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ can express the distributed
synthesis problem (Pnueli and Rosner, 1990). This problem asks whether there
are strategies for components $a_{1},\dots,a_{n}$ of a distributed system to
enforce some property given as an LTL formula $\psi$ against all behaviours of
the environment. This can be expressed by the
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ formula
$\Phi_{\textsc{Synth}}:=\langle\\!\langle
x_{1}\rangle\\!\rangle^{o_{1}}\dots\langle\\!\langle
x_{n}\rangle\\!\rangle^{o_{n}}(a_{1},x_{1})\dots(a_{n},x_{n}){\bf A}\psi$,
where $o_{i}$ represents the local view of component $a_{i}$. Also,
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ can express more complicated
specifications by alternating quantifiers, binding the same strategy to
different agents and rebinding (these are inherited from SL), as well as
changing observations. For instance, it can express the existence of Nash
equilibria.

Main result. Of course, the high expressivity of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ comes at a cost from a
computational complexity point of view. Its satisfiability problem is
undecidable (this is already true of SL), and so is its model-checking problem
(this is already true of $\textnormal{{ATL}}^{*}_{\textnormal{\scriptsize
i,R}}$ even for the single formula $\langle\\{a,b\\}\rangle{\bf F}p$ (Dima and
Tiplea, 2011), which means that agents $a$ and $b$ have a strategy profile to
reach a situation where $p$ holds). We mentioned that the two main settings in
which decidability is retrieved for distributed synthesis are hierarchical
information and public actions. We extend the first approach to the setting of
strategic logics by introducing a syntactic class of “hierarchical instances”
of $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$, i.e., formula/model
pairs, and proving that the model-checking problem on this class of instances
is decidable. Intuitively, an instance of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ is hierarchical if, as one
goes down the syntactic tree of the formula, the observations annotating
strategy quantifications can only become finer. Although the class of
hierarchical instances refers not only to the syntax of the logic but also to
the model, the class is syntactical in the sense that it depends only on the
structure of the formula and the observations in the model. Moreover, it is
straightforward to check (in linear time) whether an instance is hierarchical
or not.

Applications. Because the syntax of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ allows for arbitrary
alternations of quantifiers in the formulas, our decidability result for
hierarchical instances allows one to decide strategic problems more involved
than module checking and distributed synthesis. For instance, we show in
Section 7 how one can apply our result to establish that the existence of Nash
equilibria is decidable in games with imperfect information, in the case of
hierarchical observations and deterministic strategies. This problem is
relevant as Nash equilibria do not always exist in games with imperfect
information (Filiot et al., 2018). We then consider the problem of rational
synthesis (Fisman et al., 2010; Kupferman et al., 2016; Condurache et al.,
2016; Filiot et al., 2018), both in its cooperative and non-cooperative
variants. We introduce the generalisations of these problems to the case of
imperfect information, and call them cooperative and non-cooperative _rational
distributed synthesis_. We then apply again our main result to establish that
they are decidable in hierarchical systems for deterministic strategies. For
the non-cooperative variant, we need the additional assumption that the
environment is at least as informed as the system. This is the case for
example when one ignores the actual observation power of the environment, and
considers that it plays with perfect information. Doing so yields systems that
are robust to any observation power the environment may have. As Reif puts it,
this amounts to synthesising strategies that are winning even if the opponent
“cheats” and uses information it is not supposed to have access to (Reif,
1984).

Approach. In order to solve the model-checking problem for
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ we introduce an intermediate
logic $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$, an extension to
the imperfect-information setting of $\textnormal{{QCTL}}^{*}$ (Laroussinie
and Markey, 2014), itself an extension of $\textnormal{{CTL}}^{*}$ by second-
order quantifiers over atoms. This is a low-level logic that does not mention
strategies and into which one can effectively compile instances of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$. States of the models of the
logic $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ have internal
structure, much like the multi-player game structures from (Peterson et al.,
2001) and distributed systems (Halpern and Vardi, 1989). Model-checking
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is also undecidable
(indeed, we show how to reduce from the MSO-theory of the binary tree extended
with the equal-length predicate, known to be undecidable (Läuchli and Savioz,
1987)). We introduce the syntactical class
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i,$\tiny{\subseteq}$}}$ of
hierarchical formulas as those in which innermost quantifiers observe more
than outermost quantifiers, and prove that model-checking is decidable using
an extension of the automata-theoretic approach for branching-time logics. We
provide a reduction from model checking
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ to model checking
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ that preserves being
hierarchical, thus establishing our main contribution, i.e., that model
checking the hierarchical instances of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ is decidable.

Complexity. To establish the precise complexity of the problems we solve, we
introduce a new measure on formulas called _simulation depth_. This measure
resembles the notion of alternation depth (see, e.g., (Mogavero et al.,
2014)), which counts alternations between existential and universal strategy
(or second-order) quantifications. But instead of merely counting alternations
between such operators, simulation depth reflects the underlying automata
operations required to treat formulas, while remaining a purely syntactical
notion. We prove that the model-checking problem for the hierarchical fragment
of $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ and
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ are both $(k+1)$-Exptime
-complete for formulas of simulation depth at most $k$. Already for the
perfect-information fragment, this result is more precise than what was
previously known. Indeed, precise upper bounds based on alternation depth were
known for syntactic fragments of SL but not for the full logic (Mogavero et
al., 2014).

Related work. The literature on imperfect information in formal methods and
artificial intelligence is very vast. Imperfect information has been
considered in two-player games (Reif, 1984; Doyen and Raskin, 2011; Berwanger
et al., 2010), module checking (Kupferman et al., 2001; Jamroga and Murano,
2015), distributed synthesis of reactive systems (Pnueli and Rosner, 1990;
Kupferman and Vardi, 2001; Finkbeiner and Schewe, 2005) and strategies in
multiplayer games (Peterson and Reif, 1979; Peterson et al., 2002; Berwanger
et al., 2018), Nash equilibria (Ramanujam and Simon, 2010; Bouyer et al.,
2017; Bouyer, 2018), rational synthesis (Filiot et al., 2018; Gutierrez et
al., 2018), doomsday equilibria (Chatterjee et al., 2017), admissible
strategies (Brenguier et al., 2017), quantitative objectives (Degorre et al.,
2010; Pérez, 2017), and more, some of which we detail below.

Limited alternation of strategy quantification was studied in (Chatterjee and
Doyen, 2014a), in which several decidability results are proved for two and
three alternations of existential and universal quantifiers. Except for one
where the first player has perfect information, all the problems solved in
this work are hierarchical instances, and are thus particular cases of our
main result.

Quantified $\mu$-Calculus with partial observation is studied in (Pinchinat
and Riedweg, 2005), where the model-checking problem is solved by considering
a syntactic constraint based on hierarchical information, as we do for
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$. However they consider
asynchronous perfect recall, and the automata techniques they use to deal with
imperfect information cannot be used in the synchronous perfect-recall setting
that we consider in this work. Similarly the narrowing operation on tree
automata (see Section 4.1), which is crucial in our model-checking procedure,
considers synchronous perfect recall and does not seem easy to adapt to the
asynchronous setting.

A number of works have considered strategic logics with imperfect information.
Various semantics for ATL with imperfect information have been studied in,
e.g., (Jamroga and Bulling, 2011; Jamroga and van der Hoek, 2004). The model-
checking problem for these logics, which is undecidable for agents with
perfect recall (Dima and Tiplea, 2011), has been studied for agents with
bounded memory, for which decidability is recovered (Schobbens, 2004; Lomuscio
and Raimondi, 2006). An epistemic strategic logic with original operators
different from those of ATL and SL is proposed in (Huang and Van Der Meyden,
2014). It considers imperfect information strategies, but only for agents
without memory. Concerning perfect recall, which interest us in this work,
decidability results have also been obtained for ATL (Guelev et al., 2011) and
ATL with strategy context (Laroussinie et al., 2015) when agents have the same
information.

In (Knight and Maubert, 2019), a branching-time variant of SL is extended with
epistemic operators and agents with perfect recall. Strategies are not
required to be uniform in the semantics, but this requirement can be expressed
in the language. However no decidability result is provided. Another variant
of SL extended with epistemic operators and imperfect-information, perfect-
recall strategies is presented in (Belardinelli, 2015), but model checking is
not studied. The latter logic is extended in (Belardinelli et al., 2017a), in
which its model-checking problem is solved on the class of systems where all
agents’ actions are public, which is an assumption orthogonal to hierarchical
information.

The work closest to ours is (Finkbeiner and Schewe, 2010) which introduces a
logic CL in which one can encode many distributed synthesis problems. In this
logic, hierarchical information is a necessary consequence of the syntax and
semantics, and as a result its model-checking problem is decidable. However,
CL is close in spirit to our $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subseteq}$}}$, and its semantics is less intuitive than that of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$. Furthermore, by means of a
natural translation we derive that CL is strictly included in the hierarchical
instances of $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ (Section 6.2).
In particular, hierarchical instances of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ can express non-observable
goals, while CL cannot. When considering players that choose their own goals
it may be natural to assume that they can observe the facts that define
whether their objectives are satisfied or not. But when synthesising programs
for instance, it may be enough that their behaviours enforce the desired
properties, without them having the knowledge that it is enforced. Such non-
observable winning conditions have been studied in, e.g., (Chatterjee and
Doyen, 2010; Degorre et al., 2010; Berwanger et al., 2018).

Outline. In Section 2 we define $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$ and hierarchical instances, and present some examples. In Section 3 we
define $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ and its
hierarchical fragment $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subseteq}$}}$. The proof that model checking
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i,$\tiny{\subseteq}$}}$ is
decidable, including the required automata preliminaries, is in Section 4. The
hierarchy-preserving translation of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ into
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is in Section 5. In
Section 6 we compare $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ with
related logics, and in Section 7 we apply our main result to obtain
decidability results for various strategic problems under imperfect
information. Finally we conclude and discuss future work in Section 8.

##  2\. SL with imperfect information

In this section we introduce $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$, an extension of SL to the imperfect-information setting with
synchronous perfect-recall. Our logic presents several original features
compared to SL, which we discuss in detail in Section 2.3: we introduce an
_outcome quantifier_ akin to the path quantifier in branching-time temporal
logics, we allow for nondeterministic strategies and unbinding agents from
their strategies, and we annotate strategy quantifiers with observation
symbols which denote the information available to strategies. We first fix
some basic notations.

###  2.1. Notations

Let $\Sigma$ be an alphabet. A _finite_ (resp. _infinite_) _word_ over
$\Sigma$ is an element of $\Sigma^{*}$ (resp. $\Sigma^{\omega}$). Words are
written $w=w_{0}w_{1}w_{2}\ldots$, i.e., indexing begins with $0$. The
_length_ of a finite word $w=w_{0}w_{1}\ldots w_{n}$ is $|w|:=n+1$, and
$\mbox{last}(w):=w_{n}$ is its last letter. Given a finite (resp. infinite)
word $w$ and $0\leq i<|w|$ (resp. $i\in\mathbb{N}$), we let $w_{i}$ be the
letter at position $i$ in $w$, $w_{\leq i}$ is the prefix of $w$ that ends at
position $i$ and $w_{\geq i}$ is the suffix of $w$ that starts at position
$i$. We write $w\preccurlyeq w^{\prime}$ if $w$ is a prefix of $w^{\prime}$,
and $\textit{pref}\,(w)$ is the set of finite prefixes of word $w$. Finally,
the domain of a mapping $f$ is written $\textit{dom}(f)$, its codomain
$\textit{codom}(f)$, and for $n\in\mathbb{N}$ we let
$[n]:=\\{i\in\mathbb{N}:1\leq i\leq n\\}$.

###  2.2. Syntax

For the rest of the paper, for convenience we fix a number of parameters for
our logics and models: AP is a finite non-empty set of _atomic propositions_ ,
Ag is a finite non-empty set of _agents_ or _players_ , and Var is a finite
non-empty set of _variables_. The main novelty of our logic is that we specify
which information is available to a strategy, by annotating strategy
quantifiers $\langle\\!\langle x\rangle\\!\rangle$ with _observation symbols_
$o$ from a finite set Obs, that we also fix for the rest of the paper. When we
consider model-checking problems, these data are implicitly part of the input.

###### Definition 2.1 ($\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$
Syntax).

The syntax of $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ is defined by
the following grammar:

$\displaystyle\varphi:=$
$\displaystyle\;p\mid\neg\varphi\mid\varphi\vee\varphi\mid\langle\\!\langle
x\rangle\\!\rangle^{o}\varphi\mid(a,x)\varphi\mid(a,\operatorname{?})\varphi\mid{\bf
E}\psi$ $\displaystyle\psi:=$
$\displaystyle\;\varphi\mid\neg\psi\mid\psi\vee\psi\mid{\bf X}\psi\mid\psi{\bf
U}\psi$

where $p\in\textnormal{AP}$, $x\in\textnormal{Var}$, $o\in\textnormal{Obs}$
and $a\in\textnormal{Ag}$.

Formulas of type $\varphi$ are called _state formulas_ , those of type $\psi$
are called _path formulas_ , and $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$ consists of all the state formulas defined by the grammar.

Boolean operators and temporal operators, ${\bf X}$ (read “next”) and ${\bf
U}$ (read “until”), have the usual meaning. The _strategy quantifier_
$\langle\\!\langle x\rangle\\!\rangle^{o}$ is a first-order-like
quantification on strategies: $\langle\\!\langle
x\rangle\\!\rangle^{o}\varphi$ reads as “there exists a strategy $x$ that
takes decisions based on observation $o$ such that $\varphi$ holds”, where $x$
is a strategy variable. The _binding operator_ $(a,x)$ assigns a strategy to
an agent, and $(a,x)\varphi$ reads as “when agent $a$ plays strategy $x$,
$\varphi$ holds”. The _unbinding operator_ $(a,\operatorname{?})$ instead
releases agent $a$ from her current strategy, if she has one, and
$(a,\operatorname{?})\varphi$ reads as “when agent $a$ is not assigned any
strategy, $\varphi$ holds”. Finally, the _outcome quantifier_ ${\bf E}$
quantifies on outcomes of strategies currently in use: ${\bf E}\psi$ reads as
“$\psi$ holds in some outcome of the strategies currently used by the
players”.

We use abbreviations $\top:=p\vee\neg p$, $\perp:=\neg\top$,
$\varphi\to\varphi^{\prime}:=\neg\varphi\vee\varphi^{\prime}$,
$\varphi\leftrightarrow\varphi^{\prime}:=\varphi\to\varphi^{\prime}\wedge\varphi^{\prime}\to\varphi$
for boolean connectives, ${\bf F}\varphi:=\top{\bf U}\varphi$ (read
“eventually $\varphi$”), ${\bf G}\varphi:=\neg{\bf F}\neg\varphi$ (read
“globally $\varphi$”) for temporal operators,
$[\\![x]\\!]^{o}\varphi:=\neg\langle\\!\langle
x\rangle\\!\rangle^{o}\neg\varphi$ (read “for all strategies $x$ based on
observation $o$, $\varphi$ holds”) and ${\bf A}\psi:=\neg{\bf E}\neg\psi$
(read “all outcomes of the current strategies satisfy $\psi$”).

For every formula $\varphi\in\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$,
we let $\textit{free}\,(\varphi)$ be the set of variables that appear free in
$\varphi$, i.e., that appear out of the scope of a strategy quantifier. A
formula $\varphi$ is a _sentence_ if $\textit{free}\,(\varphi)$ is empty.
Finally, we let the _size_ $|\varphi|$ of a formula $\varphi$ be the number of
symbols in $\varphi$.

###  2.3. Discussion on the syntax

We discuss the syntactic differences between our logic and usual Strategy
Logic.

Outcome quantifier. This quantifier was introduced in Branching-time Strategy
Logic (BSL) (Knight and Maubert, 2019), which corresponds to the perfect-
information fragment of the logic we define here. It removes a quirk of
previous definitions, in which temporal operators could only be evaluated in
contexts where all agents were assigned a strategy. The outcome quantifier,
instead, allows for evaluation of temporal properties on partial assignments.
As a result, the notions of free agents and agent-complete assignments from
previous definitions of Strategy Logic are no longer needed (see, e.g.,
(Mogavero et al., 2014)). In addition, the outcome quantifier highlights the
inherent branching-time nature of Strategy Logic: indeed, in SL, branching-
time properties can be expressed by resorting to artificial strategy
quantifications for all agents. It will also make the correspondence with
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ tighter, which will
allow us to establish the precise complexity of the problem we solve, while
the exact complexity of model checking classic SL with perfect information is
still not known. Finally, since the usual definition of SL requires that the
current strategies define a unique outcome on which linear-time temporal
operators are evaluated, only deterministic strategies were considered. The
introduction of the outcome quantifier allows us to consider nondeterministic
strategies.

Unbinding. With the possibility to evaluate temporal operators even when some
agents are not bound to any strategy, it becomes interesting to include the
unbinding operator $(a,\operatorname{?})$, introduced in (Laroussinie and
Markey, 2015) for ATL with strategy context and also present in BSL. Note that
the outcome quantifier and unbinding operator do not increase the expressivity
of SL, at the level of sentences (Knight and Maubert, 2019).

Observations. In games with imperfect information and ATL-like logics with
imperfect information, a strategy is always bound to some player, and thus it
is clear with regards to what observations it should be defined. In SL on the
other hand, strategy quantification and binding are separate. This adds
expressive power with regards to ATL by allowing, for instance, to assign the
same strategy to two different players, but it also entails that when a
quantification is made on a strategy, one does not know with regards to which
observation this strategy should be defined. We know of three ways to solve
this. One is the approach followed here, which consists in associating with
strategy quantifiers an observation power. The second solution is to abandon
the separation between quantification and binding and to use instead
quantifiers of the form $\exists_{a}$, meaning “there exists a strategy for
player $a$”, like in (Chatterjee et al., 2010b; Belardinelli, 2014): with this
operator, the strategy is immediately bound to player $a$, which indicates
with regards to which observation the strategy should be compatible. The third
one, adopted in (Belardinelli et al., 2017a), consists in requiring that a
strategy be uniform for all agents to whom it will be bound in the formula. We
chose to adopt the first solution for its simplicity and expressiveness.
Indeed the second solution limits expressiveness by disallowing, for instance,
binding the same strategy to different agents. The third solution leads to a
logic that is more expressive than the second one, but less than the first
one. Indeed, the logic that we study here can capture the logic from
(Belardinelli et al., 2017a) (assuming that models contain observations
corresponding to unions of individual observations), and in addition
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ can express changes of
agents’ observation power.

###  2.4. Semantics

The models of $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ are classic
concurrent game structures extended by an interpretation for observation
symbols in Obs.

###### Definition 2.2 ($\textrm{CGS}_{\textnormal{ii}}$ ).

A _concurrent game structure with imperfect information_ (or
$\textrm{CGS}_{\textnormal{ii}}$ for short) is a tuple
$\mathcal{G}=(\textnormal{Ac},V,E,\ell,v_{\iota},\mathcal{O})$ where

  * •

Ac is a finite non-empty set of _actions_ ,

  * •

$V$ is a finite non-empty set of _positions_ ,

  * •

$E:V\times\textnormal{Ac}^{\textnormal{Ag}}\to V$ is a _transition function_ ,

  * •

$\ell:V\to 2^{\textnormal{AP}}$ is a _labelling function_ ,

  * •

$v_{\iota}\in V$ is an _initial position_ , and

  * •

$\mathcal{O}:\textnormal{Obs}\to 2^{V\times V}$ is an _observation
interpretation_.

For $o\in\textnormal{Obs}$, $\mathcal{O}(o)$ is an equivalence relation on
positions, that we may write $\sim_{o}$. It represents what a strategy with
observation $o$ can see: $\mathcal{O}(o)$-equivalent positions are
indistinguishable to such a strategy. Also, $\ell(v)$ is the set of atomic
propositions that hold in position $v$.

We define the size $|\mathcal{G}|$ of a $\textrm{CGS}_{\textnormal{ii}}$
$\mathcal{G}=(\textnormal{Ac},V,E,\ell,v_{\iota},\mathcal{O})$ as the size of
an explicit encoding of the transition function:
$|\mathcal{G}|:=|V|\times|\textnormal{Ac}|^{|\textnormal{Ag}|}\times\lceil\log(|V|)\rceil$.
We may write $v\in\mathcal{G}$ for $v\in V$.

We now introduce a number of notions involved in the semantics of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$. Consider a
$\textrm{CGS}_{\textnormal{ii}}$
$\mathcal{G}=(\textnormal{Ac},V,E,\ell,v_{\iota},\mathcal{O})$.

Joint actions. In a position $v\in V$, each player $a$ chooses an action
$c_{a}\in\textnormal{Ac}$, and the game proceeds to position $E(v,\bm{c})$,
where $\bm{c}\in\textnormal{Ac}^{\textnormal{Ag}}$ stands for the _joint
action_ $(c_{a})_{a\in\textnormal{Ag}}$. Given a joint action
$\bm{c}=(c_{a})_{a\in\textnormal{Ag}}$ and $a\in\textnormal{Ag}$, we let
$\bm{c}_{a}$ denote $c_{a}$.

Plays. A _finite_ (resp. _infinite_) _play_ is a finite (resp. infinite) word
$\rho=v_{0}\ldots v_{n}$ (resp. $\pi=v_{0}v_{1}\ldots$) such that
$v_{0}=v_{\iota}$ and for every $i$ such that $0\leq i<|\rho|-1$ (resp. $i\geq
0$), there exists a joint action $\bm{c}$ such that $E(v_{i},\bm{c})=v_{i+1}$.

Strategies. A (nondeterministic) _strategy_ is a function $\sigma:V^{+}\to
2^{\textnormal{Ac}}\setminus\emptyset$ that maps each finite play to a
nonempty finite set of actions that the player may play. A strategy $\sigma$
is _deterministic_ if for all $\rho$, $\sigma(\rho)$ is a singleton. We let
Str denote the set of all strategies.

Assignments. An _assignment_ is a partial function
$\chi:\textnormal{Ag}\cup\textnormal{Var}\rightharpoonup\mbox{\emph{Str}}$,
assigning to each player and variable in its domain a strategy. For an
assignment $\chi$, a player $a$ and a strategy $\sigma$,
$\chi[a\mapsto\sigma]$ is the assignment of domain
$\textit{dom}(\chi)\cup\\{a\\}$ that maps $a$ to $\sigma$ and is equal to
$\chi$ on the rest of its domain, and $\chi[x\mapsto\sigma]$ is defined
similarly, where $x$ is a variable; also, $\chi[a\mapsto\operatorname{?}]$ is
the restriction of $\chi$ to domain $\textit{dom}(\chi)\setminus\\{a\\}$. In
addition, given a formula
$\varphi\in\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$, an assignment is
_variable-complete for $\varphi$_ if its domain contains all free variables of
$\varphi$.

Outcomes. For an assignment $\chi$ and a finite play $\rho$, we let
$\textnormal{Out}(\chi,\rho)$ be the set of infinite plays that start with
$\rho$ and are then extended by letting players follow the strategies assigned
by $\chi$. Formally, $\textnormal{Out}(\chi,\rho)$ is the set of plays of the
form $\rho\cdot v_{1}v_{2}\ldots$ such that for all $i\geq 0$, there exists
$\bm{c}$ such that for all $a\in\textit{dom}(\chi)\cap\textnormal{Ag}$,
$\bm{c}_{a}\in\chi(a)(\rho\cdot v_{1}\ldots v_{i})$ and
$v_{i+1}=E(v_{i},\bm{c})$,  with  $v_{0}=\mbox{last}(\rho)$.

Synchronous perfect recall. In this work we consider players with _synchronous
perfect recall_ , meaning that each player remembers the whole history of a
play, a classic assumption in games with imperfect information and logics of
knowledge and time. Each observation relation is thus extended to finite plays
as follows: $\rho\sim_{o}\rho^{\prime}$ if $|\rho|=|\rho^{\prime}|$ and
$\rho_{i}\sim_{o}\rho^{\prime}_{i}$ for every $i\in\\{0,\ldots,|\rho|-1\\}$.

Imperfect-information strategies. For $o\in\textnormal{Obs}$, a strategy
$\sigma$ is an _$o$ -strategy_ if $\sigma(\rho)=\sigma(\rho^{\prime})$
whenever $\rho\sim_{o}\rho^{\prime}$. The latter constraint captures the
essence of imperfect information, which is that players can base their
strategic choices only on the information available to them. For
$o\in\textnormal{Obs}$ we let $\mbox{\emph{Str}}_{o}$ be the set of all
$o$-strategies.

###### Definition 2.3 ($\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$
semantics).

The semantics of a state formula is defined on a
$\textrm{CGS}_{\textnormal{ii}}$ $\mathcal{G}$, an assignment $\chi$ that is
variable-complete for $\varphi$, and a finite play $\rho$. For a path formula
$\psi$, the finite play is replaced with an infinite play $\pi$ and an index
$i\in\mathbb{N}$. The definition by mutual induction is as follows:

$\begin{array}[]{lcl}\mathcal{G},\chi,\rho\models p&\text{ if
}&p\in\ell(\mbox{last}(\rho))\\\\[1.0pt]
\mathcal{G},\chi,\rho\models\neg\varphi&\text{ if
}&\mathcal{G},\chi,\rho\not\models\varphi\\\\[1.0pt]
\mathcal{G},\chi,\rho\models\varphi\vee\varphi^{\prime}&\text{ if
}&\mathcal{G},\chi,\rho\models\varphi\;\text{ or
}\;\mathcal{G},\chi,\rho\models\varphi^{\prime}\\\\[1.0pt]
\mathcal{G},\chi,\rho\models\langle\\!\langle
x\rangle\\!\rangle^{o}\varphi&\text{ if
}&\exists\,\sigma\in\mbox{\emph{Str}}_{o}\;\text{ s.t.
}\;\mathcal{G},\chi[x\mapsto\sigma],\rho\models\varphi\\\\[1.0pt]
\mathcal{G},\chi,\rho\models(a,x)\varphi&\text{ if
}&\mathcal{G},\chi[a\mapsto\chi(x)],\rho\models\varphi\\\\[1.0pt]
\mathcal{G},\chi,\rho\models(a,\operatorname{?})\varphi&\text{ if
}&\mathcal{G},\chi[a\mapsto\operatorname{?}],\rho\models\varphi\\\\[1.0pt]
\mathcal{G},\chi,\rho\models{\bf E}\psi&\text{ if }&\text{there exists
}\pi\in\textnormal{Out}(\chi,\rho)\text{ such that
}\mathcal{G},\chi,\pi,|\rho|-1\models\psi\\\\[5.0pt]
\mathcal{G},\chi,\pi,i\models\varphi&\text{ if }&\mathcal{G},\chi,\pi_{\leq
i}\models\varphi\\\\[1.0pt] \mathcal{G},\chi,\pi,i\models\neg\psi&\text{ if
}&\mathcal{G},\chi,\pi,i\not\models\psi\\\\[1.0pt]
\mathcal{G},\chi,\pi,i\models\psi\vee\psi^{\prime}&\text{ if
}&\mathcal{G},\chi,\pi,i\models\psi\;\text{ or
}\;\mathcal{G},\chi,\pi,i\models\psi^{\prime}\\\\[1.0pt]
\mathcal{G},\chi,\pi,i\models{\bf X}\psi&\text{ if
}&\mathcal{G},\chi,\pi,i+1\models\psi\\\\[1.0pt]
\mathcal{G},\chi,\pi,i\models\psi{\bf U}\psi^{\prime}&\text{ if
}&\exists\,j\geq i\mbox{ s.t. }\mathcal{G},\chi,\pi,j\models\psi^{\prime}\\\
&&\text{ and }\forall\,k\text{ s.t. }i\leq
k<j,\;\mathcal{G},\chi,\pi,k\models\psi\end{array}$

######  Remark 1.

Observe that because of the semantics of the outcome quantifier, and unlike
usual definitions of SL, the meaning of an
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ sentence depends on the
assignment in which it is evaluated. For instance the
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ formula ${\bf A}{\bf F}p$ is
clearly a sentence, but whether $\mathcal{G},\chi,\rho\models{\bf A}{\bf F}p$
holds or not depends on which agents are bound to a strategy in $\chi$ and
what these strategies are. However, as usual, a sentence does not require an
assignment to be evaluated, and for an
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ sentence $\varphi$ we let
$\mathcal{G},\rho\models\varphi$ if $\mathcal{G},\emptyset,\rho\models\varphi$
for the empty assignment $\emptyset$, and we write $\mathcal{G}\models\varphi$
if $\mathcal{G},v_{\iota}\models\varphi$.

SL is the fragment of $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$
obtained by interpreting all observation symbols as the identity relation
(which models perfect information), restricting to deterministic strategies,
and considering only assignments in which each agent has a strategy (in this
case the outcome of an assignment consists of a single play; one can thus get
rid of the outcome quantifier and evaluate temporal operators in the unique
outcome of the current assignment, as usually done in SL). Also,
$\textnormal{{CTL}}^{*}$ is the fragment of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ which uses no binding,
unbinding or strategy quantification.

###  2.5. Discussion on the semantics

We now discuss some aspects of the semantics.

Evaluation on finite plays. Unlike previous definitions of Strategy Logic, we
evaluate formulas on finite plays (instead of positions), where the finite
play represents the whole history starting from the initial position of the
$\textrm{CGS}_{\textnormal{ii}}$ in which the formula is evaluated. There are
several reasons to do so. First, it allows us to define the semantics more
simply without having to resort to the notion of assignment translations.
Second, it makes it easier to see the correctness of the reduction to
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$, that we present in
Section 5. In SL, a strategy only has access to the history of the game
starting from the point where the strategy quantifier from which it arises has
been evaluated. In contrast, in $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$ strategies have access to the whole history, starting from the initial
position. However this does not affect the semantics, in the sense that the
perfect-information fragment of $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$ with deterministic strategies corresponds to SL. Indeed, when agents
have perfect information, having access to the past or not does not affect the
existence of strategies to enforce temporal properties that only concern the
future.

Players not remembering their actions. Our definition of synchronous perfect
recall only considers the sequence of positions in finite plays, and forgets
about actions taken by players. In particular, it is possible in this
definition that a player cannot distinguish between two finite plays in which
she plays different actions. This definition is standard in games with
imperfect information (van der Meyden and Wilke, 2005; Berwanger et al., 2010;
Doyen and Raskin, 2011; Berwanger et al., 2018), since remembering one’s
actions or not is indifferent for the existence of distributed winning
strategies or Nash equilibria. However it makes a difference for some more
involved solution concepts that are expressible in strategic logics such as
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$. For instance it is observed
in (Bouyer, 2017, Appendix A) that some games admit subgame-perfect equilibria
only if agents remember their own past actions. Nonetheless we consider the
setting where agents do not remember their actions, as it is the most general.
Indeed, as noted in (Chatterjee and Doyen, 2014b, Remark 2.1, p.8), one can
simulate agents that remember their own actions by storing in positions of the
game the information of the last joint move played (this may create
$|\textnormal{Ac}|^{|\textnormal{Ag}|}$ copies of each position, but the
branching degree is unchanged). One can then adapt indistinguishability
relations to take actions into account. For instance, for an observation
symbol $o$ and an agent $a$, one could consider a new observation symbol
$o_{a}$ that would be interpreted in the enriched game structure as the
refinement of $\sim_{o}$ that considers two positions indistinguishable if
they are indistinguishable for $\sim_{o}$ and contain the same last action for
agent $a$. Binding agent $a$ only to strategies that use observation of the
form $o_{a}$ for some $o$ captures the fact that agent $a$ remembers her
actions.

Agents changing observation. In $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$ observations are not bound to agents but to strategies. And because
agents can change their strategy thanks to the binding operator, it follows
that they can change observation, or more precisely they can successively play
with strategies that have different observations. For instance consider a
controller that observes a system through a set of $n$ sensors
$S=\\{s_{1},\ldots,s_{n}\\}$ as in, e.g., (Bittner et al., 2012). Let $o_{i}$
be the observation power provided by the set of sensors
$S\setminus\\{s_{i}\\}$ (one can think of a system where states are tuples of
local states, each sensor observing one component). Also let $o$ be the
observation power provided by the full set $S$ of sensors, and let atom
$\text{fault}_{i}$ represent the fact that a fault occurs on sensor $s_{i}$.
The formula

$\varphi:=\langle\\!\langle x\rangle\\!\rangle^{o}(a,x){\bf A}{\bf
G}\left(\text{safe}\wedge\bigwedge_{i=1}^{n}\text{fault}_{i}\to\langle\\!\langle
x\rangle\\!\rangle^{o_{i}}(a,x){\bf A}{\bf G}\text{\,safe}_{i}\right)$

expresses that the controller $a$ has a strategy (which uses all sensors in
$S$) to maintain the system safe, and if a sensor is lost, it can respond by
switching to a strategy using the remaining sensors to maintain some
alternative, possibly weaker, security requirement $\text{safe}_{i}$.

###  2.6. Model checking and hierarchical instances

We now introduce the main decision problem of this paper, which is the model-
checking problem for $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$. An
_$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ -instance_ is a model
together with a formula, i.e., it is a pair $(\mathcal{G},\Phi)$ where
$\mathcal{G}$ is a $\textrm{CGS}_{\textnormal{ii}}$ and
$\Phi\in\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$.

###### Definition 2.4 (Model checking
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$).

The _model-checking problem_ for $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$ is the decision problem that, given an
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$-instance
$(\mathcal{G},\Phi)$, returns ‘Yes’ if $\mathcal{G}\models\Phi$, and ‘No’
otherwise.

It is well known that deciding the existence of winning strategies in multi-
player games with imperfect information is undecidable for reachability
objectives (Peterson et al., 2001). Since this problem is easily reduced to
the model-checking problem for $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$, we get the following result.

###### Theorem 2.5.

The model-checking problem for $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$ is undecidable.

Hierarchical instances. We now isolate a sub-problem obtained by restricting
attention to _hierarchical instances_. Intuitively, an
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$-instance
$(\mathcal{G},\Phi)$ is hierarchical if, as one goes down a path in the
syntactic tree of $\Phi$, the observations tied to quantifications become
finer.

###### Definition 2.6 (Hierarchical instances).

An $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$-instance
$(\mathcal{G},\Phi)$ is _hierarchical_ if for every subformula
$\varphi_{1}=\langle\\!\langle y\rangle\\!\rangle^{o_{1}}\varphi^{\prime}_{1}$
of $\Phi$ and subformula $\varphi_{2}=\langle\\!\langle
x\rangle\\!\rangle^{o_{2}}\varphi^{\prime}_{2}$ of $\varphi^{\prime}_{1}$, it
holds that $\mathcal{O}(o_{2})\subseteq\mathcal{O}(o_{1})$.

If $\mathcal{O}(o_{2})\subseteq\mathcal{O}(o_{1})$ we say that $o_{2}$ is
_finer_ than $o_{1}$ in $\mathcal{G}$, and that $o_{1}$ is _coarser_ than
$o_{2}$ in $\mathcal{G}$. Intuitively, this means that a player with
observation $o_{2}$ observes game $\mathcal{G}$ no worse than, i.e., knows at
least as much as a player with observation $o_{1}$.

######  Remark 2.

If one uses the trick described in Section 2.5 to model agents that remember
their own actions, then for an agent $a$ to know at least as much as another
agent $b$ it needs to be the case that, in particular, agent $a$ observes all
actions played by agent $b$.

###### Example 2.7 (Fault-tolerant diagnosibility).

Consider the following formula from Section 2.5:

$\varphi:=\langle\\!\langle x\rangle\\!\rangle^{o}(a,x){\bf A}{\bf
G}\left(\text{safe}\wedge\bigwedge_{i=1}^{n}\text{fault}_{i}\to\langle\\!\langle
x\rangle\\!\rangle^{o_{i}}(a,x){\bf A}{\bf G}\text{\,safe}_{i}\right)$

As already discussed, it expresses that the controller can react to the loss
of a sensor to keep ensuring some property of the system. Clearly, the
controller’s observation $o_{i}$ after the loss of sensor $i$ is coarser than
its original observation $o$, and thus formula $\varphi$ in such a system does
not form a hierarchical instance.

We now give an example of scenario where hierarchical instances occur
naturally.

###### Example 2.8 (Security levels).

Consider a system with different “security levels”, where higher levels have
access to more data (i.e., can observe more). Assume that the
$\textrm{CGS}_{\textnormal{ii}}$ $\mathcal{G}$ is such that
$\mathcal{O}(o_{n})\subseteq\mathcal{O}(o_{n-1})\subseteq\ldots\subseteq\mathcal{O}(o_{1})$:
in other words, level $n$ has the highest security clearance, while level $1$
has the lowest. Consider that agent $a$ wants to reach some objective marked
by atom “goal”, that it starts with the lowest observation clearance $o_{1}$,
and that atomic formula “$\text{promote}_{i}$” means that the agent is granted
access to level $i$ (observe that whenever we have $\text{promote}_{i}$, we
should also have $\text{promote}_{j}$ for all $j<i$). For every $i$ we let

$\varphi_{i}(\varphi^{\prime}):=\text{goal}\vee(\text{promote}_{i}\wedge\langle\\!\langle
x\rangle\\!\rangle^{o_{i}}(a,x){\bf A}{\bf F}\varphi^{\prime})$

Now the formula

$\varphi:=\varphi_{1}(\varphi_{2}(\ldots\varphi_{n-1}(\varphi_{n}(\text{goal}))\ldots))$

means that agent $a$ can enforce her goal, possibly by first getting access to
higher security levels and using this additional observation power to reach
the goal. Because the strategy quantifications that are deeper in the formula
have access to more information, this formula forms a hierarchical instance in
$\mathcal{G}$.

Here is the main contribution of this work:

###### Theorem 2.9.

The model-checking problem for $\textnormal{{SL}}_{\textnormal{\scriptsize
ii}}$ restricted to the class of hierarchical instances is decidable.

We prove this result in Section 5 by reducing it to the model-checking problem
for the hierarchical fragment of a logic called $\textnormal{{QCTL}}^{*}$ with
imperfect information, which we now introduce and study in order to use it as
an intermediate, “low-level” logic between tree automata and
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$. We then discuss some
applications of this theorem in Section 7.

##  3\. $\textnormal{{QCTL}}^{*}$ with imperfect information

In this section we introduce an imperfect-information extension of
$\textnormal{{QCTL}}^{*}$ (Sistla, 1983; Kupferman, 1999; Kupferman et al.,
2000a; French, 2001; Laroussinie and Markey, 2014), which is an extension of
$\textnormal{{CTL}}^{*}$ with second-order quantification on atomic
propositions. In order to introduce imperfect information, instead of
considering equivalence relations between states as in concurrent game
structures, we will enrich Kripke structures by giving internal structure to
their states, i.e., we see states as $n$-tuples of local states. This way of
modelling imperfect information is inspired from Reif’s multi-player game
structures (Peterson et al., 2001) and distributed systems (Halpern and Vardi,
1989), and we find it very suitable to application of automata techniques, as
discussed in Section 3.3.

The syntax of $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is
similar to that of $\textnormal{{QCTL}}^{*}$, except that we annotate second-
order quantifiers by subsets $\textnormal{{o}}\subseteq[n]$. The idea is that
quantifiers annotated by o can only “observe” the local states indexed by
$i\in\textnormal{{o}}$. We define the tree-semantics of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$: this means that we
interpret formulas on trees that are the unfoldings of Kripke structures (this
will capture the fact that players in
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$ have synchronous perfect
recall). We then define the syntactic class of _hierarchical formulas_ and
prove, using an automata-theoretic approach, that model checking this class of
formulas is decidable.

For the rest of the section we fix some natural number $n\in\mathbb{N}$ which
parameterises the logic $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$, and which is the number of components in states of the models.

###  3.1. $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ Syntax

The syntax of $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is very
similar to that of $\textnormal{{QCTL}}^{*}$: the only difference is that we
annotate quantifiers by a set of indices that defines the “observation” of
that quantifier.

Concrete observations. A set $\textnormal{{o}}\subseteq[n]$ is called a
_concrete observation_ (to distinguish it from observations $o$ in the
definitions of $\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$).

###### Definition 3.1 ($\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$
Syntax).

The syntax of $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is
defined by the following grammar:

$\displaystyle\varphi:=$
$\displaystyle\;p\mid\neg\varphi\mid\varphi\vee\varphi\mid{\bf
E}\psi\mid\exists^{\textnormal{{o}}}p.\,\varphi$ $\displaystyle\psi:=$
$\displaystyle\;\varphi\mid\neg\psi\mid\psi\vee\psi\mid{\bf X}\psi\mid\psi{\bf
U}\psi$

where $p\in\textnormal{AP}$ and $\textnormal{{o}}\subseteq[n]$.

Formulas of type $\varphi$ are called _state formulas_ , those of type $\psi$
are called _path formulas_ , and
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ consists of all the
state formulas defined by the grammar. We use standard abbreviation ${\bf
A}\psi:=\neg{\bf E}\neg\psi$. We also use $\exists p.\,\varphi$ as a shorthand
for $\exists^{[n]}p.\,\varphi$, and we let $\forall p.\,\varphi:=\neg\exists
p.\,\neg\varphi$.

Given a $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ formula
$\varphi$, we define the set of _quantified propositions_
${\textnormal{AP}_{\exists}}(\varphi)\subseteq\textnormal{AP}$ as the set of
atomic propositions $p$ such that $\varphi$ has a subformula of the form
$\exists^{\textnormal{{o}}}p.\,\varphi$. We also define the set of _free
propositions_ $\textnormal{AP}_{f}(\varphi)\subseteq\textnormal{AP}$ as the
set of atomic propositions that have an occurrence which is not under the
scope of any quantifier of the form $\exists^{\textnormal{{o}}}p.\,$ Observe
that ${\textnormal{AP}_{\exists}}(\varphi)\cap\textnormal{AP}_{f}(\varphi)$
may not be empty, i.e., a proposition may appear both free and quantified in
(different places of) a formula.

###  3.2. $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ semantics

Several semantics have been considered for $\textnormal{{QCTL}}^{*}$, the two
most studied being the _structure semantics_ and the _tree semantics_ (see
(Laroussinie and Markey, 2014) for more details). For the semantics of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ we adapt the tree
semantics, and we explain the reasons for doing so in Section 3.3.

As already mentioned, for $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$ we consider structures whose states are tuples of local states. We now
define these structures and related notions.

###### Definition 3.2 (Compound Kripke structures).

A _compound Kripke structure_ , or CKS , over AP is a tuple
$\mathcal{S}=(S,R,\ell,s_{\iota})$ where

  * •

$S\subseteq\prod_{i\in[n]}L_{i}$ is a set of _states_ , with
$\\{L_{i}\\}_{i\in[n]}$ a family of $n$ disjoint finite sets of _local states_
,

  * •

$R\subseteq S\times S$ is a left-total111i.e., for all $s\in S$, there exists
$s^{\prime}$ such that $(s,s^{\prime})\in R$. _transition relation_ ,

  * •

$\ell:S\to 2^{\textnormal{AP}}$ is a _labelling function_ and

  * •

$s_{\iota}\in S$ is an _initial state_.

A _path_ in $\mathcal{S}$ is an infinite sequence of states
$\lambda=s_{0}s_{1}\ldots$ such that for all $i\in\mathbb{N}$,
$(s_{i},s_{i+1})\in R$. A _finite path_ is a finite non-empty prefix of a
path. We may write $s\in\mathcal{S}$ for $s\in S$, and we define the _size_
$|\mathcal{S}|$ of a CKS $\mathcal{S}=(S,R,s_{\iota},\ell)$ as its number of
states: $|\mathcal{S}|:=|S|$.

Since we will interpret $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$ on unfoldings of CKS , we now define infinite trees.

Trees. In many works, trees are defined as prefix-closed sets of words with
the empty word $\epsilon$ as root. Here trees represent unfoldings of Kripke
structures, and we find it more convenient to see a node $u$ as a sequence of
states and the root as the initial state. Let $X$ be a finite set of
_directions_ (typically a set of states). An _$X$ -tree_ $\tau$ is a nonempty
set of words $\tau\subseteq X^{+}$ such that:

  * •

there exists $r\in X$, called the _root_ of $\tau$, such that each $u\in\tau$
starts with $r$ ($r\preccurlyeq u$);

  * •

if $u\cdot x\in\tau$ and $u\cdot x\neq r$, then $u\in\tau$,

  * •

if $u\in\tau$ then there exists $x\in X$ such that $u\cdot x\in\tau$.

The elements of a tree $\tau$ are called _nodes_. If $u\cdot x\in\tau$, we say
that $u\cdot x$ is a _child_ of $u$. The _depth_ of a node $u$ is $|u|$. An
$X$-tree $\tau$ is _complete_ if for every $u\in\tau$ and $x\in X$, $u\cdot
x\in\tau$. A _path_ in $\tau$ is an infinite sequence of nodes
$\lambda=u_{0}u_{1}\ldots$ such that for all $i\in\mathbb{N}$, $u_{i+1}$ is a
child of $u_{i}$, and $Paths(u)$ is the set of paths that start in node $u$.

Labellings. An _AP -labelled $X$-tree_, or _$(\textnormal{AP},X)$ -tree_ for
short, is a pair $t=(\tau,\ell)$, where $\tau$ is an $X$-tree called the
_domain_ of $t$ and $\ell:\tau\rightarrow 2^{\textnormal{AP}}$ is a
_labelling_ , which maps each node to the set of propositions that hold there.
For $p\in\textnormal{AP}$, a _$p$ -labelling_ for a tree is a mapping
$\ell_{p}:\tau\to\\{0,1\\}$ that indicates in which nodes $p$ holds, and for a
labelled tree $t=(\tau,\ell)$, the $p$-labelling of $t$ is the $p$-labelling
$u\mapsto 1$ if $p\in\ell(u)$, 0 otherwise. The composition of a labelled tree
$t=(\tau,\ell)$ with a $p$-labelling $\ell_{p}$ for $\tau$ is defined as
$t\otimes\ell_{p}:=(\tau,\ell^{\prime})$, where
$\ell^{\prime}(u)=\ell(u)\cup\\{p\\}$ if $\ell_{p}(u)=1$, and
$\ell(u)\setminus\\{p\\}$ otherwise. A $p$-labelling for a labelled tree
$t=(\tau,\ell)$ is a $p$-labelling for its domain $\tau$. A _pointed labelled
tree_ is a pair $(t,u)$ where $u$ is a node of $t$.

If $u=w\cdot x$, the _subtree_ $t_{u}$ of $t=(\tau,\ell)$ is defined as
$t_{u}:=(\tau_{u},\ell_{u})$ with $\tau_{u}=\\{x\cdot w^{\prime}\mid w\cdot
x\cdot w^{\prime}\in\tau\\}$, and $\ell_{u}(x\cdot w^{\prime})=\ell(w\cdot
x\cdot w^{\prime})$. A labelled tree is _regular_ if it has finitely many
disctinct subtrees.

In the tree semantics of $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$ that we consider here, formulas are evaluated on tree unfoldings of CKS
, which we now define.

Tree unfoldings. Let $\mathcal{S}=(S,R,\ell,s_{\iota})$ be a compound Kripke
structure over AP. The _tree-unfolding of $\mathcal{S}$_ is the
$(\textnormal{AP},S)$-tree $t_{\mathcal{S}}:=(\tau,\ell^{\prime})$, where
$\tau$ is the set of all finite paths that start in $s_{\iota}$, and for every
$u\in\tau$, $\ell^{\prime}(u):=\ell(\mbox{last}(u))$.

Note that a labelled tree is regular if and only if it is the unfolding of
some finite Kripke structure.

Narrowing. Let $X$ and $Y$ be two finite sets, and let $(x,y)\in X\times Y$.
The _$X$ -narrowing_ of $(x,y)$ is ${(x,y)\\!\downarrow_{X}}:=x$. This
definition extends naturally to words and trees over $X\times Y$ (point-wise).

Given a family of (disjoint) sets of local states $\\{L_{i}\\}_{i\in[n]}$ and
a subset $I\subseteq[n]$, we let $L_{I}:=\prod_{i\in I}L_{i}$ if
$I\neq\emptyset$ and $L_{\emptyset}:=\\{\mathbf{0}\\}$, where $\mathbf{0}$ is
a special symbol. For $I,J\subseteq[n]$ and $z\in L_{I}$, we also define
${z\\!\downarrow_{J}}:=z\\!\downarrow_{L_{I\cap J}}$, where $z$ is seen as a
pair $z=(x,y)\in L_{I\cap J}\times L_{I\setminus J}$, i.e., we apply the above
definition with $X=L_{I\cap J}$ and $Y=L_{I\setminus J}$. This is well defined
because having taken sets $L_{i}$ to be disjoint, the ordering of local states
in $z$ is indifferent. We also extend this definition to words and trees. In
particular, for every $L_{I}$-tree $\tau$, $\tau\\!\downarrow_{\emptyset}$ is
the only $L_{\emptyset}$-tree, $\mathbf{0}^{\omega}$.

Quantification and uniformity. In
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$
$\exists^{\textnormal{{o}}}p.\,\varphi$ holds in a tree $t$ if there is some
o-uniform $p$-labelling of $t$ such that $t$ with this $p$-labelling satisfies
$\varphi$. Intuitively, a $p$-labelling of a tree is o-uniform if every two
nodes that are indistinguishable for observation o agree on $p$.

###### Definition 3.3 (o-indistinguishability and o-uniformity in $p$).

Fix $\textnormal{{o}}\subseteq[n]$ and $I\subseteq[n]$.

  * •

Two tuples $x,x^{\prime}\in L_{I}$ are _o -indistinguishable_, written
$x\approx_{\textnormal{{o}}}x^{\prime}$, if
$x\\!\downarrow_{\textnormal{{o}}}=x^{\prime}\\!\downarrow_{\textnormal{{o}}}$.

  * •

Two words $u=u_{0}\ldots u_{i}$ and $u^{\prime}=u^{\prime}_{0}\ldots
u^{\prime}_{j}$ over alphabet $L_{I}$ are _o -indistinguishable_, written
$u\approx_{\textnormal{{o}}}u^{\prime}$, if $i=j$ and for all
$k\in\\{0,\ldots,i\\}$ we have
$u_{k}\approx_{\textnormal{{o}}}u^{\prime}_{k}$.

  * •

A $p$-labelling for a tree $\tau$ is _o -uniform_ if for all
$u,u^{\prime}\in\tau$, $u\approx_{\textnormal{{o}}}u^{\prime}$ implies
$\ell_{p}(u)=\ell_{p}(u^{\prime})$.

###### Definition 3.4 ($\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$
semantics).

We define by induction the satisfaction relation $\models$ of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$. Let $t=(\tau,\ell)$
be an AP-labelled $L_{I}$-tree, $u$ a node and $\lambda$ a path in $\tau$:

$\displaystyle t,u\models$ $\displaystyle\,p$ if $\displaystyle\quad
p\in\ell(u)$ $\displaystyle t,u\models$ $\displaystyle\,\neg\varphi$ if
$\displaystyle\quad t,u\not\models\varphi$ $\displaystyle t,u\models$
$\displaystyle\,\varphi\vee\varphi^{\prime}$ if $\displaystyle\quad
t,u\models\varphi\mbox{ or }t,u\models\varphi^{\prime}$ $\displaystyle
t,u\models$ $\displaystyle\,{\bf E}\psi$ if
$\displaystyle\quad\exists\,\lambda\in Paths(u)\mbox{ s.t.
}t,\lambda\models\psi$ $\displaystyle t,u\models$
$\displaystyle\,\exists^{\textnormal{{o}}}p.\,\varphi$ if
$\displaystyle\quad\exists\,\ell_{p}\mbox{ a $\textnormal{{o}}$-uniform
$p$-labelling for $t$ such that }t\otimes\ell_{p},u\models\varphi$
$\displaystyle t,\lambda\models$ $\displaystyle\,\varphi$ if
$\displaystyle\quad t,\lambda_{0}\models\varphi$ $\displaystyle
t,\lambda\models$ $\displaystyle\,\neg\psi$ if $\displaystyle\quad
t,\lambda\not\models\psi$ $\displaystyle t,\lambda\models$
$\displaystyle\,\psi\vee\psi^{\prime}\quad$ if $\displaystyle\quad
t,\lambda\models\psi\mbox{ or }t,\lambda\models\psi^{\prime}$ $\displaystyle
t,\lambda\models$ $\displaystyle\,{\bf X}\psi$ if $\displaystyle\quad
t,\lambda_{\geq 1}\models\psi$ $\displaystyle t,\lambda\models$
$\displaystyle\,\psi{\bf U}\psi^{\prime}$ if $\displaystyle\quad\exists\,i\geq
0\mbox{ s.t. }t,\lambda_{\geq i}\models\psi^{\prime}\text{ and }\forall
j\text{ s.t. }0\leq j<i,\;t,\lambda_{\geq j}\models\psi$

We write $t\models\varphi$ for $t,r\models\varphi$, where $r$ is the root of
$t$. Given a CKS $\mathcal{S}$ and a
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ formula $\varphi$, we
also write $\mathcal{S}\models\varphi$ if
$\mathcal{S},s_{\iota}\models\varphi$.

###### Example 3.5.

Consider the following CTL formula:

$\mathbf{border}(p):={\bf A}{\bf F}p\wedge{\bf A}{\bf G}(p\rightarrow{\bf
A}{\bf X}{\bf A}{\bf G}\neg p).$

This formula holds in a labelled tree if and only if each path contains
exactly one node labelled with $p$. Now, consider the following
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ formula:

$\mathbf{level}(p):=\exists^{\emptyset}p.\,\mathbf{border}(p).$

For a blind quantifier, two nodes of a tree are indistinguishable if and only
if they have same depth. Therefore, this formula holds on a tree iff the $p$’s
label all and only the nodes at some fixed depth. This formula can thus be
used to capture the equal level predicate on trees. Actually, just as
$\textnormal{{QCTL}}^{*}$ captures MSO, one can prove that
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ with tree semantics
subsumes MSO with equal level (Elgot and Rabin, 1966; Läuchli and Savioz,
1987; Thomas, 1992). In Theorem 3.7 we make use of a similar observation to
prove that model-checking $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$ is undecidable.

###  3.3. Discussion on the definition of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$

We now motivate in detail some aspects of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$.

Modelling of imperfect information. We model imperfect information by means of
local states (rather than equivalence relations) because this greatly
facilitates the use of automata techniques. More precisely, in our decision
procedure of Section 4 we use an operation on tree automata called _narrowing_
, which was introduced in (Kupferman and Vardi, 1999) to deal with imperfect-
information in the context of distributed synthesis for temporal
specifications. Given an automaton $\mathcal{A}$ that works on $X\times
Y$-trees, where $X$ and $Y$ are two finite sets, and assuming that we want to
model an operation performed on trees while observing only the $X$ component
of each node, this narrowing operation allows one to build from $\mathcal{A}$
an automaton $\mathcal{A}^{\prime}$ that works on $X$-trees, such that
$\mathcal{A}^{\prime}$ accepts an $X$-tree if and only if $\mathcal{A}$
accepts its widening to $X\times Y$ (intuitively, this widening is the
$X\times Y$-tree in which each node is labelled as its projection on the
original $X$-tree; see Section 4 for details).

With our definition of compound Kripke structures, their unfoldings are trees
over the Cartesian product $L_{[n]}$. To model a quantification
$\exists^{\textnormal{{o}}}p$ with observation $\textnormal{{o}}\subseteq[n]$,
we can thus use the narrowing operation to forget about components $L_{i}$,
for $i\in[n]\setminus\textnormal{{o}}$. We then use the classic projection of
nondeterministic tree automata to perform existential quantification on atomic
proposition $p$. Since the choice of the $p$-labelling is made directly on
$L_{\textnormal{{o}}}$-trees, it is necessarily o-uniform.

Choice of the tree semantics. The two most studied semantics for
$\textnormal{{QCTL}}^{*}$ are the _structure semantics_ , in which formulas
are evaluated directly on Kripke structures, and the _tree semantics_ , in
which Kripke structures are first unfolded into infinite trees. Tree semantics
thus allows quantifiers to choose the value of a quantified atomic proposition
in each _finite path_ of the model, while in structure semantics the choice is
only made in each state. When $\textnormal{{QCTL}}^{*}$ is used to express
existence of strategies, existential quantification on atomic propositions
labels the structure with strategic choices; in this kind of application,
structure semantics reflects so-called _positional_ or _memoryless_
strategies, while tree semantics captures _perfect-recall_ or _memoryful_
strategies. Since in this work we are interested in perfect-recall strategies,
we only consider the tree semantics.

###  3.4. Model checking $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$

We now define the model-checking problem studied in the rest of this section.

###### Definition 3.6 (Model checking
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$).

The _model-checking problem for
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$_ is the following
decision problem: given an instance $(\mathcal{S},\Phi)$ where $\mathcal{S}$
is a CKS, and $\Phi$ is a $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$ formula, return ‘Yes’ if $\mathcal{S}\models\Phi$ and ‘No’ otherwise.

We now prove that the model-checking problem for
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is undecidable. This
comes as no surprise since, as we will show in Section 5,
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ can express the
existence of distributed winning strategies in imperfect-information games.
However we propose a proof that shows the connection between
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ and MSO with equal-
level predicate (Elgot and Rabin, 1966; Läuchli and Savioz, 1987; Thomas,
1992). This proof also has the benefit of showing that
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is undecidable already
for formulas that involve only propositional quantifiers that observe either
everything or nothing.

###### Theorem 3.7.

The model-checking problem for
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is undecidable.

###### Proof.

Let $\textnormal{{MSO}}_{\textnormal{eq}}$ denote the extension of the logic
MSO (without unary predicates) by a binary predicate symbol eq.
$\textnormal{{MSO}}_{\textnormal{eq}}$ is interpreted on the full binary tree,
and the semantics of $\text{eq}(x,y)$ is that $x$ and $y$ have the same depth
in the tree. We show how to effectively translate
$\textnormal{{MSO}}_{\textnormal{eq}}$ into
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$, and our result
follows since the $\textnormal{{MSO}}_{\textnormal{eq}}$-theory of the binary
tree is undecidable (Läuchli and Savioz, 1987). The translation from
$\textnormal{{MSO}}_{\textnormal{eq}}$ to
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is obtained by
extending that from MSO to QCTL (Laroussinie and Markey, 2014), using the
formula $\mathbf{level}(\cdot)$ from Example 3.5 to help capture the equal-
length predicate.

We define a translation $\widehat{\quad}$ from
$\textnormal{{MSO}}_{\textnormal{eq}}$ to
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ such that for every
tree $t$ with root $r$, nodes $u_{1},\ldots,u_{i}\in t$ and sets of nodes
$U_{1},\ldots,U_{j}\subseteq t$, and every
$\textnormal{{MSO}}_{\textnormal{eq}}$ formula
${\varphi(x,x_{1},\ldots,x_{i},X_{1},\ldots,X_{j})}$, we have that

(1)
$t,r,u_{1},\ldots,u_{i},U_{1},\ldots,U_{j}\models\varphi(x,x_{1},\ldots,x_{i},X_{1},\ldots,X_{j})\text{\quad
if and only if \quad}\widehat{t},r\models\widehat{\varphi}$

where $\widehat{t}$ is obtained from $t$ by defining the labelling for fresh
atomic propositions $p_{x_{k}}$ and $p_{X_{k}}$, with $k\in[i]$, as follows:
$p_{x_{k}}\in\widehat{\ell}(u)$ if $u=u_{k}$ and
$p_{X_{k}}\in\widehat{\ell}(u)$ if $u\in U_{k}$.

The translation of MSO to $\textnormal{{QCTL}}^{*}$ from (Laroussinie and
Markey, 2014) can be extended to one from
$\textnormal{{MSO}}_{\textnormal{eq}}$ to
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ by adding rules for
the equal level predicate. Indeed, for
$\varphi(x,x_{1},\ldots,x_{i},X_{1},\ldots,X_{j})\in\textnormal{{MSO}}_{\textnormal{eq}}$,
we inductively define the $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$ formula $\widehat{\varphi}$ as follows, where $k\in[i]$:

$\begin{array}[]{rclcrcl}\widehat{x=x_{k}}&:=&p_{x_{k}}&&\widehat{x_{k}=x_{l}}&:=&{\bf
E}{\bf F}(p_{x_{k}}\wedge p_{x_{l}})\\\\[5.0pt] \widehat{x\in
X_{k}}&:=&p_{X_{k}}&&\widehat{x_{k}\in X_{l}}&:=&{\bf E}{\bf
F}(p_{x_{k}}\wedge p_{X_{l}})\\\\[5.0pt]
\widehat{\neg\varphi^{\prime}}&:=&\neg\widehat{\varphi^{\prime}}&&\widehat{\varphi_{1}\vee\varphi_{2}}&:=&\widehat{\varphi_{1}}\vee\widehat{\varphi_{2}}\\\\[5.0pt]
\widehat{\exists x_{k}.\varphi^{\prime}}&:=&\lx@intercol\exists
<EMAIL_ADDRESS>\widehat{\exists X_{k}.\varphi^{\prime}}&:=&\lx@intercol\exists
<EMAIL_ADDRESS>\widehat{S(x,x_{k})}&:=&{\bf E}{\bf
X}p_{x_{k}}&&\widehat{S(x_{k},x)}&:=&\perp\\\\[5.0pt]
\widehat{S(x_{k},x_{l})}&:=&\lx@intercol{\bf E}{\bf F}(p_{x_{k}}\wedge{\bf
E}{\bf X}p_{x_{l}})\hfil\lx@intercol\end{array}$

where $\mathrm{uniq}(p):={\bf E}{\bf F}p\wedge\forall q.\;\left({\bf E}{\bf
F}(p\wedge q)\rightarrow{\bf A}{\bf G}(p\rightarrow q)\right)$ holds in a tree
iff it has exactly one node labelled with $p$. To understand the $x=x_{k}$ and
$x\in X_{k}$ cases, consider that $x$ will be interpreted as the root. For the
$S(x_{k},x)$ case, observe that $x$ has no incoming edge since it is
interpreted as the root. Second-order quantification $\exists X_{k}$ is
translated into quantification on atomic proposition $p_{X_{k}}$, and first-
order quantification $\exists x_{k}$ is treated similarly, with the additional
constraint that quantification is limited to $p_{x_{k}}$-labellings that set
$p_{x_{k}}$ to true in one and only one node of the tree.

The rules for eq are as follows:

$\displaystyle\widehat{\text{eq}(x,x_{k})}$ $\displaystyle:=p_{x_{k}}$
$\displaystyle\widehat{\text{eq}(x_{k},x_{l})}$
$\displaystyle:=\exists^{\emptyset}p.\,\mathbf{border}(p)\wedge{\bf A}{\bf
G}(p_{x_{k}}\rightarrow p\wedge p_{x_{l}}\rightarrow p)$

To understand the first case, observe that since $x$ is interpreted as the
root, $x_{k}$ is on the same level as $x$ if and only if it is also assigned
the root. For the second case, recall from Example 3.5 that the
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ formula
$\exists^{\emptyset}p.\,\mathbf{border}(p)$ places one unique horizontal line
of $p$’s in the tree, and thus requiring that $x_{k}$ and $x_{l}$ be both on
this line ensures that they are on the same level. The correctness of the
translation follows from (1), which is proven by induction.

Now take an instance $(t,\varphi(x))$ of the model-checking problem for
$\textnormal{{MSO}}_{\textnormal{eq}}$ on the full binary tree $t$. Let
$\mathcal{S}$ be a CKS with two states $s_{0}$ and $s_{1}$ (local states are
irrelevant here), whose transition relation is the complete relation, and with
empty labelling function. Clearly, $t_{\mathcal{S}}=t$, and applying (1) we
get:

$t,s_{0}\models\varphi(x)\text{\quad
iff\quad}\widehat{t},s_{0}\models\widehat{\varphi}.$

Observe that in the previous line, because there are no free variables besides
$x$, which stands for the root, we have that $\widehat{t}=t=t_{\mathcal{S}}$,
hence we have indeed produced an instance of the model-checking problem for
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$. ∎

##  4\. A decidable fragment of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$: hierarchy on
observations

The main result of this section is the identification of an important
decidable fragment of $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$.

###### Definition 4.1 (Hierarchical formulas).

A $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ formula $\varphi$ is
_hierarchical_ if for all subformulas
$\varphi_{1}=\exists^{\textnormal{{o}}_{1}}p_{1}.\,\varphi^{\prime}_{1}$ and
$\varphi_{2}=\exists^{\textnormal{{o}}_{2}}p_{2}.\,\varphi^{\prime}_{2}$ of
$\varphi$ where $\varphi_{2}$ is a subformula of $\varphi^{\prime}_{1}$, we
have $\textnormal{{o}}_{1}\subseteq\textnormal{{o}}_{2}$.

In other words, a formula is hierarchical if innermore propositional
quantifiers observe at least as much as outermore ones.

###### Example 4.2.

Formula $\exists^{\\{1,2\\}}p.\,\exists^{\\{1,2,4\\}}q.\,{\bf A}{\bf G}(p\vee
q)$ is hierarchical because $\\{1,2\\}\subseteq\\{1,2,4\\}$. On the other
hand, formula $\exists^{\\{1,2\\}}p.\,\big{(}\exists^{\\{1,2,4\\}}q.\,{\bf
A}{\bf G}(p\vee q)\wedge\exists^{\\{3\\}}q^{\prime}.\,{\bf E}{\bf F}(p\wedge
q^{\prime})\big{)}$ is not, because $\\{1,2\\}\not\subseteq\\{3\\}$. Note that
neither is it the case that $\\{3\\}\subseteq\\{1,2\\}$: the observation power
of quantifiers $\exists^{\\{1,2\\}}p.\,$ and $\exists^{\\{3\\}}q^{\prime}.\,$
are incomparable. Finally, formula
$\forall^{\\{1,2,3\\}}p.\,\exists^{\\{1,2\\}}q.\,.{\bf A}{\bf G}(p\vee q)$ is
not hierarchical even though $\\{1,2\\}\subseteq\\{1,2,3\\}$, as the
quantifier that observes best is _higher_ in the syntactic tree.

We let $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subseteq}$}}$ be the set of hierarchical
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ formulas.

###### Theorem 4.3.

Model checking $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subseteq}$}}$ is non-elementary decidable.

Since our decision procedure for the hierarchical fragment of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ is based on an
automata-theoretic approach, we recall some definitions and results for
alternating tree automata.

###  4.1. Alternating parity tree automata

We recall alternating parity tree automata. Because their semantics is defined
via acceptance games, we start with basic definitions for two-player turn-
based parity games, or simply parity games.

Parity games. A _parity game_ is a structure $\mathcal{G}=(V,E,v_{\iota},C)$,
where $V=V_{E}\uplus V_{A}$ is a set of _positions_ partitioned between
positions of Eve ($V_{E}$) and those of Adam ($V_{A}$), $E\subseteq V\times V$
is a set of _moves_ , $v_{\iota}$ is an initial position and
$C:V\to\mathbb{N}$ is a colouring function of finite codomain. In positions
$V_{E}$, Eve chooses the next position, while Adam chooses in positions
$V_{A}$. A play is an infinite sequence of positions $v_{0}v_{1}v_{2}\ldots$
such that $v_{0}=v_{\iota}$ and for all $i\geq 0$, $(v_{i},v_{i+1})\in E$
(written $v_{i}\to v_{i+1}$). We assume that for every $v\in V$ there exists
$v^{\prime}\in V$ such that $v\to v^{\prime}$. A strategy for Eve is a partial
function $V^{*}\rightharpoonup V$ that maps each finite prefix of a play
ending in a position $v\in V_{E}$ to a next position $v^{\prime}$ such that
$v\to v^{\prime}$. A play $v_{0}v_{1}v_{2}\ldots$ _follows_ a strategy
$\sigma$ of Eve if for every $i\geq 0$ such that $v_{i}\in V_{E}$,
$v_{i+1}=\sigma(v_{0}\ldots v_{i})$. A strategy $\sigma$ is winning if every
play that follows it satisfies the parity condition, i.e., the least colour
seen infinitely often along the play is even.

Parity tree automata. Because it is sufficient for our needs and simplifies
definitions, we assume that all input trees are complete trees. For a set $Z$,
$\mathbb{B}^{+}(Z)$ is the set of formulas built from the elements of $Z$ as
atomic propositions using the connectives $\vee$ and $\wedge$, and with
$\top,\perp\in\mathbb{B}^{+}(Z)$. An _alternating tree automaton (ATA ) on
$(\textnormal{AP},X)$-trees_ is a structure
$\mathcal{A}=(Q,\delta,q_{{\iota}},C)$ where $Q$ is a finite set of states,
$q_{{\iota}}\in Q$ is an initial state, $\delta:Q\times
2^{\textnormal{AP}}\rightarrow\mathbb{B}^{+}(X\times Q)$ is a transition
function, and $C:Q\to\mathbb{N}$ is a colouring function. To ease reading we
shall write atoms in $\mathbb{B}^{+}(X\times Q)$ between brackets, such as
$[x,q]$. A _nondeterministic tree automaton (NTA ) on
$(\textnormal{AP},X)$-trees_ is an ATA $\mathcal{A}=(Q,\delta,q_{{\iota}},C)$
such that for every $q\in Q$ and $a\in 2^{\textnormal{AP}}$, $\delta(q,a)$ is
written in disjunctive normal form and for every direction $x\in X$ each
disjunct contains exactly one element of $\\{x\\}\times Q$. An NTA is
_deterministic_ if for each $q\in Q$ and $a\in 2^{\textnormal{AP}}$,
$\delta(q,a)$ consists of a single disjunct.

Acceptance of a pointed labelled tree $(t,u_{\iota})$, where $t=(\tau,\ell)$,
by an ATA $\mathcal{A}=(Q,\delta,q_{\iota},C)$ is defined via the parity game
$\mathcal{G}(\mathcal{A},t,u_{\iota})=(V,E,v_{\iota},C^{\prime})$ where
$V=\tau\times Q\times\mathbb{B}^{+}(X\times Q)$, position $(u,q,\alpha)$
belongs to Eve if $\alpha$ is of the form $\alpha_{1}\vee\alpha_{2}$ or
$[x,q^{\prime}]$, and to Adam otherwise,
$v_{{\iota}}=(u_{\iota},q_{\iota},\delta(q_{\iota},u_{\iota}))$, and
$C^{\prime}(u,q,\alpha)=C(q)$. Moves in $\mathcal{G}(\mathcal{A},t,u_{\iota})$
are defined by the following rules:

$\begin{array}[]{ll}(u,q,\alpha_{1}\;\mbox{$\dagger$}\;\alpha_{2})\rightarrow(u,q,\alpha_{i})&\mbox{where
}\mbox{$\dagger$}\in\\{\vee,\wedge\\}\mbox{ and }i\in\\{1,2\\},\\\
\lx@intercol(u,q,[x,q^{\prime}])\rightarrow(u\cdot
x,q^{\prime},\delta(q^{\prime},\ell(u\cdot x)))\hfil\lx@intercol\end{array}$

Positions of the form $(u,q,\top)$ and $(u,q,\perp)$ are sinks, winning for
Eve and Adam respectively.

A pointed labelled tree $(t,u)$ is _accepted_ by $\mathcal{A}$ if Eve has a
winning strategy in $\mathcal{G}(\mathcal{A},t,u)$, and the _language_ of
$\mathcal{A}$ is the set of pointed labelled trees accepted by $\mathcal{A}$,
written $\mathcal{L}(\mathcal{A})$. We write $t\in\mathcal{L}(\mathcal{A})$ if
$(t,r)\in\mathcal{L}(\mathcal{A})$, where $r$ is the root of $t$. Finally, the
_size_ $|\mathcal{A}|$ of an ATA $\mathcal{A}$ is its number of states plus
the sum of the sizes of all formulas appearing in the transition function.

Word automata. When the set of directions $X$ is a singleton, directions can
be forgotten and infinite trees can be identified with infinite words. We thus
call _parity word automaton_ a parity tree automaton on
$(\textnormal{AP},X)$-trees where $X$ is a singleton. In the case of a
nondeterministic parity word automaton, transitions can be represented as
usual as a mapping $\Delta:Q\times 2^{\textnormal{AP}}\to 2^{Q}$ which, in a
state $q\in Q$, reading the label $a\in 2^{\textnormal{AP}}$ of the current
position in the word, indicates a set of states $\Delta(q,a)$ from which Eve
can choose to send in the next position of the word.

We recall four classic operations on tree automata.

Complementation. Given an ATA $\mathcal{A}=(Q,\delta,q_{{\iota}},C)$, we
define its _dual_
$\overline{\mathcal{A}}=(Q,\overline{\delta},q_{{\iota}},\overline{C})$ where,
for each $q\in Q$ and $a\in 2^{\textnormal{AP}}$, $\overline{\delta}(q,a)$ is
the dual of $\delta(q,a)$, i.e., conjunctions become disjunctions and vice
versa, and $C(q):=C(q)+1$.

###### Theorem 4.4 (Complementation (Muller and Schupp, 1995)).

For every labelled tree $t$ and node $u$ in $t$,

$(t,u)\in\mathcal{L}(\overline{\mathcal{A}})\mbox{ if, and only if,
}(t,u)\notin\mathcal{L}(\mathcal{A}).$

Projection. The second construction is a projection operation, used by Rabin
to deal with second-order monadic quantification:

###### Theorem 4.5 (Projection (Rabin, 1969)).

Given an NTA $\mathcal{N}$ on $(\textnormal{AP},X)$-trees and an atomic
proposition $p\in\textnormal{AP}$, one can build in linear time an NTA
$\mathcal{N}\\!\Downarrow_{p}$ on $(\textnormal{AP}\setminus\\{p\\},X)$-trees
such that

$(t,u)\in\mathcal{L}(\mathcal{N}\\!\Downarrow_{p})\mbox{\;\;\;iff\;\;\;}\mbox{
there exists a $p$-labelling $\ell_{p}$ for $t$ s.t.
}(t\otimes\ell_{p},u)\in\mathcal{L}(\mathcal{N}).$

Intuitively, ${\mathcal{N}\\!\Downarrow_{p}}$ is automaton $\mathcal{N}$ with
the only difference that when it reads the label of a node, it can choose to
run as if $p$ was either true or false: if $\delta$ is the transition function
of $\mathcal{N}$, that of ${\mathcal{N}\\!\Downarrow_{p}}$ is
$\delta^{\prime}(q,a)=\delta(q,a\cup\\{p\\})\vee\delta(q,a\setminus\\{p\\})$,
for any state $q$ and label $a\in 2^{\textnormal{AP}}$. Another way of seeing
it is that $\mathcal{N}\\!\Downarrow_{p}$ guesses a $p$-labelling for the
input tree, and simulates $\mathcal{N}$ on this modified input.

Simulation. To prevent $\mathcal{N}\\!\Downarrow_{p}$ from guessing different
labels for a same node in different executions, it is crucial that
$\mathcal{N}$ be nondeterministic, which is the reason why we need the
following result:

###### Theorem 4.6 (Simulation (Muller and Schupp, 1995)).

Given an ATA $\mathcal{A}$, one can build in exponential time an NTA
$\mathcal{N}$ such that $\mathcal{L}(\mathcal{N})=\mathcal{L}(\mathcal{A})$.

The last construction was introduced by Kupferman and Vardi to deal with
imperfect information aspects in distributed synthesis. To describe it we need
to define a widening operation on trees which expands the directions in a
tree.

Tree widening. We generalise the widening operation defined in (Kupferman and
Vardi, 1999). In the following definitions we fix a CKS
$\mathcal{S}=(S,R,s_{\iota},\ell)$, and for $I\subseteq[n]$ we let
$S_{I}:=\\{s\\!\downarrow_{I}\,\mid s\in S\\}\subseteq L_{I}$ (recall that
$L_{I}=\prod_{i\in I}L_{i}$). Let $J\subseteq I\subseteq[n]$. For every
$S_{J}$-tree $\tau$ rooted in $s_{J}$ and $s_{I}\in S_{I}$ such that
$s_{I}\\!\downarrow_{J}=s_{J}$, we define the _$I$ -widening_ of $\tau$ as the
$S_{I}$-tree

$\tau\\!\uparrow^{I}_{s_{I}}:=\\{u\in s_{I}\cdot S_{I}^{*}\mid
u\\!\downarrow_{J}\in\tau\\}.$

For an $(\textnormal{AP},S_{J})$-tree $t=(\tau,\ell)$ rooted in $s_{J}$ and
$s_{I}\in S_{I}$ such that $s_{I}\\!\downarrow_{J}=s_{J}$, we let

$t\\!\uparrow^{I}_{s_{I}}:=(\tau\\!\uparrow^{I}_{s_{I}},\ell^{\prime}),\mbox{
where }\ell^{\prime}(u):=\ell(u\\!\downarrow_{J}).$

When clear from the context we may omit the subscript $s_{I}$. It is the case
in particular when referring to _pointed_ widenings of trees:
$(t\\!\uparrow^{I},u)$ stands for $(t\\!\uparrow^{I}_{u_{0}},u)$.

Narrowing. We now state a result from (Kupferman and Vardi, 1999) in our
slightly more general setting (the proof can be adapted straightforwardly).
The rough idea of this narrowing operation on ATA is that, if one just
observes $S_{J}$, uniform $p$-labellings on $S_{I}$-trees can be obtained by
choosing the labellings directly on $S_{J}$-trees, and then lifting them to
$S_{I}$.

###### Theorem 4.7 (Narrowing (Kupferman and Vardi, 1999)).

Given an ATA $\mathcal{A}$ on $S_{I}$-trees one can build in linear time an
ATA ${\mathcal{A}\\!\downarrow_{J}}$ on $S_{J}$-trees such that for every
pointed $(\textnormal{AP},S_{J})$-tree $(t,u)$ and every $u^{\prime}\in
S_{I}^{+}$ such that $u^{\prime}\\!\downarrow_{J}=u$,

$(t,u)\in\mathcal{L}(\mathcal{A}\\!\downarrow_{J})\mbox{ iff
}(t\\!\uparrow^{I},u^{\prime})\in\mathcal{L}(\mathcal{A}).$

###  4.2. Translating $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subseteq}$}}$ to ATA

In order to prove Theorem 4.3 we need some more notations and a technical
lemma that contains the automata construction.

###### Definition 4.8.

For every $\varphi\in\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$,
we let

$I_{\varphi}:=\bigcap_{\textnormal{{o}}\in\textnormal{Obs}(\varphi)}\textnormal{{o}}\subseteq[n],$

where $\textnormal{Obs}(\varphi)$ is the set of concrete observations that
occur in $\varphi$, with the intersection over the empty set defined as $[n]$.
For a CKS $\mathcal{S}$ with state set $S\subseteq\prod_{i\in[n]}L_{i}$ we
also let $S_{\varphi}:=\\{s\\!\downarrow_{I_{\varphi}}\mid s\in S\\}$.

Elements of $S_{\varphi}$ will be the possible directions used by the
automaton we build for $\varphi$. In other words, the automaton for $\varphi$
will work on $S_{\varphi}$-trees. The intuition is that the observations in
$\varphi$ determine which components of the model’s states can be observed by
the automaton.

Our construction, that transforms a
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i,$\tiny{\subseteq}$}}$
formula $\varphi$ and a CKS $\mathcal{S}$ into an ATA, builds upon the classic
construction from (Kupferman et al., 2000b), which builds ATA for
$\textnormal{{CTL}}^{*}$ formulas. In addition, we use projection of automata
to treat second-order quantification, and to deal with imperfect information
we resort to automata narrowing.

Moreover, we use tree automata in an original way that allows us to deal with
non-observable atomic propositions, which in turn makes it possible to
consider non-observable winning conditions in our decidable fragment of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$. The classical approach to
model checking via tree automata is to build an automaton that accepts all
tree models of the input formula, and check whether it accepts the unfolding
of the model (Kupferman et al., 2000b). We instead encode the model in the
automata, using the input tree only to guess labellings for quantified
propositions.

Encoding the model in the automaton. Quantification on atomic propositions is
classically performed by means of automata projection (see Theorem 4.5). But
in order to obtain a labelling that is uniform with regards to the observation
of the quantifier, we need to make use of the narrowing operation (see Theorem
4.7). Intuitively, to check that a formula
$\exists^{\textnormal{{o}}}p.\,\varphi$ holds in a tree $t$, we would like to
work on its narrowing $t^{\prime}:=t\\!\downarrow_{\textnormal{{o}}}$, guess a
labelling for $p$ on this tree thanks to automata projection, thus obtaining a
tree $t^{\prime}_{p}$, take its widening
$t_{p}^{\prime\prime}:=t^{\prime}_{p}\\!\uparrow^{[n]}$, obtaining a tree with
an o-uniform labelling for $p$, and then check that $\varphi$ holds on
$t_{p}^{\prime\prime}$. The problem is that unless $t=(\tau,\ell)$ is
o-uniform in every atomic proposition in AP, there is no way to define the
labelling of $\tau\\!\downarrow_{\textnormal{{o}}}$ without losing
information. This implies that, unless we restrict to models where all atomic
propositions are observable for all observations o, we cannot pass the model
as input to our automata, which will work on narrowings of trees.

Therefore, to model check a $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}$ formula $\varphi$ on a CKS $\mathcal{S}$, each state of the automaton
that we build for $\varphi$ will contain a state of $\mathcal{S}$. The
automaton can thus guess paths in $\mathcal{S}$, and evaluate free occurrences
of atomic propositions in $\mathcal{S}$ without reading the input tree. The
input tree no longer represents the model, but we use it to carry labellings
for quantified atomic propositions in ${\textnormal{AP}_{\exists}}(\varphi)$:
we provide the automaton with an input tree whose labelling is initially
empty, and the automaton, through successive narrowing and projection
operations, decorates it with uniform labellings for quantified atomic
propositions.

We remark that this technique allows one to go beyond Coordination Logic
(Finkbeiner and Schewe, 2010): by separating between quantified atomic
propositions (that need to be uniform and are carried by the input tree) and
free atomic propositions (that state facts about the model and are coded in
the automaton), we manage to remove the restriction present in CL, that
requires all facts about the model to be known to every strategy (see
Proposition 6.3 in Section 6.2). To do this we assume without loss of
generality that propositions that are quantified in $\varphi$ do not appear
free in $\varphi$, i.e.,
${\textnormal{AP}_{\exists}}(\varphi)\cap\textnormal{AP}_{f}(\varphi)=\emptyset$.

Finally, given a formula $\varphi$, a CKS $\mathcal{S}$ and a state
$s\in\mathcal{S}$, the truth value of $\varphi$ in $(\mathcal{S},s)$ does not
depend on the labelling of $\mathcal{S}$ for atoms in
${\textnormal{AP}_{\exists}}(\varphi)$, which can thus be forgotten. Thus,
from now on we will assume that an instance $(\mathcal{S},\Phi)$ of the model-
checking problem for $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$
is such that
${\textnormal{AP}_{\exists}}(\Phi)\cap\textnormal{AP}_{f}(\Phi)=\emptyset$ and
$\mathcal{S}$ is a CKS over $\textnormal{AP}_{f}(\Phi)$.

Merging the decorated input tree and the model. To state the correctness of
our construction, we will need to merge the labels for quantified
propositions, carried by the input tree, with those for free propositions,
carried by CKS $\mathcal{S}$. Because, through successive widenings, the input
tree (represented by $t$ in the definition below) will necessarily be a
complete tree, its domain will always contain the domain of the unfolding of
$\mathcal{S}$ (represented by $t^{\prime}$ below), hence the following
definition.

###### Definition 4.9 (Merge).

Let $t=(\tau,\ell)$ be a complete $(\textnormal{AP},X)$-tree and
$t^{\prime}=(\tau^{\prime},\ell^{\prime})$ an
$(\textnormal{AP}\,^{\prime},X)$-tree with same root as $t$, where
$\textnormal{AP}\cap\textnormal{AP}\,^{\prime}=\emptyset$. We define the
_merge_ of $t$ and $t^{\prime}$ as the
$(\textnormal{AP}\cup\textnormal{AP}\,^{\prime},X)$-tree

$t\merge
t^{\prime}:=(\tau\cap\tau^{\prime}=\tau^{\prime},\ell^{\prime\prime}),$

where $\ell^{\prime\prime}(u)=\ell(u)\cup\ell^{\prime}(u)$.

We now describe our automata construction. Let $(\mathcal{S},\Phi)$ be an
instance of the model-checking problem for
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i,$\tiny{\subseteq}$}}$,
where $\mathcal{S}=(S,R,\ell_{\mathcal{S}},s_{\iota})$.

###### Lemma 4.10 (Translation).

For every subformula $\varphi$ of $\Phi$ and state $s$ of $\mathcal{S}$, one
can build an ATA $\mathcal{A}_{s}^{\varphi}$ on
$({\textnormal{AP}_{\exists}}(\Phi),S_{\varphi})$-trees such that for every
$({\textnormal{AP}_{\exists}}(\Phi),S_{\varphi})$-tree $t$ rooted in
$s_{\iota}\\!\downarrow_{I_{\varphi}}$, every $u\in t_{\mathcal{S}}$ ending in
$s$, it holds that

$(t,u\\!\downarrow_{I_{\varphi}})\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})\mbox{\;\;\;iff\;\;\;}t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\varphi.$

###### Proof.

Let ${\textnormal{AP}_{\exists}}={\textnormal{AP}_{\exists}}(\Phi)$ and
$\textnormal{AP}_{f}=\textnormal{AP}_{f}(\Phi)$, and recall that $\mathcal{S}$
is labelled over $\textnormal{AP}_{f}$. For each state $s\in S$ and each
subformula $\varphi$ of $\Phi$ (note that all subformulas of $\Phi$ are also
hierarchical), we define by induction on $\varphi$ the ATA
$\mathcal{A}_{s}^{\varphi}$ on
$({\textnormal{AP}_{\exists}},S_{\varphi})$-trees.

$\bm{\varphi=p:}$ First, by Definition 4.8, $S_{\varphi}=S_{[n]}=S$. We let
$\mathcal{A}_{s}^{p}$ be the ATA over $S$-trees with one unique state
$q_{\iota}$, with transition function defined as follows:

$\delta(q_{\iota},a)=\begin{cases}\top&\mbox{if
}\begin{array}[]{c}p\in\textnormal{AP}_{f}\mbox{ and
}p\in\ell_{\mathcal{S}}(s)\\\ \mbox{ or }\\\
p\in{\textnormal{AP}_{\exists}}\mbox{ and }p\in a\end{array}\\\ \perp&\mbox{if
}\begin{array}[]{c}p\in\textnormal{AP}_{f}\mbox{ and
}p\notin\ell_{\mathcal{S}}(s)\\\ \mbox{ or }\\\
p\in{\textnormal{AP}_{\exists}}\mbox{ and }p\notin a\end{array}\end{cases}$

$\bm{\varphi=\neg\varphi^{\prime}:}$ We let
$\mathcal{A}_{s}^{\varphi}:=\overline{\mathcal{A}_{s}^{\varphi^{\prime}}}$.

$\bm{\varphi=\varphi_{1}\vee\varphi_{2}:}$ Because
$I_{\varphi}=I_{\varphi_{1}}\cap I_{\varphi_{2}}$, and each
$\mathcal{A}_{s}^{\varphi_{i}}$ for $i\in\\{1,2\\}$ works on
$L_{\varphi_{i}}$-trees, we first narrow them so that they work on
$L_{\varphi}$-trees: for $i\in\\{1,2\\}$, we let
$\mathcal{A}_{i}:={\mathcal{A}_{s}^{\varphi_{i}}\\!\downarrow_{I_{\varphi}}}=(Q^{i},\delta^{i},q_{\iota}^{i},C^{i})$.
Letting $q_{\iota}$ be a fresh initial state we define
$\mathcal{A}_{s}^{\varphi}:=(\\{q_{\iota}\\}\cup Q^{1}\cup
Q^{2},\delta,q_{\iota},C)$, where $\delta$ and $C$ agree with $\delta^{i}$ and
$C^{i}$, respectively, on states from $Q^{i}$, and
$\delta(q_{\iota},a)=\delta^{1}(q_{\iota}^{1},a)\vee\delta^{2}(q_{\iota}^{2},a)$.
The colour of $q_{\iota}$ does not matter.

$\bm{\varphi={\bf E}\psi:}$ Let
$\max(\psi)=\\{\varphi_{1},\ldots,\varphi_{k}\\}$ be the set of maximal state
subformulas of $\psi$. In a first step we see these maximal state subformulas
as atomic propositions, we see $\psi$ as an LTL formula over $\max(\psi)$, and
we build a nondeterministic parity word automaton
$\mathcal{W}^{\psi}=(Q^{\psi},\Delta^{\psi},q^{\psi}_{\iota},C^{\psi})$ over
alphabet $2^{\max(\psi)}$ that accepts exactly the models of $\psi$ (and uses
two colours) (Vardi and Wolper, 1994). We define the ATA $\mathcal{A}$ that,
given as input a $(\max(\psi),S_{\varphi})$-tree $t$, nondeterministically
guesses a path $\lambda$ in $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}$, or
equivalently a path in $\mathcal{S}$ starting from $s$, and simulates
$\mathcal{W}^{\psi}$ on it, assuming that the labels it reads while following
$\lambda\\!\downarrow_{I_{\varphi}}$ in its input $t$ correctly represent the
truth value of formulas in $\max(\psi)$ along $\lambda$. Recall that
$\mathcal{S}=(S,R,s_{\iota},\ell_{\mathcal{S}})$; we define
$\mathcal{A}:=(Q,\delta,q_{{\iota}},C)$, where

  * •

$Q=Q^{\psi}\times S$,

  * •

$q_{{\iota}}=(q^{\psi}_{{\iota}},s)$,

  * •

for each $(q^{\psi},s^{\prime})\in Q$,
$C(q^{\psi},s^{\prime})=C^{\psi}(q^{\psi})$, and

  * •

for each $(q^{\psi},s^{\prime})\in Q$ and $a\in 2^{\max(\psi)}$,

$\delta((q^{\psi},s^{\prime}),a)=\bigvee_{q^{\prime}\in\Delta^{\psi}(q^{\psi},a)}\bigvee_{s^{\prime\prime}\in
R(s^{\prime})}[s^{\prime\prime}\\!\downarrow_{I_{\varphi}},\left(q^{\prime},s^{\prime\prime}\right)].$

The intuition is that $\mathcal{A}$ reads the current label in
$2^{\max(\psi)}$, chooses nondeterministically a transition in
$\mathcal{W}^{\psi}$, chooses a next state $s^{\prime\prime}$ in $S$ and
proceeds in the corresponding direction
$s^{\prime\prime}\\!\downarrow_{I_{\varphi}}\in S_{\varphi}$.

Now from $\mathcal{A}$ we build the automaton $\mathcal{A}_{s}^{\varphi}$ over
$S_{\varphi}$-trees labelled with “real” atomic propositions in
${\textnormal{AP}_{\exists}}$. Intuitively, in each node it visits,
$\mathcal{A}_{s}^{\varphi}$ guesses what should be its labelling over
$\max(\psi)$, it simulates $\mathcal{A}$ accordingly, and checks that the
guess it made is correct. If, after having guessed a finite path $u\in
t_{\mathcal{S}}$ ending in state $s^{\prime}$, $\mathcal{A}_{s}^{\varphi}$
guesses that $\varphi_{i}$ holds, it checks this guess by starting a copy of
automaton $\mathcal{A}_{s^{\prime}}^{\varphi_{i}}$ from node
$v=u\\!\downarrow_{I_{\varphi}}$ in its input $t$.

Formally, for each $s^{\prime}\in\mathcal{S}$ and each
$\varphi_{i}\in\max(\psi)$ we first build
$\mathcal{A}_{s^{\prime}}^{\varphi_{i}}$, which works on
$S_{\varphi_{i}}$-trees. Observe that
$I_{\varphi}=\cap_{i=1}^{k}I_{\varphi_{i}}$, so that we need to narrow down
these automata222In the conference version of this work (Berthon et al., 2017)
we made a mistake here: we wrote that $I_{\varphi}=I_{\varphi_{i}}$, which is
not the case in general. As a consequence we do need to narrow down automata,
unlike what was written in the conference version.: We let
$\mathcal{A}^{i}_{s^{\prime}}:=\mathcal{A}_{s^{\prime}}^{\varphi_{i}}\\!\downarrow_{I_{\varphi}}=(Q^{i}_{s^{\prime}},\delta^{i}_{s^{\prime}},q^{i}_{s^{\prime}},C^{i}_{s^{\prime}})$.
We also let
$\overline{\mathcal{A}^{i}_{s^{\prime}}}=(\overline{Q^{i}_{s^{\prime}}},\overline{\delta^{i}_{s^{\prime}}},\overline{q^{i}_{s^{\prime}}},\overline{C^{i}_{s^{\prime}}})$
be the dualisation of $\mathcal{A}^{i}_{s^{\prime}}$, and we assume without
loss of generality all the state sets are pairwise disjoint. We define the ATA

$\mathcal{A}_{s}^{\varphi}=(Q\cup\bigcup_{i,s^{\prime}}Q^{i}_{s^{\prime}}\cup\overline{Q^{i}_{s^{\prime}}},\delta^{\prime},q_{{\iota}},C^{\prime}),$

where the colours of states are left as they were in their original automaton,
and $\delta^{\prime}$ is defined as follows. For states in
$Q^{i}_{s^{\prime}}$ (resp. $\overline{Q^{i}_{s^{\prime}}}$),
$\delta^{\prime}$ agrees with $\delta^{i}_{s^{\prime}}$ (resp.
$\overline{\delta^{i}_{s^{\prime}}}$), and for $(q^{\psi},s^{\prime})\in Q$
and $a\in 2^{{\textnormal{AP}_{\exists}}}$ we let
$\delta^{\prime}((q^{\psi},s^{\prime}),a)$ be the disjunction over
${a^{\prime}\in 2^{\max(\psi)}}$ of

(2)
$\displaystyle\Bigg{(}\delta\left((q^{\psi},s^{\prime}),a^{\prime}\right)\wedge\bigwedge_{\varphi_{i}\in
a^{\prime}}\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a)\;\wedge\bigwedge_{\varphi_{i}\notin
a^{\prime}}\overline{\delta^{i}_{s^{\prime}}}(\overline{q^{i}_{s^{\prime}}},a)\Bigg{)}.$

Note that in general it is not possible to define a $\max(\psi)$-labelling of
$t$ that faithfully represents the truth values of formulas in $\max(\psi)$
for all nodes in $t_{\mathcal{S}}$, because a node in $t$ may correspond to
different nodes in $t_{\mathcal{S}}$ that have same projection on
$S_{\varphi}$ but satisfy different formulas of $\max(\psi)$. However this is
not a problem because different copies of $\mathcal{A}_{s}^{\varphi}$ that
visit the same node can guess different labellings, depending on the actual
state of $\mathcal{S}$ (which is part of the state of
$\mathcal{A}_{s}^{\varphi}$).

$\bm{\varphi=\exists}^{\bm{\textnormal{{o}}}}\bm{p.\,\varphi^{\prime}:}$ We
build automaton $\mathcal{A}_{s}^{\varphi^{\prime}}$ that works on
$S_{\varphi^{\prime}}$-trees; because $\varphi$ is hierarchical, we have that
$\textnormal{{o}}\subseteq I_{\varphi^{\prime}}$ and we can narrow down
$\mathcal{A}_{s}^{\varphi^{\prime}}$ to work on $S_{\textnormal{{o}}}$-trees
and obtain
$\mathcal{A}_{1}:={\mathcal{A}_{s}^{\varphi^{\prime}}\\!\downarrow_{\textnormal{{o}}}}$.
By Theorem 4.6 we can nondeterminise it to get $\mathcal{A}_{2}$, which by
Theorem 4.5 we can project with respect to $p$, finally obtaining
$\mathcal{A}_{s}^{\varphi}:=\mathcal{A}_{2}\\!\Downarrow_{p}$.

Correctness. We now prove by induction on $\varphi$ that the construction is
correct. In each case, we let $t=(\tau,\ell)$ be a complete
$({\textnormal{AP}_{\exists}},S_{\varphi})$-tree rooted in
$s_{\iota}\\!\downarrow_{I_{\varphi}}$.

$\bm{\varphi=p:}$ First, note that $I_{p}=[n]$, so that $t$ is rooted in
$s_{\iota}\\!\downarrow_{I_{\varphi}}=s_{\iota}$, and
$u\\!\downarrow_{I_{\varphi}}=u$. Also recall that $u$ ends in $s$. Let us
consider first the case where $p\in\textnormal{AP}_{f}$. By definition of
$\mathcal{A}_{s}^{p}$, we have that $(t,u)\in\mathcal{L}(\mathcal{A}_{s}^{p})$
if and only if $p\in\ell_{\mathcal{S}}(s)$. We also have
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models p$ if and only if
$p\in\ell^{\prime}(u)$, where $\ell^{\prime}$ is the labelling of tree
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}$. By definition of unfolding and
merge, we have that $\ell^{\prime}(u)=\ell_{\mathcal{S}}(s)$, which concludes
this direction. Now if $p\in{\textnormal{AP}_{\exists}}$: by definition of
$\mathcal{A}_{s}^{p}$, we have $(t,u)\in\mathcal{L}(\mathcal{A}_{s}^{p})$ if
and only if $p\in\ell(u)$; also, by definition of the merge and unfolding, we
have that $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models p$ if and only
if $p\in\ell(u)$, and we are done.

$\bm{\varphi=\neg\varphi^{\prime}:}$ Correctness follows from the induction
hypothesis and Theorem 4.4.

$\bm{\varphi_{1}\vee\varphi_{2}:}$ We have
$\mathcal{A}_{i}=\mathcal{A}_{s}^{\varphi_{i}}\\!\downarrow_{I_{\varphi}}$, so
by Theorem 4.7 we have
$(t,u\\!\downarrow_{I_{\varphi}})\in\mathcal{L}(\mathcal{A}_{i})$ if and only
if
$(t\\!\uparrow^{I_{\varphi_{i}}},u\\!\downarrow_{I_{\varphi_{i}}})\in\mathcal{L}(\mathcal{A}_{s}^{\varphi_{i}})$,
which by induction hypothesis holds if and only if
$(t\\!\uparrow^{I_{\varphi_{i}}})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\varphi_{i}$,
i.e., $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\varphi_{i}$. We
conclude by observing that
$\mathcal{L}(\mathcal{A}_{s}^{\varphi})=\mathcal{L}(\mathcal{A}_{1})\cup\mathcal{L}(\mathcal{A}_{2})$.

$\bm{\varphi={\bf E}\psi:}$ Suppose that
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models{\bf E}\psi$. There exists
an infinite path $\lambda$ in $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}$
starting at $u$ such that
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},\lambda\models\psi$. Again, let
$\max(\psi)$ be the set of maximal state subformulas of $\varphi$, and let $w$
be the infinite word over $2^{\max(\psi)}$ that agrees with $\lambda$ on the
state formulas in $\max(\psi)$, i.e., for each node $\lambda_{k}$ of $\lambda$
and formula $\varphi_{i}\in\max(\psi)$, it holds that $\varphi_{i}\in w_{k}$
if and only if
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},\lambda_{k}\models\varphi_{i}$. To
show that
$(t,u\\!\downarrow_{I_{\varphi}})\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})$ we
show that Eve can win the acceptance game
$\mathcal{G}(\mathcal{A}_{s}^{\varphi},t,u\\!\downarrow_{I_{\varphi}})$. In
this game, Eve can guess the path $\lambda$ while the automaton follows
$\lambda\\!\downarrow_{I_{\varphi}}$ in its input $t$, and she can also guess
the corresponding word $w$ on $2^{\max(\psi)}$. By construction of
$\mathcal{W}^{\psi}$, Eve has a winning strategy $\sigma_{\psi}$ in the
acceptance game of $\mathcal{W}^{\psi}$ on $w$. From $\lambda$, $w$ and
$\sigma_{\psi}$ we can easily define a strategy for Eve in
$\mathcal{G}(\mathcal{A}_{s}^{\varphi},t,u\\!\downarrow_{I_{\varphi}})$ on all
positions that can be reached while Adam does not choose to challenge her on a
guess she made for the truth value of some maximal state subformula, and on
such plays this strategy is winning because $\sigma_{\psi}$ is winning.

Now if Adam challenges her on one of these guesses: Let $\lambda_{k}\in
t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}$ be a node along $\lambda$, let
$s^{\prime}$ be its last direction and let
$\lambda_{k}^{\prime}=\lambda_{k}\\!\downarrow_{I_{\varphi}}\in t$. Assume
that in node $\lambda^{\prime}_{k}$ of the input tree, in a state
$(q^{\psi},s^{\prime})\in Q$, Adam challenges Eve on some
$\varphi_{i}\in\max(\psi)$ that she assumes to be true in
$\lambda^{\prime}_{k}$, i.e., such that $\varphi_{i}\in w_{k}$. Formally, in
the evaluation game this means that Adam chooses the conjunct
$\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a)$ in transition formula 2, where
$a=\ell(\lambda^{\prime}_{k})$, thus moving to position
$(\lambda^{\prime}_{k},(q^{\psi},s^{\prime}),\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a))$.
We want to show that Eve wins from this position. To do so we first show that
$(t,\lambda^{\prime}_{k})\in\mathcal{L}(\mathcal{A}^{i}_{s^{\prime}})$.

First, since
$\mathcal{A}^{i}_{s^{\prime}}=\mathcal{A}_{s^{\prime}}^{\varphi_{i}}\\!\downarrow_{I_{\varphi}}$,
by Theorem 4.7,
$(t,\lambda^{\prime}_{k})\in\mathcal{L}(\mathcal{A}^{i}_{s^{\prime}})$ if and
only if
$(t\\!\uparrow^{I_{\varphi_{i}}},\lambda_{k}\\!\downarrow_{I_{\varphi_{i}}})\in\mathcal{L}(\mathcal{A}_{s^{\prime}}^{\varphi_{i}})$.
Next, by applying the induction hypothesis we get that
$(t\\!\uparrow^{I_{\varphi_{i}}},\lambda_{k}\\!\downarrow_{I_{\varphi_{i}}})\in\mathcal{L}(\mathcal{A}_{s^{\prime}}^{\varphi_{i}})$
if and only if
$t\\!\uparrow^{I_{\varphi_{i}}}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},\lambda_{k}\models\varphi_{i}$,
i.e.,
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},\lambda_{k}\models\varphi_{i}$. The
latter holds because $\varphi_{i}\in w_{k}$, and by assumption $w_{k}$ agrees
with $\lambda_{k}$ on $\varphi_{i}$. Thus
$(t,\lambda^{\prime}_{k})\in\mathcal{L}(\mathcal{A}^{i}_{s^{\prime}})$.

This means that Eve has a winning strategy from the initial position
$(\lambda^{\prime}_{k},q^{i}_{s^{\prime}},\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a))$
of the acceptance game of $\mathcal{A}^{i}_{s^{\prime}}$ on
$(t,\lambda^{\prime}_{k})$. Since
$(\lambda^{\prime}_{k},q^{i}_{s^{\prime}},\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a))$
and
$(\lambda^{\prime}_{k},(q^{\psi},s^{\prime}),\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a))$
contain the same node $\lambda^{\prime}_{k}$ and transition formula
$\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a)$, the subgames that start in
these positions are isomorphic and a winning strategy in one of these
positions induces a winning strategy in the other, and therefore Eve wins
Adam’s challenge (recall that positional strategies are sufficient in parity
games (Zielonka, 1998)). With a similar argument, we get that also when Adam
challenges Eve on some $\varphi_{i}\in\max(\psi)$ assumed not to be true in
node $\lambda_{k}$, Eve wins the challenge. Finally, Eve wins the acceptance
game of $\mathcal{A}_{s}^{\varphi}$ on $(t,u\\!\downarrow_{I_{\varphi}})$, and
thus
$(t,u\\!\downarrow_{I_{\varphi}})\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})$.

For the other direction, assume that
$(t,u\\!\downarrow_{I_{\varphi}})\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})$,
i.e., Eve wins the evaluation game of $\mathcal{A}_{s}^{\varphi}$ on
$(t,u\\!\downarrow_{I_{\varphi}})$. A winning strategy for Eve describes a
path $\lambda$ in $t_{\mathcal{S}}$ from $s$, which is also a path in
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}$ from $u$. This winning strategy
also defines an infinite word $w$ over $2^{\max(\psi)}$ such that $w$ agrees
with $\lambda$ on the formulas in $\max(\psi)$, and it also describes a
winning strategy for Eve in the acceptance game of $\mathcal{W}^{\psi}$ on
$w$. Hence $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},\lambda\models\psi$, and
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\varphi$.

$\bm{\varphi=\exists}^{\bm{\textnormal{{o}}}}\bm{p.\,\varphi^{\prime}:}$
First, by definition we have $I_{\varphi}=\textnormal{{o}}\cap
I_{\varphi^{\prime}}$. Because $\varphi$ is hierarchical,
$\textnormal{{o}}\subseteq\textnormal{{o}}^{\prime}$ for every
$\textnormal{{o}}^{\prime}$ that occurs in $\varphi^{\prime}$, and thus
$\textnormal{{o}}\subseteq I_{\varphi^{\prime}}$. It follows that
$I_{\varphi}=\textnormal{{o}}$. Next, by Theorem 4.5 we have that

(3)
$(t,u\\!\downarrow_{I_{\varphi}})\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})\mbox{\;\;\;iff\;\;\;}\exists\,\ell_{p}\mbox{
a $p$-labelling for $t$ such that
}(t\otimes\ell_{p},u)\in\mathcal{L}(\mathcal{A}_{2}).$

By Theorem 4.6, $\mathcal{L}(\mathcal{A}_{2})=\mathcal{L}(\mathcal{A}_{1})$,
and since
$\mathcal{A}_{1}=\mathcal{A}_{s}^{\varphi^{\prime}}\\!\downarrow_{\textnormal{{o}}}=\mathcal{A}_{s}^{\varphi^{\prime}}\\!\downarrow_{I_{\varphi}}$
we get by Theorem 4.7 that

(4)
$(t\otimes\ell_{p},u\\!\downarrow_{I_{\varphi}})\in\mathcal{L}(\mathcal{A}_{2})\mbox{\;\;\;iff\;\;\;}((t\otimes\ell_{p})\\!\uparrow^{L_{\varphi^{\prime}}},u\\!\downarrow_{I_{\varphi^{\prime}}})\in\mathcal{L}(\mathcal{A}_{s}^{\varphi^{\prime}}).$

By induction hypothesis,

(5)
$((t\otimes\ell_{p})\\!\uparrow^{L_{\varphi^{\prime}}},u\\!\downarrow_{I_{\varphi^{\prime}}})\in\mathcal{L}(\mathcal{A}_{s}^{\varphi^{\prime}})\mbox{\;\;\;iff\;\;\;}(t\otimes\ell_{p})\\!\uparrow^{L_{\varphi^{\prime}}}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\varphi^{\prime}.$

Now, by points (3), (4) and (5) and the fact that
$(t\otimes\ell_{p})\\!\uparrow^{I_{\varphi^{\prime}}}\\!\uparrow^{[n]}=(t\otimes\ell_{p})\\!\uparrow^{[n]}$,
we get that

(6)
$(t,u\\!\downarrow_{I_{\varphi}})\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})\mbox{\;\;\;iff\;\;\;}\exists\,\ell_{p}\mbox{
a $p$-labelling for $t$ such that
}(t\otimes\ell_{p})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\varphi^{\prime}.$

We now prove the following equation which, together with point (6), concludes
the proof:

(7) $\begin{array}[]{c}\exists\,\ell_{p}\mbox{ a $p$-labelling for $t$ such
that
}(t\otimes\ell_{p})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\varphi^{\prime}\\\
\mbox{\;\;\;iff\;\;\;}\\\
t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\exists^{\textnormal{{o}}}p.\,\varphi^{\prime}\end{array}$

Assume that there exists a $p$-labelling $\ell_{p}$ for $t$ such that
$(t\otimes\ell_{p})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\varphi^{\prime}$.
Let $\ell_{p}^{\prime}$ be the $p$-labelling of
$(t\otimes\ell_{p})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}$. By definition of
the merge, $\ell_{p}^{\prime}$ is equal to the $p$-labelling of
$(t\otimes\ell_{p})\\!\uparrow^{[n]}$, which by definition of the widening is
$I_{\varphi}$-uniform, i.e., it is o-uniform. In addition, it is clear that
$(t\otimes\ell_{p})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}=(t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}})\otimes\ell_{p}^{\prime}$,
which concludes this direction.

For the other direction, assume that
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\exists^{\textnormal{{o}}}p.\,\varphi^{\prime}$:
there exists a o-uniform $p$-labelling $\ell_{p}^{\prime}$ for
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}$ such that
$(t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}})\otimes\ell_{p}^{\prime},u\models\varphi^{\prime}$.
We define a $p$-labelling $\ell_{p}$ for $t$ such that
$(t\otimes\ell_{p})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\varphi^{\prime}$.
First, let us write
$t^{\prime}=t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}=(\tau^{\prime},\ell^{\prime})$.
For each node $u$ of $t$, let

$\ell_{p}(u)=\begin{cases}\ell_{p}^{\prime}(u^{\prime})&\mbox{if there exists
}u^{\prime}\in\tau^{\prime}\mbox{ such that
}u^{\prime}\\!\downarrow_{\textnormal{{o}}}=u,\\\
0&\mbox{otherwise.}\end{cases}$

This is well defined because $\ell_{p}^{\prime}$ is o-uniform in $p$, so that
if two nodes $u^{\prime},v^{\prime}$ project on $u$, we have
$u^{\prime}\approx_{\textnormal{{o}}}v^{\prime}$ and thus
$\ell_{p}^{\prime}(u^{\prime})=\ell_{p}^{\prime}(v^{\prime})$. In case there
is no $u^{\prime}\in\tau^{\prime}$ such that
$u^{\prime}\\!\downarrow_{I_{\varphi}}=u$, the value of $\ell_{p}(u)$ has no
impact on $(t\otimes\ell_{p})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}$.
Finally,
$(t\otimes\ell_{p})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}=(t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}})\otimes\ell_{p}^{\prime}$,
hence the result.

∎

###  4.3. Proof of Theorem 4.3

We now prove Theorem 4.3. Let $\mathcal{S}$ be a CKS with initial state
$s_{\iota}$, and let $\Phi\in\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subseteq}$}}$. By Lemma 4.10 one can build an ATA
$\mathcal{A}_{s_{\iota}}^{\Phi}$ such that for every labelled
$S_{\varphi}$-tree $t$ rooted in $s_{\iota}\\!\downarrow_{I_{\varphi}}$, and
every node $u\in t_{\mathcal{S}}$,
$(t,u\\!\downarrow_{I_{\varphi}})\in\mathcal{L}(\mathcal{A}_{s_{\iota}}^{\varphi})$
if, and only if, $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}},u\models\Phi$.

Let $\tau$ be the full $S_{\varphi}$-tree rooted in
$s_{\iota}\\!\downarrow_{I_{\varphi}}$, and let $t=(\tau,\ell_{\emptyset})$,
where $\ell_{\emptyset}$ is the empty labelling. Clearly,
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S}}=t_{\mathcal{S}}$, and because $t$
is rooted in $s_{\iota}\\!\downarrow_{I_{\varphi}}$, we get that
$t\in\mathcal{L}(\mathcal{A}_{s_{\iota}}^{\varphi})$ if, and only if
$t_{\mathcal{S}}\models\Phi$, i.e., $\mathcal{S}\models\Phi$. It remains to
check whether tree $t$, which is regular, is accepted by
$\mathcal{A}_{s_{\iota}}^{\Phi}$. This can be done by solving a parity game
built from the product of $\mathcal{A}_{s_{\iota}}^{\Phi}$ with a finite
Kripke structure representing $t$ (Löding, 2011).

###  4.4. Complexity

To state a precise upper bound on the complexity of our procedure, we first
introduce a syntactic notion of _simulation depth_ for formulas of
$\textnormal{{SL}}_{\textnormal{\scriptsize ii}}$. While alternation depth
(see, e.g., (Mogavero et al., 2014)) simply counts the number of alternations
between existential and universal strategy quantifications, simulation depth
reflects automata operations required to treat a formula, and counts the
maximum number of nested simulations of alternating tree automata that need to
be performed when applying our automata construction. However, like
alternation depth, it is a purely syntactic notion. Formally we define a
function $\mbox{sd}:\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
ii}}\to\mathbb{N}\times\\{\mbox{nd},\mbox{alt}\\}$ which returns, for each
formula $\varphi$, a pair $\mbox{sd}(\varphi)=(k,x)$ where $k$ is the
simulation depth of $\varphi$, and $x\in\\{\mbox{nd},\mbox{alt}\\}$ indicates
whether the automaton $\mathcal{A}_{s}^{\varphi}$ built from $\varphi$ and a
state $s$ of a CKS $\mathcal{S}$ is nondeterministic (nd) or alternating
(alt). If $\mbox{sd}(\varphi)=(k,x)$ we shall denote $k$ by
$\mbox{sd}_{k}(\varphi)$ and $x$ by $\mbox{sd}_{x}(\varphi)$. The inductive
definition for state formulas is as follows:

$\begin{array}[]{l}\mbox{sd}(p):=(0,\mbox{nd})\\\\[5.0pt]
\mbox{sd}(\neg\varphi):=(\mbox{sd}_{k}(\varphi),\mbox{alt})\\\\[5.0pt]
\mbox{sd}(\varphi_{1}\vee\varphi_{2}):=\left(\max_{i\in\\{1,2\\}}\mbox{sd}_{k}(\varphi_{i}),x\right),\\\
\hfill\mbox{where }x=\begin{cases}\mbox{nd}&\mbox{if
}\mbox{sd}_{x}(\varphi_{1})=\mbox{sd}_{x}(\varphi_{2})=\mbox{nd}\\\
\mbox{alt}&\mbox{otherwise}\end{cases}\\\\[15.0pt] \mbox{sd}({\bf
E}\psi):=\begin{cases}(0,\mbox{nd})&\mbox{if }\psi\in\textnormal{LTL}\\\
(\max_{\varphi\in\max(\psi)}\mbox{sd}_{k}(\varphi),\mbox{alt})&\mbox{otherwise}\end{cases}\\\\[15.0pt]
\mbox{sd}(\exists^{\textnormal{{o}}}p.\,\varphi):=(k,\mbox{nd}),\\\
\hfill\quad\quad\quad\quad\quad\mbox{where
}k=\begin{cases}\mbox{sd}_{k}(\varphi)&\mbox{if
}\mbox{sd}_{x}(\varphi)=\mbox{nd}\mbox{ and
}\textnormal{{o}}=I_{\varphi}\quad\mbox{(recall Definition~{}\ref{def-
Iphi})}\\\ \mbox{sd}_{k}(\varphi)+1&\mbox{otherwise}\end{cases}\end{array}$

We explain each case. For an atomic proposition $p$, the automaton
$\mathcal{A}_{s}^{p}$ is clearly nondeterministic and no simulation is
involved in its construction. For a formula $\neg\varphi$, the automaton
$\mathcal{A}_{s}^{\neg\varphi}$ is obtained by dualising
$\mathcal{A}_{s}^{\varphi}$, an operation that in general does not return a
nondeterministic automaton but an alternating one; also this dualisation does
not involve any simulation, hence the definition of the first component. Now
for the disjunction, the first component should be clear; for the second one,
observe that by construction of
$\mathcal{A}_{s}^{\varphi_{1}\vee\varphi_{2}}$, if both
$\mathcal{A}_{s}^{\varphi_{1}}$ and $\mathcal{A}_{s}^{\varphi_{2}}$ are
nondeterministic, then so is $\mathcal{A}_{s}^{\varphi_{1}\vee\varphi_{2}}$;
otherwise, it is alternating. For the path quantifier, by construction
$\mathcal{A}_{s}^{{\bf E}\psi}$ is alternating in the general case as it
starts copies of automata for each maximal state subformula in $\psi$; for the
first component, we recall that $\max(\psi)$ denotes the set of these maximal
state subformulas and we observe that no additional simulation is performed to
build $\mathcal{A}_{s}^{{\bf E}\psi}$ besides those needed to construct the
automata for the maximal state subformulas. If $\psi$ is an LTL formula, then
one can build the nondeterministic word automaton $\mathcal{W}^{\psi}$
directly working on “real” atomic propositions in
${\textnormal{AP}_{\exists}}\cup\textnormal{AP}_{f}$. The automaton
$\mathcal{A}$ can then be built working directly on
${\textnormal{AP}_{\exists}}$, with $\mathcal{W}^{\psi}$ reading valuations
for ${\textnormal{AP}_{\exists}}$ in the input tree and those for atoms in
$\textnormal{AP}_{f}$ in the current state of $\mathcal{S}$. Because we do not
need to guess valuations of maximal state subformulas and launch additional
automata to check that these guesses are correct, we obtain a nondeterministic
automaton. Finally, for a formula of the form
$\exists^{\textnormal{{o}}}p.\,\varphi$, to build automaton
$\mathcal{A}_{s}^{\exists^{\textnormal{{o}}}p.\,\varphi}$ we first build
$\mathcal{A}_{s}^{\varphi}$, which we then narrow down to work on
$L_{\textnormal{{o}}}$-trees. Since the narrowing operation introduces
alternation, we need to nondeterminise the resulting automaton before
projecting it with respect to $p$. Now observe that if
$I_{\varphi}=\textnormal{{o}}$ we do not need to perform this narrowing, and
thus if $\mathcal{A}_{s}^{\varphi}$ is a nondeterministic automaton we can
directly perform the projection. This justifies the definition of the first
component; for the second one, observe that the projection of a
nondeterministic automaton is also nondeterministic.

###### Example 4.11.

Assume that $n=3$, i.e., states of CKS have three components (recall that
$[3]=\\{1,2,3\\}$). Let us consider formula
$\varphi=\forall^{\\{1,3\\}}p.\,\forall^{[3]}q.\,\exists^{[3]}r.\,{\bf E}{\bf
G}(p\wedge q\vee r)$. We describe how its simulation depth is computed. First,
let us rewrite
$\varphi=\neg\exists^{\\{1,3\\}}p.\,\exists^{[3]}q.\,\neg\exists^{[3]}r.\,{\bf
E}{\bf G}(p\wedge q\vee r)$.

Since ${\bf G}(p\wedge q\vee r)$ is an LTL formula, $\mbox{sd}({\bf E}{\bf
G}(p\wedge q\vee r))=(0,\mbox{nd})$. Next, because $I_{{\bf E}{\bf G}(p\wedge
q\vee r)}=[3]$, it follows that $\mbox{sd}(\exists^{[3]}r.\,{\bf E}{\bf
G}(p\wedge q\vee r))=(0,\mbox{nd})$, and $\mbox{sd}(\neg\exists^{[3]}r.\,{\bf
E}{\bf G}(p\wedge q\vee r))=(0,\mbox{alt})$. Next we have that
$\mbox{sd}(\exists^{[3]}q.\,\neg\exists^{[3]}r.\,{\bf E}{\bf G}(p\wedge q\vee
r))=(1,\mbox{nd})$. This reflects the fact that the automaton obtained for
formula $\neg\exists^{[3]}r.\,{\bf E}{\bf G}(p\wedge q\vee r)$, which is
alternating because of complementation, needs to be simulated before
projecting it over $q$. Then, because $\\{1,3\\}\neq[3]$, it holds that
$\mbox{sd}(\exists^{\\{1,3\\}}p.\,\exists^{[3]}q.\,\neg\exists^{[3]}r.\,{\bf
E}{\bf G}(p\wedge q\vee r))=(2,\mbox{nd})$: to project over $p$ we first need
to narrow down the previous automaton to make it see only components 1 and 3,
and because the narrowing operation introduces alternation, the resulting
automaton needs to be simulated before projecting it. Finally, we get that
$\mbox{sd}(\varphi)=(2,\mbox{alt})$

We now introduce two additional depth measures on
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ formulas, which help
us establish more precise upper bounds on the sizes of the automata we build.
For every $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ formula
$\varphi$, we let ${\bf E}\mathrm{d}(\varphi)$ be the maximum number of nested
path quantifiers ${\bf E}$ in $\varphi$, and $\exists\mathrm{d}(\varphi)$ is
the maximum number of nested second-order quantifiers $\exists$ in $\varphi$.
We also inductively define the function $\mathrm{exp}\big{(}k\mid n\big{)}$,
for $k,n\in\mathbb{N}$, as follows: $\mathrm{exp}\big{(}0\mid n\big{)}:=n$ and
$\mathrm{exp}\big{(}k+1\mid n\big{)}:=2^{\mathrm{exp}\big{(}k\mid n\big{)}}$.

###### Proposition 4.12.

Let $\Phi$ be a $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subseteq}$}}$ formula, $\mathcal{S}$ a CKS and $s\in\mathcal{S}$ a
state.

  * •

If $\mbox{sd}_{k}(\Phi)=0$, $\mathcal{A}_{s}^{\Phi}$ has at most
$f_{\mathcal{S}}^{\Phi}$ states and 2 colours, and

  * •

if $\mbox{sd}_{k}(\Phi)\geq 1$, $\mathcal{A}_{s}^{\Phi}$ has at most
$\mathrm{exp}\big{(}\mbox{sd}_{k}(\Phi)\mid f_{\mathcal{S}}^{\Phi}\log
f_{\mathcal{S}}^{\Phi}\big{)}$ states and its number of colours is at most
$\mathrm{exp}\big{(}\mbox{sd}_{k}(\Phi)-1\mid f_{\mathcal{S}}^{\Phi}\log
f_{\mathcal{S}}^{\Phi}\big{)}$,

where
$f_{\mathcal{S}}^{\Phi}=m_{1}^{\exists\mathrm{d}(\Phi)}|\Phi||\mathcal{S}|^{{\bf
E}\mathrm{d}(\Phi)}2^{m_{2}|\Phi|{\bf E}\mathrm{d}(\Phi)}$, with
$m_{1},m_{2}\in\mathbb{N}$ constants.

Also, if $\mathcal{A}_{s}^{\varphi}$ has state set $Q$ then for each $q\in Q$
and $a\in 2^{{\textnormal{AP}_{\exists}}(\Phi)}$ we have
$|\delta(q,a)|\leq|\mathcal{S}||Q|^{|\mathcal{S}|}2^{H|\varphi|}$, where
$H=1+{\bf E}\mathrm{d}(\varphi)$.

Constants $m_{1}$ and $m_{2}$ are derived from constants in the complexity of,
respectively, the simulation procedure, and the procedure that builds a
nondeterministic word automaton for an LTL formula. For more detail, see the
proof of Proposition 4.12 in Appendix A.

From this we get the following complexity result.

###### Proposition 4.13.

The model-checking problem for
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i,$\tiny{\subseteq}$}}$
formulas of simulation depth at most $k$ is $(k+1)$-Exptime -complete.

###### Proof.

We start with the upper bounds. For an instance $(\Phi,\mathcal{S})$, our
decision procedure in Section 4.3 first builds automaton
$\mathcal{A}_{s_{\iota}}^{\Phi}$, and concludes by testing whether the full
$S_{\Phi}$-tree with empty labelling $t$ is accepted by
$\mathcal{A}_{s_{\iota}}^{\Phi}$. This can be done in time
$O((|\mathcal{A}_{s_{\iota}}^{\Phi}|\cdot|t|)^{l})$, where $|t|$ is the size
of a smallest Kripke structure representing the regular tree $t$,
$|\mathcal{A}_{s_{\iota}}^{\Phi}|$ is the sum of the number of states and
sizes of formulas in the transition function of
$\mathcal{A}_{s_{\iota}}^{\Phi}$, and $l$ the number of colours it uses
(Löding, 2011). Clearly $t$ can be represented by a Kripke structure of size
$|S_{\Phi}|$, so that $|t|\leq|S_{\Phi}|\leq|\mathcal{S}|$.

By Proposition 4.12, each formula in the transition function of
$\mathcal{A}_{s_{\iota}}^{\Phi}$ is of size at most
$|\mathcal{S}||Q|^{|\mathcal{S}|}2^{H|\Phi|}$, where $Q$ is the set of states
in $\mathcal{A}_{s_{\iota}}^{\Phi}$ and $H=1+{\bf E}\mathrm{d}(\Phi)$. There
are at most $|Q|2^{|{\textnormal{AP}_{\exists}}(\Phi)|}$ such formulas333In
fact the final automaton $\mathcal{A}_{s_{\iota}}^{\Phi}$ does not read
anything in its input, hence the alphabet could be considered to be a
singleton. We thus have only $|Q|$ different formulas in the transition
function, at most. and $|{\textnormal{AP}_{\exists}}(\Phi)|\leq|\Phi|$, so
that
$|\mathcal{A}_{s_{\iota}}^{\Phi}|\leq|Q|+|Q|2^{|{\textnormal{AP}_{\exists}}(\Phi)|}|\mathcal{S}||Q|^{|\mathcal{S}|}2^{H|\Phi|}\leq
2|\mathcal{S}||Q|^{|\mathcal{S}|+1}2^{(H+1)|\Phi|}$. Also $H+1\leq|\Phi|$, so
we finally have $|\mathcal{A}_{s_{\iota}}^{\Phi}|\leq
2|\mathcal{S}||Q|^{|\mathcal{S}|+1}2^{|\Phi|^{2}}$.

If $k=0$, by Proposition 4.12 $\mathcal{A}_{s_{\iota}}^{\Phi}$ has at most
$f_{\mathcal{S}}^{\Phi}$ states and 2 colours, and $f_{\mathcal{S}}^{\Phi}$ is
polynomial in $|\mathcal{S}|$ but exponential in $|\Phi|$. Therefore
$|\mathcal{A}_{s_{\iota}}^{\Phi}|$ is exponential in $|\Phi|$ and in
$|\mathcal{S}|$, and so is the complexity of checking that $t$ is accepted by
$\mathcal{A}_{s_{\iota}}^{\Phi}$.

If $k\geq 1$, by Proposition 4.12, $|Q|$ is $k$-exponential in
$f_{\mathcal{S}}^{\Phi}\log f_{\mathcal{S}}^{\Phi}$, and
$f_{\mathcal{S}}^{\Phi}\log f_{\mathcal{S}}^{\Phi}$ itself is polynomial in
$|\mathcal{S}|$ but exponential in $|\Phi|$. As a result,
$|\mathcal{A}_{s_{\iota}}^{\Phi}|$ is $(k+1)$-exponential in $|\Phi|$ and
$k$-exponential in $|\mathcal{S}|$. Finally, still by Proposition 4.12, the
number of colours $l$ is $(k-1)$-exponential in $f_{\mathcal{S}}^{\Phi}\log
f_{\mathcal{S}}^{\Phi}$, hence $k$-exponential in $|\Phi|$. Checking that $t$
is accepted by $\mathcal{A}_{s_{\iota}}^{\Phi}$ can thus be done in time
$(k+1)$-exponential in $|\Phi|$, and $k$-exponential in $|\mathcal{S}|$, which
finishes to establish the upper bounds.

For the lower bounds, consider the fragment
$\textnormal{{EQ}}^{k}\textnormal{{CTL}}^{*}$ of $\textnormal{{QCTL}}^{*}$
(with perfect information) which consists in formulas in prenex normal form,
i.e., with all second-order quantifications at the beginning, with at most $k$
alternations between existential and universal quantifiers, counting the first
quantifier as one alternation (see (Laroussinie and Markey, 2014, p.8) for a
formal definition). Clearly, $\textnormal{{EQ}}^{k}\textnormal{{CTL}}^{*}$ is
a fragment of $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ (with
$n=1$), and formulas of $\textnormal{{EQ}}^{k}\textnormal{{CTL}}^{*}$ have
simulation depth at most $k$. It is proved in (Laroussinie and Markey, 2014)
that model checking $\textnormal{{EQ}}^{k}\textnormal{{CTL}}^{*}$ is
$(k+1)$-Exptime -hard. ∎

######  Remark 3.

One may wonder why we do not get our lower bounds from the distributed
synthesis problem in systems with hierarchical information. The reason is that
this problem is $k$-Exptime -complete for LTL or $\textnormal{{CTL}}^{*}$
specifications (Pnueli and Rosner, 1990; Kupferman and Vardi, 2001) and can be
expressed with formulas of simulation depth $k$, and thus would only provide
$k$-Exptime lower-bounds for simulation depth $k$, while our problem is
$k+1$-Exptime -complete. This may seem surprising, but we point out that
thanks to alternation of existential and universal quantifiers,
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize ii}}$ formulas with