Raphaël Berthon, Bastien Maubert and Aniello Murano

# Quantified CTL with imperfect information111This project has received
funding from the European Union’s Horizon 2020 research and innovation
programme under the Marie Sklodowska-Curie grant agreement No 709188.

Raphaël Berthon  École Normale Supérieure de Rennes, France
<EMAIL_ADDRESS>Bastien Maubert  Università degli Studi di
Napoli Federico II, Italy
<EMAIL_ADDRESS>Aniello Murano  Università degli Studi di Napoli
Federico II, Italy
<EMAIL_ADDRESS>
###### Abstract.

Quantified CTL (QCTL) is a well-studied temporal logic that extends CTL with
quantification over atomic propositions. It has recently come to the fore as a
powerful intermediary framework to study logics for strategic reasoning. We
extend it to include imperfect information by parameterising quantifiers with
an observation that defines how well they observe the model, thus constraining
their behaviour. We consider two different semantics, one related to the
notion of _no memory_ , the other to _perfect recall_. We study the
expressiveness of our logic, and show that it coincides with MSO for the first
semantics and with MSO with equal level for the second one. We establish that
the model-checking problem is Pspace -complete for the first semantics. While
it is undecidable for the second one, we identify a syntactic fragment,
defined by a notion of hierarchical formula, which we prove to be decidable
thanks to an automata-theoretic approach.

###### Key words and phrases:

Temporal logics, formal verification, imperfect information, automata,
strategic reasoning, MSO

###### 1991 Mathematics Subject Classification:

F.4.1 Mathematical Logic

##  1\. Introduction

Temporal logic is a powerful framework widely used in formal system-design and
verification [9, 41]. It allows reasoning over the temporal evolution of a
system, without referring explicitly to the elapsing of time. One of the most
significant contributions of the field is _model checking_ , which allows to
verify system correctness by checking whether a mathematical model of the
system satisfies a temporal logic formula expressing its desired behaviour [8,
9, 26, 27].
Depending on the view of the nature of time, two types of temporal logics are
mainly considered. In _linear-time temporal logics_ such as LTL [41] time is
treated as if each moment in time had a unique possible future. Conversely, in
_branching-time temporal logics_ such as CTL [8] and $\textnormal{{CTL}}^{*}$
[16], each moment in time may split into various possible futures; existential
and universal quantifiers then allow expressing properties of either one or
all the possible futures. While LTL is suitable to express path properties,
CTL is more appropriate for state-based ones, and $\textnormal{{CTL}}^{*}$ for
both. These logics are “easy-to-use”, can express important system properties
such as _liveness_ or _safety_ , enjoy good fundamental theoretical properties
such as invariance under tree-unwinding of models, and come with reasonable
complexities for the main related decision problems. For instance, the model-
checking and satisfiability problems for $\textnormal{{CTL}}^{*}$ are Pspace
-Complete [1] and 2-Exptime -Complete [48], respectively.
Along the years, $\textnormal{{CTL}}^{*}$ has been extended in a number of
ways in order to verify the behavior of a broad variety of systems. In multi-
agent open-system verification, _Alternating-Time Temporal Logic_
($\textnormal{{ATL}}^{*}$), introduced by Alur, Henzinger, and Kupferman [3],
is particularly successful. This generalization of $\textnormal{{CTL}}^{*}$
replaces path quantifiers with _strategic modalities_ , that is modalities
over teams of agents that describe the ability to cooperate in order to
achieve a goal against adversaries. $\textnormal{{ATL}}^{*}$ model checking is
a very active area of research and it has been studied in several domains,
including communication protocols [47], fair exchange protocols [21, 19], and
agent-oriented programs [11]. The complexity of the problem has been
extensively studied in a multitude of papers, and algorithms have been
implemented in tools [32]. Remarkably, $\textnormal{{ATL}}^{*}$ has inspired
fresh and more powerful logics such as _Strategy Logic_ (SL) [7, 35, 34],
_$\textnormal{{ATL}}^{*}$ with strategy context_
($\textnormal{{ATL}}^{*}_{\textit{\scriptsize sc}}$) [5, 10],
_$\textnormal{{ATL}}^{*}$ with Irrevocable strategies_
(I$\textnormal{{ATL}}^{*}$) [2] and _Memoryful $\textnormal{{ATL}}^{*}$_
(m$\textnormal{{ATL}}^{*}$) [36]. These logics are progressively overtaking
$\textnormal{{ATL}}^{*}$; in particular this is the case for SL as it can can
express fundamental game-theoretic concepts such as Nash Equilibrium and
Subgame Perfect Equilibrium [34].
In the landscape of temporal logics, another breakthrough contribution comes
from _Quantified $\textnormal{{CTL}}^{*}$_ ($\textnormal{{QCTL}}^{*}$), which
extends $\textnormal{{CTL}}^{*}$ with the possibility to quantify over atomic
propositions [45, 23, 24, 17, 30]. $\textnormal{{QCTL}}^{*}$ turns out to be
very expressive (indeed, it is equivalent to Monadic Second-Order Logic, MSO
for short) and was usefully applied in a number of scenarios. Recently it has
come to the fore as a convenient and uniform intermediary logic to easily
obtain algorithms for $\textnormal{{ATL}}^{*}_{\textit{\scriptsize sc}}$, SL,
as well as related formalisms [30, 33, 34]. Indeed, strategies can be
represented by atomic propositions labelling the execution tree of the game
structure under study, and strategy quantification can thus be expressed by
means of propositional quantifications. As a remark, quantification in
$\textnormal{{QCTL}}^{*}$ can be interpreted either on Kripke structures
(_structure semantics_) or their execution tree (_tree semantics_), allowing
for the encoding of memoryless or perfect-recall strategies, respectively.
This difference impacts also the complexity of the related decision problems:
for instance, moving from structure to tree semantics, model checking jumps
from Pspace to non-elementary.
In game theory and open-system verification an important body of work has been
devoted to _imperfect information_ , which refers to settings in which players
have partial information about the moves taken by the others [6, 13, 20, 25,
42]. This is a common situation in real-life scenarios where players have to
act without having all the relevant information at hand. In computer science
this situation occurs for example when some system’s variables are
internal/private [44]. Imperfect information is usually modelled by
indistinguishability relations over the states of the game. During a play,
some players may not know precisely in which state they are, and therefore
they cannot base their actions on the exact current situation: they must
choose their actions uniformly over indistinguishable states [25].
This uniformity constraint deeply impacts the complexity of decision problems.
It is well known that multi-player games with imperfect information are
computationally hard, in general undecidable [38], and to retain positive
complexity results one needs to restrict players’ capabilities, by bounding
their memory of past moves [12] or putting some hierarchical order over their
observational power [42]. Unfortunately, most of the approaches exploited
under full observation are not appropriate for imperfect information. In
particular this is the case of $\textnormal{{QCTL}}^{*}$, unless opportunely
adapted. In this paper we work in this direction by incorporating in
$\textnormal{{QCTL}}^{*}$ the essence of imperfect information, that is the
uniformity constraint on choices. We believe it may provide a uniform
framework to obtain new results on logics for strategic reasoning under
imperfect information, as does $\textnormal{{QCTL}}^{*}$ in the perfect
information setting.
Our contribution. We introduce
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$, an opportune extension
of $\textnormal{{QCTL}}^{*}$ that integrates the central feature of imperfect
information, _i.e._ , uniformity constraint on choices. We add internal
structure to the states of the models, much like in Reif’s multiplayer game
structures [38] or distributed systems [18], and we parameterise propositional
quantifiers with observations that define what portions of the states a
quantifier can “observe”. The semantics is adapted to capture the idea of
quantifications on atomic propositions being made with partial observation.
Like in [30], we consider both structure and tree semantics.
We study the expressive power of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$. By using the same
argument as for $\textnormal{{QCTL}}^{*}$ [30], we first show that
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ and
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ are equally expressive for
both semantics. Then we prove that for the structure semantics, these logics
are no more expressive than QCTL, and thus coincide with MSO. Finally we show
that under tree semantics $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$
is expressively equivalent to MSO extended with the equal level predicate
($\textnormal{{MSO}}_{\textnormal{eq}}$, see [14, 31, 46]).
Concerning the model-checking problem we first prove that under structure
semantics it is Pspace -complete for both
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ and
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$, like QCTL. Under tree
semantics, undecidability follows from the equivalence with
$\textnormal{{MSO}}_{\textnormal{eq}}$. However we identify a decidable
syntactic fragment, consisting of those formulas in which nested quantifiers
have hierarchically ordered observations, innermost ones observing more than
outermost ones. We call such formulas _hierarchical formulas_. Interestingly,
a decidability result for Quantified $\mu$-Calculus with partial observation
[40] uses a similar syntactic restriction. This logic is very close to ours,
but orthogonal: while our tree semantics relies on a synchronous perfect-
recall notion of imperfect information, theirs is asynchronous. This
hierarchical restriction is also related to decidability results for games
with imperfect information [39, 4] and distributed synthesis [22]. Our
decision procedure relies on automata constructions involving the _narrowing_
operation introduced by Kupferman and Vardi in [28] for distributed synthesis.
We believe that our choice of modelling imperfect information by means of
local states eases greatly the use of automata techniques to tackle imperfect
information. Finally, our result provides new decidability results for
$\textnormal{{ATL}}^{*}_{\textit{\scriptsize sc}}$ with imperfect information
(not presented here), and we trust it will find applications in other logics,
such as SL with imperfect information.
Plan. In Section 2 we recall Kripke structures and trees, and the syntax and
semantics of $\textnormal{{QCTL}}^{*}$. We then present
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ in Section 3, we study
its expressiveness in Section 4 and its model-checking problem in Section 5.
We conclude and discuss future work in Section 6.

##  2\. Preliminaries

Let $\Sigma$ be an alphabet. A _finite_ (resp. _infinite_) _word_ over
$\Sigma$ is an element of $\Sigma^{*}$ (resp. $\Sigma^{\omega}$). The empty
word is classically noted $\epsilon$, and
$\Sigma^{+}=\Sigma^{*}\setminus\\{\epsilon\\}$. The _length_ of a word is
$|w|:=0$ if $w$ is the empty word $\epsilon$, if $w=w_{0}w_{1}\ldots w_{n}$ is
a finite non-empty word then $|w|:=n+1$, and for an infinite word $w$ we let
$|w|:=\omega$. Given a word $w$ and $0\leq i,j\leq|w|-1$, we let $w_{i}$ be
the letter at position $i$ in $w$ and $w[i,j]$ be the subword of $w$ that
starts at position $i$ and ends at position $j$. If $w$ is infinite, we let
$w^{i}:=w[i,\omega]$. We write $w\preccurlyeq w^{\prime}$ if $w$ is a prefix
of $w^{\prime}$, and ${w}^{\preccurlyeq}$ is the set of finite prefixes of
word $w$. Finally, for $n\in\mathbb{N}$ we let $[n]:=\\{1,\ldots,n\\}$.

###  2.1. Kripke structures and trees

Let $\mathcal{AP}$ be a countably infinite set of _atomic propositions_ and
let $\textit{AP}\subset\mathcal{AP}$ be a finite subset.

######  Definition 2.1.

A _Kripke structure_ over AP is a tuple $\mathcal{S}=(S,R,\ell)$ where $S$ is
a set of _states_ , $R\subseteq S\times S$ is a left-total222 _i.e._ , for all
$s\in S$, there exists $s^{\prime}$ such that $(s,s^{\prime})\in R$.
_transition relation_ and $\ell:S\to 2^{\textit{AP}}$ is a _labelling
function_.

A _pointed Kripke structure_ is a pair $(\mathcal{S},s)$ where
$s\in\mathcal{S}$, and the _size_ $|\mathcal{S}|$ of a Kripke structure
$\mathcal{S}$ is its number of states. A _path_ in a structure
$\mathcal{S}=(S,R,\ell)$ is an infinite word $\lambda\in S^{\omega}$ such that
for all $i\in\mathbb{N}$, $(\lambda_{i},\lambda_{i+1})\in R$. For $s\in S$, we
let $\text{Paths}(s)$ be the set of all paths that start in $s$. A _finite
path_ is a finite non-empty prefix of a path.

We now define (infinite) trees. In many works, trees are defined as prefixed-
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 as a sequence of states and the root as the initial state, hence
the following definition, where $X$ is a finite set:

######  Definition 2.2.

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$;

  * •

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

  * •

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$. An $X$-tree is _full_ if every node $u$
has a child $u\cdot x$ for each $x\in X$. The _depth_ of a node $u$ is $|u|$.
Similarly to Kripke structures, a _path_ 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$.
An _AP -labelled $X$-tree_, or _$(\textit{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^{\textit{AP}}$ is a _labelling_. For a labelled tree
$t=(\tau,\ell)$ and an atomic proposition $p\in\mathcal{AP}$, we define the
_$p$ -projection of $t$_ as the labelled tree
$t\\!\Downarrow_{p}\;:=(\tau,\ell\\!\Downarrow_{p})$, where for each
$u\in\tau$, $\ell\\!\Downarrow_{p}\\!(u):=\ell(u)\setminus\\{p\\}$. For a set
of trees $\mathcal{L}$, we let
$\mathcal{L}\\!\Downarrow_{p}\;:=\\{t\\!\Downarrow_{p}\;\mid
t\in\mathcal{L}\\}$.

######  Definition 2.3 (Tree unfoldings).

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

###  2.2. $\textnormal{{QCTL}}^{*}$, syntax and semantics

We recall the syntax of $\textnormal{{QCTL}}^{*}$, as well as both the
structure and tree semantics.

######  Definition 2.4.

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

$\displaystyle\varphi:=$
$\displaystyle\;p\mid\neg\varphi\mid\varphi\vee\varphi\mid{\bf
E}\psi\mid\exists 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\mathcal{AP}$. Formulas of type $\varphi$ are called _state
formulas_ , those of type $\psi$ are called _path formulas_ , and
$\textnormal{{QCTL}}^{*}$ consists of state formulas.

Like in [30] we consider two different semantics, the _structure semantics_
and the _tree semantics_ : in the former formulas are evaluated directly on
the structure, while in the latter the structure is first unfolded into an
infinite tree. In the first case, quantifying over $p$ means choosing a truth
value for $p$ in each state of the structure, while in the second case it is
possible to choose a different truth value for $p$ in each finite path of the
structure.

####  2.2.1. Structure semantics

A $\textnormal{{QCTL}}^{*}$ state (resp. path) formula is evaluated in a state
(resp. path) of a Kripke structure. To define the semantics of quantifications
over propositions, the following definition is handy.

######  Definition 2.5.

For $p\in\mathcal{AP}$, two structures $\mathcal{S}=(S,R,\ell)$ and
$\mathcal{S}^{\prime}=(S^{\prime},R^{\prime},\ell^{\prime})$ are _equivalent
modulo $p$_, written $\mathcal{S}\equiv_{p}\mathcal{S}^{\prime}$, if
$S=S^{\prime}$, $R=R^{\prime}$ and for each state $s\in S$,
$\ell(s)\setminus\\{p\\}=\ell^{\prime}(s)\setminus\\{p\\}$. This definition
also applies to labelled trees seen as infinite Kripke structures.

The satisfaction relation $\models_{s}$ for the structure semantics is defined
inductively as follows, where $\mathcal{S}=(S,R,\ell)$ is a Kripke structure,
$s$ is a state and $\lambda$ is a path in $\mathcal{S}$:

$\begin{array}[]{lclclcl}\mathcal{S},s\models_{s}p&\mbox{if}&p\in\ell(s)&\makebox[0.0pt]{}&\mathcal{S},s\models_{s}\neg\varphi&\mbox{if}&\mathcal{S},s\not\models_{s}\varphi\\\
\mathcal{S},s\models_{s}\varphi\vee\varphi^{\prime}&\mbox{if}&\mathcal{S},s\models_{s}\varphi\mbox{
or }\mathcal{S},s\models_{s}\varphi^{\prime}\\\ \mathcal{S},s\models_{s}{\bf
E}\psi&\mbox{if}&\lx@intercol\mbox{there exists
}\lambda\in\text{Paths}(s)\mbox{ such that
}\mathcal{S},\lambda\models_{s}\psi\hfil\lx@intercol\\\
\mathcal{S},s\models_{s}\exists p.\;\varphi&\mbox{if}&\lx@intercol\mbox{there
exists }\mathcal{S}^{\prime}\equiv_{p}\mathcal{S}\mbox{ such that
}\mathcal{S}^{\prime},s\models\varphi\hfil\lx@intercol\\\
\mathcal{S},\lambda\models_{s}\varphi&\mbox{if}&\mathcal{S},\lambda_{0}\models_{s}\varphi&\makebox[0.0pt]{}&\mathcal{S},\lambda\models_{s}\neg\psi&\mbox{if}&\mathcal{S},\lambda\not\models_{s}\psi\\\
\mathcal{S},\lambda\models_{s}\psi\vee\psi^{\prime}&\mbox{if}&\mathcal{S},\lambda\models_{s}\psi\mbox{
or
}\mathcal{S},\lambda\models_{s}\psi^{\prime}&\makebox[0.0pt]{}&\mathcal{S},\lambda\models_{s}{\bf
X}\psi&\mbox{if}&\mathcal{S},\lambda^{1}\models_{s}\psi\\\
\mathcal{S},\lambda\models_{s}\psi{\bf
U}\psi^{\prime}&\mbox{if}&\lx@intercol\mbox{there exists }i\geq 0\mbox{ such
that }\mathcal{S},\lambda^{i}\models_{s}\psi^{\prime}\mbox{ and for }0\leq
j<i,\;\mathcal{S},\lambda^{j}\models_{s}\psi\hfil\lx@intercol\end{array}$

####  2.2.2. Tree semantics

In the tree semantics, a formula holds in a state $s$ of a structure
$\mathcal{S}$ if it holds in the tree-unfolding of $\mathcal{S}$ from $s$. The
semantics of $\textnormal{{QCTL}}^{*}$ on trees could be derived from the
structure semantics, seeing $2^{\textit{AP}}$-labelled trees as infinite-state
Kripke structures. We define it explicitly on trees though, as it will make
the presentation of the semantics for
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ clearer.

The satisfaction relation $\models_{t}$ for the tree semantics is thus defined
inductively as follows, where $t=(\tau,\ell)$ is a $2^{\textit{AP}}$-labelled
$X$-tree, $u$ is a node and $\lambda$ is a path in $\tau$:

$\begin{array}[]{lclclcl}t,u\models_{t}p&\mbox{if}&p\in\ell(u)&\makebox[0.0pt]{}&t,u\models_{t}\neg\varphi&\mbox{if}&t,u\not\models_{t}\varphi\\\
t,u\models_{t}\varphi\vee\varphi^{\prime}&\mbox{if}&\lx@intercol
t,u\models_{t}\varphi\mbox{ or
}t,u\models_{t}\varphi^{\prime}\hfil\lx@intercol\\\ t,u\models_{t}{\bf
E}\psi&\mbox{if}&\lx@intercol\mbox{there exists }\lambda\in Paths(u)\mbox{
such that }t,\lambda\models_{t}\psi\hfil\lx@intercol\\\ t,u\models_{t}\exists
p.\;\varphi&\mbox{if}&\lx@intercol\mbox{there exists
}t^{\prime}\equiv_{p}t\mbox{ such that
}t^{\prime},u\models\varphi\hfil\lx@intercol\\\
t,\lambda\models_{t}\varphi&\mbox{if}&t,\lambda_{0}\models_{t}\varphi&\makebox[0.0pt]{}&t,\lambda\models_{t}\neg\psi&\mbox{if}&t,\lambda\not\models_{t}\psi\\\
t,\lambda\models_{t}\psi\vee\psi^{\prime}&\mbox{if}&t,\lambda\models_{t}\psi\mbox{
or
}t,\lambda\models_{t}\psi^{\prime}&\makebox[0.0pt]{}&t,\lambda\models_{t}{\bf
X}\psi&\mbox{if}&t,\lambda^{1}\models_{t}\psi\\\ t,\lambda\models_{t}\psi{\bf
U}\psi^{\prime}&\mbox{if}&\lx@intercol\mbox{there exists }i\geq 0\mbox{ such
that }t,\lambda^{i}\models_{t}\psi^{\prime}\mbox{ and for }0\leq
j<i,\;t,\lambda^{j}\models_{t}\psi\hfil\lx@intercol\end{array}$

We may write $t\models_{t}\varphi$ for $t,r\models_{t}\varphi$, where $r$ is
the root of $t$, and given a Kripke structure $\mathcal{S}$, a state $s$ and a
$\textnormal{{QCTL}}^{*}$ formula $\varphi$, we write
$\mathcal{S},s\models_{t}\varphi$ if $t_{\mathcal{S},s}\models_{t}\varphi$.

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

We now enrich the models, syntax and semantics to capture the idea of
quantifications on atomic propositions being made with a partial observation
of the system.

###  3.1. Compound Kripke structures

First, we enrich Kripke structures by adding internal structure to states: we
set them as tuples of local states. To ease presentation and obtain finite
alphabets for our tree automata in Section 5.2.2, we fix a collection
$\\{L_{i}\\}_{i\in[n]}$ of $n$ disjoint finite sets of _local states_.

For $I\subseteq[n]$, we let $X_{I}:={}_{i\in I}L_{i}$. Let $J\subseteq
I\subseteq[n]$. For $x=(l_{i})_{i\in I}\in X_{I}$, we define the _$X_{J}$
-projection_ of $x$ as $x\\!\downarrow_{X_{J}}:=(l_{i})_{i\in J}$. If
$J=\emptyset$, we let $x\\!\downarrow_{\emptyset}:=\mathbf{0}$, where
$\mathbf{0}$ is a special symbol, and we let
$X_{\emptyset}:=\\{\mathbf{0}\\}$. This definition extends naturally to words
and trees over $X_{I}$. Observe that when projecting a tree, nodes with same
projection are merged. In particular, for every $X_{I}$-tree $\tau$,
$\tau\\!\downarrow_{\emptyset}$ is the only $X_{\emptyset}$-tree,
$\mathbf{0}^{\omega}$. We also define a _lift_ operator $\\!\uparrow^{I}_{y}$
that, given an $X_{J}$-tree rooted in $x$ and a tuple $y\in X_{I\setminus J}$,
produces the $X_{I}$-tree rooted in $(x,y)$ defined as
$\tau\\!\uparrow^{X_{I}}_{y}:=\\{u\in(x,y)\cdot X_{I}^{*}\mid
u\\!\downarrow_{X_{J}}\in\tau\\}$. Observe that because the sets
$\\{L_{i}\\}_{i\in[n]}$ are disjoint, the ordering of elements in tuples of
$X_{I}$ does not matter. For an $(\textit{AP},X_{J})$-tree $t=(\tau,\ell)$, we
define $t\\!\uparrow^{X_{I}}_{y}:=(\tau\\!\uparrow^{X_{I}}_{y},\ell^{\prime})$
where $\ell^{\prime}(u):=\ell(u\\!\downarrow_{X_{J}})$. In the following we
may write $\\!\uparrow^{I}_{y}$ for $\\!\uparrow^{X_{I}}_{y}$, and
$\\!\downarrow_{J}$ instead of $\\!\downarrow_{X_{J}}$.

######  Definition 3.1.

A _compound Kripke structure_ , or CKS , is a Kripke structure
$\mathcal{S}=(S,R,\ell)$ such that $S\subseteq X_{[n]}$. We call $n$ the
_dimension_ of CKSs.

######  Remark 3.2.

Note that by fixing finite sets of local states, we also fix a finite set of
possible states. If it were not so, our translation from
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ to QCTL in Theorem 4.2, as
well as the one from $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ to
$\textnormal{{MSO}}_{\textnormal{eq}}$ in Theorem 4.6 would no longer be
valid, making us also lose Corollary 4.5. We would no longer have equivalence
in expressivity, but we would still have that
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ is at least as expressive
as MSO (resp. $\textnormal{{MSO}}_{\textnormal{eq}}$) for structure semantics
(resp. tree semantics). Also our results on model checking in Section 5, and
in particular our main result, Theorem 5.9, would still be valid.

To model the fact that quantifiers may not observe some local states, we
define a notion of observation and the associated notion of observational
indistinguishability.

######  Definition 3.3.

An _observation_ is a finite set of indices $o\subset\mathbb{N}$. For an
observation $o$ and $I\subseteq[n]$, two tuples $x,x^{\prime}\in X_{I}$ are
_$o$ -indistinguishable_, written $x\sim_{o}x^{\prime}$, if
$x\\!\downarrow_{I\cap o}=x^{\prime}\\!\downarrow_{I\cap o}$.

Intuitively, a quantifier with observation $o$ must choose the valuation of
atomic propositions _uniformly_ with respect to $o$, and this notion of
uniformity will vary between the structure semantics and the tree semantics.
But first, let us introduce the syntax of
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$.

###  3.2. $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$, syntax and
semantics

The syntax of $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ is that
of $\textnormal{{QCTL}}^{*}$, except that quantifiers over atomic propositions
are parameterised by a set of indices that defines what local states the
quantifier can “observe”.

######  Definition 3.4.

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

$\displaystyle\varphi:=$
$\displaystyle\;p\mid\neg\varphi\mid\varphi\vee\varphi\mid{\bf
E}\psi\mid\exists^{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\mathcal{AP}$ and $o\subset\mathbb{N}$ is an observation.

We use standard abbreviations: $\top:=p\vee\neg p$, $\perp:=\neg\top$, ${\bf
F}\psi:=\top{\bf U}\psi$, ${\bf G}\psi:=\neg{\bf F}\neg\psi$ and ${\bf
A}\psi:=\neg{\bf E}\neg\psi$. The size $|\varphi|$ of a formula $\varphi$ is
defined inductively as usual, but the following case:
$|\exists^{o}p.\;\varphi|:=1+|o|+|\varphi|$. We also classically define the
syntactic fragment $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$:

######  Definition 3.5.

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

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

where $p\in\mathcal{AP}$ and $o\subset\mathbb{N}$ is an observation.

####  3.2.1. Structure semantics

In the case of structure semantics, uniformity is defined as follows:

######  Definition 3.6.

Let $\mathcal{S}=(S,R,\ell)$ be a CKS , $p\in\mathcal{AP}$ and
$o\subset\mathbb{N}$. $\mathcal{S}$ is _$o$ -uniform in $p$_ if for every pair
of states $s,s^{\prime}\in S$ such that $s\sim_{o}s^{\prime}$, it holds that
$p\in\ell(s)$ if and only if $p\in\ell(s^{\prime})$.

We enrich the satisfaction relation $\models_{s}$ with the following inductive
case, where $(\mathcal{S},s)$ is a pointed CKS :

$\begin{array}[]{lcl}\mathcal{S},s\models_{s}\exists^{o}p.\;\varphi&\mbox{if}&\mbox{there
exists }\mathcal{S}^{\prime}\equiv_{p}\mathcal{S}\mbox{ such that
}\mathcal{S}^{\prime}\mbox{ is $o$-uniform in $p$ and
}\mathcal{S}^{\prime},s\models_{s}\varphi\end{array}$

Observe that $\exists^{\\{1,\ldots,n\\}}p.\;\varphi$ is equivalent to the
$\textnormal{{QCTL}}^{*}$ formula $\exists p.\;\varphi$.

####  3.2.2. Tree semantics

As observed in the introduction, propositional quantifiers can be seen as
having perfect recall in the tree semantics and no memory in the structure
semantics. The following definition for indistinguishability on trees, which
differs from that for CKS , reflects this difference.

######  Definition 3.7.

Let $t=(\tau,\ell)$ be a labelled $X_{I}$-tree, $p\in\mathcal{AP}$ an atomic
proposition and $o\subset\mathbb{N}$ an observation. Two nodes $u=u_{0}\ldots
u_{i}$ and $u^{\prime}=u^{\prime}_{0}\ldots u^{\prime}_{j}$ of $\tau$ are _$o$
-indistinguishable_, written $u\approx_{o}u^{\prime}$, if $i=j$ and for all
$k\in\\{0,\ldots,i\\}$ we have $u_{k}\sim_{o}u^{\prime}_{k}$. Tree $t$ is _$o$
-uniform in $p$_ if for every pair of nodes $u,u^{\prime}\in\tau$ such that
$u\approx_{o}u^{\prime}$, we have $p\in\ell(u)$ iff $p\in\ell(u^{\prime})$.

The tree semantics for $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$
is defined on labelled $X_{n}$-trees, and it is obtained by enriching
$\models_{t}$ as follows:

$\begin{array}[]{lcl}t,u\models_{t}\exists^{o}p.\;\varphi&\mbox{if}&\mbox{there
exists }t^{\prime}\equiv_{p}t\mbox{ such that }t^{\prime}\mbox{ is $o$-uniform
in $p$ and }t^{\prime},u\models_{t}\varphi.\end{array}$

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$. Therefore, evaluating the
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ formula
$\exists^{\emptyset}p.\;\mathbf{border}(p)$ amounts to choosing a level of the
tree where to place one horizontal line of $p$’s.

##  4\. Expressiveness

In this section we study the expressive power of our logics. We first observe
that for both semantics, $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i}}$ and $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ are equally
expressive. We then prove that with structure semantics
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ is expressively equivalent
to QCTL, and thus also to MSO. Finally we show that under tree semantics
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ is expressively
equivalent to MSO with equal level predicate. Note that Theorem 4.2, Corollary
4.5 and Theorem 4.6 below only hold if the logics can talk about the local
states. For this reason, in this section we assume a set of dedicated atomic
propositions $\textit{AP}_{l}=\bigcup_{i\in[n]}\bigcup_{l\in
L_{i}}\\{p_{l}\\}\subset\mathcal{AP}$ such that for every CKS
$\mathcal{S}=(S,R,\ell)$, for each $i\in[n]$ and $l\in L_{i}$, for each state
$s=(l_{1},\ldots,l_{n})\in S$, we have $p_{l}\in\ell(s)$ iff $l_{i}=l$.

###  4.1. $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$,
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ and QCTL

We first remark that for the same reason why $\textnormal{{QCTL}}^{*}$ is no
more expressive than QCTL, also
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ and
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ are equally expressive (the
proof of [30, Proposition 3.8] readily applies):

######  Theorem 4.1.

Under both semantics, $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$
and $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ are expressively
equivalent.

We now prove that for the structure semantics,
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ is no more expressive than
QCTL, and thus has the same expressivity as MSO.

######  Theorem 4.2.

Under structure semantics, $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$
and QCTL are expressively equivalent.

######  Proof 4.3.

It is quite clear that $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$
subsumes QCTL. Observe however that the quantifier on propositions from QCTL
can be translated using the quantifier $\exists^{[n]}$ only because we have
fixed the dimension of our models. If we allowed for models with arbitrary
dimension we would have to add the classic quantifier $\exists$ in the syntax
of $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ for it to capture QCTL.

For the other direction, we define a translation
$\widetilde{\leavevmode\nobreak\ \leavevmode\nobreak\ }$ from
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ to QCTL. We only provide
the inductive case for the quantification on propositions, the others being
trivial.

$\widetilde{\exists^{o}p.\;\varphi}:=\exists
p.\;\left(\bigwedge_{(l_{{1}},\ldots,l_{{k}})\in X_{o\cap[n]}}{\bf A}{\bf
G}(\bigwedge_{i=1}^{k}p_{l_{{i}}}\rightarrow p)\vee{\bf A}{\bf
G}(\bigwedge_{i=1}^{k}p_{l_{{i}}}\rightarrow\neg
p)\right)\wedge\;\widetilde{\varphi}.$

Observe that checking uniformity of $p$ in the reachable part of the model is
sufficient, as the labelling of unreachable states is indifferent. It can be
proven easily that for every CKS $\mathcal{S}$, state $s\in\mathcal{S}$ and
formula $\varphi\in\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$, it holds
that $\mathcal{S},s\models_{s}\varphi\mbox{\;\; iff\;\;
}\mathcal{S},s\models_{s}\widetilde{\varphi}$.

######  Remark 4.4.

One can check that $|\widetilde{\varphi}|=O(nm^{n}|\varphi|)$, where
$m=\max_{i\in[n]}|L_{i}|$.

###  4.2. $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ and MSO with
equal level

We briefly recall the definition $\textnormal{{MSO}}_{\textnormal{eq}}$ (see,
_e.g._ , [14, 46] for more detail). In the following,
$\textit{Var}_{1}=\\{x,y,\ldots\\}$ (resp.
$\textit{Var}_{2}=\\{X,Y,\ldots\\}$) is a countably-infinite set of first-
order (resp. second-order) variables. We also use a predicate $P_{p}$ for each
atomic proposition $p\in\mathcal{AP}$.

The syntax of MSO with equal level relation, or
$\textnormal{{MSO}}_{\textnormal{eq}}$, is given by the following grammar:

$\varphi::=P_{p}(x)\mid x=y\mid S(x,y)\mid x\in
X\mid\text{eq}(x,y)\mid\neg\varphi\mid\varphi\vee\varphi\mid\exists
x.\varphi\mid\exists X.\varphi$

where $p\in\mathcal{AP}$, $x,y\in\textit{Var}_{1}$ and $X\in\textit{Var}_{2}$.

The syntax of MSO is obtained by removing the $\text{eq}(x,y)$ production
rule. We write $\varphi(x_{1},\ldots,x_{i},X_{1},\ldots,X_{j})$ to indicate
that variables $x_{1},\ldots,x_{i}$ and $X_{1},\ldots,X_{j}$ may appear free
in $\varphi$. Without loss of generality we assume that a variable cannot
appear both free and quantified in a formula. We use the standard semantics of
MSO, the successor relation symbol $S$ being interpreted by the transition
relation on Kripke structures, and by the child relation on trees. The
semantics for $\textnormal{{MSO}}_{\textnormal{eq}}$ is only defined on trees,
and $\text{eq}(x,y)$ holds if the nodes denoted by $x$ and $y$ are at the same
depth in the tree. We write
$\mathcal{M},s_{1},\ldots,s_{i},S_{1},\ldots,S_{j}\models\varphi(x_{1},\ldots,x_{i},X_{1},\ldots,X_{j})$
when $\varphi$ holds in model $\mathcal{M}$ when $x_{k}$ (resp. $X_{k}$) is
interpreted as $s_{k}$ (resp. $S_{k}$) for $k\in[i]$ (resp. $k\in[j]$).

Since we aim at comparing the expressivity of MSO (with equal level predicate
in the case of tree semantics) with that of the modal logic
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$, we will consider MSO
formulas of the form $\varphi(x)$, where $x$ is a free variable representing
the point of evaluation in the model.

First, we have seen that under the structure semantics
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ has the same expressivity
as QCTL. Since QCTL has the same expressivity as MSO (evaluated on reachable
parts of the structures) [30], we obtain the following corollary of Theorem
4.2:

######  Corollary 4.5.

Under structure semantics, MSO and
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ are equally expressive.

We now turn to the case of the tree semantics. The constraint put on the tree
semantics for the proposition quantifier involves testing length equality for
arbitrarily long paths or, in terms of trees, comparing the depths of
arbitrarily deep nodes. It is thus not a surprise that
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ with tree semantics is more
expressive than MSO on trees. It also seems natural that extending MSO with
the equal level predicate allows to capture this constraint on proposition
quantification, and thus that $\textnormal{{MSO}}_{\textnormal{eq}}$ is as
expressive as $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ with tree
semantics. We establish with the following theorem that in fact the other
direction also holds.

######  Theorem 4.6.

Under tree semantics, $\textnormal{{MSO}}_{\textnormal{eq}}$ and
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ are equally expressive.

######  Proof 4.7.

We first show how to express in $\textnormal{{MSO}}_{\textnormal{eq}}$ that
two nodes in the unfolding of a CKS are $o$-indistinguishable (see Definition
3.7). Let $o$ be an observation. We define the
$\textnormal{{MSO}}_{\textnormal{eq}}$ formula $\varphi^{o}(x,y)$ as follows:

$\varphi^{o}(x,y):=\text{eq}(x,y)\wedge\forall x^{\prime}.\forall
y^{\prime}.\left(x^{\prime}\preccurlyeq x\wedge y^{\prime}\preccurlyeq
y\wedge\text{eq}(x^{\prime},y^{\prime})\rightarrow\bigwedge_{i\in
o\cap[n]}\bigwedge_{l\in L_{i}}P_{p_{l}}(x^{\prime})\leftrightarrow
P_{p_{l}}(y^{\prime})\right)$

where $x^{\prime}\preccurlyeq x$ is an MSO formula expressing that there is a
path from $x^{\prime}$ to $x$.

Clearly, for every CKS $\mathcal{S}$ and nodes $u,u^{\prime}$ in its unfolding
$t_{\mathcal{S},s}$ from some state $s$,

$t_{\mathcal{S},s},u,u^{\prime}\models\varphi^{o}(x,y)\mbox{ \;\;iff\;\;
}u\approx_{o}u^{\prime}.$

It is then easy to see that $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$
with tree semantics can be translated into
$\textnormal{{MSO}}_{\textnormal{eq}}$: the translation for CTL is standard,
and propositional quantification with imperfect information can be expressed
using second order quantification and the above formula for
$o$-indistinguishability.

For the other direction, we build upon the following translation from MSO to
QCTL, presented in [30]. For
$\varphi(x,x_{1},\ldots,x_{i},X_{1},\ldots,X_{j})\in\textnormal{{MSO}}$, we
inductively define $\widehat{\varphi}$ as:

$\begin{array}[]{rclcrcl}\widehat{P_{p}(x)}&=&p&\mbox{\hskip
56.9055pt}&\widehat{P_{p}(x_{k})}&=&{\bf E}{\bf F}(p_{x_{k}}\wedge
p)\\\\[2.0pt] \widehat{x=x_{k}}&=&p_{x_{k}}&&\widehat{x_{k}=x_{l}}&=&{\bf
E}{\bf F}(p_{x_{k}}\wedge p_{x_{l}})\\\\[2.0pt] \widehat{x\in
X_{k}}&=&p_{X_{k}}&&\widehat{x_{k}\in X_{k}}&=&{\bf E}{\bf F}(p_{x_{k}}\wedge
p_{X_{k}})\\\\[2.0pt]
\widehat{\neg\varphi^{\prime}}&=&\neg\widehat{\varphi^{\prime}}&&\widehat{\varphi_{1}\vee\varphi_{2}}&=&\widehat{\varphi_{1}}\vee\widehat{\varphi_{2}}\\\\[2.0pt]
\widehat{\exists x_{k}.\varphi^{\prime}}&=&\exists
p_{x_{k}}.\;\mathrm{uniq}(p_{x_{k}})\wedge\widehat{\varphi^{\prime}}&&\widehat{\exists
X_{k}.\varphi^{\prime}}&=&\exists
p_{X_{k}}.\;\widehat{\varphi^{\prime}}\\\\[2.0pt] \widehat{S(x,x_{k})}&=&{\bf
E}{\bf X}p_{x_{k}}&&\widehat{S(x_{k},x)}&=&\perp\\\\[2.0pt]
\lx@intercol\hfil\widehat{S(x_{k},x_{l})}\;\;\;=\;\;\;{\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$. Observe that $x$ being
interpreted as the root of a tree it has no incoming edge, hence the
translation of $S(x_{k},x)$.

We extend this translation into one from
$\textnormal{{MSO}}_{\textnormal{eq}}$ to
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ by adding the following
rules:

$\begin{array}[]{rclcrcl}\widehat{\text{eq}(x,x_{k})}&=&p_{x_{k}}&\mbox{\hskip
28.45274pt}&\widehat{\text{eq}(x_{k},x_{l})}&=&\exists^{\emptyset}p.\;\mathbf{border}(p)\wedge{\bf
A}{\bf G}(p_{x_{k}}\rightarrow p\wedge p_{x_{l}}\rightarrow p)\end{array}$

Observe that $x$ being interpreted as the root, $x_{k}$ is on the same level
as $x$ if and only if it is also assigned the root. Concerning the second
case, recall from Section 3.2.2 that the
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ formula
$\exists^{\emptyset}p.\;\mathbf{border}(p)$ places in the tree one unique
horizontal line of $p$’s. Requiring that $x_{k}$ and $x_{l}$ be both on this
line thus ensures that they are on the same level. It is then easy to prove by
induction the following lemma:

######  Lemma 4.8.

For every
$\varphi(x,x_{1},\ldots,x_{i},X_{1},\ldots,X_{j})\in\textnormal{{MSO}}_{\textnormal{eq}}$
and every pointed CKS $(\mathcal{S},s)$,

$t_{\mathcal{S},s},s,u_{1},\ldots,u_{i},U_{1},\ldots,U_{j}\models\varphi(x,x_{1},\ldots,x_{i},X_{1},\ldots,X_{j})\;\;iff\;\;t^{\prime}_{\mathcal{S}}(s),s\models_{t}\widehat{\varphi}$

where $t_{\mathcal{S},s}^{\prime}$ is obtained from $t_{\mathcal{S},s}$ by
changing the labelling for variables $p_{x_{k}}$ and $p_{X_{k}}$ as follows:
$p_{x_{k}}\in\ell^{\prime}(u)$ if $u=u_{k}$ and $p_{X_{k}}\in\ell^{\prime}(u)$
if $u\in U_{k}$.

In particular, it follows that $t_{\mathcal{S},s},s\models\varphi(x)$ iff
$t_{\mathcal{S},s},s\models\widehat{\varphi}$.

######  Remark 4.9.

The two-way translation between $\textnormal{{QCTL}}_{\textnormal{\scriptsize
i}}$ and $\textnormal{{MSO}}_{\textnormal{eq}}$ shows that when local states
are identified by atomic propositions, there is a normal form for
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ formulas involving only
blind and perfect-information quantifiers.

##  5\. Model checking $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$

We now study the model-checking problem for
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$, both for structure and
tree semantics. In other terms, we study the problem of deciding, given a
finite CKS $\mathcal{S}$, a state $s\in\mathcal{S}$ and a
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ formula $\varphi$,
whether it holds that $\mathcal{S},s\models_{s}\varphi$ (or
$\mathcal{S},s\models_{t}\varphi$ for the tree semantics).

###  5.1. Structure semantics

We first prove that under structure semantics, similarly to
$\textnormal{{QCTL}}^{*}$ and QCTL, the model-checking problem is Pspace
-complete for both $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ and
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$. Observe that if $n$ is
fixed the translation from $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$
to QCTL from Theorem 4.2 suffices to obtain the upper bound. But this
translation, being exponential in $n$ (see Remark 4.4), is not enough if $n$
is not fixed; we provide an algorithm to show that the result holds even if
$n$ is part of the input.

######  Theorem 5.1.

Under structure semantics, model checking
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ is Pspace -complete.

######  Proof 5.2.

Hardness follows from the Pspace -hardness of model checking QCTL [30]. For
the upper bound, we modify the algorithm described in [30, Theorem 4.2]. The
main difference is that when we guess a labelling for $p$ on a CKS
$\mathcal{S}$, we need to check that this labelling is uniform. With structure
semantics this can be done in deterministic time $O(|\mathcal{S}|^{2}\cdot
n)$: look at every pair of states, and check that if they are observationally
equivalent (tested by comparing at most $n$ pairs of local states) then they
agree on $p$.

We prove that the model-checking problem for
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ is in Pspace by
induction on the nesting depth $k$ of propositional quantification in input
formulas. If $k=0$, _i.e._ , the input formula is a $\textnormal{{CTL}}^{*}$
formula, call a $\textnormal{{CTL}}^{*}$ model-checking algorithm running in
polynomial space. For nesting depth $k+1$, the input formula $\varphi$ is of
the form $\varphi=\Phi[q_{i}\mapsto\exists^{o_{i}}p_{i}.\;\varphi_{i}]$, where
$\Phi$ is a $\textnormal{{CTL}}^{*}$ formula and for each $i$, $q_{i}$ is a
fresh atomic proposition, $o_{i}$ is an observation and $\varphi_{i}$ a
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$ formula of nesting
depth at most $k$. For each $i$, guess in linear time a labelling for $p_{i}$,
check in quadratic time that it is uniform, evaluate formula $\varphi_{i}$ in
each state with this labelling, and mark states where it holds with $q_{i}$.
By induction hypothesis, evaluating $\varphi_{i}$ can be done in polynomial
space. It just remains to evaluate the $\textnormal{{CTL}}^{*}$ formula $\Phi$
in polynomial space. The overall procedure thus runs in nondeterministic
polynomial space, and because NPspace = Pspace , the problem is in Pspace .

###  5.2. Tree semantics

We turn to the case of tree semantics. The first undecidability result comes
at no surprise since $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ can
express the existence of winning strategies in imperfect-information games.

######  Theorem 5.3.

Under tree semantics, the model-checking problem for
$\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ is undecidable.

######  Proof 5.4.

The $\textnormal{{MSO}}_{\textnormal{eq}}$ theory of the binary tree is
undecidable [31], and with Lemma 4.8 we obtain a reduction to the model-
checking problem for $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$.

####  5.2.1. Alternating tree automata

We briefly recall the notion of alternating (parity) tree automata. For a set
$Z$, $\mathbb{B}^{+}(Z)$ is the set of formulas built with elements of $Z$ as
atomic propositions, using only connectives $\vee$ and $\wedge$, and with
$\top,\perp\in\mathbb{B}^{+}(Z)$. An _alternating tree automaton (ATA ) on
$(\textit{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^{\textit{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 transition formulas between brackets, such as
$[x,q]$. A _nondeterministic tree automaton (NTA ) on $(\textit{AP},X)$-trees_
is an ATA $\mathcal{A}=(Q,\delta,q_{{\iota}},C)$ such that for every $q\in Q$
and $a\in 2^{\textit{AP}}$, if $\delta(q,a)$ is written in disjunctive normal
form, then for every direction $x\in X$, each disjunct contains exactly one
element of $\\{x\\}\times Q$. The _size_ of an ATA is its number of states and
its _index_ is its number of different colours.

Because we work with trees that are not necessarily complete as they represent
unfoldings of Kripke structures, we find it convenient to assume that the
state set is partitioned between $Q^{\top}$ and $Q^{\perp}$: when sent in a
direction where there is no node in the input tree, states in $Q^{\top}$
accept immediately while states in $Q^{\perp}$ reject immediately333Note that
we could also work only with complete trees, with a special symbol labelling
missing nodes..

We also recall the definition of acceptance by ATA via games between Eve and
Adam. Let $\mathcal{A}=(Q,\delta,q_{\iota},C)$ be an ATA over
$(\textit{AP},X)$-trees, let $t=(\tau,\ell)$ be such a tree and let
$u_{\iota}\in\tau$. We define the parity game
$\mathcal{G}(\mathcal{A},t,u_{\iota})=(V,E,v_{\iota},C^{\prime})$: the set of
positions is $V=\tau\times Q\times\mathbb{B}^{+}(X\times Q)$, the initial
position is $v_{{\iota}}=(u_{\iota},q_{\iota},\delta(q_{\iota},u_{\iota}))$,
and a position $(u,q,\alpha)$ belongs to Eve if $\alpha$ is of the form
$\alpha_{1}\vee\alpha_{2}$ or $[x,q^{\prime}]$; otherwise it belongs to Adam.
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\begin{cases}(u\cdot
x,q^{\prime},\delta(q^{\prime},\ell(u\cdot x)))&\mbox{if }u\cdot x\in t\\\
(u,q,\top)&\mbox{if }u\cdot x\notin t\mbox{ and }q\in Q^{\top}\\\
(u,q,\perp)&\mbox{if }u\cdot x\notin t\mbox{ and }q\in
Q^{\perp}\end{cases}\hfil\lx@intercol\end{array}$

Positions of the form $(u,q,\top)$ and $(u,q,\perp)$ are deadlocks, winning
for Eve and Adam respectively. The colouring is inherited from the one of the
automaton: $C^{\prime}(u,q,\alpha)=C(q)$.

A tree $t$ is _accepted_ from node $u$ by $\mathcal{A}$ if Eve has a winning
strategy in $\mathcal{G}(\mathcal{A},t,u)$, and we let
$\mathcal{L}(\mathcal{A})$ be the set of trees accepted by $\mathcal{A}$ from
their root.

We recall three classic results on tree automata. The first one is that
nondeterministic tree automata are closed under projection, and was
established by Rabin to deal with second-order monadic quantification:

######  Theorem 5.5 (Projection [43]).

Given an NTA $\mathcal{N}$ and an atomic proposition $p\in\mathcal{AP}$, one
can build an NTA $\mathcal{N}\\!\Downarrow_{p}$ of same size and index such
that
$\mathcal{L}(\mathcal{N}\\!\Downarrow_{p})=\mathcal{L}(\mathcal{N})\\!\Downarrow_{p}$.

Because it will be important to understand the automata construction for our
decision procedure in Section 5.2.2, we briefly recall that the projected
automaton $\mathcal{N}\\!\Downarrow_{p}$ is simply automaton $\mathcal{N}$
with the only difference that when it reads the label of a node, it can choose
whether $p$ is there or not: 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^{\textit{AP}}$. Another way of seeing it
is that $\mathcal{N}\\!\Downarrow_{p}$ first guesses a $p$-labelling for the
input tree, and then simulates $\mathcal{N}$ on this modified input. 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, reason why we need the next classic result: the crucial
simulation theorem, due to Muller and Schupp.

######  Theorem 5.6 (Simulation [37]).

Given an ATA $\mathcal{A}$, one can build an NTA $\mathcal{N}$ of exponential
size and linear index such that
$\mathcal{L}(\mathcal{N})=\mathcal{L}(\mathcal{A})$.

The last one was established by Kupferman and Vardi to deal with imperfect
information aspects in distributed synthesis. The rough idea is that, if one
just observes $X$, uniform $p$-labellings on $X\times Y$-trees can be obtained
by choosing the labellings directly on $X$-trees, and then lifting them to
$X\times Y$.

######  Theorem 5.7 (Narrowing [28]).

Given an ATA $\mathcal{A}$ on $X\times Y$-trees, one can build an ATA
$\mathcal{A}\\!\downarrow_{X}$ on $X$-trees of same size such that for all
$y\in Y$, $t\in\mathcal{L}(\mathcal{A}\\!\downarrow_{X})$ iff
$t\\!\uparrow^{X\times Y}_{y}\in\mathcal{L}(\mathcal{A})$.

In fact the result in [28] is stated for $t$ (and thus also
$t\\!\uparrow^{X\times Y}$) a complete tree, but the proof transfers
straightforwadly to this slightly more general result.

####  5.2.2. A decidable fragment: hierarchy on observations

We turn to our main result, which is the identification of an important
decidable fragment.

######  Definition 5.8.

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

In other words, a formula is hierarchical if innermost propositional
quantifiers observe at least as much as outermost ones. We let
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i,$\tiny{\subset}$}}$ be the
set of hierarchical $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$
formulas.

######  Theorem 5.9.

Under tree semantics, model checking
$\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i,$\tiny{\subset}$}}$ is
non-elementary decidable.

In order to prove this we establish Lemma 5.11 below, but we first introduce a
few more notations. For every
$\varphi\in\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$, we let
$I_{\varphi}:=\bigcap_{o\in O}o$, where $O$ is the set of observations that
occur in $\varphi$, with the intersection over the empty set defined as $[n]$.
We also let $X_{\varphi}:=X_{I_{\varphi}}$ (recall that for $I\subseteq[n]$,
$X_{I}={}_{i\in I}L_{i}$). We will need a final important definition.

######  Definition 5.10 (Merge).

Let $t=(\tau,\ell)$ be an $(\textit{AP},X)$-tree and
$t^{\prime}=(\tau^{\prime},\ell^{\prime})$ an
$(\textit{AP}\,^{\prime},X)$-tree. We define the _merge_ of $t$ and
$t^{\prime}$ as the $(\textit{AP}\cup\textit{AP}\,^{\prime})$-labelled
$X$-tree $t\merge t^{\prime}:=(\tau\cap\tau^{\prime},\ell^{\prime\prime})$,
where $\ell^{\prime\prime}(u)=\ell(u)\cup\ell^{\prime}(u)$.

We explain the idea behind this definition. In our decision procedure,
quantification on atomic propositions is performed by means of automata
projection (see Theorem 5.5). But in order to obtain uniform labellings for
these propositions, we need to first narrow down our automata and our trees
(see Theorem 5.7), and in this process we lose information on the labelling of
atomic propositions in the CKS $\mathcal{S}$ on which we evaluate the formula.
To address this problem, first we assume without loss of generality that
propositions that are quantified upon in $\Phi$ do not appear free in $\Phi$.
We can then partition propositions in $\Phi$ between those that are quantified
upon, $\textit{AP}_{\,\exists}$, and those that appear free,
$\textit{AP}_{f}$. We use the input tree of the automaton we build to carry
the labelling for $\textit{AP}_{\,\exists}$, and in the end the input tree is
merged with the unfolding of $\mathcal{S}$ that carries the labelling to
evaluate propositions in $\textit{AP}_{f}$.

######  Lemma 5.11.

Let $\Phi\in\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subset}$}}$ with $\textit{AP}_{\,\exists}$ and $\textit{AP}_{f}$
defined as above, and let $\mathcal{S}$ be a finite CKS over
$\textit{AP}_{f}$. For every subformula $\varphi$ of $\Phi$ and state $s$ of
$\mathcal{S}$, one can build an ATA $\mathcal{A}_{s}^{\varphi}$ on
$(\textit{AP}_{\,\exists},X_{\varphi})$-trees such that for every
$(\textit{AP}_{\,\exists},X_{\varphi})$-tree $t$ rooted in
$s\\!\downarrow_{X_{\varphi}}$,

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

For an $X_{I}$-tree $t$, from now on
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$ stands for
$t\\!\uparrow^{[n]}_{y}\merge\;t_{\mathcal{S},s}$, where
$y=s\\!\downarrow_{[n]\setminus I}$.

######  Proof 5.12 (Proof).

Let $\Phi\in\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subset}$}}$, and let $\textit{AP}_{\,\exists}$ (resp.
$\textit{AP}_{f}$) be the set of atomic propositions that are quantified upon
(resp. that appear free) in $\Phi$. Modulo renaming of atomic propositions, we
can assume without loss of generality that $\textit{AP}_{\,\exists}$ and
$\textit{AP}_{f}$ are disjoint. Let $\mathcal{S}=(S,R,\ell_{\mathcal{S}})$ be
a finite CKS over $\textit{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}$. The definition builds upon the classic
construction for $\textnormal{{CTL}}^{*}$ from [29].

$\varphi=p$::

We let $\mathcal{A}_{s}^{p}$ be the ATA over $X_{[n]}$-trees with one unique
state $q_{\iota}$, with transition function defined as follows:

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

The idea is that since we know the state $s\in S$ in which we want to evaluate
the formula, we can read the labelling for atomic propositions in
$\textit{AP}_{f}$ (those that are not quantified upon) directly from $s$.
However, for propositions in $\textit{AP}_{\,\exists}$, we need to read them
from the input tree. Indeed, if $p\in\textit{AP}_{\,\exists}$ it means that
$p$ is quantified upon in $\Phi$: there is a subformula
$\exists^{o}p.\;\varphi$ of $\Phi$ such that $p$ is a subformula of $\varphi$.
The automaton $\mathcal{A}_{s}^{\exists^{o}p.\;\varphi}$ will be built by
narrowing, nondeterminising and projecting $\mathcal{A}_{s}^{\varphi}$ on $p$.
On a given input tree $t$, $\mathcal{A}_{s}^{\exists^{o}p.\;\varphi}$ will
thus guess a labelling for $p$ in each node of $t$ and simulate (the
nondeterminised narrowing of) $\mathcal{A}_{s}^{\varphi}$ on this modified
input. $\mathcal{A}_{s}^{\varphi}$ must therefore read the labelling for $p$
from its input tree.

$\varphi=\neg\varphi^{\prime}$::

We obtain $\mathcal{A}_{s}^{\varphi}$ by dualising
$\mathcal{A}_{s}^{\varphi^{\prime}}$, which is a classic operation on ATA s.

$\varphi=\varphi_{1}\vee\varphi_{2}$::

Because $I_{\varphi}=I_{\varphi_{1}}\cap I_{\varphi_{2}}$, and each
$\mathcal{A}_{s}^{\varphi_{i}}$ works on $X_{\varphi_{i}}$-trees, we need to
narrow them so that they work on $X_{\varphi}$-trees: for $i\in\\{1,2\\}$, we
let
$\mathcal{A}_{i}:=\mathcal{A}_{s}^{\varphi_{i}}\\!\downarrow_{I_{\varphi}}$.

We then build $\mathcal{A}_{s}^{\varphi}$ by taking the disjoint union of
$\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ and adding a new initial state that
nondeterministically chooses which of $\mathcal{A}_{1}$ or $\mathcal{A}_{2}$
to execute on the input tree, so that
$\mathcal{L}(\mathcal{A}_{s}^{\varphi})=\mathcal{L}(\mathcal{A}_{1})\cup\mathcal{L}(\mathcal{A}_{2})$.

$\varphi={\bf E}\psi$::

The aim is to build an automaton $\mathcal{A}_{s}^{\varphi}$ that works on
$X_{\varphi}$-trees and that on input $t$, checks for the existence of a path
in $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$ that satisfies $\psi$. To do
so, $\mathcal{A}_{s}^{\varphi}$ guesses a path $\lambda$ in $(\mathcal{S},s)$.
It remembers the current state in $\mathcal{S}$, which provides the labelling
for atomic propositions in $\textit{AP}_{f}$, and while it guesses $\lambda$
it follows its projection on $X_{\varphi}$ in its input tree $t$, reading the
labels to evaluate propositions in $\textit{AP}_{\,\exists}$.

Let $\max(\psi)=\\{\varphi_{1},\ldots,\varphi_{n}\\}$ be the set of maximal
state sub-formulas of $\psi$. In a first step we see these maximal state sub-
formulas as atomic propositions. Formula $\psi$ can thus be seen as an LTL
formula, and we can 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$. We define
the ATA $\mathcal{A}$ that, given as input a $(\max(\psi),X_{\varphi})$-tree
$t$, nondeterministically guesses a path $\lambda$ in
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$ and simulates
$\mathcal{W}^{\psi}$ on it, assuming that the labels it reads while following
$\lambda\\!\downarrow_{X_{\varphi}}$ in its input correctly represent the
truth value of formulas in $\max(\psi)$ along $\lambda$. Recall that
$\mathcal{S}=(S,R,\ell_{\mathcal{S}})$; we define
$\mathcal{A}:=(Q,\delta,q_{{\iota}},C)$, where

  * •:

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

  * •:

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

  * •:

$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_{X_{\varphi}},\left(q^{\prime},s^{\prime\prime}\right)].$

The intuition is that $\mathcal{A}$ reads the current label, chooses
nondeterministically which transition to take in $\mathcal{W}^{\psi}$, chooses
a next state in $\mathcal{S}$ and proceeds in the corresponding direction in
$X_{\varphi}$. To ensure444Actually this is not very important since the tree
$t$ on which our automata will work will always be such that the domain of
$t\\!\uparrow^{[n]}$ contains the domain of $t_{\mathcal{S},s}$. that the path
it guesses is not only in $t_{\mathcal{S},s}$ but also in
$t\\!\uparrow^{[n]}$, it is enough to make sure that it always tries to stay
inside its input tree $t$, which is achieved by letting $Q^{\top}=\emptyset$
and $Q^{\perp}=Q$. Thus, $\mathcal{A}$ accepts exactly the
$\max(\varphi)$-labelled $X_{\varphi}$-trees $t$ in which there exists a path
that corresponds to some path in $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$
that satisfies $\psi$, where maximal state formulas are considered as atomic
propositions.

Now from $\mathcal{A}$ we build the automaton $\mathcal{A}_{s}^{\varphi}$ over
$X_{\varphi}$-trees labelled with real atomic propositions in
$\textit{AP}_{\,\exists}$. In each node it visits, this automaton guesses what
should be its labelling over $\max(\psi)$, it simulates $\mathcal{A}$
accordingly, and checks that the guesses it makes are correct. If the path
being guessed in $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$ is currently in
node $u$ ending with state $s^{\prime}$, and $\mathcal{A}_{s}^{\varphi}$
guesses that $\varphi_{i}$ holds in $u$, it checks this guess by starting a
simulation of automaton $\mathcal{A}_{s^{\prime}}^{\varphi_{i}}$ from node
$v=u\\!\downarrow_{X_{\varphi}}$ in its input $t$.

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
$X_{\varphi_{i}}$-trees. Observe that
$I_{\varphi}=\cap_{i=1}^{n}I_{\varphi_{i}}$, so that we need to narrow down
these automata: 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 its dualisation, and we assume w.l.o.g. that 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$ is defined as follows. For states in $Q^{i}_{s^{\prime}}$ (resp.
$\overline{Q^{i}_{s^{\prime}}}$), $\delta$ agrees with
$\delta^{i}_{s^{\prime}}$ (resp. $\overline{\delta^{i}_{s^{\prime}}}$), and
for $(q^{\psi},s^{\prime})\in Q$ and $a\in 2^{\textit{AP}_{\,\exists}}$ we let

$\delta^{\prime}((q^{\psi},s^{\prime}),a)=\bigvee_{a^{\prime}\in
2^{\max(\psi)}}\left(\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)\right).$

$\varphi=\exists^{o}p.\;\varphi^{\prime}$::

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

We now prove by induction on $\varphi$ that the construction is correct. In
each case, we let $t=(\tau,\ell)$ be an
$(\textit{AP}_{\,\exists},X_{\varphi})$-tree rooted in
$s\\!\downarrow_{X_{\varphi}}$.

$\varphi=p$::

First, note that $I_{p}=[n]$, so that $t$ is rooted in
$s\\!\downarrow_{X_{p}}=s$. Let us consider first the case where
$p\in\textit{AP}_{f}$. By definition of $\mathcal{A}_{s}^{p}$, we have that
$t\in\mathcal{L}(\mathcal{A}_{s}^{p})$ iff $p\in\ell_{\mathcal{S}}(s)$. On the
other hand, by definition of the merge operation, of the unfolding, and
because $\textit{AP}_{\,\exists}$ and $\textit{AP}_{f}$ are disjoint, we have
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models p$ iff
$p\in\ell_{\mathcal{S}}(s)$, and we are done. Now if
$p\in\textit{AP}_{\,\exists}$: by definition of $\mathcal{A}_{s}^{p}$, we have
$t\in\mathcal{L}(\mathcal{A}_{s}^{p})$ iff $p\in\ell(s)$; also, by definition
of the merge, we have that $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models
p$ iff $p\in\ell(s)$, which concludes.

$\varphi=\neg\varphi^{\prime}$::

trivial.

$\varphi=\varphi_{1}\vee\varphi_{2}$::

We have
$\mathcal{A}_{i}=\mathcal{A}_{s}^{\varphi_{i}}\\!\downarrow_{X_{\varphi}}$, so
by Theorem 5.7 we get that $t\in\mathcal{L}(\mathcal{A}_{i})$ iff
$t\\!\uparrow^{X_{\varphi_{i}}}\in\mathcal{L}(\mathcal{A}_{s}^{\varphi_{i}})$,
which by induction hypothesis holds iff
$(t\\!\uparrow^{X_{\varphi_{i}}})\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models_{t}\varphi_{i}$,
_i.e._ , iff
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models_{t}\varphi_{i}$. We
conclude by reminding that
$\mathcal{L}(\mathcal{A}_{s}^{\varphi})=\mathcal{L}(\mathcal{A}_{1})\cup\mathcal{L}(\mathcal{A}_{2})$.

$\varphi={\bf E}\psi$::

Suppose that
$t^{\prime}=t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models_{t}{\bf
E}\psi$. There exists a path $\lambda$ starting at the root $s$ of
$t^{\prime}$ such that $t^{\prime},\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 n $\lambda$ on the
state formulas in $\max(\psi)$. By definition, $\mathcal{W}^{\psi}$ has an
accepting execution on $w$. Now in the acceptance game of
$\mathcal{A}_{s}^{\varphi}$ on $t$, Eve can guess the path $\lambda$,
following $\lambda\\!\downarrow_{X_{\varphi}}$ in its input $t$, and she can
also guess the corresponding word $w$ on $2^{\max(\psi)}$ and an accepting
execution of $\mathcal{W}^{\psi}$ on $w$. Let $u^{\prime}\in t^{\prime}$ be a
node of $\lambda$, $s^{\prime}$ its last direction and let
$u=u^{\prime}\\!\downarrow_{X_{\varphi}}\in t$. Assume that in node $u$ 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 $u^{\prime}$,
_i.e._ , Adam chooses the conjunct
$\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a)$, where $a$ is the label of
$u$. Note that in the evaluation game this means that Adam moves to position
$(u,(q^{\psi},s^{\prime}),\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a))$. We
want to show that Eve wins from this position.

Let $t_{u}$ (resp. $t^{\prime}_{u^{\prime}}$) be the subtree of $t$ (resp.
$t^{\prime}$) starting in $u$ (resp. $u^{\prime}$)555If $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})$: we remove
from each node all directions before $\mbox{last}(u)$.. It is enough to show
that $t_{u}$ is accepted by
$\mathcal{A}^{i}_{s^{\prime}}=\mathcal{A}_{s^{\prime}}^{\varphi_{i}}\\!\downarrow_{I_{\varphi}}$.
Observe that $t_{u}$ is rooted in the last direction of
$u=u^{\prime}\\!\downarrow_{I_{\varphi}}$, and since the last direction of
$u^{\prime}$ is $s^{\prime}$ we have that $t_{u}$ is rooted in
$s^{\prime}\\!\downarrow_{I_{\varphi}}$. Let us write
$t^{\prime\prime}=t_{u}\\!\uparrow^{I_{\varphi_{i}}}_{s^{\prime\prime}}$,
where $s^{\prime\prime}=s^{\prime}\\!\downarrow_{I_{\varphi_{i}}}$. By Theorem
5.7, because
$\mathcal{A}^{i}_{s^{\prime}}=\mathcal{A}_{s^{\prime}}^{\varphi_{i}}\\!\downarrow_{I_{\varphi}}$
and
$s^{\prime}\\!\downarrow_{I_{\varphi}}=(s^{\prime}\\!\downarrow_{I_{\varphi_{i}}})\\!\downarrow_{I_{\varphi}}$,
we have that

$t_{u}\in\mathcal{L}(\mathcal{A}^{i}_{s^{\prime}})\mbox{\;\;\;iff\;\;\;}t^{\prime\prime}\in\mathcal{L}(\mathcal{A}_{s^{\prime}}^{\varphi_{i}}).$
(1)

Since $t^{\prime\prime}$ is rooted in
$s^{\prime}\\!\downarrow_{I_{\varphi_{i}}}$ we can apply the induction
hypothesis on $t^{\prime\prime}$ with $\varphi_{i}$, and we get that

$t^{\prime\prime}\in\mathcal{L}(\mathcal{A}_{s^{\prime}}^{\varphi_{i}})\mbox{\;\;\;iff\;\;\;}t^{\prime\prime}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s^{\prime}}\models_{t}\varphi_{i}.$
(2)

Now, because $u^{\prime}$ ends in $s^{\prime}$ we also have that

$t^{\prime}_{u^{\prime}}=t^{\prime\prime}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s^{\prime}}.$
(3)

Putting (1), (2) and (3) together, we obtain that

$t_{u}\in\mathcal{L}(\mathcal{A}^{i}_{s^{\prime}})\quad\mbox{iff}\quad
t^{\prime}_{u^{\prime}}\models_{t}\varphi_{i}.$ (4)

Because we have assumed that Eve guesses $w$ correctly, we also have that
$t^{\prime},u^{\prime}\models_{t}\varphi_{i}$, _i.e._ ,
$t^{\prime}_{u^{\prime}}\models_{t}\varphi_{i}$. This, together with (4),
gives us that $t_{u}$ is accepted by $\mathcal{A}^{i}_{s^{\prime}}$.

Eve thus has a winning strategy from the initial position of the acceptance
game of $\mathcal{A}^{i}_{s^{\prime}}$ on $t_{u}$. This initial position is
$(u,q^{i}_{s^{\prime}},\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a))$. Since
$(u,q^{i}_{s^{\prime}},\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a))$ and
$(u,(q^{\psi},s^{\prime}),\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a))$
contain the same node $u$ and transition formula
$\delta^{i}_{s^{\prime}}(q^{i}_{s^{\prime}},a)$, a winning strategy in one of
these positions666Recall that positional strategies are sufficient in parity
games [49]. is also a winning strategy in the other, and therefore Eve wins
Adam’s challenge. With a similar argument, we get that also when Adam
challenges Eve on some $\varphi_{i}$ assumed not to be true in node $v$, Eve
wins the challenge. Finally, Eve wins the acceptance game of
$\mathcal{A}_{s}^{\varphi}$ on $t$, and thus
$t\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})$.

For the other direction, assume that
$t\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})$, _i.e._ , Eve wins the evaluation
game of $\mathcal{A}_{s}^{\varphi}$ on $t$. Again, let
$t^{\prime}=t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$. A winning strategy
for Eve describes a path $\lambda$ in $t_{\mathcal{S},s}$, which is also a
path in $t^{\prime}$. 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 an accepting run of $\mathcal{W}^{\psi}$
on $w$. Hence $t^{\prime},\lambda\models_{t}\psi$, and
$t^{\prime}\models_{t}\varphi$.

$\varphi=\exists^{o}p.\;\varphi^{\prime}$::

First, observe that because $\varphi$ is hierarchical, we have that
$I_{\varphi}=o$. Next, by Theorem 5.5 we have that

$t\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})\mbox{\;\;\;iff\;\;\;there exists
}t_{p}\equiv_{p}t\mbox{ such that }t_{p}\in\mathcal{L}(\mathcal{A}_{2}).$ (5)

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

$t_{p}\in\mathcal{L}(\mathcal{A}_{2})\mbox{\;\;\;iff\;\;\;}t_{p}\\!\uparrow^{X_{\varphi^{\prime}}}_{y}\in\mathcal{L}(\mathcal{A}_{s}^{\varphi^{\prime}}),\mbox{
where $y=s\\!\downarrow_{(I_{\varphi^{\prime}}\setminus I_{\varphi})}$.}$ (6)

Now $t_{p}$ and $t$ have the same root, $s\\!\downarrow_{X_{\varphi}}$. The
root of $t_{p}\\!\uparrow^{X_{\varphi^{\prime}}}_{y}$ is thus
$(s\\!\downarrow_{X_{\varphi}},y)=s\\!\downarrow_{X_{\varphi^{\prime}}}$, and
we can apply the induction hypothesis on
$t_{p}\\!\uparrow^{X_{\varphi^{\prime}}}_{y}$ with $\varphi^{\prime}$:

$t_{p}\\!\uparrow^{X_{\varphi^{\prime}}}_{y}\in\mathcal{L}(\mathcal{A}_{s}^{\varphi^{\prime}})\mbox{\;\;\;iff\;\;\;}t_{p}\\!\uparrow^{X_{\varphi^{\prime}}}_{y}\,\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models_{t}\varphi^{\prime}.$
(7)

Now, with (5), (6) and (7) together with the fact that
$t_{p}\\!\uparrow^{X_{\varphi^{\prime}}}_{y}\,\\!\uparrow^{[n]}\,=t_{p}\\!\uparrow^{[n]}$,
we get that

$t\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})\mbox{\;\;\;iff\;\;\;there exists
}t_{p}\equiv_{p}t\mbox{ such that
}t_{p}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models_{t}\varphi^{\prime}.$
(8)

Let us prove that the right-hand side of (8) holds if and only if
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models_{t}\exists^{o}p.\;\varphi^{\prime}$.
For the first direction, assume that there exists $t_{p}\equiv_{p}t\mbox{ such
that
}t_{p}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models_{t}\varphi^{\prime}$.
First, by definition of the merge, because $p\in\textit{AP}_{\,\exists}$ and
$\textit{AP}_{\,\exists}$ and $\textit{AP}_{f}$ are disjoint, the
$p$-labelling of $t_{p}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$ is
determined by the $p$-labelling of $t_{p}\\!\uparrow^{[n]}$, which by
definition of the lift is $o$-uniform. In addition it is clear that
$t_{p}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\equiv_{p}t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$,
which concludes this direction.

For the other direction, assume that
$t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models_{t}\exists^{o}p.\;\varphi^{\prime}$:
there exists
$t^{\prime}_{p}\equiv_{p}t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$ such
that $t^{\prime}_{p}$ is $o$-uniform in $p$ and
$t^{\prime}_{p}\models_{t}\varphi^{\prime}$. Let us write
$t^{\prime}_{p}=(\tau^{\prime},\ell^{\prime}_{p})$ and $t=(\tau,\ell)$. We
define $t_{p}:=(\tau,\ell_{p})$ where for each $u\in\tau$, if there exists
$u^{\prime}\in\tau^{\prime}$ such that $u^{\prime}\\!\downarrow_{o}=u$, we let

$\ell_{p}(u)=\begin{cases}\ell(u)\cup\\{p\\}&\mbox{if
}p\in\ell^{\prime}_{p}(u^{\prime})\\\
\ell(u)\setminus\\{p\\}&\mbox{otherwise}.\end{cases}$

This is well defined because $t^{\prime}_{p}$ is $o$-uniform in $p$: if two
nodes $u^{\prime},v^{\prime}$ project on $u$, we have
$u^{\prime}\approx_{o}v^{\prime}$ and thus they agree on $p$. In case there is
no $u^{\prime}\in\tau^{\prime}$ such that
$u^{\prime}\\!\downarrow_{X_{\varphi}}=u$, we can let $\ell_{p}(u)=\ell(u)$ as
this node disappears in $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$.
Clearly, $t_{p}\equiv_{p}t$. Now we write
$t^{\prime\prime}_{p}=t_{p}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$ and we
prove that $t^{\prime\prime}_{p}=t^{\prime}_{p}$ hence
$t^{\prime\prime}_{p}\models_{t}\varphi^{\prime}$, which concludes. It is
clear that $t^{\prime\prime}_{p}$ and $t^{\prime}_{p}$ have the same domain.
Also, because
$t^{\prime}_{p}\equiv_{p}t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$ and
$t^{\prime\prime}_{p}=t_{p}\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}$, by
definition of the merge both agree with $t_{\mathcal{S},s}$ for all atomic
propositions in $\textit{AP}_{f}$. Because $t_{p}\equiv_{p}t$, and again by
definition of the merge, $t^{\prime\prime}_{p}$ and $t^{\prime}_{p}$ also
agree on all atomic propositions in $\textit{AP}_{\,\exists}\setminus\\{p\\}$.
Finally, by definition of $t_{p}$ and because $t_{p}^{\prime}$ is $o$-uniform
in $p$, we get that $t^{\prime\prime}_{p}$ and $t^{\prime}_{p}$ also agree on
$p$, and therefore $t^{\prime\prime}_{p}=t^{\prime}_{p}$.

We can now prove Theorem 5.9. Let $(\mathcal{S},s)$ be a pointed CKS , and let
$\varphi\in\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize
i,$\tiny{\subset}$}}$. By Lemma 5.11 one can build an ATA
$\mathcal{A}_{s}^{\varphi}$ such that for every labelled $X_{\varphi}$-tree
$t$ rooted in $s\\!\downarrow_{X_{\varphi}}$, it holds that
$t\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})\mbox{ iff
}t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}\models_{t}\varphi$. Let $\tau$ be
the full $X_{\varphi}$-tree rooted in $s\\!\downarrow_{X_{\varphi}}$, and let
$t=(\tau,\ell_{\emptyset})$, where $\ell_{\emptyset}$ is the empty labelling.
Clearly, $t\\!\uparrow^{[n]}\merge\;t_{\mathcal{S},s}=t_{\mathcal{S},s}$, and
because $t$ is rooted in $s\\!\downarrow_{X_{\varphi}}$, we have
$t\in\mathcal{L}(\mathcal{A}_{s}^{\varphi})\mbox{ iff
}t_{\mathcal{S},s}\models_{t}\varphi$. It only remains to build a simple
deterministic tree automaton $\mathcal{A}$ over $X_{\varphi}$-trees such that
$\mathcal{L}(\mathcal{A})=\\{t\\}$, and check for emptiness of the alternating
tree automaton $\mathcal{L}(\mathcal{A}\cap\mathcal{A}_{s}^{\varphi})$.
Because nondeterminisation makes the size of the automaton gain one
exponential for each nested quantifier on propositions, the procedure is
nonelementary, and hardness is inherited from the model-checking problem for
QCTL [30].

##  6\. Conclusion and future work

We have introduced the essence of imperfect information in
$\textnormal{{QCTL}}^{*}$, by adding internal structure to states of the
models and parameterising propositional quantifiers with observational power
over this internal structure. We considered both the structure and tree
semantics, intimately related to the notions of _no memory_ and _perfect
recall_ in game strategies, respectively. For the structure semantics we
showed that our logic coincides with QCTL in expressive power, and thus also
with MSO, and that the model-checking problem is Pspace -complete, as for
QCTL. For the tree semantics however we showed that our logic is expressively
equivalent to MSO with equal level, and that its model-checking problem is
thus undecidable. But we established, thanks to automata techniques made
possible by our modelling choices, that model checking hierarchical formulas
is decidable.

Several future work directions await us. First it would be interesting to
study $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$ under the amorphous
semantics, studied by French for QCTL in [17]. We would also like to
investigate fragments with better complexity, as well as the satisfiability
problem for $\textnormal{{QCTL}}_{\textnormal{\scriptsize i}}$. Then we
believe that there may be interesting connections with Chain Logic with equal
level, a restriction of $\textnormal{{MSO}}_{\textnormal{eq}}$ that is
decidable on trees. Does it correspond to another interesting decidable
fragment of $\textnormal{{QCTL}}^{*}_{\textnormal{\scriptsize i}}$? Finally,
we aim at exploiting our last result in various logics for strategic reasoning
with imperfect information, such as
$\textnormal{{ATL}}^{*}_{\textit{\scriptsize sc}}$ and SL.

## References

  * [1] E. A.Emerson and C.-L. Lei.  Modalities for model checking: Branching time strikes back.  In PL’85, pages 84–96. ACM Press, 1985.
  * [2] T. Ågotnes, V. Goranko, and W. Jamroga.  Alternating-Time Temporal Logics with Irrevocable Strategies.  In TARK’07, pages 15–24, 2007.
  * [3] R. Alur, T.A. Henzinger, and O. Kupferman.  Alternating-Time Temporal Logic.  JACM, 49(5):672–713, 2002.
  * [4] Dietmar Berwanger, Anup Basil Mathew, and Marie van den Bogaard.  Hierarchical information patterns and distributed strategy synthesis.  In Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings, pages 378–393, 2015.  doi:10.1007/978-3-319-24953-7\\_28.
  * [5] T. Brihaye, A. Da Costa Lopes, F. Laroussinie, and N. Markey.  ATL with Strategy Contexts and Bounded Memory.  In LFCS’09, LNCS 5407, pages 92–106. Springer, 2009.
  * [6] P. Čermák, A. Lomuscio, F. Mogavero, and A. Murano.  MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications.  In CAV’14, LNCS 8559, pages 524–531. Springer, 2014.
  * [7] K. Chatterjee, T.A. Henzinger, and N. Piterman.  Strategy Logic.  Information and Computation, 208(6):677–693, 2010.
  * [8] E.M. Clarke and E.A. Emerson.  Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic.  In LP’81, LNCS 131, pages 52–71. Springer, 1981.
  * [9] E.M. Clarke, O. Grumberg, and D.A. Peled.  Model Checking. MIT Press, 2002.
  * [10] A. Da Costa, F. Laroussinie, and N. Markey.  ATL with Strategy Contexts: Expressiveness and Model Checking.  In FSTTCS’10, LIPIcs 8, pages 120–132, 2010.
  * [11] M. Dastani and W. Jamroga.  Reasoning about strategies of multi-agent programs.  In AAMAS’10, pages 997–1004. IFAAMAS, 2010.
  * [12] C. Dima and F. L. Tiplea.  Model-checking ATL under imperfect information and perfect recall semantics is undecidable.  CoRR, abs/1102.4225, 2011.
  * [13] C. Dima and F.L. Tiplea.  Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable.  Technical report, arXiv, 2011.
  * [14] C. C. Elgot and M. O. Rabin.  Decidability and undecidability of extensions of second (first) order theory of (generalized) successor.  J. Symb. Log., 31(2):169–181, 1966.  URL: http://dx.doi.org/10.2307/2269808, doi:10.2307/2269808.
  * [15] E Allen Emerson and A Prasad Sistla.  Deciding branching time logic.  In Proceedings of the sixteenth annual ACM symposium on Theory of computing, pages 14–24. ACM, 1984.
  * [16] E.A. Emerson and J.Y. Halpern.  “Sometimes” and “Not Never” Revisited: On Branching Versus Linear Time.  JACM, 33(1):151–178, 1986.
  * [17] Tim French.  Decidability of quantifed propositional branching time logics.  In Australian Joint Conference on Artificial Intelligence, pages 165–176. Springer, 2001.
  * [18] Joseph Y Halpern and Moshe Y Vardi.  The complexity of reasoning about knowledge and time. i. lower bounds.  Journal of Computer and System Sciences, 38(1):195–237, 1989.
  * [19] W. Jamroga, S. Mauw, and M. Melissen.  Fairness in non-repudiation protocols.  In Proceedings of STM’11, volume 7170 of LNCS, pages 122–139, 2012.
  * [20] W. Jamroga and A. Murano.  On Module Checking and Strategies.  In AAMAS’14, pages 701–708. IFAAMAS, 2014.
  * [21] S. Kremer and J.-F. Raskin.  A game-based verification of non-repudiation and fair exchange protocols.  Journal of Computer Security, 11(3), 2003.
  * [22] O Kupermann and M.Y Vardi.  Synthesizing distributed systems.  In Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on, pages 389–398. IEEE, 2001.
  * [23] O. Kupferman.  Augmenting branching temporal logics with existential quantification over atomic propositions.  In CAV’95, LNCS 939, pages 325–338. Springer, 1995.
  * [24] O. Kupferman, P. Madhusudan, P. S. Thiagarajan, and M. Y. Vardi.  Open systems in reactive environments: Control and synthesis.  In CONCUR’00, LNCS 1877, pages 92–107. Springer, 2000.
  * [25] O. Kupferman and M. Y. Vardi.  Module checking revisited.  In CAV’97, volume 1254 of LNCS, pages 36–47. Springer, 1997\.
  * [26] O. Kupferman, M.Y. Vardi, and P. Wolper.  An Automata Theoretic Approach to Branching-Time Model Checking.  JACM, 47(2):312–360, 2000.
  * [27] O. Kupferman, M.Y. Vardi, and P. Wolper.  Module Checking.  IC, 164(2):322–344, 2001.
  * [28] Orna Kupferman and Moshe Y Vardi.  Church’s problem revisited.  Bulletin of Symbolic Logic, pages 245–263, 1999.
  * [29] Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper.  An automata-theoretic approach to branching-time model checking.  J. ACM, 47(2):312–360, 2000.
  * [30] François Laroussinie and Nicolas Markey.  Quantified CTL: expressiveness and complexity.  Logical Methods in Computer Science, 10(4), 2014.  URL: http://dx.doi.org/10.2168/LMCS-10(4:17)2014, doi:10.2168/LMCS-10(4:17)2014.
  * [31] Hans Läuchli and Christian Savioz.  Monadic second order definable relations on the binary tree.  The Journal of Symbolic Logic, 52(01):219–226, 1987.
  * [32] A. Lomuscio and F. Raimondi.  MCMAS : A model checker for multi-agent systems.  In TACAS’06, LNCS 4314, pages 450–454, 2006.
  * [33] A.D.C. Lopes, F. Laroussinie, and N. Markey.  ATL with Strategy Contexts: Expressiveness and Model Checking.  In FSTTCS’10, LIPIcs 8, pages 120–132. Leibniz-Zentrum fuer Informatik, 2010.
  * [34] F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi.  Reasoning About Strategies: On the Model-Checking Problem.  TOCL, 15(4):34:1–42, 2014.
  * [35] F. Mogavero, A. Murano, and M.Y. Vardi.  Reasoning About Strategies.  In FSTTCS’10, LIPIcs 8, pages 133–144. Leibniz-Zentrum fuer Informatik, 2010.
  * [36] F. Mogavero, A. Murano, and M.Y. Vardi.  Relentful Strategic Reasoning in Alternating-Time Temporal Logic.  In LPAR’10, LNAI 6355, pages 371–387. Springer, 2010.
  * [37] David E. Muller and Paul E. Schupp.  Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of rabin, mcnaughton and safra.  Theor. Comput. Sci., 141(1&2):69–107, 1995.
  * [38] Gary Peterson, John Reif, and Salman Azhar.  Lower bounds for multiplayer noncooperative games of incomplete information.  Computers & Mathematics with Applications, 41(7):957–992, 2001\.
  * [39] Gary Peterson, John Reif, and Salman Azhar.  Decision algorithms for multiplayer noncooperative games of incomplete information.  Computers & Mathematics with Applications, 43(1):179–206, 2002\.
  * [40] Sophie Pinchinat and Stéphane Riedweg.  A decidable class of problems for control under partial observation.  Information Processing Letters, 95(4):454–460, 2005.
  * [41] A. Pnueli.  The Temporal Logic of Programs.  In FOCS’77, pages 46–57. IEEE Computer Society, 1977.
  * [42] A. Pnueli and R. Rosner.  On the Synthesis of a Reactive Module.  In POPL’89, pages 179–190. Association for Computing Machinery, 1989.
  * [43] Michael O Rabin.  Decidability of second-order theories and automata on infinite trees.  Transactions of the american Mathematical Society, 141:1–35, 1969\.
  * [44] John H. Reif.  The complexity of two-player games of incomplete information.  J. Comput. Syst. Sci., 29(2):274–301, 1984.
  * [45] A.P. Sistla.  Theoretical Issues in the Design and Cerification of Distributed Systems. PhD thesis, Harvard University, Cambridge, MA, USA, 1983.
  * [46] W. Thomas.  Infinite trees and automaton-definable relations over omega-words.  Theor. Comput. Sci., 103(1):143–159, 1992.
  * [47] W. van der Hoek and M. Wooldridge.  Cooperation, knowledge and time: Alternating-time Temporal Epistemic Logic and its applications.  Studia Logica, 75(1):125–157, 2003.
  * [48] M.Y. Vardi and L.J. Stockmeyer.  Improved upper and lower bounds for modal logics of programs: Preliminary report.  In STOC’85, pages 240–251, 1985.
  * [49] Wieslaw Zielonka.  Infinite games on finitely coloured graphs with applications to automata on infinite trees.  Theor. Comput. Sci., 200(1-2):135–183, 1998.