quantification prefix over a set $\VSet \subseteq \VarSet$ of variables,
and $\bpElm \in \BndSet(\VSet)$ a binding.
Then, the dependence-vs-valuation game for $\GName$ in $\sElm$ over
$\PSet$ w.r.t. $\qpElm$ and $\bpElm$ is the  $\HName(\GName, \sElm,
\PSet, \qpElm, \bpElm) \defeq \TPGTuple {\AName(\GName, \sElm, \qpElm,
\bpElm)} {\PSet}$, where the  $\AName(\GName, \sElm, \qpElm, \bpElm)
\defeq \TPATuple {\StSet} {\StSet \times \SpcSet[\AcSet](\qpElm)}
{\EdgRel} {\sElm}$ has the edge relations defined as follows:

* $\EdgERel \defeq \set{ (\tElm, (\tElm, \spcFun)) }{ \tElm \in \StSet
\land \spcFun \in \SpcSet[\AcSet](\qpElm) }$;

* $\EdgORel \defeq \set{ ((\tElm, \spcFun), \trnFun(\tElm,
\spcFun(\valFun) \cmp \bndFun[\bpElm])) }{ \tElm \in \StSet \land
\spcFun \in \SpcSet[\AcSet](\qpElm) \land \valFun \in
\ValSet[\AcSet](\QPAVSet{\qpElm}) }$ [By $\gFun[2] \cmp
\gFun[1] : \XSet \to \ZSet$ we denote the operation of
composition of two functions $\gFun[1] : \XSet \to \YSet[1]$
and $\gFun[2] : \YSet[2] \to \ZSet$ with $\YSet[1] \subseteq
\YSet[2]$.].

In the next lemma we state a fundamental relationship between
dependence-vs-valuation games and their duals.
Basically, we prove that if a player wins the game then the opposite player
can win the dual game, and vice versa.

Let $\GName$ be a , $\sElm \in \StSet$ one of its states, $\PSet
\subseteq \PthSet(\sElm)$ a set of paths, $\qpElm \in \QPSet(\VSet)$ a
quantification prefix over a set $\VSet \subseteq \VarSet$ of variables,
and $\bpElm \in \BndSet(\VSet)$ a binding.
Then, player even wins the  $\HName(\GName, \sElm, \PSet, \qpElm,
\bpElm)$ iff player odd wins the dual  $\HName(\GName, \sElm,
\PthSet(\sElm) \setminus \PSet, \dual{\qpElm}, \bpElm)$.

Now, we are going to give the definition of the important concept of
Informally, an encasement is a particular subset of paths in a given 		that “works to encase” an elementary dependence map on strategies, in the
sense that it contains all plays obtainable by complete assignments derived
from the evaluation of the above mentioned dependence map.
In our context, this concept is used to summarize all

Let $\GName$ be a , $\sElm \in \StSet$ one of its states, $\PSet
\subseteq \PthSet(\sElm)$ a set of paths, $\qpElm \in \QPSet(\VSet)$ a
quantification prefix over a set $\VSet \subseteq \VarSet$ of variables,
and $\bpElm \in \BndSet(\VSet)$ a binding.
Then, $\PSet$ is an encasement w.r.t. $\qpElm$ and $\bpElm$ if
there exists an elementary dependence map $\spcFun \!\in\! \ESpcSet[
{\StrSet(\sElm)} ](\qpElm)$ such that, for all assignments $\asgFun
\!\in\! \AsgSet(\QPAVSet{\qpElm}, \sElm)$, it holds that
$\playFun(\spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm) \!\in\! \PSet$.

In the next lemma, we give the second of the two crucial steps in our
elementariness proof.
In particular, we are able to show a one-to-one relationship between the
wining in the dependence-vs-valuation game of player even and the
verification of the encasement property of the associated winning set.
Moreover, in the case that the latter is a Borelian set, by using Martin's
Determinacy Theorem <cit.>, we obtain a complete characterization of
the winning concept by means of that of encasements.

Let $\GName$ be a , $\sElm \in \StSet$ one of its states, $\PSet
\subseteq \PthSet(\sElm)$ a set of paths, $\qpElm \in \QPSet(\VSet)$ a
quantification prefix over a set $\VSet \subseteq \VarSet$ of variables,
and $\bpElm \in \BndSet(\VSet)$ a binding.
Then, the following hold:

player even wins $\HName(\GName, \sElm, \PSet, \qpElm, \bpElm)$ iff
$\PSet$ is an encasement w.r.t. $\qpElm$ and $\bpElm$;

if player odd wins $\HName(\GName, \sElm, \PSet, \qpElm, \bpElm)$ then
$\PSet$ is not an encasement w.r.t. $\qpElm$ and $\bpElm$;

if $\PSet$ is a Borelian set and it is not an encasement w.r.t.					$\qpElm$ and $\bpElm$ then player odd wins $\HName(\GName, \sElm,
\PSet, \qpElm, \bpElm)$.

Finally, we have all technical tools useful to prove the elementariness of
the satisfiability for .
Intuitively, we describe a bidirectional reduction of the problem of
interest to the verification of the winning in the dependence-vs-valuation
The idea behind this construction resides in the strong similarity between
the statement of Corollary <ref> of  strategy
quantification and the definition of the winning condition in a two-player
Indeed, on one hand, we say that a sentence is satisfiable iff “there
exists a dependence map such that, for all all assignments, it holds that
On the other hand, we say that player even wins a game iff “there exists
an even scheme such that, for all odd schemes, it holds that ...”.
In particular, for the  fragment, we can resolve the gap between these
two formulations, by using the concept of elementary quantification.

Let $\GName$ be a , $\varphi$ an  formula, $\sElm \in \StSet$ a
state, and $\asgFun \in \AsgSet(\sElm)$ an $\sElm$-total assignment with
$\free{\varphi} \subseteq \dom{\asgFun}$.
Then, it holds that $\GName, \asgFun, \sElm \models \varphi$ iff $\GName,
\asgFun, \sElm \emodels \varphi$.

The proof proceeds by induction on the structure of the formula.
For the sake of succinctness, we only show the most important inductive
case of principal subsentences $\phi \in \psnt{\varphi}$, i.e., when
$\phi$ is of the form $\qpSym \bpElm \psi$, where $\qpElm \in
\QPSet(\VSet)$ and $\bpElm \in \BPSet(\VSet)$ are, respectively, a
quantification and binding prefix over a set $\VSet \subseteq \VarSet$ of
variables, and $\psi$ is a variable-closed formula.

The proof of this direction is practically the same of the one used in
Theorem <ref> of  elementary coherence.
So, we omit to report it here.

[Only if].

Assume that $\GName, \emptyfun, \sElm \models \qpSym \bpElm \psi$.
Then, it is easy to see that, for all elementary dependence maps $\spcFun
\in \ESpcSet[ {\StrSet(\sElm)} ](\dual{\qpElm})$, there is an assignment
$\asgFun \in \AsgSet(\QPAVSet{\dual{\qpElm}}, \sElm)$ such that $\GName,
\spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm \models \psi$.

Indeed, suppose by contradiction that there exists an elementary
dependence map $\spcFun \in \ESpcSet[ {\StrSet(\sElm)} ](\dual{\qpElm})$
such that, for all assignments $\asgFun \in
\AsgSet(\QPAVSet{\dual{\qpElm}}, \sElm)$, it holds that $\GName,
\spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm \not\models \psi$, i.e.,
$\GName, \spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm \models \neg \psi$,
and so $\GName, \spcFun(\asgFun), \sElm \models \bpElm \neg \psi$.
Then, by Corollary <ref> of  strategy quantification,
we have that $\GName, \emptyfun, \sElm \models \dual{\qpElm} \bpElm \neg
\psi$, i.e., $\GName, \emptyfun, \sElm \models \neg \qpElm \bpElm \psi$,
and so $\GName, \emptyfun, \sElm \not\models \qpElm \bpElm \psi$, which is

Now, let $\PSet \defeq \set{ \playFun(\asgFun, \sElm) \in \PthSet(\sElm)
}{ \asgFun \in \AsgSet(\AgSet, \sElm) \land \GName, \asgFun, \sElm
\not\models \psi}$.
Then, it is evident that, for all elementary dependence maps $\spcFun \in
\ESpcSet[ {\StrSet(\sElm)} ](\dual{\qpElm})$, there is an assignment
$\asgFun \in \AsgSet(\QPAVSet{\dual{\qpElm}}, \sElm)$ such that
$\playFun(\spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm) \not\in \PSet$.

At this point, by Definition <ref> of encasement, it is
clear that $\PSet$ is not an encasement w.r.t. $\dual{\qpElm}$ and
Moreover, since $\psi$ describes a regular language, the derived set
$\PSet$ is Borelian <cit.>.
Consequently, by Item <ref> of
Lemma <ref> of encasement characterization, we have that
player odd wins the  $\HName(\GName, \sElm, \PSet, \dual{\qpElm},
\bpElm)$.
Thus, by Lemma <ref> of dependence-vs-valuation duality,
player even wins the dual  $\HName(\GName, \sElm, \PthSet(\sElm)
\setminus \PSet, \qpElm, \bpElm)$.
Hence, by Item <ref> of Lemma <ref>,
we have that $\PthSet(\sElm) \setminus \PSet$ is an encasement w.r.t.			$\qpElm$ and $\bpElm$.
Finally, again by Definition <ref>, there exists an
elementary dependence map $\spcFun \in \ESpcSet[ {\StrSet(\sElm)}
](\qpElm)$ such that, for all assignments $\asgFun \in
\AsgSet(\QPAVSet{\qpElm}, \sElm)$, it holds that
$\playFun(\spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm) \in \PthSet(\sElm)
\setminus \PSet$.

Now, it is immediate to observe that $\PthSet(\sElm) \setminus \PSet =
\set{ \playFun(\asgFun, \sElm) \in \PthSet(\sElm) }{ \asgFun \in
\AsgSet(\AgSet, \sElm) \land \GName, \asgFun, \sElm \models \psi}$.
So, by the inductive hypothesis, we have that $\PthSet(\sElm) \setminus
\PSet = \set{ \playFun(\asgFun, \sElm) \in \PthSet(\sElm) }{ \asgFun \in
\AsgSet(\AgSet, \sElm) \land \GName, \asgFun, \sElm \emodels \psi}$, from
which we derive that there exists an elementary dependence map $\spcFun
\in \ESpcSet[ {\StrSet(\sElm)} ](\qpElm)$ such that, for all assignments
$\asgFun \in \AsgSet(\QPAVSet{\qpElm}, \sElm)$, it holds that $\GName,
\spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm \emodels \psi$.
Consequently, by Definition <ref> of 			elementary semantics, we have that $\GName, \emptyfun, \sElm \emodels
\qpSym \bpElm \psi$.

As an immediate consequence of the previous theorem, we derive the following
fundamental corollary.

Let $\GName$ be a  and $\varphi$ an  sentence.
Then, $\GName \models \varphi$ iff $\GName \emodels \varphi$.

It is worth to observe that the elementariness property for  is a
crucial difference w.r.t. , which allows us to obtain an elementary
decision procedure for the related model-checking problem, as described in
the last part of the next section.

Model-Checking Procedures

In this section, we study the model-checking problem for  and show that,
in general, it is non-elementarily decidable, while, in the particular case of
sentences, it is just 2, as for .

For the algorithmic procedures, we follow an automata-theoretic
approach <cit.>, reducing the decision problem for the logics to the
emptiness problem of an automaton.
In particular, we use a bottom-up technique through which we recursively
label each state of the  of interest by all principal subsentences of the
specification that are satisfied on it, starting from the innermost
subsentences and terminating with the sentence under exam.
In this way, at a given step of the recursion, since the satisfaction of all
subsentences of the given principal sentence has already been determined, we
can assume that the matrix of the latter is only composed by Boolean
combinations and nesting of goals whose temporal part is simply .
The procedure we propose here extends that used for  in <cit.> by
means of a richer structure of the automata involved in.

The rest of this section is organized as follows.
In Subsection <ref>, we recall the definition of alternating
parity tree automata.
Then, in Subsection <ref>, we build an automaton accepting a
tree encoding of a  iff this satisfies the formula of interest, which is
used to prove the main result about  and  model checking.
Finally, in Subsection <ref>, we refine the previous result
to obtain an elementary decision procedure for .

Alternating tree automata

Nondeterministic tree automata are a generalization to infinite trees
of the classical nondeterministic word automata on infinite words
(see <cit.>, for an introduction).

Alternating tree automata are a further generalization of
nondeterministic tree automata <cit.>.
Intuitively, on visiting a node of the input tree, while the latter sends
exactly one copy of itself to each of the successors of the node, the former
can send several own copies to the same successor.

Here we use, in particular, alternating parity tree automata, which
are alternating tree automata along with a parity acceptance
condition (see <cit.>, for a survey).

We now give the formal definition of alternating tree automata.

An alternating tree automaton (, for short) is a tuple
$\AName \defeq \ATAStruct$, where $\LabSet$, $\DirSet$, and $\QSet$ are,
respectively, non-empty finite sets of input symbols,
directions, and states, $\qElm[0] \in \QSet$ is an
initial state, $\aleph$ is an acceptance condition to be
defined later, and $\delta : \QSet \times \LabSet \to \PBoolSet(\DirSet
\times \QSet)$ is an alternating transition function that maps each
pair of states and input symbols to a positive Boolean combination on the
set of propositions of the form $(\dElm, \qElm) \in \DirSet \times \QSet$,
a.k.a. moves.

On one side, a nondeterministic tree automaton (, for
short) is a special case of  in which each conjunction in the
transition function $\delta$ has exactly one move $(\dElm, \qElm)$
associated with each direction $\dElm$.
This means that, for all states $\qElm \in \QSet$ and symbols $\sigma \in
\LabSet$, we have that $\atFun(\qElm, \sigma)$ is equivalent to a Boolean
formula of the form $\bigvee_{i} \bigwedge_{\dElm \in \DirSet} (\dElm,
\qElm[i, \dElm])$.

On the other side, a universal tree automaton (, for
short) is a special case of  in which all the Boolean combinations that
appear in $\delta$ are conjunctions of moves.
Thus, we have that $\atFun(\qElm, \sigma) = \bigwedge_{i} (\dElm[i],
\qElm[i])$, for all states $\qElm \in \QSet$ and symbols $\sigma \in
\LabSet$.

The semantics of the s is given through the following concept of run.

A run of an  $\AName = \ATAStruct$ on a $\LabSet$-labeled
$\DirSet$-tree $\TName = \LTStruct$ is a $(\DirSet \times \QSet)$-tree
$\RSet$ such that, for all nodes $\xElm \in \RSet$, where $\xElm =
\prod_{i = 1}^{n} (\dElm[i], \qElm[i])$ and $\yElm \defeq \prod_{i =
1}^{n} \dElm[i]$ with $n \in \numco{0}{\omega}$, it holds that (i)
$\yElm \in \TSet$ and (ii), there is a set of moves $\SSet
\subseteq \DirSet \times \QSet$ with $\SSet \models \delta(\qElm[n],
\vFun(\yElm))$ such that $\xElm \cdot (\dElm, \qElm) \in \RSet$, for all
$(\dElm, \qElm) \in \SSet$.

In the following, we consider s along with the parity acceptance
condition (, for short) $\aleph \defeq (\FSet_{1}, \ldots,
\FSet_{k}) \in (\pow{\QSet})^{+}$ with $\FSet_{1} \subseteq \ldots \subseteq
\FSet_{k} = \QSet$ (see <cit.>, for more).
The number $k$ of sets in the tuple $\aleph$ is called the index of
the automaton.
We also consider s with the co-Büchi acceptance condition
(, for short) that is the special parity condition with index

Let $\RSet$ be a run of an  $\AName$ on a tree $\TName$ and $\wElm$ one
of its branches.
Then, by $\infFun(\wElm) \defeq \set{ \qElm \in \QSet }{ \card{\set{ i \in
\SetN }{ \exists \dElm \in \DirSet . (w)_{i} = (\dElm, \qElm) }} = \omega }$
we denote the set of states that occur infinitely often as the second
component of the letters along the branch $w$.
Moreover, we say that $w$ satisfies the parity acceptance condition $\aleph
\!=\! (\FSet_{1}, \ldots, \FSet_{k})$ if the least index $i \!\in\!
\numcc{1}{k}$ for which $\infFun(w) \cap \FSet_{i} \neq \emptyset$ is even.

At this point, we can define the concept of language accepted by an .

An  $\AName = \ATAStruct$ accepts a $\LabSet$-labeled
$\DirSet$-tree $\TName$ iff is there exists a run $\RSet$ of $\AName$ on
$\TName$ such that all its infinite branches satisfy the acceptance
condition $\aleph$.

By $\LangSet(\AName)$ we denote the language accepted by the  $\AName$,
i.e., the set of trees $\TName$ accepted by $\AName$.
Moreover, $\AName$ is said to be empty if $\LangSet(\AName) =
\emptyset$.
The emptiness problem for $\AName$ is to decide whether
$\LangSet(\AName) = \emptyset$.

We finally show a simple but useful result about the  direction
To do this, we first need to introduce an extra notation.
Let $\fElm \in \BoolSet(\PSet)$ be a Boolean formula on a set of
propositions $\PSet$.
Then, by $\fElm[][\pElm / \qElm \:\!|\:\! \pElm \in \PSet']$ we denote the
formula in which all occurrences of the propositions $\pElm \in \PSet'
\subseteq \PSet$ in $\fElm$ are replaced by the proposition $\qElm$
belonging to a possibly different set.

Let $\AName \defeq \TATuple {\LabSet \times \DirSet} {\DirSet} {\QSet}
{\atFun} {\qElm[0]} {\aleph}$ be an  over a set of $m$ directions
with $n$ states and index $k$.
Moreover, let $\dElm[0] \in \DirSet$ be a distinguished direction.
Then, there exists an  $\NName^{\dElm[0]} \defeq \TATuple {\LabSet}
{\DirSet} {\QSet'} {\atFun'} {\qElm[0 | ']} {\aleph'}$ with $m \cdot
2^{\AOmicron{k \cdot n \cdot \log n}}$ states and index $\AOmicron{k \cdot
n \cdot \log n}$ such that, for all $\LabSet$-labeled $\DirSet$-tree
$\TName \defeq \LTStruct$, it holds that $\TName \in
\LangSet(\NName^{\dElm[0]})$ iff $\TName' \in \LangSet(\AName)$, where
$\TName'$ is the $(\LabSet \times \DirSet)$-labeled $\DirSet$-tree
$\LTTuple{}{}{\TSet}{\vFun'}$ such that $\vFun'(\tElm) \defeq (\vFun(t),
\lst{\dElm[0] \cdot t})$, for all $\tElm \in \TSet$.

As first step, we use the well-known nondeterminization procedure for
s <cit.> in order to transform the  $\AName$ into an
equivalent  $\NName = \TATuple {\LabSet \times \DirSet} {\DirSet}
{\QSet''} {\atFun''} {\qElm[0 | '']} {\aleph''}$ with $2^{\AOmicron{k
\cdot n \cdot \log n}}$ states and index $k' = \AOmicron{k \cdot n \cdot
\log n}$.
Then, we transform the latter into the new  $\NName^{\dElm[0]} \defeq
\TATuple {\LabSet} {\DirSet} {\QSet'} {\atFun'} {\qElm[0 | ']} {\aleph'}$
with $m \cdot 2^{\AOmicron{k \cdot n \cdot \log n}}$ states and same index
$k'$, where $\QSet' \defeq \QSet'' \times \DirSet$, $\qElm[0 | '] \defeq
(\qElm[0 | ''], \dElm[0])$, $\aleph' \defeq (\FSet[1] \times \DirSet,
\ldots, \FSet[k'] \times \DirSet)$ with $\aleph'' \defeq (\FSet[1],
\ldots, \FSet[k'])$, and $\atFun'((\qElm, \dElm), \sigma) \defeq
\atFun''(\qElm, (\sigma, \dElm)) [(\dElm', \qElm') / (\dElm', (\qElm',
\dElm')) \:\!|\:\! (\dElm', \qElm') \in \DirSet \times \QSet'']$, for all
$(\qElm, \dElm) \in \QSet'$ and $\sigma \in \LabSet$.
Now, it easy to see that $\NName^{\dElm[0]}$ satisfies the declared

Model Checking

A first step towards our construction of an algorithmic procedure for the
solution of the  model-checking problem is to define, for each possible
formula $\varphi$, an alternating parity tree automaton $\AName[\varphi |
^{\GName}]$ that recognizes a tree encoding $\TName$ of a 		$\GName$, containing the information on an assignment $\asgFun$ on the free
variables/agents of $\varphi$, iff $\GName$ is a model of $\varphi$ under
The high-level idea at the base of this construction is an evolution and
merging of those behind the translations of  and , respectively,

To proceed with the formal description of the model-checking procedure, we
have to introduce a concept of encoding for the assignments of a .

Let $\GName$ be a , $\sElm \in \StSet[\GName]$ one of its states, and
$\asgFun \in \AsgSet[\GName](\VSet, \sElm)$ an assignment defined on the
set $\VSet \subseteq \VarSet \cup \AgSet$.
Then, a $(\ValSet[ {\AcSet[\GName]} ](\VSet) \times
\StSet[\GName])$-labeled $\StSet[\GName]$-tree $\TName \defeq
\LTTuple{}{}{\TSet}{\uFun}$, where $\TSet \defeq \set{ \trkElm_{\geq 1} }{
\trkElm \in \TrkSet[\GName](\sElm) }$, is an assignment-state
encoding for $\asgFun$ if it holds that $\uFun(\tElm) \defeq
(\flip{\asgFun}(\sElm \cdot \tElm), \lst{\sElm \cdot \tElm})$, for all
$\tElm \in \TSet$.

Observe that there is a unique assignment-state encoding for each given

In the next lemma, we prove the existence of an  for each  and
formula that is able to recognize all the assignment-state encodings of
an a priori given assignment, made the assumption that the formula is
satisfied on the  under this assignment.

Let $\GName$ be a  and $\varphi$ an  formula.
Then, there exists an  $\AName[\varphi | ^{\GName}] \defeq \TATuple
{\ValSet[ {\AcSet[\GName]} ](\free{\varphi}) \times \StSet[\GName]}
{\StSet[\GName]} {\QSet[\varphi]} {\atFun[\varphi]} {\qElm[0\varphi]}
{\aleph_{\varphi}}$ such that, for all states $\sElm \in \StSet[\GName]$
and assignments $\asgFun \in \AsgSet[\GName](\free{\varphi}, \sElm)$, it
holds that $\GName, \asgFun, \sElm \models \varphi$ iff $\TName \in
\LangSet(\AName[\varphi | ^{\GName}])$, where $\TName$ is the
assignment-state encoding for $\asgFun$.

The construction of the  $\AName[\varphi | ^{\GName}]$ is done
recursively on the structure of the formula $\varphi$, which w.l.o.g.			is supposed to be in , by using a variation of the transformation,
via alternating tree automata, of the S$1$S and S$k$S logics into
nondeterministic Büchi word and tree automata recognizing all models of
the formula of interest <cit.>.

The detailed construction of $\AName[\varphi | ^{\GName}]$, by a case
analysis on $\varphi$, follows.

* If $\varphi \in \APSet$, the automaton has to verify if the atomic
proposition is locally satisfied or not.
To do this, we set $\AName[\varphi | ^{\GName}] \defeq \TATuple
{\ValSet[ {\AcSet[\GName]} ](\emptyset) \times \StSet[\GName]}
{\StSet[\GName]} {\{ \varphi \}} {\atFun[\varphi]} {\varphi} {(\{
\varphi \})}$, where $\atFun[\varphi](\varphi, (\valFun, \sElm))
\defeq \Tt$, if $\varphi \in \labFun[\GName](\sElm)$, and
$\atFun[\varphi](\varphi, (\valFun, \sElm)) \defeq \Ff$, otherwise.
Intuitively, $\AName[\varphi | ^{\GName}]$ only verifies that the
state $\sElm$ in the labeling of the root of the assignment-state
encoding of the empty assignment $\emptyfun$ satisfies $\varphi$.

* The boolean case $\varphi = \neg \varphi'$ is treated in the classical
way, by simply dualizing the automaton $\AName[\varphi' | ^{\GName}] =
\TATuple {\ValSet[ {\AcSet[\GName]} ](\free{\varphi'}) \times
\StSet[\GName]} {\StSet[\GName]} {\QSet[\varphi']} {\atFun[\varphi']}
{\qElm[0\varphi']} {\aleph_{\varphi'}}$ <cit.>.

* The boolean cases $\varphi = \varphi_{1} \Opr \varphi_{2}$, with $\Opr
\in \{ \wedge, \vee \}$, are treated in a way that is similar to the
classical one, by simply merging the two automata $\AName[\varphi_{1}
| ^{\GName}] = \TATuple {\ValSet[ {\AcSet[\GName]}
](\free{\varphi_{1}}) \times \StSet[\GName]} {\StSet[\GName]}
{\QSet[\varphi_{1}]} {\atFun[\varphi_{1}]} {\qElm[0\varphi_{1}]}
{\aleph_{\varphi_{1}}}$ and $\AName[\varphi_{2} | ^{\GName}] =
\TATuple {\ValSet[ {\AcSet[\GName]} ](\free{\varphi_{2}}) \times
\StSet[\GName]} {\StSet[\GName]} {\QSet[\varphi_{2}]}
{\atFun[\varphi_{2}]} {\qElm[0\varphi_{2}]} {\aleph_{\varphi_{2}}}$
into the automaton $\AName[\varphi | ^{\GName}] \defeq \TATuple
{\ValSet[ {\AcSet[\GName]} ](\free{\varphi}) \times \StSet[\GName]}
{\StSet[\GName]} {\QSet[\varphi]} {\atFun[\varphi]} {\qElm[0\varphi]}
{\aleph_{\varphi}}$, where the following hold:

* $\QSet[\varphi] \defeq \{ \qElm[0\varphi] \} \cup
\QSet[\varphi_{1}] \cup \QSet[\varphi_{2}]$, with $\qElm[0\varphi]
\not\in \QSet[\varphi_{1}] \cup \QSet[\varphi_{2}]$;

* $\atFun[\varphi](\qElm[0\varphi], (\valFun, \sElm)) \defeq
\atFun[\varphi_{1}](\qElm[0\varphi_{1}], (\valFun_{\rst
\free{\varphi_{1}}}, \sElm)) \:\Opr
\atFun[\varphi_{2}](\qElm[0\varphi_{2}], (\valFun_{\rst
\free{\varphi_{2}}}, \sElm))$, for all $(\valFun, \sElm) \in
\ValSet[ {\AcSet[\GName]} ](\free{\varphi}) \times
\StSet[\GName]$;

* $\atFun[\varphi](\qElm, (\valFun, \sElm)) \defeq
\atFun[\varphi_{1}](\qElm, (\valFun_{\rst \free{\varphi_{1}}},
\sElm))$, if $\qElm \in \QSet[\varphi_{1}]$, and
$\atFun[\varphi](\qElm, (\valFun, \sElm)) \defeq
\atFun[\varphi_{2}](\qElm, (\valFun_{\rst \free{\varphi_{2}}},
\sElm))$, otherwise, for all $\qElm \in \QSet[\varphi_{1}] \cup
\QSet[\varphi_{2}]$ and $(\valFun, \sElm) \in \ValSet[
{\AcSet[\GName]} ](\free{\varphi}) \times \StSet[\GName]$;

* $\aleph_{\varphi} \defeq (\FSet[1\varphi], \ldots,
\FSet[k\varphi])$, where (i) $\aleph_{\varphi_{1}} \defeq
(\FSet[1\varphi_{1}], \ldots, \FSet[k_{1}\varphi_{1}])$ and
$\aleph_{\varphi_{2}} \defeq (\FSet[1\varphi_{2}], \ldots,
\FSet[k_{2}\varphi_{2}])$, (ii) $h = \min \{ k_{1}, k_{2}
\}$ and $k = \max \{ k_{1}, k_{2} \}$, (iii)
$\FSet[i\varphi] \defeq \FSet[i\varphi_{1}] \cup
\FSet[i\varphi_{2}]$, for $i \in \numcc{1}{h}$, (iv)
$\FSet[i\varphi] \defeq \FSet[i\varphi_{j}]$, for $i \in
\numcc{h + 1}{k - 1}$ with $k_{j} = k$, and (v)
$\FSet[k\varphi] \defeq \QSet[\varphi]$.

* The case $\varphi = \X \varphi'$ is solved by running the automaton
$\AName[\varphi' | ^{\GName}] = \TATuple {\ValSet[ {\AcSet[\GName]}
](\free{\varphi'}) \times \StSet[\GName]} {\StSet[\GName]}
{\QSet[\varphi']} {\atFun[\varphi']} {\qElm[0\varphi']}
{\aleph_{\varphi'}}$ on the successor node of the root of the
assignment-state encoding in the direction individuated by the
assignment itself.
To do this, we use the automaton $\AName[\varphi | ^{\GName}] \defeq
\TATuple {\ValSet[ {\AcSet[\GName]} ](\free{\varphi}) \times
\StSet[\GName]} {\StSet[\GName]} {\QSet[\varphi]} {\atFun[\varphi]}
{\qElm[0\varphi]} {\aleph_{\varphi}}$, where the following hold:

* $\QSet[\varphi] \defeq \{ \qElm[0\varphi] \} \cup
\QSet[\varphi']$, with $\qElm[0\varphi] \not\in \QSet[\varphi']$;

* $\atFun[\varphi](\qElm[0\varphi], (\valFun, \sElm)) \defeq
(\trnFun[\GName](\sElm, \valFun_{\rst \AgSet}),
\qElm[0\varphi'])$, for all $(\valFun, \sElm) \in \ValSet[
{\AcSet[\GName]} ](\free{\varphi}) \times \StSet[\GName]$;

* $\atFun[\varphi](\qElm, (\valFun, \sElm)) \defeq
\atFun[\varphi'](\qElm, (\valFun_{\rst \free{\varphi'}}, \sElm))$,
for all $\qElm \in \QSet[\varphi']$ and $(\valFun, \sElm) \in
\ValSet[ {\AcSet[\GName]} ](\free{\varphi}) \times
\StSet[\GName]$;

* $\aleph_{\varphi} \defeq (\FSet[1\varphi'], \ldots,
\FSet[k\varphi'] \cup \{ \qElm[0\varphi] \})$, where
$\aleph_{\varphi'} \defeq (\FSet[1\varphi'], \ldots,
\FSet[k\varphi'])$.

* To handle the case $\varphi = \varphi_{1} \U \varphi_{2}$, we use
the automaton $\AName[\varphi | ^{\GName}] \defeq \TATuple {\ValSet[
{\AcSet[\GName]} ](\free{\varphi}) \times \StSet[\GName]}
{\StSet[\GName]} {\QSet[\varphi]} {\atFun[\varphi]} {\qElm[0\varphi]}
{\aleph_{\varphi}}$ that verifies the truth of the until operator
using its one-step unfolding equivalence $\varphi_{1} \U \varphi_{2}
\equiv \varphi_{2} \vee \varphi_{1} \wedge \X \varphi_{1} \U
\varphi_{2}$, by appropriately running the two automata
$\AName[\varphi_{1} | ^{\GName}] = \TATuple {\ValSet[ {\AcSet[\GName]}
](\free{\varphi_{1}}) \times \StSet[\GName]} {\StSet[\GName]}
{\QSet[\varphi_{1}]} {\atFun[\varphi_{1}]} {\qElm[0\varphi_{1}]}
{\aleph_{\varphi_{1}}}$ and $\AName[\varphi_{2} | ^{\GName}] =
\TATuple {\ValSet[ {\AcSet[\GName]} ](\free{\varphi_{2}}) \times
\StSet[\GName]} {\StSet[\GName]} {\QSet[\varphi_{2}]}
{\atFun[\varphi_{2}]} {\qElm[0\varphi_{2}]} {\aleph_{\varphi_{2}}}$
for the inner formulas $\varphi_{1}$ and $\varphi_{2}$.

* $\QSet[\varphi] \defeq \{ \qElm[0\varphi] \} \cup
\QSet[\varphi_{1}] \cup \QSet[\varphi_{2}]$, with $\qElm[0\varphi]
\not\in \QSet[\varphi_{1}] \cup \QSet[\varphi_{2}]$;

* $\atFun[\varphi](\qElm[0\varphi], (\valFun, \sElm)) \defeq
\atFun[\varphi_{2}](\qElm[0\varphi_{2}], (\valFun_{\rst
\free{\varphi_{2}}}, \sElm)) \vee
\atFun[\varphi_{1}](\qElm[0\varphi_{1}], (\valFun_{\rst
\free{\varphi_{1}}}, \sElm)) \wedge (\trnFun[\GName](\sElm,
\valFun_{\rst \AgSet}), \qElm[0\varphi])$, for all $(\valFun,
\sElm) \in \ValSet[ {\AcSet[\GName]} ](\free{\varphi}) \times
\StSet[\GName]$;

* $\atFun[\varphi](\qElm, (\valFun, \sElm)) \defeq
\atFun[\varphi_{1}](\qElm, (\valFun_{\rst \free{\varphi_{1}}},
\sElm))$, if $\qElm \in \QSet[\varphi_{1}]$, and
$\atFun[\varphi](\qElm, (\valFun, \sElm)) \defeq
\atFun[\varphi_{2}](\qElm, (\valFun_{\rst \free{\varphi_{2}}},
\sElm))$, otherwise, for all $\qElm \in \QSet[\varphi_{1}] \cup
\QSet[\varphi_{2}]$ and $(\valFun, \sElm) \in \ValSet[
{\AcSet[\GName]} ](\free{\varphi}) \times \StSet[\GName]$;

* $\aleph_{\varphi} \defeq (\FSet[1\varphi], \ldots,
\FSet[k\varphi])$, where (i) $\aleph_{\varphi_{1}} \defeq
(\FSet[1\varphi_{1}], \ldots, \FSet[k_{1}\varphi_{1}])$ and
$\aleph_{\varphi_{2}} \defeq (\FSet[1\varphi_{2}], \ldots,
\FSet[k_{2}\varphi_{2}])$, (ii) $h = \min \{ k_{1}, k_{2}
\}$ and $k = \max \{ k_{1}, k_{2} \}$, (iii)
$\FSet[i\varphi] \defeq \{ \qElm[0\varphi] \} \cup
\FSet[i\varphi_{1}] \cup \FSet[i\varphi_{2}]$, for $i \in
\numcc{1}{h}$, (iv) $\FSet[i\varphi] \defeq \{
\qElm[0\varphi] \} \cup \FSet[i\varphi_{j}]$, for $i \in \numcc{h
+ 1}{k - 1}$ with $k_{j} = k$, and (v) $\FSet[k\varphi]
\defeq \QSet[\varphi]$.

It is important to observe that the initial state $\qElm[0\varphi]$ is
included in all sets of the parity acceptance condition, in particular
in $\FSet[1\varphi]$, in order to avoid its regeneration for an
infinite number of times.

* To handle the case $\varphi = \varphi_{1} \R \varphi_{2}$, we use
the automaton $\AName[\varphi | ^{\GName}] \defeq \TATuple {\ValSet[
{\AcSet[\GName]} ](\free{\varphi}) \times \StSet[\GName]}
{\StSet[\GName]} {\QSet[\varphi]} {\atFun[\varphi]} {\qElm[0\varphi]}
{\aleph_{\varphi}}$ that verifies the truth of the release operator
using its one-step unfolding equivalence $\varphi_{1} \R \varphi_{2}
\equiv \varphi_{2} \wedge (\varphi_{1} \vee \X \varphi_{1} \R
\varphi_{2})$, by appropriately running the two automata
$\AName[\varphi_{1} | ^{\GName}] = \TATuple {\ValSet[ {\AcSet[\GName]}
](\free{\varphi_{1}}) \times \StSet[\GName]} {\StSet[\GName]}
{\QSet[\varphi_{1}]} {\atFun[\varphi_{1}]} {\qElm[0\varphi_{1}]}
{\aleph_{\varphi_{1}}}$ and $\AName[\varphi_{2} | ^{\GName}] =
\TATuple {\ValSet[ {\AcSet[\GName]} ](\free{\varphi_{2}}) \times
\StSet[\GName]} {\StSet[\GName]} {\QSet[\varphi_{2}]}
{\atFun[\varphi_{2}]} {\qElm[0\varphi_{2}]} {\aleph_{\varphi_{2}}}$
for the inner formulas $\varphi_{1}$ and $\varphi_{2}$.

* $\QSet[\varphi] \defeq \{ \qElm[0\varphi] \} \cup
\QSet[\varphi_{1}] \cup \QSet[\varphi_{2}]$, with $\qElm[0\varphi]
\not\in \QSet[\varphi_{1}] \cup \QSet[\varphi_{2}]$;

* $\atFun[\varphi](\qElm[0\varphi], (\valFun, \sElm)) \defeq
\atFun[\varphi_{2}](\qElm[0\varphi_{2}], (\valFun_{\rst
\free{\varphi_{2}}}, \sElm)) \wedge
(\atFun[\varphi_{1}](\qElm[0\varphi_{1}], (\valFun_{\rst
\free{\varphi_{1}}}, \sElm)) \vee (\trnFun[\GName](\sElm,
\valFun_{\rst \AgSet}), \qElm[0\varphi]))$, for all $(\valFun,
\sElm) \in \ValSet[ {\AcSet[\GName]} ](\free{\varphi}) \times
\StSet[\GName]$;

* $\atFun[\varphi](\qElm, (\valFun, \sElm)) \defeq
\atFun[\varphi_{1}](\qElm, (\valFun_{\rst \free{\varphi_{1}}},
\sElm))$, if $\qElm \in \QSet[\varphi_{1}]$, and
$\atFun[\varphi](\qElm, (\valFun, \sElm)) \defeq
\atFun[\varphi_{2}](\qElm, (\valFun_{\rst \free{\varphi_{2}}},
\sElm))$, otherwise, for all $\qElm \in \QSet[\varphi_{1}] \cup
\QSet[\varphi_{2}]$ and $(\valFun, \sElm) \in \ValSet[
{\AcSet[\GName]} ](\free{\varphi}) \times \StSet[\GName]$;

* $\aleph_{\varphi} \defeq (\FSet[1\varphi], \ldots,
\FSet[k\varphi])$, where (i) $\aleph_{\varphi_{1}} \defeq
(\FSet[1\varphi_{1}], \ldots, \FSet[k_{1}\varphi_{1}])$ and
$\aleph_{\varphi_{2}} \defeq (\FSet[1\varphi_{2}], \ldots,
\FSet[k_{2}\varphi_{2}])$, (ii) $h = \min \{ k_{1}, k_{2}
\}$ and $k = \max \{ k_{1}, k_{2} \}$, (iii)
$\FSet[1\varphi] \defeq \FSet[1\varphi_{1}] \cup
\FSet[1\varphi_{2}]$, (iv) $\FSet[i\varphi] \defeq \{
\qElm[0\varphi] \} \cup \FSet[i\varphi_{1}] \cup
\FSet[i\varphi_{2}]$, for $i \!\in\! \numcc{2}{h}$, (iv)
$\FSet[i\varphi] \!\defeq\! \{ \qElm[0\varphi] \} \cup
\FSet[i\varphi_{j}]$, for $i \!\in\! \numcc{h + 1}{k - 1}$ with
$k_{j} \!=\! k$, and (v) $\FSet[k\varphi] \!\defeq\!
\QSet[\varphi]$.

It is important to observe that, differently from the case of the
until operator, the initial state $\qElm[0\varphi]$ is included in all
sets of the parity acceptance condition but $\FSet[1\varphi]$, in
order to allow its regeneration for an infinite number of time.

* The case $\varphi = (\aElm, \xElm) \varphi'$ is solved by simply
transforming the transition function of the automaton $\AName[\varphi'
| ^{\GName}] = \TATuple {\ValSet[ {\AcSet[\GName]} ](\free{\varphi'})
\times \StSet[\GName]} {\StSet[\GName]} {\QSet[\varphi']}
{\atFun[\varphi']} {\qElm[0\varphi']} {\aleph_{\varphi'}}$, by setting
the value of the valuations in input w.r.t. the agent $\aElm$ to the
value of the same valuation w.r.t. the variable $\xElm$.
The definitions of the transition function for $\AName[\varphi |
^{\GName}] \defeq \TATuple {\ValSet[ {\AcSet[\GName]}
](\free{\varphi}) \times \StSet[\GName]} {\StSet[\GName]}
{\QSet[\varphi']} {\atFun[\varphi]} {\qElm[0\varphi']}
{\aleph_{\varphi'}}$ follows: $\atFun[\varphi](\qElm, (\valFun,
\sElm)) \defeq \atFun[\varphi'](\qElm, (\valFun', \sElm))$, where
$\valFun' = \valFun[][\aElm \mapsto \valFun(\xElm)]_{\rst
\free{\varphi'}}$, if $\aElm \in \free{\varphi'}$, and $\valFun' =
\valFun$, otherwise, for all $\qElm \in \QSet[\varphi']$ and
$(\valFun, \sElm) \in \ValSet[ {\AcSet[\GName]} ](\free{\varphi})
\times \StSet[\GName]$.

* To handle the case $\varphi = \EExs{\xElm} \varphi'$, assuming that
$\xElm \in \free{\varphi'}$, we use the operation of existential
projection for nondeterministic tree automata.
To do this, we have first to nondeterminize the  $\AName[\varphi'
| ^{\GName}]$, by applying the classic transformation <cit.>.
In this way, we obtain an equivalent  $\NName[\varphi' |
^{\GName}] = \TATuple {\ValSet[ {\AcSet[\GName]} ](\free{\varphi'})
\times \StSet[\GName]} {\StSet[\GName]} {\QSet[\varphi']}
{\atFun[\varphi']} {\qElm[0\varphi']} {\aleph_{\varphi'}}$.
Now, we make the projection, by defining the new  $\AName[\varphi
| ^{\GName}] \defeq \TATuple {\ValSet[ {\AcSet[\GName]}
](\free{\varphi}) \times \StSet[\GName]} {\StSet[\GName]}
{\QSet[\varphi']} {\atFun[\varphi]} {\qElm[0\varphi']}
{\aleph_{\varphi'}}$ where $\atFun[\varphi](\qElm, (\valFun, \sElm))
\defeq \bigvee_{\cElm \in \AcSet[\GName]} \atFun[\varphi'](\qElm,
(\valFun[][\xElm \mapsto \cElm], \sElm))$, for all $\qElm \in
\QSet[\varphi']$ and $(\valFun, \sElm) \in \ValSet[ {\AcSet[\GName]}
](\free{\varphi}) \times \StSet[\GName]$.

At this point, it only remains to prove that, for all states $\sElm \in
\StSet[\GName]$ and assignments $\asgFun \in
\AsgSet[\GName](\free{\varphi}, \sElm)$, it holds that $\GName, \asgFun,
\sElm \models \varphi$ iff $\TName \in \LangSet(\AName[\varphi |
^{\GName}])$, where $\TName$ is the assignment-state encoding for
The proof can be developed by a simple induction on the structure of the
formula $\varphi$ and is left to the reader as a simple exercise.

We now have the tools to describe the recursive model-checking procedure on
nested subsentences for  and its fragments under the general semantics.

To proceed, we have first to prove the following theorem that represents the
core of our automata-theoretic approach.

Let $\GName$ be a , $\sElm \in \StSet[\GName]$ one of its states, and
$\varphi$ an  sentence.
Then, there exists an  $\NName[\varphi | ^{\GName, \sElm}]$ such that
$\GName, \emptyfun, \sElm \models \varphi$ iff $\LangSet(\NName[\varphi |
^{\GName, \sElm}]) \neq \emptyset$.

To construct the  $\NName[\varphi | ^{\GName, \sElm}]$ we apply
Theorem <ref> of  direction projection with
distinguished direction $\sElm$ to the  $\AName[\varphi | ^{\GName}]$
derived by Lemma <ref> of  formula automaton.
In this way, we can ensure that the state labeling of nodes of the
assignment-state encoding is coherent with the node itself.

Observe that, since $\varphi$ is a sentence, we have that $\free{\varphi}
= \emptyset$, and so, the unique assignment-state encoding of interest is
that related to the empty assignment $\emptyfun$.

[Only if].

Suppose that $\GName, \emptyfun, \sElm \models \varphi$.
Then, by Lemma <ref>, we have that $\TName \in
\LangSet(\AName[\varphi | ^{\GName}])$, where $\TName$ is the elementary
dependence-state encoding for $\emptyfun$.
Hence, by Theorem <ref>, it holds that
$\LangSet(\NName[\varphi | ^{\GName, \sElm}]) \neq \emptyset$.

Suppose that $\LangSet(\NName[\varphi | ^{\GName, \sElm}]) \neq
\emptyset$.
Then, by Theorem <ref>, there exists an $( \{ \emptyfun \}
\times \StSet[\GName])$-labeled $\StSet[\GName]$-tree $\TName$ such that
$\TName \in \LangSet(\AName[\varphi | ^{\GName}])$.
Now, it is immediate to see that $\TName$ is the assignment-state encoding
for $\emptyfun$.
Hence, by Lemma <ref>, we have that $\GName, \emptyfun,
\sElm \models \varphi$.

Before continuing, we define the length $\lng{\varphi}$ of an  formula
$\varphi$ as the number $\card{\sub{\varphi}}$ of its subformulas.
We also introduce a generalization of the Knuth's double arrow notation in
order to represents a tower of exponentials: $a \uparrow\uparrow_{b} 0
\defeq b$ and $a \uparrow\uparrow_{b} (c + 1) \defeq a^{a
\uparrow\uparrow_{b} c}$, for all $a, b, c \in \SetN$.

At this point, we prove the main theorem about the non-elementary complexity
of  model-checking problem.

The model-checking problem for  is  w.r.t. the size of the
model and  w.r.t. the size of the specification.

By Theorem <ref> of  sentence automaton, to verify that
$\GName, \emptyfun, \sElm \models \varphi$, we simply calculate the
emptiness of the  $\NName[\varphi | ^{\GName, \sElm}]$ having
$\card{\StSet[\GName]} \cdot (2 \uparrow\uparrow_{m} m)$ states and index
$2 \uparrow\uparrow_{m} m$, where $m = \AOmicron{\lng{\varphi} \cdot \log
\lng{\varphi}}$.
It is well-known that the emptiness problem for such a kind of automaton
with $n$ states and index $h$ is solvable in time
$\AOmicron{n^{h}}$ <cit.>.
Thus, we get that the time complexity of checking whether $\GName,
\emptyfun, \sElm \models \varphi$ is $\card{\StSet[\GName]}^{2
\uparrow\uparrow_{m} m}$.
Hence, the membership of the model-checking problem for  in 			w.r.t. the size of the model and  w.r.t. the size of the
specification directly follows.
Finally, by getting the relative lower bound on the model from the same
problem for  <cit.>, the thesis is proved.

Finally, we show a refinement of the previous result, when we consider
sentences of the  fragment.

The model-checking problem for  is  w.r.t. the size of the
model and $(k + 1)$- w.r.t. the maximum alternation $k$ of the

By Theorem <ref> of  sentence automaton, to verify that
$\GName, \emptyfun, \sElm \models \qpElm \psi$, where $\qpElm \psi$ is an
principal sentence without proper subsentences, we can simply
calculate the emptiness of the  $\NName[\qpElm \psi | ^{\GName,
\sElm}]$ having $\card{\StSet[\GName]} \cdot (2 \uparrow\uparrow_{m} k)$
states and index $2 \uparrow\uparrow_{m} k$, where $m =
\AOmicron{\lng{\psi} \cdot \log \lng{\psi}}$ and $k = \alt{\qpElm \psi}$.
Thus, we get that the time complexity of checking whether $\GName,
\emptyfun, \sElm \models \qpElm \psi$ is $\card{\StSet[\GName]}^{2
\uparrow\uparrow_{m} k}$.
At this point, since we have to do this verification for each possible
state $\sElm \in \StSet[\GName]$ and principal subsentence $\qpElm \psi
\in \psnt{\varphi}$ of the whole  specification $\varphi$, we derive
that the bottom-up model-checking procedure requires time
$\card{\StSet[\GName]}^{2 \uparrow\uparrow_{\lng{\varphi}} k}$, where $k =
\max \set{ \alt{\qpElm \psi} }{ \qpElm \psi \in \psnt{\varphi} }$.
Hence, the membership of the model-checking problem for  in 			w.r.t. the size of the model and $(k + 1)$- w.r.t. the maximum
alternation $k$ of the specification directly follows.
Finally, by getting the relative lower bound on the model from the same

Model Checking

We now show how the concept of elementariness of dependence maps over
strategies can be used to enormously reduce the complexity of the
model-checking procedure for the  fragment.
The idea behind our approach is to avoid the use of projections used to
handle the strategy quantifications, by reducing them to action
quantifications, which can be managed locally on each state of the model
without a tower of exponential blow-ups.

To start with the description of the ad-hoc procedure for , we first
prove the existence of a  for each  and  goal $\bpElm \psi$
that recognizes all the assignment-state encodings of an a
priori given assignment,

Let $\GName$ be a  and $\bpElm \psi$ an  goal without principal
Then, there exists an  $\UName[\bpElm \psi | ^{\GName}] \defeq
\TATuple {\ValSet[ {\AcSet[\GName]} ](\free{\bpElm \psi}) \times
\StSet[\GName]} {\StSet[\GName]} {\QSet[\bpElm \psi]} {\atFun[\bpElm
\psi]} {\qElm[\bpElm \psi]} {\aleph_{\bpElm \psi}}$ such that, for all
states $\sElm \in \StSet[\GName]$ and assignments $\asgFun \in
\AsgSet[\GName](\free{\bpElm \psi}, \sElm)$, it holds that $\GName,
\asgFun, \sElm \models \bpElm \psi$ iff $\TName \in \LangSet(\UName[\bpElm
\psi | ^{\GName}])$, where $\TName$ is the assignment-state encoding for

A first step in the construction of the  $\UName[\bpElm \psi |
^{\GName}]$ is to consider the  $\UName[\psi] \defeq \WATuple
{\pow{\APSet}} {\QSet[\psi]} {\atFun[\psi]} {\QSet[0\psi]}
{\aleph_{\psi}}$ obtained by dualizing the  resulting from the
application of the classic Vardi-Wolper construction to the  formula
$\neg \psi$ <cit.>.
Observe that $\LangSet(\UName[\psi]) = \LangSet(\psi)$, i.e.,
$\UName[\psi]$ recognizes all infinite words on the alphabet
$\pow{\APSet}$ that satisfy the  formula $\psi$.
Then, define the components of $\UName[\bpElm \psi | ^{\GName}] \defeq
\TATuple {\ValSet[ {\AcSet[\GName]} ](\free{\bpElm \psi}) \times
\StSet[\GName]} {\StSet[\GName]} {\QSet[\bpElm \psi]} {\atFun[\bpElm
\psi]} {\qElm[0\bpElm\psi]} {\aleph_{\bpElm \psi}}$ as follows:

* $\QSet[\bpElm \psi] \defeq \{ \qElm[0\bpElm\psi] \} \cup \QSet[\psi]$,
with $\qElm[0\bpElm\psi] \not\in \QSet[\psi]$;

* $\atFun[\bpElm \psi](\qElm[0\bpElm\psi], (\valFun, \sElm)) \defeq
\bigwedge_{\qElm \in \QSet[0\psi]} \atFun[\bpElm \psi](\qElm,
(\valFun, \sElm))$, for all $(\valFun, \sElm) \in \ValSet[
{\AcSet[\GName]} ](\free{\bpElm \psi}) \times \StSet[\GName]$;

* $\atFun[\bpElm \psi](\qElm, (\valFun, \sElm)) \!\defeq\!
\bigwedge_{\qElm' \!\in\! \atFun[\psi](\qElm, \labFun[\GName](\sElm))}
(\trnFun[\GName](\sElm, \valFun \cmp \bndFun[\bpElm]), \qElm')$, for
all $\qElm \!\in\! \QSet[\psi]$ and $(\valFun, \sElm) \!\in\! \ValSet[
{\AcSet[\GName]} ](\free{\bpElm \psi}) \times \StSet[\GName]$;

* $\aleph_{\bpElm \psi} \defeq \aleph_{\psi}$.

Intuitively, the  $\UName[\bpElm \psi | ^{\GName}]$ simply runs the
$\UName[\psi]$ on the branch of the encoding individuated by the
assignment in input.
Thus, it is easy to see that, for all states $\sElm \in \StSet[\GName]$
and assignments $\asgFun \in \AsgSet[\GName](\free{\bpElm \psi}, \sElm)$,
it holds that $\GName, \asgFun, \sElm \models \bpElm \psi$ iff $\TName \in
\LangSet(\UName[\bpElm \psi | ^{\GName}])$, where $\TName$ is the
assignment-state encoding for $\asgFun$.

Now, to describe our modified technique, we introduce a new concept of
encoding regarding the elementary dependence maps over strategies.

Let $\GName$ be a , $\sElm \in \StSet[\GName]$ one of its states, and
$\spcFun \in \ESpcSet[ {\StrSet[\GName](\sElm)} ](\qpElm)$ an elementary
dependence map over strategies for a quantification prefix $\qpElm \in
\QPSet(\VSet)$ over the set $\VSet \subseteq \VarSet$.
Then, a $(\SpcSet[ {\AcSet[\GName]} ](\qpElm) \times
\StSet[\GName])$-labeled $\StSet[\GName]$-tree $\TName \defeq
\LTTuple{}{}{\TSet}{\uFun}$, where $\TSet \defeq \set{ \trkElm_{\geq 1} }{
\trkElm \in \TrkSet[\GName](\sElm) }$, is an elementary
dependence-state encoding for $\spcFun$ if it holds that $\uFun(\tElm)
\defeq (\adj{\spcFun}(\sElm \cdot \tElm), \lst{\sElm \cdot \tElm})$, for
all $\tElm \in \TSet$.

Observe that there exists a unique elementary dependence-state encoding for
each elementary dependence map over strategies.

In the next lemma, we show how to handle locally the strategy
quantifications on each state of the model, by simply using a quantification
over actions, which is modeled by the choice of an action dependence map.
Intuitively, we guess in the labeling what is the right part of the
dependence map over strategies for each node of the tree and then verify
that, for all assignments of universal variables, the corresponding complete
assignment satisfies the inner formula.

Let $\GName$ be a  and $\qpElm \bpElm \psi$ an  principal
sentence without principal subsentences.
Then, there exists a  $\UName[\qpElm \bpElm \psi | ^{\GName}] \defeq
\TATuple {\SpcSet[ {\AcSet[\GName]} ](\qpElm) \times \StSet[\GName]}
{\StSet[\GName]} {\QSet[\qpElm \bpElm \psi]} {\atFun[\qpElm \bpElm \psi]}
{\qElm[0\qpElm\bpElm\psi]} {\aleph_{\qpElm \bpElm \psi}}$ such that, for
all states $\sElm \in \StSet[\GName]$ and elementary dependence maps over
strategies $\spcFun \in \ESpcSet[ {\StrSet[\GName](\sElm)} ](\qpElm)$, it
holds that $\GName, \spcFun(\asgFun), \sElm \emodels \bpElm \psi$, for all
$\asgFun \in \AsgSet[\GName](\QPAVSet{\qpElm}, \sElm)$, iff $\TName \in
\LangSet(\UName[\qpElm \bpElm \psi | ^{\GName}])$, where $\TName$ is the
elementary dependence-state encoding for $\spcFun$.

By Lemma <ref> of  goal automaton, there is an
$\UName[\bpElm \psi | ^{\GName}] = \TATuple {\ValSet[
{\AcSet[\GName]} ](\free{\bpElm \psi}) \times \StSet[\GName]}
{\StSet[\GName]} {\QSet[\bpElm \psi]} {\atFun[\bpElm \psi]}
{\qElm[0\bpElm\psi]} {\aleph_{\bpElm \psi}}$ such that, for all states
$\sElm \!\in\! \StSet[\GName]$ and assignments $\asgFun \!\in\!
\AsgSet[\GName](\free{\bpElm \psi}, \sElm)$, it holds that $\GName,
\asgFun, \sElm \models \bpElm \psi$ iff $\TName \in \LangSet(\UName[\bpElm
\psi | ^{\GName}])$, where $\TName$ is the assignment-state encoding for

Now, transform $\UName[\bpElm \psi | ^{\GName}]$ into the new 			$\UName[\qpElm \bpElm \psi | ^{\GName}] \defeq \TATuple {\SpcSet[
{\AcSet[\GName]} ](\qpElm) \times \StSet[\GName]} {\StSet[\GName]}
{\QSet[\qpElm \bpElm \psi]} {\atFun[\qpElm \bpElm \psi]}
{\qElm[0\qpElm\bpElm\psi]} {\aleph_{\qpElm \bpElm \psi}}$, with
$\QSet[\qpElm \bpElm \psi] \defeq \QSet[\bpElm \psi]$,
$\qElm[0\qpElm\bpElm\psi] \defeq \qElm[0\bpElm\psi]$, and
$\aleph_{\qpElm \bpElm \psi} \defeq \aleph_{\bpElm \psi}$, which is used
to handle the quantification prefix $\qpElm$ atomically, where the
transition function is defined as follows: $\atFun[\qpElm \bpElm
\psi](\qElm, (\spcFun, \sElm)) \defeq \bigwedge_{\valFun \in \ValSet[
{\AcSet[\GName]} ](\QPAVSet{\qpElm})} \atFun[\bpElm \psi](\qElm,
(\spcFun(\valFun), \sElm))$, for all $\qElm \in \QSet[\qpElm \bpElm \psi]$
and $(\spcFun, \sElm) \in \SpcSet[ {\AcSet[\GName]} ](\qpElm) \times
\StSet[\GName]$.

Intuitively, $\UName[\qpElm \bpElm \psi | ^{\GName}]$ reads an action
dependence map $\spcFun$ on each node of the input tree $\TName$ labeled
with a state $s$ of $\GName$ and simulates the execution of the transition
function $\atFun[\bpElm \psi](\qElm, (\valFun, \sElm))$ of $\UName[\bpElm
\psi | ^{\GName}]$, for each possible valuation $\valFun =
\spcFun(\valFun')$ on $\free{\bpElm \psi}$ obtained from $\spcFun$ by a
universal valuation $\valFun' \in \ValSet[ {\AcSet[\GName]}

It is important to observe that we cannot move the component set $\SpcSet[
{\AcSet[\GName]} ](\qpElm)$ from the input alphabet to the states of
$\UName[\qpElm \bpElm \psi | ^{\GName}]$, by making a related guessing of
the dependence map $\spcFun$ in the transition function, since we have to
ensure that all states in a given node of the tree $\TName$, i.e., in each
track of the original model $\GName$, make the same choice for $\spcFun$.

Finally, it remains to prove that, for all states $\sElm \in
\StSet[\GName]$ and elementary dependence map over strategies $\spcFun \in
\ESpcSet[ {\StrSet[\GName](\sElm)} ](\qpElm)$, it holds that $\GName,
\spcFun(\asgFun), \sElm \emodels \bpElm \psi$, for all $\asgFun \in
\AsgSet[\GName](\QPAVSet{\qpElm}, \sElm)$, iff $\TName \in
\LangSet(\UName[\qpElm \bpElm \psi | ^{\GName}])$, where $\TName$ is the
elementary dependence-state encoding for $\spcFun$.

[Only if].

Suppose that $\GName, \spcFun(\asgFun), \sElm \emodels \bpElm \psi$, for
all $\asgFun \in \AsgSet[\GName](\QPAVSet{\qpElm}, \sElm)$.
Since $\psi$ does not contain principal subsentences, we have that
$\GName, \spcFun(\asgFun), \sElm \models \bpElm \psi$.
So, due to the property of $\UName[\bpElm \psi | ^{\GName}]$, it follows
that there exists an assignment-state encoding $\TName[\asgFun] \in
\LangSet(\UName[\bpElm \psi | ^{\GName}])$, which implies the existence of
an $(\StSet[\GName] \times \QSet[\bpElm \psi])$-tree $\RSet[\asgFun]$ that
is an accepting run for $\UName[\bpElm \psi | ^{\GName}]$ on

At this point, let $\RSet \defeq \bigcup_{\asgFun \in
\AsgSet[\GName](\QPAVSet{\qpElm}, \sElm)} \RSet[\asgFun]$ be the union of
all runs.
Then, due to the particular definition of the transition function of
$\UName[\qpElm \bpElm \psi | ^{\GName}]$, it is not hard to see that
$\RSet$ is an accepting run for $\UName[\qpElm \bpElm \psi | ^{\GName}]$
on $\TName$.
Hence, $\TName \in \LangSet(\UName[\qpElm \bpElm \psi | ^{\GName}])$.

Suppose that $\TName \in \LangSet(\UName[\qpElm \bpElm \psi |
Then, there exists an $(\StSet[\GName] \times \QSet[\qpElm \bpElm
\psi])$-tree $\RSet$ that is an accepting run for $\UName[\qpElm \bpElm
\psi | ^{\GName}]$ on $\TName$.

Now, for each $\asgFun \in \AsgSet[\GName](\QPAVSet{\qpElm}, \sElm)$, let
$\RSet[\asgFun]$ be the run for $\UName[\bpElm \psi | ^{\GName}]$ on the
assignment-state encoding $\TName[\asgFun]$ for $\spcFun(\asgFun)$.
Due to the particular definition of the transition function of
$\UName[\qpElm \bpElm \psi | ^{\GName}]$, it is easy to see that
$\RSet[\asgFun] \subseteq \RSet$.
Thus, since $\RSet$ is accepting, we have that $\RSet[\asgFun]$ is
accepting as well.
So, $\TName[\asgFun] \in \LangSet(\UName[\bpElm \psi | ^{\GName}])$.

At this point, due to the property of $\UName[\bpElm \psi | ^{\GName}]$,
it follows that $\GName, \spcFun(\asgFun), \sElm \models \bpElm \psi$.
Now, since $\psi$ does not contain principal subsentences, we have that
$\GName, \spcFun(\asgFun), \sElm \emodels \bpElm \psi$, for all $\asgFun
\in \AsgSet[\GName](\QPAVSet{\qpElm}, \sElm)$.

At this point, we can prove the following theorem that is at the base of the
elementary model-checking procedure for .

Let $\GName$ be a , $\sElm \in \StSet[\GName]$ one of its states, and
$\qpElm \bpElm \psi$ an  principal sentence without principal
Then, there exists an  $\NName[\qpElm \bpElm \psi | ^{\GName,
\sElm}]$ such that $\GName, \emptyfun, \sElm \models \qpElm \bpElm \psi$
iff $\LangSet(\NName[\qpElm \bpElm \psi | ^{\GName, \sElm}]) \neq
\emptyset$.

As in the general case of  sentence automaton, we have to ensure that
the state labeling of nodes of the elementary dependence-state encoding is
coherent with the node itself.

To do this, we apply Theorem <ref> of  direction
projection with distinguished direction $\sElm$ to the 			$\UName[\qpElm \bpElm \psi | ^{\GName}]$ derived by
Lemma <ref> of the  sentence automaton, thus
obtaining the required  $\NName[\qpElm \bpElm \psi | ^{\GName,
\sElm}]$.

[Only if].

Suppose that $\GName, \emptyfun, \sElm \models \qpElm \bpElm \psi$.
By Corollary <ref> of  elementariness, it means that
$\GName, \emptyfun, \sElm \emodels \qpElm \bpElm \psi$.
Then, by Definition <ref> of 			elementary semantics, there exists an elementary dependence map $\spcFun
\in \ESpcSet[ {\StrSet[\GName](\sElm)} ](\qpElm)$ such that $\GName,
\spcFun(\asgFun), \sElm \emodels \bpElm \psi$, for all $\asgFun \in
\AsgSet[\GName](\QPAVSet{\qpElm}, \sElm)$.
Thus, by Lemma <ref>, we have that $\TName \in
\LangSet(\UName[\qpElm \bpElm \psi | ^{\GName}])$, where $\TName$ is the
elementary dependence-state encoding for $\spcFun$.
Hence, by Theorem <ref>, it holds that
$\LangSet(\NName[\qpElm \bpElm \psi | ^{\GName, \sElm}]) \neq \emptyset$.

Suppose that $\LangSet(\NName[\qpElm \bpElm \psi | ^{\GName, \sElm}]) \neq
\emptyset$.
Then, by Theorem <ref>, there exists an $(\SpcSet[
{\AcSet[\GName]} ](\qpElm) \times \StSet[\GName])$-labeled
$\StSet[\GName]$-tree $\TName$ such that $\TName \in
\LangSet(\UName[\qpElm \bpElm \psi | ^{\GName}])$.
Now, it is immediate to see that there is an elementary dependence map
$\spcFun \in \ESpcSet[ {\StrSet[\GName](\sElm)} ](\qpElm)$ for which
$\TName$ is the elementary dependence-state encoding.
Thus, by Lemma <ref>, we have that $\GName,
\spcFun(\asgFun), \sElm \emodels \bpElm \psi$, for all $\asgFun \in
\AsgSet[\GName](\QPAVSet{\qpElm}, \sElm)$.
By Definition <ref> of  elementary
semantics, it holds that $\GName, \emptyfun, \sElm \emodels \qpElm \bpElm
\psi$.
Hence, by Corollary <ref> of  elementariness, it means
that $\GName, \emptyfun, \sElm \models \qpElm \bpElm \psi$.

Finally, we show in the next fundamental theorem the precise complexity of
the model-checking for .

The model-checking problem for  is  w.r.t. the size of the
model and 2 w.r.t. the size of the specification.

By Theorem <ref> of  sentence automaton, to verify
that $\GName, \emptyfun, \sElm \models \qpElm \bpElm \psi$, we simply
calculate the emptiness of the  $\NName[\qpElm \bpElm \psi |
^{\GName, \sElm}]$.

This automaton is obtained by the operation of direction projection on the
$\UName[\qpElm \bpElm \psi | ^{\GName}]$, which is in turn derived
by the  $\UName[\bpElm \psi | ^{\GName}]$.

Now, it is easy to see that the number of states of $\UName[\bpElm \psi |
^{\GName}]$, and consequently of $\UName[\qpElm \bpElm \psi | ^{\GName}]$,
is $2^{\AOmicron{\lng{\psi}}}$.
So, $\NName[\qpElm \bpElm \psi | ^{\GName, \sElm}]$ has
$\card{\StSet[\GName]} \cdot 2^{2^{\AOmicron{\lng{\psi}}}}$ states and
index $2^{\AOmicron{\lng{\psi}}}$.

The emptiness problem for such a kind of automaton with $n$ states and
index $h$ is solvable in time $\AOmicron{n^{h}}$ <cit.>.
Thus, we get that the time complexity of checking whether $\GName,
\emptyfun, \sElm \models \qpElm \bpElm \psi$ is

At this point, since we have to do this verification for each possible
state $\sElm \in \StSet[\GName]$ and principal subsentence $\qpElm \bpElm
\psi \in \psnt{\varphi}$ of the whole  specification $\varphi$, we
derive that the whole bottom-up model-checking procedure requires time

Hence, the membership of the model-checking problem for  in 			w.r.t. the size of the model and 2 w.r.t. the size of the
specification directly follows.

Finally the thesis is proved, by getting the relative lower bounds from
the same problem for  <cit.>.

In this paper, we introduced and studied  as a very powerful logic
formalism to reasoning about strategic behaviors of multi-agent concurrent
In particular, we proved that it subsumes the classical temporal and game
logics not using explicit fix-points.
As one of the main results about , we shown that the relative
model-checking problem is decidable but non-elementary hard.

As further and interesting practical results, we investigated several of its
syntactic fragments.
The most appealing one is , which is obtained by restricting  to deal
with one temporal goal at a time.
Interestingly,  strictly extends , while maintaining all its
positive properties.
In fact, the model-checking problem is 2, hence not harder than the
one for .
Moreover, although for the sake of space it is not reported in this paper, we
shown that it is invariant under bisimulation and decision-unwinding, and
consequently, it has the decision-tree model property.

The main reason why  has all these positive properties is that it
satisfies a special model property, which we name “elementariness”.
Informally, this property asserts that all strategy quantifications in a
sentence can be reduced to a set of quantifications over actions, which turn
out to be easier to handle.
We remark that among all  fragments we investigated,  is the only
one that satisfies this property.

As far as we know,  is the first significant proper extension of 	having an elementary model-checking problem, and even more, with the same
computational complexity.
All these positive aspects make us strongly believe that  is a valid
alternative to  to be used in the field of formal verification for
multi-agent concurrent systems.

As another interesting fragment we investigated in this paper, we recall
This logic allows us to express important game-theoretic properties, such as
Nash equilibrium, which cannot be defined in .
Unfortunately, we do not have an elementary model-checking procedure for it,
neither we can exclude it.
We leave to investigate this as future work.

Last but not least, from a theoretical point of view, we are convinced that
our framework can be used as a unifying basis for logic reasonings about
strategic behaviors in multi-agent scenarios and their relationships.

In particular, it can be used to study variations and extensions of  in
a way similar as it has been done in the literature for .
For example, it could be interesting to investigate memoryful , by
inheriting and extending the “memoryful” concept used for  and 	and investigated in <cit.> and <cit.>, respectively.
Also, we recall that this concept implicitly allows to deal with backwards
temporal modalities.

As another example, it would be interesting to investigate the graded
extension of , in a way similar as it has been done
in <cit.> and <cit.> for  and ,
We recall that graded quantifiers in branching-time temporal logics allow to
count how many equivalent classes of paths satisfy a given property.
This concept in  would further allow the counting of strategies and so
to succinctly check the existence of more than one nonequivalent winning
strategy for a given agent, in one shot.
We hope to lift to graded  questions left open about graded
branching-time temporal logic, such as the precise satisfiability complexity
of graded full computation tree logic <cit.>.

Mathematical Notation

In this short reference appendix, we report the classical mathematical
notation and some common definitions that are used along the whole work.

*Classic objects

We consider $\SetN$ as the set of natural numbers and $\numcc{m}{n}
\defeq \set{ k \in \SetN }{ m \leq k \leq n }$, $\numco{m}{n} \defeq \set{ k
\in \SetN }{ m \leq k < n }$, $\numoc{m}{n} \defeq \set{ k \in \SetN }{ m <
k \leq n }$, and $\numoo{m}{n} \defeq \set{ k \in \SetN }{ m < k < n }$ as
its interval subsets, with $m \in \SetN$ and $n \in \SetNI \defeq
\SetN \cup \{ \omega \}$, where $\omega$ is the numerable infinity,
i.e., the least infinite ordinal.

Given a set $\XSet$ of objects, we denote by $\card{\XSet} \in
\SetNI \cup \{ \infty \}$ the cardinality of $\XSet$, i.e., the
number of its elements, where $\infty$ represents a more than
countable cardinality, and by $\pow{\XSet} \defeq \set{ \YSet }{ \YSet
\subseteq \XSet }$ the powerset of $\XSet$, i.e., the set of all its

By $\RRel \subseteq \XSet \times \YSet$ we denote a relation between
the domain $\dom{\RRel} \defeq \XSet$ and codomain
$\cod{\RRel} \defeq \YSet$, whose range is indicated by $\rng{\RRel}
\defeq \set{ \yElm \in \YSet }{ \exists \xElm \in \XSet .\: (\xElm, \yElm)
\in \RRel }$.

We use $\RRel^{-1} \defeq \set{ (\yElm, \xElm) \in \YSet \times \XSet }{
(\xElm, \yElm) \in \RRel }$ to represent the inverse of $\RRel$

Moreover, by $\SRel \cmp \RRel$, with $\RRel \subseteq \XSet \times \YSet$
and $\SRel \subseteq \YSet \times \ZSet$, we denote the composition
of $\RRel$ with $\SRel$, i.e., the relation $\SRel \cmp \RRel \defeq \set{
(\xElm, \zElm) \in \XSet \times \ZSet }{ \exists \yElm \in \YSet .\: (\xElm,
\yElm) \in \RRel \land (\yElm, \zElm) \in \SRel }$.

We also use $\RRel^{n} \defeq \RRel^{n - 1} \cmp \RRel$, with $n \in
\numco{1}{\omega}\!$, to indicate the $n$-iteration of $\RRel
\subseteq \XSet \times \YSet$, where $\YSet \subseteq \XSet$ and $\RRel^{0}
\defeq \set{ (\yElm, \yElm) }{ \yElm \in \YSet }$ is the identity on
With $\RRel^{+} \defeq \bigcup_{n = 1}^{< \omega} \RRel^{n}$ and $\RRel^{*}
\defeq \RRel^{+} \cup \RRel^{0}$ we denote, respectively, the
transitive and reflexive-transitive closure of $\RRel$.

Finally, for an equivalence relation $\RRel \subseteq \XSet \times
\XSet$ on $\XSet$, we represent with $\class{ \XSet }{ \:\RRel } \defeq
\set{ [\xElm]_{\RRel} }{ \xElm \in \XSet }$, where $[\xElm]_{\RRel} \defeq
\set{ \xElm' \in \XSet }{ (\xElm, \xElm') \in \RRel }$, the quotient
set of $\XSet$ w.r.t. $\RRel$, i.e., the set of all related equivalence
classes $[\cdot]_{\RRel}$.

We use the symbol $\YSet^{\XSet} \subseteq \pow{\XSet \times \YSet}$ to
denote the set of total functions $\fFun$ from $\XSet$ to $\YSet$,
i.e., the relations $\fFun \subseteq \XSet \times \YSet$ such that for all
$\xElm \in \dom{\fFun}$ there is exactly one element $\yElm \in \cod{\fFun}$
such that $(\xElm, \yElm) \in \fFun$.
Often, we write $\fFun : \XSet \to \YSet$ and $\fFun : \XSet \pto \YSet$ to
indicate, respectively, $\fFun \in \YSet^{\XSet}$ and $\fFun \in
\bigcup_{\XSet' \subseteq \XSet} \YSet^{\XSet'}$.
Regarding the latter, note that we consider $\fFun$ as a partial
function from $\XSet$ to $\YSet$, where $\dom{\fFun} \subseteq \XSet$
contains all and only the elements for which $\fFun$ is defined.

Given a set $\ZSet$, by $\fFun[\rst \ZSet] \defeq \fFun \cap (\ZSet \times
\YSet)$ we denote the restriction of $\fFun$ to the set $\XSet \cap
\ZSet$, i.e., the function $\fFun[\rst \ZSet] : \XSet \cap \ZSet \pto \YSet$
such that, for all $\xElm \in \dom{\fFun} \cap \ZSet$, it holds that
$\fFun[\rst \ZSet](\xElm) = \fFun(\xElm)$.
Moreover, with $\emptyfun$ we indicate a generic empty function,
i.e., a function with empty domain.
Note that $\XSet \cap \ZSet = \emptyset$ implies $\fFun[\rst \ZSet] =
\emptyfun$.

Finally, for two partial functions $\fFun, \gFun : \XSet \pto \YSet$, we use
$\fFun \Cup \gFun$ and $\fFun \Cap \gFun$ to represent, respectively, the
union and intersection of these functions defined as follows:
$\dom{\fFun \Cup \gFun} \defeq \dom{\fFun} \cup \dom{\gFun} \setminus \set{
\xElm \in \dom{\fFun} \cap \dom{\gFun} }{ \fFun(\xElm) \neq \gFun(\xElm) }$,
$\dom{\fFun \Cap \gFun} \defeq \set{ \xElm \in \dom{\fFun} \cap \dom{\gFun}
}{ \fFun(\xElm) = \gFun(\xElm) }$, $(\fFun \Cup \gFun)(\xElm) =
\fFun(\xElm)$ for $\xElm \in \dom{\fFun \Cup \gFun} \cap \dom{\fFun}$,
$(\fFun \Cup \gFun)(\xElm) = \gFun(\xElm)$ for $\xElm \in \dom{\fFun \Cup
\gFun} \cap \dom{\gFun}$, and $(\fFun \Cap \gFun)(\xElm) = \fFun(\xElm)$ for
$\xElm \in \dom{\fFun \Cap \gFun}$.

By $\XSet^{n}$, with $n \in \SetN$, we denote the set of all
$n$-tuples of elements from $\XSet$, by $\XSet^{*} \defeq \bigcup_{n
= 0}^{< \omega} \XSet^{n}$ the set of finite words on the
alphabet $\XSet$, by $\XSet^{+} \defeq \XSet^{*} \setminus \{
\epsilon \}$ the set of non-empty words, and by $\XSet^{\omega}$ the
set of infinite words, where, as usual, $\epsilon \in \XSet^{*}$ is
the empty word.

The length of a word $\wElm \in \XSet^{\infty} \defeq \XSet^{*} \cup
\XSet^{\omega}$ is represented with $\card{\wElm} \in \SetNI$.

By $(\wElm)_{i}$ we indicate the $i$-th letter of the finite word
$\wElm \in \XSet^{+}$, with $i \in \numco{0}{\card{\wElm}}$.
Furthermore, by $\fst{\wElm} \defeq (\wElm)_{0}$ (resp., $\lst{\wElm} \defeq
(\wElm)_{\card{\wElm} - 1}$), we denote the first (resp.,
last) letter of $\wElm$.
In addition, by $(\wElm)_{\leq i}$ (resp., $(\wElm)_{> i}$), we indicate the
prefix up to (resp., suffix after) the letter of index $i$ of
$\wElm$, i.e., the finite word built by the first $i + 1$ (resp., last
$\card{\wElm} - i - 1$) letters $(\wElm)_{0}, \ldots, (\wElm)_{i}$ (resp.,
$(\wElm)_{i + 1}, \ldots, (\wElm)_{\card{\wElm} - 1}$).
We also set, $(\wElm)_{< 0} \defeq \epsilon$, $(\wElm)_{< i} \defeq
(\wElm)_{\leq i - 1}$, $(\wElm)_{\geq 0} \defeq \wElm$, and $(\wElm)_{\geq
i} \defeq (\wElm)_{> i - 1}$, for $i \in \numco{1}{\card{\wElm}}$.
Mutatis mutandis, the notations of $i$-th letter, first, prefix, and suffix
apply to infinite words too.

Finally, by $\pfx{\wElm[1], \wElm[2]} \in \XSet^{\infty}$ we denote the
maximal common prefix of two different words $\wElm[1], \wElm[2] \in
\XSet^{\infty}$, i.e., the finite word $\wElm \in \XSet^{*}$ for which
there are two words $\wElm[1|'], \wElm[2|'] \in \XSet^{\infty}$ such that
$\wElm[1] = \wElm \cdot \wElm[1|']$, $\wElm[2] = \wElm \cdot \wElm[2|']$,
and $\fst{\wElm[1|']} \neq \fst{\wElm[2|']}$.
By convention, we set $\pfx{\wElm, \wElm} \defeq \wElm$.

For a set $\DirSet$ of objects, called directions, a
$\DirSet$-tree is a set $\TSet \subseteq \DirSet^{*}$ closed under
prefix, i.e., if $\tElm \cdot \dElm \in \TSet$, with $\dElm \in \DirSet$,
then also $\tElm \in \TSet$.

We say that it is complete if it holds that $\tElm \cdot \dElm' \in
\TSet$ whenever $\tElm \cdot \dElm \in \TSet$, for all $\dElm' < \dElm$,
where $< \: \subseteq \DirSet \times \DirSet$ is an a priori fixed strict
total order on the set of directions that is clear from the context.
Moreover, it is full if $\TSet = \DirSet^{*}$.

The elements of $\TSet$ are called nodes and the empty word
$\epsilon$ is the root of $\TSet$.
For every $\tElm \in \TSet$ and $\dElm \in \DirSet$, the node $\tElm \cdot
\dElm \in \TSet$ is a successor of $\tElm$ in $\TSet$.

The tree is $b$-bounded if the maximal number $b$ of its successor
nodes is finite, i.e., $b = \max_{\tElm \in \TSet} \card{\set{ \tElm \cdot
\dElm \in \TSet }{ \dElm \in \DirSet }} < \omega$.

A branch of the tree is an infinite word $\wElm \in \DirSet^{\omega}$
such that $(\wElm)_{\leq i} \in \TSet$, for all $i \in \SetN$.

For a finite set $\LabSet$ of objects, called symbols, a
$\LabSet$-labeled $\DirSet$-tree is a quadruple
$\LTDef{\LabSet}{\DirSet}$, where $\TSet$ is a $\DirSet$-tree and $\vFun :
\TSet \to \LabSet$ is a labeling function.
When $\DirSet$ and $\LabSet$ are clear from the context, we call $\LTStruct$
simply a (labeled) tree.

Proofs of Section <ref>

In this appendix, we report the proofs of lemmas needed to prove the
elementariness of .

Before this, we describe two relevant properties that link together dependence
maps of a given quantification prefix with those of the dual one.
These properties report, in the dependence maps framework, what is known to
hold, in an equivalent way, for first and second order logic.
In particular, they result to be two key points towards a complete
understanding of the strategy quantifications of our logic.

The first of these properties enlighten the fact that two arbitrary dual
dependence maps $\spcFun$ and $\dual{\spcFun}$ always share a common valuation
To better understand this concept, consider for instance the functions
$\spcFun[1]$ and $\dual[6]{\spcFun}$ of the examples illustrated just after
Definition <ref> of dependence maps.
Then, it is easy to see that the valuation $\valFun \in
\ValSet[\DSet](\VSet)$ with $\valFun(\xSym) = \valFun(\ySym) = 1$ and
$\valFun(\zSym) = 0$ resides in both the ranges of $\spcFun[1]$ and
$\dual[6]{\spcFun}$, i.e., $\valFun \in \rng{\spcFun[1]} \cap
\rng{\dual[6]{\spcFun}}$.

Let $\qpElm \in \QPSet(\VSet)$ be a quantification prefix over a set of
variables $\VSet \subseteq \VarSet$ and $\DSet$ a generic set.
Moreover, let $\spcFun \in \SpcSet[\DSet](\qpElm)$ and $\dual{\spcFun} \in
\SpcSet[\DSet](\dual{\qpElm})$ be two dependence maps.
Then, there exists a valuation $\valFun \in \ValSet[\DSet](\VSet)$ such
that $\valFun = \spcFun(\valFun_{\rst \QPAVSet{\qpElm}}) =
\dual{\spcFun}(\valFun_{\rst \QPAVSet{\dual{\qpElm}}})$.

W.l.o.g., suppose that $\qpElm$ starts with an existential quantifier.
If this is not the case, the dual prefix $\dual{\qpElm}$ necessarily
satisfies the above requirement, so, we can simply shift our reasoning on

The whole proof proceeds by induction on the alternation number
$\alt{\qpElm}$ of $\qpElm$.

As base case, if $\alt{\qpElm} = 0$, we define $\valFun \defeq
\spcFun(\emptyfun)$, since $\QPAVSet{\qpElm} = \emptyset$.
Obviously, it holds that $\valFun = \spcFun(\valFun_{\rst
\QPAVSet{\qpElm}}) = \dual{\spcFun}(\valFun_{\rst
\QPAVSet{\dual{\qpElm}}})$, due to the fact that $\valFun_{\rst
\QPAVSet{\qpElm}} = \emptyfun$ and $\valFun_{\rst
\QPAVSet{\dual{\qpElm}}} = \valFun$.

Now, as inductive case, suppose that the statement is true for all
prefixes $\qpElm' \in \QPSet(\VSet')$ with $\alt{\qpElm'} = n$, where
$\VSet' \subset \VSet$.
Then, we prove that it is true for all prefixes $\qpElm \in \QPSet(\VSet)$
with $\alt{\qpElm} = n + 1$ too.

To do this, we have to uniquely split $\qpElm = \qpElm' \cdot \qpElm''$
into the two prefixes $\qpElm' \in \QPSet(\VSet')$ and $\qpElm'' \in
\QPSet(\VSet \setminus \VSet')$ such that $\alt{\qpElm'} = n$ and
$\alt{\qpElm''} = 0$.

At this point, the following two cases can arise.

* If $n$ is even, it is immediate to see that $\QPEVSet{\qpElm''} =
\emptyset$.
So, consider the dependence maps $\spcFun' \in \SpcSet[\DSet](\qpElm')$
and $\dual{\spcFun'} \in \SpcSet[\DSet](\dual{\qpElm'})$ such that
$\spcFun'(\valFun_{\rst \QPAVSet{\qpElm'}}) = \spcFun(\valFun)_{\rst
\VSet'}$ and $\dual{\spcFun'}(\dual{\valFun}) =
\dual{\spcFun}(\dual{\valFun})_{\rst \VSet'}$, for all valuations
$\valFun \in \ValSet[\DSet](\QPAVSet{\qpElm})$ and $\dual{\valFun} \in
\ValSet[\DSet](\QPAVSet{\dual{\qpElm}}) =
\ValSet[\DSet](\QPAVSet{\dual{\qpElm'}})$.
By the inductive hypothesis, there exists a valuation $\valFun' \in
\ValSet[\DSet](\VSet')$ such that $\valFun' = \spcFun'(\valFun'_{\rst
\QPAVSet{\qpElm'}}) = \dual{\spcFun'}(\valFun'_{\rst
\QPAVSet{\dual{\qpElm'}}})$.
So, set $\valFun \defeq \dual{\spcFun}(\valFun'_{\rst
\QPAVSet{\dual{\qpElm}}})$.

* If $n$ is odd, it is immediate to see that $\QPAVSet{\qpElm''} =
\emptyset$.
So, consider the dependence maps $\spcFun' \in \SpcSet[\DSet](\qpElm')$
and $\dual{\spcFun'} \in \SpcSet[\DSet](\dual{\qpElm'})$ such that
$\spcFun'(\valFun) = \spcFun(\valFun)_{\rst \VSet'}$ and
$\dual{\spcFun'}(\dual{\valFun}_{\rst \QPAVSet{\dual{\qpElm'}}}) =
\dual{\spcFun}(\dual{\valFun})_{\rst \VSet'}$, for all valuations
$\valFun \in \ValSet[\DSet](\QPAVSet{\qpElm}) =
\ValSet[\DSet](\QPAVSet{\qpElm'})$ and $\dual{\valFun} \in
\ValSet[\DSet](\QPAVSet{\dual{\qpElm}})$.
By the inductive hypothesis, there exists a valuation $\valFun' \in
\ValSet[\DSet](\VSet')$ such that $\valFun' = \spcFun'(\valFun'_{\rst
\QPAVSet{\qpElm'}}) = \dual{\spcFun'}(\valFun'_{\rst
\QPAVSet{\dual{\qpElm'}}})$.
So, set $\valFun \defeq \spcFun(\valFun'_{\rst
\QPAVSet{\qpElm}})$.

Now, it is easy to see that in both cases the valuation $\valFun$
satisfies the thesis, i.e., $\valFun = \spcFun(\valFun_{\rst
\QPAVSet{\qpElm}}) = \dual{\spcFun}(\valFun_{\rst
\QPAVSet{\dual{\qpElm}}})$.

The second property we are going to prove describes the fact that, if all
dependence maps $\spcFun$ of a given prefix $\qpElm$, for a dependent specific
universal valuation $\valFun$, share a given property then there is a dual
dependence maps $\dual{\spcFun}$ that has the same property, for all universal
valuations $\dual{\valFun}$.
To have a better understanding of this idea, consider again the examples
reported just after Definition <ref> and let $\PSet \defeq \{ (0,
0, 1), (0, 1, 0) \} \subset \ValSet[\DSet](\VSet)$, where the triple $(\lElm,
\mElm, \nElm)$ stands for the valuation that assigns $\lElm$ to $\xSym$,
$\mElm$ to $\ySym$, and $\nElm$ to $\zSym$.
Then, it is easy to see that all ranges of the dependence maps $\spcFun[i]$
for $\qpSym$ intersect $\PSet$, i.e., for all $i \in \numcc{0}{3}$, there is
$\valFun \in \ValSet[\DSet](\QPAVSet{\qpSym})$ such that $\spcFun[i](\valFun)
\in \PSet$.
Moreover, consider the dual dependence maps $\dual[2]{\spcFun}$ for
Then, it is not hard to see that $\dual[2]{\spcFun}(\dual{\valFun}) \in
\PSet$, for all $\dual{\valFun} \in
\ValSet[\DSet](\QPAVSet{\dual{\qpSym}})$.

Let $\qpElm \in \QPSet(\VSet)$ be a quantification prefix over a set of
variables $\VSet \subseteq \VarSet$, $\DSet$ a generic set, and $\PSet
\subseteq \ValSet[\DSet](\VSet)$ a set of valuations of $\VSet$ over
Moreover, suppose that, for all dependence maps $\spcFun \in
\SpcSet[\DSet](\qpElm)$, there is a valuation $\valFun \in
\ValSet[\DSet](\QPAVSet{\qpElm})$ such that $\spcFun(\valFun) \in \PSet$.
Then, there exists a dependence map $\dual{\spcFun} \in
\SpcSet[\DSet](\dual{\qpElm})$ such that, for all valuations
$\dual{\valFun} \in \ValSet[\DSet](\QPAVSet{\dual{\qpElm}})$, it holds
that $\dual{\spcFun}(\dual{\valFun}) \in \PSet$.

The proof easily proceeds by induction on the length of the prefix

As base case, when $\card{\qpElm} = 0$, we have that
$\SpcSet[\DSet](\qpElm) = \SpcSet[\DSet](\dual{\qpElm}) = \{ \emptyfun
\}$, i.e., the only possible dependence maps is the empty function, which
means that the statement is vacuously verified.

As inductive case, we have to distinguish between two cases, as follows.

* $\qpElm = \EExs{\xElm} \cdot \qpElm'$.

As first thing, note that $\QPAVSet{\qpElm} = \QPAVSet{\qpElm'}$ and,
for all elements $\eElm \in \DSet$, consider the projection
$\PSet[\eElm] \defeq \set{ \valFun' \in
\ValSet[\DSet](\QPVSet(\qpElm'))}{ \valFun'[\xElm \mapsto \eElm] \in
\PSet }$ of $\PSet$ on	the variable $\xElm$ with value $\eElm$.

Then, by hypothesis, we can derive that, for all $\eElm \in \DSet$ and
$\spcFun' \in \SpcSet[\DSet](\qpElm')$, there exists $\valFun' \in
\ValSet[\DSet](\QPAVSet{\qpElm'})$ such that $\spcFun'(\valFun') \in
\PSet[\eElm]$.

Indeed, let $\eElm \in \DSet$ and $\spcFun' \in
\SpcSet[\DSet](\qpElm')$, and build the function $\spcFun :
\ValSet[\DSet](\QPAVSet{\qpElm}) \to \ValSet[\DSet](\VSet)$ given by
$\spcFun(\valFun') \defeq \spcFun'(\valFun')[\xElm \mapsto \eElm]$,
for all $\valFun' \in \ValSet[\DSet](\QPAVSet{\qpElm}) =
\ValSet[\DSet](\QPAVSet{\qpElm'})$.
It is immediate to see that $\spcFun \in \SpcSet[\DSet](\qpElm)$.
So, by the hypothesis, there is $\valFun' \in
\ValSet[\DSet](\QPAVSet{\qpElm})$ such that $\spcFun(\valFun') \in
\PSet$, which implies $\spcFun'(\valFun')[\xElm \mapsto \eElm] \in
\PSet$, and so, $\spcFun'(\valFun') \in	\PSet[\eElm]$.

Now, by the inductive hypothesis, for all elements $\eElm \in \DSet$,
there exists $\dual[\eElm]{\spcFun'} \in
\SpcSet[\DSet](\dual{\qpElm'})$ such that, for all	$\dual{\valFun'}
\in \ValSet[\DSet](\QPAVSet{\dual{\qpElm'}})$, it holds that
$\dual[\eElm]{\spcFun'}(\dual{\valFun'}) \in \PSet[\eElm]$, i.e.,
$\dual[\eElm]{\spcFun'}(\dual{\valFun'})[\xElm \mapsto \eElm] \in
\PSet$.

At this point, consider the function $\dual{\spcFun} :
\ValSet[\DSet](\QPAVSet{\dual{\qpElm}}) \to \ValSet[\DSet](\VSet)$
given by $\dual{\spcFun}(\dual{\valFun}) \defeq
\dual[{\dual{\valFun}(\xElm)}]{\spcFun'}(\dual{\valFun}_{\rst
\QPAVSet{\dual{\qpElm'}}})[\xElm \mapsto \dual{\valFun}(\xElm)]$,
for all $\dual{\valFun} \in
\ValSet[\DSet](\QPAVSet{\dual{\qpElm}})$.
Then, it is possible to verify that $\dual{\spcFun} \in
\SpcSet[\DSet](\dual{\qpElm})$.

Indeed, for each $\yElm \in \QPAVSet{\dual{\qpElm}}$ and
$\dual{\valFun} \in \ValSet[\DSet](\QPAVSet{\dual{\qpElm}})$, we
have that $\dual{\spcFun}(\dual{\valFun})(\yElm) =
\dual[{\dual{\valFun}(\xElm)}]{\spcFun'}(\dual{\valFun}_{\rst
\QPAVSet{\dual{\qpElm'}}})[\xElm \mapsto
\dual{\valFun}(\xElm)](\yElm)$.

Now, if $\yElm = \xElm$ then $\dual{\spcFun}(\dual{\valFun})(\yElm)
= \dual{\valFun}(\yElm)$.
Otherwise, since $\dual[\dual{\valFun}(\xElm)]{\spcFun'}$ is a
dependence map, it holds that $\dual{\spcFun}(\dual{\valFun})(\yElm) =
\dual[{\dual{\valFun}(\xElm)}]{\spcFun'}(\dual{\valFun}_{\rst
\QPAVSet{\dual{\qpElm'}}})(\yElm) = \dual{\valFun}_{\rst
\QPAVSet{\dual{\qpElm'}}}(\yElm) = \dual{\valFun}(\yElm)$.
So, Item <ref> of Definition <ref> of
dependence maps is verified.

It only remains to prove Item <ref>.
Let $\yElm \in \QPEVSet{\dual{\qpElm}}$ and $\dual{\valFun[1]},
\dual{\valFun[2]} \in \ValSet[\DSet](\QPAVSet{\dual{\qpElm}})$, with
$\dual{\valFun[1]}_{\rst \QPDepSet(\dual{\qpElm}, \yElm)} =
\dual{\valFun[2]}_{\rst \QPDepSet(\dual{\qpElm}, \yElm)}$.
It is immediate to see that $\xElm \in \QPDepSet(\dual{\qpElm},
\yElm)$, so, $\dual{\valFun[1]}(\xElm) = \dual{\valFun[2]}(\xElm)$,
which implies	that $\dual[\dual{\valFun[1]}(\xElm)]{\spcFun'} =
\dual[\dual{\valFun[2]}(\xElm)]{\spcFun'}$.
At this point, again for the fact that
$\dual[\dual{\valFun}(\xElm)]{\spcFun'}$ is a dependence map, for each
$\dual{\valFun} \in \ValSet[\DSet](\QPAVSet{\dual{\qpElm}})$, we have
that $\dual[\dual{\valFun[1]}(\xElm)]{\spcFun'}(\dual{\valFun[1]}_{\rst
\QPAVSet{\dual{\qpElm'}}})(\yElm) =
\dual[\dual{\valFun[2]}(\xElm)]{\spcFun'}(\dual{\valFun[2]}_{\rst
\QPAVSet{\dual{\qpElm'}}})(\yElm)$.
Thus, it holds that $\dual{\spcFun}(\dual{\valFun[1]})(\yElm) \!=\!
\dual[\dual{\valFun[1]}(\xElm)]{\spcFun'}(\dual{\valFun[1]}_{\rst
\QPAVSet{\dual{\qpElm'}}})[\xElm \mapsto
\dual{\valFun[1]}(\xElm)](\yElm) =
\dual[\dual{\valFun[2]}(\xElm)]{\spcFun'}(\dual{\valFun[2]}_{\rst
\QPAVSet{\dual{\qpElm'}}})[\xElm \mapsto
\dual{\valFun[2]}(\xElm)](\yElm) =
\dual{\spcFun}(\dual{\valFun[2]})(\yElm)$.

Finally, it is enough to observe that, by construction,
$\dual{\spcFun}(\dual{\valFun}) \in \PSet$, for all $\dual{\valFun} \in
\ValSet[\DSet](\QPAVSet{\dual{\qpElm}})$, since
\QPAVSet{\dual{\qpElm'}}}) \in \PSet[{\dual{\valFun}(\xElm)}]$.
Thus, the thesis holds for this case.

* $\qpElm = \AAll{\xElm} \cdot \qpElm'$.

We first show that there exists $\eElm \in \DSet$ such that, for all
$\spcFun' \in \SpcSet[\DSet](\qpElm')$, there is $\valFun' \in
\ValSet[\DSet](\QPAVSet{\qpElm'})$ for which $\spcFun'(\valFun')
\in \PSet[\eElm]$ holds, where the set $\PSet[\eElm]$ is defined as

To do this, suppose by contradiction that, for all $\eElm \in \DSet$,
there is a $\spcFun[\eElm|'] \in \SpcSet[\DSet](\qpElm')$ such that,
for all $\valFun' \in \ValSet[\DSet](\QPAVSet{\qpElm'})$, it holds
that $\spcFun[\eElm|'](\valFun') \not\in \PSet[\eElm]$.
Also, consider the function $\spcFun :
\ValSet[\DSet](\QPAVSet{\qpElm}) \to \ValSet[\DSet](\VSet)$ given by
$\spcFun(\valFun) \defeq \spcFun[\valFun(\xElm)|'](\valFun_{\rst
\QPAVSet{\qpElm'}})[\xElm \mapsto \valFun(\xElm)]$, for all $\valFun
\in \ValSet[\DSet](\QPAVSet{\qpElm})$.
Then, is possible to verify that $\spcFun \in \SpcSet[\DSet](\qpElm)$.

Indeed, for each $\yElm \in \QPAVSet{\qpElm}$ and $\valFun \in
\ValSet[\DSet](\QPAVSet{\qpElm})$, we have that
$\spcFun(\valFun)(\yElm) = \spcFun[\valFun(\xElm)|'](\valFun_{\rst
\QPAVSet{\qpElm'}})[\xElm \mapsto \valFun(\xElm)](\yElm)$.

Now, if $\yElm = \xElm$ then $\spcFun(\valFun)(\yElm) =
\valFun(\yElm)$.
Otherwise, since $\spcFun[\valFun(\xElm)|']$ is a dependence map, it
holds that $\spcFun(\valFun)(\yElm) =
\spcFun[\valFun(\xElm)|'](\valFun_{\rst \QPAVSet{\qpElm'}})(\yElm) =
\valFun_{\rst \QPAVSet{\qpElm'}}(\yElm) = \valFun(\yElm)$.
So, Item <ref> of Definition <ref> of
dependence maps is verified.

It only remains to prove Item <ref>.
Let $\yElm \in \QPEVSet{\qpElm}$ and $\valFun[1], \valFun[2] \in
\ValSet[\DSet](\QPAVSet{\qpElm})$, with $\valFun[1]_{\rst
\QPDepSet(\qpElm, \yElm)} = \valFun[2]_{\rst \QPDepSet(\qpElm,
\yElm)}$.
It is immediate to see that $\xElm \in \QPDepSet(\qpElm, \yElm)$, so,
$\valFun[1](\xElm) = \valFun[2](\xElm)$, which implies	that
$\spcFun[{\valFun[1](\xElm)}|'] = \spcFun[{\valFun[2](\xElm)}|']$.
At this point, again for the fact that $\spcFun[\valFun(\xElm)|']$ is a
dependence map, for each $\valFun \in \ValSet[\DSet](\QPAVSet{\qpElm})$,
we have that $\spcFun[{\valFun[1](\xElm)}|'](\valFun[1]_{\rst
\QPAVSet{\qpElm'}})(\yElm) =
\spcFun[{\valFun[2](\xElm)}|'](\valFun[2]_{\rst
\QPAVSet{\qpElm'}})(\yElm)$.
Thus, it holds that $\spcFun(\valFun[1])(\yElm) =
\spcFun[{\valFun[1](\xElm)}|'](\valFun[1]_{\rst
\QPAVSet{\qpElm'}})[\xElm \mapsto \valFun[1](\xElm)](\yElm) =
\spcFun[{\valFun[2](\xElm)}|'](\valFun[2]_{\rst
\QPAVSet{\qpElm'}})[\xElm \mapsto \valFun[2](\xElm)](\yElm) =
\spcFun(\valFun[2])(\yElm)$.

Now, by the contradiction hypothesis, we have that $\spcFun(\valFun)
\not\in \PSet$, for all $\valFun \in \ValSet(\QPAVSet{\qpElm})$, since
$\spcFun[\valFun(\xElm)|'](\valFun_{\rst \QPAVSet{\qpElm'}}) \not\in
\PSet[\valFun(\xElm)]$, which is in evident contradiction with the

At this point, by the inductive hypothesis, there exists
$\dual{\spcFun'} \in \SpcSet[\DSet](\dual{\qpElm'})$ such that, for
all $\dual{\valFun'} \in \ValSet[\DSet](\QPAVSet{\dual{\qpElm'}})$, it
holds that $\dual{\spcFun'}(\dual{\valFun'}) \in \PSet[\eElm]$, i.e.,
$\dual{\spcFun'}(\dual{\valFun'})[\xElm \mapsto \eElm] \in \PSet$.

Finally, build the function $\dual{\spcFun} :
\ValSet[\DSet](\QPAVSet{\dual{\qpElm}}) \to \ValSet[\DSet](\VSet)$
given by $\dual{\spcFun}(\dual{\valFun}) \defeq
\dual{\spcFun'}(\dual{\valFun})[\xElm \mapsto \eElm]$, for all
$\dual{\valFun} \in \ValSet[\DSet](\QPAVSet{\dual{\qpElm}}) =
\ValSet[\DSet](\QPAVSet{\dual{\qpElm'}})$.
It is immediate to see that $\dual{\spcFun} \in
\SpcSet[\DSet](\dual{\qpElm})$.
Moreover, for all valuations $\dual{\valFun} \in
\ValSet[\DSet](\QPAVSet{\dual{\qpElm}})$, it holds that
$\dual{\spcFun}(\dual{\valFun}) \in \PSet$.
Thus, the thesis holds for this case too.

Hence, we have done with the proof of the lemma.

At this point, we are able to give the proofs of Lemma <ref> of
adjoint dependence maps, Lemma <ref> of dependence-vs-valuation
duality, and Lemma <ref> of encasement characterization.

Let $\qpElm \in \QPSet(\VSet)$ be a quantification prefix over a set of
variables $\VSet \subseteq \VarSet$, $\DSet$ and $\TSet$ two generic sets,
and $\spcFun : \ValSet[\TSet \to \DSet](\QPAVSet{\qpElm}) \to
\ValSet[\TSet \to \DSet](\VSet)$ and $\adj{\spcFun} : \TSet \to
(\ValSet[\DSet](\QPAVSet{\qpElm}) \to \ValSet[\DSet](\VSet))$ two
functions such that $\adj{\spcFun}$ is the adjoint of $\spcFun$.
Then, $\spcFun \in \SpcSet[\TSet \to \DSet](\qpElm)$ iff, for all $t \in
\TSet$, it holds that $\adj{\spcFun}(t) \in \SpcSet[\DSet](\qpElm)$.

To prove the statement, it is enough to show, separately, that
Items <ref> and <ref> of
Definition <ref> of dependence maps hold for $\spcFun$ if the
$\adj{\spcFun}(\tElm)$ satisfies the same items, for all $\tElm \in \TSet$,
and vice versa.

[Item <ref>, if].

Assume that $\adj{\spcFun}(\tElm)$ satisfies Item <ref>,
for each $\tElm \in \TSet$, i.e., $\adj{\spcFun}(\tElm)(\valFun)_{\rst
\QPAVSet{\qpElm}} = \valFun$, for all $\valFun \in
\ValSet[\DSet](\QPAVSet{\qpElm})$.
Then, we have that $\adj{\spcFun}(\tElm)(\flip{\gFun}(\tElm)) =
\flip{\gFun}(\tElm)$, so,
$\adj{\spcFun}(\tElm)(\flip{\gFun}(\tElm))(\xElm) =
\flip{\gFun}(\tElm)(\xElm)$, for all $\gFun \in \ValSet[\TSet \to
\DSet](\QPAVSet{\qpElm})$ and $\xElm \in \QPAVSet{\qpElm}$.
By hypothesis, we have that $\spcFun(\gFun)(\xElm)(\tElm) =
\adj{\spcFun}(\tElm)(\flip{\gFun}(\tElm))(\xElm)$, thus
$\spcFun(\gFun)(\xElm)(\tElm) = \flip{\gFun}(\tElm)(\xElm) =
\gFun(\xElm)(\tElm)$, which means that $\spcFun(\gFun)_{\rst
\QPAVSet{\qpElm}} = \gFun$, for all $\gFun \in \ValSet[\TSet \to
\DSet](\QPAVSet{\qpElm})$.

[Item <ref>, only if].

Assume now that $\spcFun$ satisfies Item <ref>,
i.e., $\spcFun(\gFun)_{\rst \QPAVSet{\qpElm}} = \gFun$, for all $\gFun \in
\ValSet[\TSet \to \DSet](\QPAVSet{\qpElm})$.
Then, we have that $\spcFun(\gFun)(\xElm)(\tElm) = \gFun(\xElm)(\tElm)$,
for all $\xElm \in \QPAVSet{\qpElm}$ and $\tElm \in \TSet$.
By hypothesis, we have that
$\adj{\spcFun}(\tElm)(\flip{\gFun}(\tElm))(\xElm) =
\spcFun(\gFun)(\xElm)(\tElm)$, so,
$\adj{\spcFun}(\tElm)(\flip{\gFun}(\tElm))(\xElm) = \gFun(\xElm)(\tElm) =
\flip{\gFun}(\tElm)(\xElm)$, which means that
$\adj{\spcFun}(\tElm)(\flip{\gFun}(\tElm))_{\rst \QPAVSet{\qpElm}} =
\flip{\gFun}(\tElm)$.
Now, since for each $\valFun \in \ValSet[\DSet](\QPAVSet{\qpElm})$, there
is an $\gFun \in \ValSet[\TSet \to \DSet](\QPAVSet{\qpElm})$ such that
$\flip{\gFun}(\tElm) = \valFun$, we obtain that
$\adj{\spcFun}(\tElm)(\valFun)_{\rst \QPAVSet{\qpElm}} = \valFun$, for all
$\valFun \in \ValSet[\DSet](\QPAVSet{\qpElm})$ and $\tElm \in \TSet$.

[Item <ref>, if].

Assume that $\adj{\spcFun}(\tElm)$ satisfies Item <ref>,
for each $\tElm \in \TSet$, i.e., $\adj{\spcFun}(\tElm)(\valFun[1])(\xElm)
= \adj{\spcFun}(\tElm)(\valFun[2])(\xElm)$, for all $\valFun[1],
\valFun[2] \in \ValSet[\DSet](\QPAVSet{\qpElm})$ and $\xElm \in
\QPEVSet{\qpElm}$ such that $\valFun[1]_{\rst \QPDepSet(\qpElm, \xElm)} =
\valFun[2]_{\rst \QPDepSet(\qpElm, \xElm)}$.
Then, we have that $\adj{\spcFun}(\tElm)(\flip{\gFun[1]}(\tElm))(\xElm) =
\adj{\spcFun}(\tElm)(\flip{\gFun[2]}(\tElm))(\xElm)$, for all $\gFun[1],
\gFun[2] \in \ValSet[\TSet \to \DSet](\QPAVSet{\qpElm})$ such that
$\gFun[1]_{\rst \QPDepSet(\qpElm, \xElm)} = \gFun[2]_{\rst
\QPDepSet(\qpElm, \xElm)}$.
By hypothesis, we have that $\spcFun(\gFun[1])(\xElm)(\tElm) =
\adj{\spcFun}(\tElm)(\flip{\gFun[1]}(\tElm))(\xElm)$ and
$\adj{\spcFun}(\tElm)(\flip{\gFun[2]}(\tElm))(\xElm) =
\spcFun(\gFun[2])(\xElm)(\tElm)$, thus $\spcFun(\gFun[1])(\xElm)(\tElm) =
\spcFun(\gFun[2])(\xElm)(\tElm)$.
Hence, $\spcFun(\gFun[1])(\xElm) \!=\! \spcFun(\gFun[2])(\xElm)$, for all
$\gFun[1], \gFun[2] \in \ValSet[\TSet \to \DSet](\QPAVSet{\qpElm})$ and
$\xElm \in \QPEVSet{\qpElm}$ such that $\gFun[1]_{\rst \QPDepSet(\qpElm,
\xElm)} = \gFun[2]_{\rst \QPDepSet(\qpElm, \xElm)}$.

[Item <ref>, only if].

Assume that $\spcFun$ satisfies Item <ref>, i.e.,
$\spcFun(\gFun[1])(\xElm) = \spcFun(\gFun[2])(\xElm)$, for all $\gFun[1],
\gFun[2] \in \ValSet[\TSet \to \DSet](\QPAVSet{\qpElm})$ and $\xElm \in
\QPEVSet{\qpElm}$ such that $\gFun[1]_{\rst \QPDepSet(\qpElm, \xElm)} =
\gFun[2]_{\rst \QPDepSet(\qpElm, \xElm)}$.
Then, we have that $\spcFun(\gFun[1])(\xElm)(\tElm) =
\spcFun(\gFun[2])(\xElm)(\tElm)$, for all $\tElm \in \TSet$.
By hypothesis, we have that
$\adj{\spcFun}(\tElm)(\flip{\gFun[1]}(\tElm))(\xElm) \allowbreak =
\spcFun(\gFun[1])(\xElm)(\tElm)$ and $\spcFun(\gFun[2])(\xElm)(\tElm) =
\adj{\spcFun}(\tElm)(\flip{\gFun[2]}(\tElm))(\xElm)$, hence
$\adj{\spcFun}(\tElm)(\flip{\gFun[1]}(\tElm))(\xElm) =
\adj{\spcFun}(\tElm)(\flip{\gFun[2]}(\tElm))(\xElm)$.
Now, since for each $\valFun[1], \valFun[2] \in
\ValSet[\DSet](\QPAVSet{\qpElm})$, with $\valFun[1]_{\rst
\QPDepSet(\qpElm, \xElm)} = \valFun[2]_{\rst \QPDepSet(\qpElm, \xElm)}$,
there are $\gFun[1], \gFun[2] \in \ValSet[\TSet \to
\DSet](\QPAVSet{\qpElm})$ such that $\flip{\gFun[1]}(\tElm) = \valFun[1]$
and $\flip{\gFun[2]}(\tElm) = \valFun[2]$, with $\gFun[1]_{\rst
\QPDepSet(\qpElm, \xElm)} = \gFun[2]_{\rst \QPDepSet(\qpElm, \xElm)}$, we
obtain that $\adj{\spcFun}(\tElm)(\valFun[1])(\xElm) =
\adj{\spcFun}(\tElm)(\valFun[2])(\xElm)$, for all $\valFun[1], \valFun[2]
\in \ValSet[\DSet](\QPAVSet{\qpElm})$ and $\xElm \in \QPEVSet{\qpElm}$
such that $\valFun[1]_{\rst \QPDepSet(\qpElm, \xElm)} = \valFun[2]_{\rst
\QPDepSet(\qpElm, \xElm)}$.

Let $\GName$ be a , $\sElm \in \StSet$ one of its states, $\PSet
\subseteq \PthSet(\sElm)$ a set of paths, $\qpElm \in \QPSet(\VSet)$ a
quantification prefix over a set of variables $\VSet \subseteq \VarSet$,
and $\bpElm \in \BndSet(\VSet)$ a binding.
Then, player even wins the  $\HName(\GName, \sElm, \PSet, \qpElm,
\bpElm)$ iff player odd wins the dual  $\HName(\GName, \sElm,
\PthSet(\sElm) \setminus \PSet, \dual{\qpElm}, \bpElm)$.

Let $\AName$ and $\dual{\AName}$ be, respectively, the two s
$\AName(\GName, \sElm, \qpElm, \bpElm)$ and $\AName(\GName, \sElm,
\dual{\qpElm}, \bpElm)$.
It is easy to observe that $\PosESet[\AName] = \PosESet[\dual{\AName}] =
\TrkSet(\sElm)$.
Moreover, it holds that $\PosOSet[\AName] = \set{ \trkElm \cdot
(\lst{\trkElm}, \spcFun) }{ \trkElm \in \TrkSet(\sElm) \land \spcFun \in
\SpcSet[\AcSet](\qpElm) }$ and $\PosOSet[\dual{\AName}] = \set{ \trkElm
\cdot (\lst{\trkElm}, \dual{\spcFun}) }{ \trkElm \in \TrkSet(\sElm) \land
\dual{\spcFun} \in \SpcSet[\AcSet](\dual{\qpElm}) }$.
We now prove, separately, the two directions of the statement.

[Only if].

Suppose that player even wins the  $\HName(\GName, \sElm, \PSet,
\qpElm, \bpElm)$.
Then, there exists an even scheme $\scheFun \in \SchESet[\AName]$ such
that, for all odd schemes $\schoFun \in \SchOSet[\AName]$, it holds that
$\mtcFun[\AName](\scheFun, \schoFun) \in \PSet$.
Now, to prove that odd wins the dual  $\HName(\GName, \sElm,
\PthSet(\sElm) \setminus \PSet, \dual{\qpElm}, \bpElm)$, we have to show
that there exists an odd scheme $\dual{\schoFun} \in
\SchOSet[\dual{\AName}]$ such that, for all even schemes $\dual{\scheFun}
\in \SchESet[\dual{\AName}]$, it holds that
$\mtcFun[\dual{\AName}](\dual{\scheFun}, \dual{\schoFun}) \in \PSet$.

To do this, let us first consider a function $\zFun :
\SpcSet[\AcSet](\qpElm) \times \SpcSet[\AcSet](\dual{\qpElm}) \to
\ValSet[\AcSet](\VSet)$ such that $\zFun(\spcFun, \dual{\spcFun}) =
\spcFun(\zFun(\spcFun, \dual{\spcFun})_{\rst \QPAVSet{\qpElm}}) =
\dual{\spcFun}(\zFun(\spcFun, \dual{\spcFun})_{\rst
\QPAVSet{\dual{\qpElm}}})$, for all $\spcFun \in \SpcSet[\AcSet](\qpElm)$
and $\dual{\spcFun} \in \SpcSet[\AcSet](\dual{\qpElm})$.
The existence of such a function is ensured by Lemma <ref> on
the dependence incidence.

Now, define the odd scheme $\dual{\schoFun} \in \SchOSet[\dual{\AName}]$
in $\dual{\AName}$ as follows: $\dual{\schoFun}(\trkElm \cdot
(\lst{\trkElm}, \dual{\spcFun})) \defeq \trnFun(\lst{\trkElm}, \allowbreak
\zFun(\spcFun, \dual{\spcFun}) \cmp \bndFun[\bpElm])$, for all $\trkElm
\in \TrkSet(\sElm)$ and $\dual{\spcFun} \in
\SpcSet[\AcSet](\dual{\qpElm})$, where $\spcFun \in
\SpcSet[\AcSet](\qpElm)$ is such that $\scheFun(\trkElm) = (\lst{\trkElm},
\spcFun)$.

Moreover, let $\dual{\scheFun} \in \SchESet[\dual{\AName}]$ be a generic
even scheme in $\dual{\AName}$ and consider the derived odd scheme
$\schoFun \in \SchOSet[\AName]$ in $\AName$ defined as follows:
$\schoFun(\trkElm \cdot (\lst{\trkElm}, \spcFun)) \defeq
\trnFun(\lst{\trkElm}, \zFun(\spcFun, \dual{\spcFun}) \cmp
\bndFun[\bpElm])$, for all $\trkElm \in \TrkSet(\sElm)$ and $\spcFun \in
\SpcSet[\AcSet](\qpElm)$, where $\dual{\spcFun} \in
\SpcSet[\AcSet](\dual{\qpElm})$ is such that $\dual{\scheFun}(\trkElm) =
(\lst{\trkElm}, \dual{\spcFun})$.

At this point, it remains only to prove that $\mtcElm = \dual{\mtcElm}$,
where $\mtcElm \defeq \mtcFun[\AName](\scheFun, \schoFun)$ and
$\dual{\mtcElm} \defeq \mtcFun[\dual{\AName}](\dual{\scheFun},
\dual{\schoFun})$.
To do this, we proceed by induction on the prefixes of the matches, i.e.,
we show that $(\mtcElm)_{\leq i} = (\dual{\mtcElm})_{\leq i}$, for all $i
\in \SetN$.

The base case is immediate by definition of match, since we have that
$(\mtcElm)_{\leq 0} = \sElm = (\dual{\mtcElm})_{\leq 0}$.

Now, as inductive case, suppose that $(\mtcElm)_{\leq i} =
(\dual{\mtcElm})_{\leq i}$, for $i \in \SetN$.
By the definition of match, we have that $(\mtcElm)_{i + 1} =
\schoFun((\mtcElm)_{\leq i} \cdot \scheFun((\mtcElm)_{\leq i}))$ and
$(\dual{\mtcElm})_{i + 1} = \dual{\schoFun}((\dual{\mtcElm})_{\leq i}
\cdot \dual{\scheFun}((\dual{\mtcElm})_{\leq i}))$.
Moreover, by the inductive hypothesis, it follows that
$\schoFun((\mtcElm)_{\leq i} \cdot \scheFun((\mtcElm)_{\leq i})) =
\schoFun((\dual{\mtcElm})_{\leq i} \cdot \scheFun((\dual{\mtcElm})_{\leq
At this point, let $\spcFun \in \SpcSet[\AcSet](\qpElm)$ and
$\dual{\spcFun} \in \SpcSet[\AcSet](\dual{\qpElm})$ be two quantification
dependence maps such that $\scheFun((\dual{\mtcElm})_{\leq i}) =
((\dual{\mtcElm})_{i}, \spcFun)$ and
$\dual{\scheFun}((\dual{\mtcElm})_{\leq i}) = ((\dual{\mtcElm})_{i},
\dual{\spcFun})$.
Consequently, by substituting the values of the even schemes $\scheFun$
and $\dual{\scheFun}$, it holds that $(\mtcElm)_{i + 1} =
\schoFun((\dual{\mtcElm})_{\leq i} \cdot ((\dual{\mtcElm})_{i}, \spcFun))$
and $(\dual{\mtcElm})_{i + 1} = \dual{\schoFun}((\dual{\mtcElm})_{\leq i}
\cdot ((\dual{\mtcElm})_{i}, \dual{\spcFun}))$.
Furthermore, by the definition of the odd schemes $\schoFun$ and
$\dual{\schoFun}$, it follows that $\schoFun((\dual{\mtcElm})_{\leq i}
\cdot ((\dual{\mtcElm})_{i}, \spcFun)) = \trnFun((\dual{\mtcElm})_{i},
\zFun(\spcFun, \dual{\spcFun}) \cmp \bpFun[\bpElm]) =
\dual{\schoFun}((\dual{\mtcElm})_{\leq i} \cdot ((\dual{\mtcElm})_{i},
\dual{\spcFun}))$.
Thus, we have that $(\mtcElm)_{i + 1} = (\dual{\mtcElm})_{i + 1}$, which
implies $(\mtcElm)_{\leq i + 1} = (\dual{\mtcElm})_{\leq i + 1}$.

Suppose that player odd wins the dual  $\HName(\GName, \sElm,
\PthSet(\sElm) \setminus \PSet, \dual{\qpElm}, \bpElm)$.
Then, there exists an odd scheme $\dual{\schoFun} \in
\SchOSet[\dual{\AName}]$ such that, for all even schemes $\dual{\scheFun}
\in \SchESet[\dual{\AName}]$, it holds that
$\mtcFun[\dual{\AName}](\dual{\scheFun}, \dual{\schoFun}) \in \PSet$.
Now, to prove that even wins the  $\HName(\GName, \sElm, \PSet,
\qpElm, \bpElm)$, we have to show that there exists an even scheme
$\scheFun \in \SchESet[\AName]$ such that, for all odd schemes $\schoFun
\in \SchOSet[\AName]$, it holds that $\mtcFun[\AName](\scheFun, \schoFun)
\in \PSet$.

To do this, let us first consider the two functions $\gFun :
\TrkSet(\sElm) \to \pow{\ValSet[\AcSet](\VSet)}$ and $\hFun :
\TrkSet(\sElm) \to \pow{\StSet}$ such that $\gFun(\trkElm) \defeq \set{
\dual{\spcFun}(\dual{\valFun}) }{ \dual{\spcFun} \in
\SpcSet[\AcSet](\dual{\qpElm}) \land \dual{\valFun} \in
\ValSet[\AcSet](\QPAVSet{\dual{\qpElm}}) \land \dual{\schoFun}(\trkElm
\cdot (\lst{\trkElm}, \dual{\spcFun})) = \trnFun(\lst{\trkElm},
\dual{\spcFun}(\dual{\valFun}) \cmp \bndFun[\bpElm]) }$ and
$\hFun(\trkElm) \defeq \set{ \dual{\schoFun}(\trkElm \cdot (\lst{\trkElm},
\dual{\spcFun})) }{ \dual{\spcFun} \in \SpcSet[\AcSet](\dual{\qpElm}) }$,
for all $\trkElm \in \TrkSet(\sElm)$.
Now, it is easy to see that, for each $\trkElm \in \TrkSet(\sElm)$ and
$\dual{\spcFun} \in \SpcSet[\AcSet](\dual{\qpElm})$, there is
$\dual{\valFun} \in \ValSet[\AcSet](\QPAVSet{\dual{\qpElm}})$ such that
$\dual{\spcFun}(\dual{\valFun}) \in \gFun(\trkElm)$.
Consequently, by Lemma <ref> on dependence dualization, for all
$\trkElm \in \TrkSet(\sElm)$, there is $\spcFun[\trkElm] \in
\SpcSet[\AcSet](\qpElm)$ such that, for each $\valFun \in
\ValSet[\AcSet](\QPAVSet{\qpElm})$, it holds that
$\spcFun[\trkElm](\valFun) \in \gFun(\trkElm)$, and so,
$\trnFun(\lst{\trkElm}, \spcFun[\trkElm](\valFun) \cmp \bndFun[\bpElm])
\in \hFun(\trkElm)$.

Now, define the even scheme $\scheFun \in \SchESet[\AName]$ in $\AName$ as
follows: $\scheFun(\trkElm) \defeq (\lst{\trkElm}, \spcFun[\trkElm])$, for
all $\trkElm \in \TrkSet(\sElm)$.

Moreover, let $\schoFun \in \SchESet[\AName]$ be a generic odd scheme in
$\AName$ and consider the derived even scheme $\dual{\scheFun} \in
\SchESet[\dual{\AName}]$ in $\dual{\AName}$ defined as follows:
$\dual{\scheFun}(\trkElm) \defeq (\lst{\trkElm},
\dual[\trkElm]{\spcFun})$, for all $\trkElm \in \TrkSet(\sElm)$, where
$\dual[\trkElm]{\spcFun} \in \SpcSet[\AcSet](\dual{\qpElm})$ is such that
$\schoFun(\trkElm \cdot (\lst{\trkElm}, \spcFun[\trkElm])) =
\dual{\schoFun}(\trkElm \cdot (\lst{\trkElm}, \dual[\trkElm]{\spcFun}))$.
The existence of such a dependence map is ensure by the previous membership
of the successor of $\lst{\trkElm}$ in $\hFun(\trkElm)$.

At this point, it remains only to prove that $\mtcElm = \dual{\mtcElm}$,
where $\mtcElm \defeq \mtcFun[\AName](\scheFun, \schoFun)$ and
$\dual{\mtcElm} \defeq \mtcFun[\dual{\AName}](\dual{\scheFun},
\dual{\schoFun})$.
To do this, we proceed by induction on the prefixes of the matches, i.e.,
we show that $(\mtcElm)_{\leq i} = (\dual{\mtcElm})_{\leq i}$, for all $i
\in \SetN$.

The base case is immediate by definition of match, since we have that
$(\mtcElm)_{\leq 0} = \sElm = (\dual{\mtcElm})_{\leq 0}$.

Now, as inductive case, suppose that $(\mtcElm)_{\leq i} =
(\dual{\mtcElm})_{\leq i}$, for $i \in \SetN$.
By the definition of match, we have that $(\mtcElm)_{i + 1} =
\schoFun((\mtcElm)_{\leq i} \cdot \scheFun((\mtcElm)_{\leq i}))$ and
$(\dual{\mtcElm})_{i + 1} = \dual{\schoFun}((\dual{\mtcElm})_{\leq i}
\cdot \dual{\scheFun}((\dual{\mtcElm})_{\leq i}))$.
Moreover, by the inductive hypothesis, it follows that
$\schoFun((\mtcElm)_{\leq i} \cdot \scheFun((\mtcElm)_{\leq i})) =
\schoFun((\dual{\mtcElm})_{\leq i} \cdot \scheFun((\dual{\mtcElm})_{\leq
Now, by substituting the values of the even schemes $\scheFun$ and
$\dual{\scheFun}$, we have that $(\mtcElm)_{i + 1} =
\schoFun((\dual{\mtcElm})_{\leq i} \cdot ((\dual{\mtcElm})_{i},
\spcFun_{(\dual{\mtcElm})_{\leq i}}))$ and $(\dual{\mtcElm})_{i + 1} =
\dual{\schoFun}((\dual{\mtcElm})_{\leq i} \cdot ((\dual{\mtcElm})_{i},
\dual{\spcFun}_{\dual{\mtcElm}_{\leq i}}))$.
At this point, due to the choice of the dependence map
$\dual{\spcFun}_{(\dual{\mtcElm})_{\leq i}}$, it holds that
$\schoFun((\dual{\mtcElm})_{\leq i} \cdot ((\dual{\mtcElm})_{i},
\spcFun_{(\dual{\mtcElm})_{\leq i}})) =
\dual{\schoFun}((\dual{\mtcElm})_{\leq i} \cdot ((\dual{\mtcElm})_{i},
\dual{\spcFun}_{(\dual{\mtcElm})_{\leq i}}))$.
Thus, we have that $(\mtcElm)_{i + 1} = (\dual{\mtcElm})_{i + 1}$, which
implies $(\mtcElm)_{\leq i + 1} = (\dual{\mtcElm})_{\leq i + 1}$.

Let $\GName$ be a , $\sElm \in \StSet$ one of its states, $\PSet
\subseteq \PthSet(\sElm)$ a set of paths, $\qpElm \in \QPSet(\VSet)$ a
quantification prefix over a set of variables $\VSet \subseteq \VarSet$,
and $\bpElm \in \BndSet(\VSet)$ a binding.
Then, the following hold:

* player even wins $\HName(\GName, \sElm, \PSet, \qpElm, \bpElm)$ iff
$\PSet$ is an encasement w.r.t. $\qpElm$ and $\bpElm$;

* if player odd wins $\HName(\GName, \sElm, \PSet, \qpElm, \bpElm)$ then
$\PSet$ is not an encasement w.r.t. $\qpElm$ and $\bpElm$;

* if $\PSet$ is a Borelian set and it is not an encasement w.r.t.				$\qpElm$ and $\bpElm$ then player odd wins $\HName(\GName, \sElm,
\PSet, \qpElm, \bpElm)$.

[Item <ref>, only if].

Suppose that player even wins the  $\HName(\GName, \sElm, \PSet,
\qpElm, \bpElm)$.
Then, there exists an even scheme $\scheFun \in \SchESet$ such that, for
all odd schemes $\schoFun \in \SchOSet$, it holds that $\mtcFun(\scheFun,
\schoFun) \in \PSet$.
Now, to prove the statement, we have to show that there exists an elementary
dependence map $\spcFun \in \ESpcSet[ {\StrSet(\sElm)} ](\qpElm)$ such that,
for all assignments $\asgFun \in \AsgSet(\QPAVSet{\qpElm}, \sElm)$, it holds
that $\playFun(\spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm) \in \PSet$.

To do this, consider the function $\wFun : \TrkSet(\sElm) \to
\SpcSet[\AcSet](\qpElm)$ constituting the projection of $\scheFun$ on the
second component of its codomain, i.e., for all $\trkElm \in
\TrkSet(\sElm)$, it holds that $\scheFun(\trkElm) = (\lst{\trkElm},
\wFun(\trkElm))$.

By Lemma <ref> on adjoint dependence maps, there exists an
elementary dependence map $\spcFun \in \ESpcSet[ {\StrSet(\sElm)} ](\qpElm)$
for which $\wFun$ is the adjoint, i.e., $\wFun = \adj{\spcFun}$.

Moreover, let $\asgFun \in \AsgSet(\QPAVSet{\qpElm}, \sElm)$ be a generic
assignment and consider the derived odd scheme $\schoFun \in \SchOSet$
defined ad follows: $\schoFun(\trkElm \cdot (\lst{\trkElm},
\spcFun')) = \trnFun(\lst{\trkElm}, \spcFun'(\flip{\asgFun}(\trkElm)) \cmp
\bndFun[\bpElm])$, for all $\trkElm \in \TrkSet(\sElm)$ and $\spcFun' \in
\SpcSet[\AcSet](\qpElm)$.

At this point, it remains only to prove that $\playElm = \mtcElm$, where
$\playElm \defeq \playFun(\spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm)$
and $\mtcElm \defeq \mtcFun(\scheFun, \schoFun)$.
To do this, we proceed by induction on the prefixes of both the play and
the match, i.e., we show that $(\playElm)_{\leq i} = (\mtcElm)_{\leq i}$,
for all $i \in \SetN$.

The base case is immediate by definition, since we have that
$(\playElm)_{\leq 0} = \sElm = (\mtcElm)_{\leq 0}$.

Now, as inductive case, suppose that $(\playElm)_{\leq i} =
(\mtcElm)_{\leq i}$, for $i \in \SetN$.
On one hand, by the definition of match, we have that $(\mtcElm)_{i + 1} =
\schoFun((\mtcElm)_{\leq i} \cdot \scheFun((\mtcElm)_{\leq i}))$, from
which, by substituting the value of the even scheme $\scheFun$, we derive
$(\mtcElm)_{i + 1} = \schoFun((\mtcElm)_{\leq i} \cdot ((\mtcElm)_{i},
\adj{\spcFun}((\mtcElm)_{\leq i})))$.
On the other hand, by the definition of play, we have that $(\pthElm)_{i +
1} = \trnFun((\pthElm)_{i}, \adj{\spcFun}((\pthElm)_{\leq
i})(\flip{\asgFun}((\pthElm)_{\leq i}))\cmp \bpFun[\bpElm])$, from which,
by using the definition of the odd scheme $\schoFun$, we derive
$(\pthElm)_{i + 1} = \schoFun((\pthElm)_{\leq i} \cdot ((\pthElm)_{i},
\adj{\spcFun}((\pthElm)_{\leq i})))$.
Then, by the inductive hypothesis, we have that $(\mtcElm)_{i + 1} =
\schoFun((\mtcElm)_{\leq i} \cdot ((\mtcElm)_{i},
\adj{\spcFun}((\mtcElm)_{\leq i}))) = \schoFun((\pthElm)_{\leq i} \cdot
((\pthElm)_{i}, \adj{\spcFun}((\pthElm)_{\leq i}))) = (\pthElm)_{i + 1}$,
which implies $(\mtcElm)_{\leq i + 1} = (\pthElm)_{\leq i + 1}$.

[Item <ref>, if].

Suppose that $\PSet$ is an encasement w.r.t. $\qpElm$ and $\bpElm$.
Then, there exists an elementary dependence map $\spcFun \in \ESpcSet[
{\StrSet(\sElm)} ](\qpElm)$ such that, for all assignments $\asgFun \in
\AsgSet(\QPAVSet{\qpElm}, \sElm)$, it holds that $\playFun(\spcFun(\asgFun)
\cmp \bndFun[\bpElm], \sElm) \in \PSet$.
Now, to prove the statement, we have to show that there exists an even
scheme $\scheFun \in \SchESet$ such that, for all odd schemes $\schoFun
\in \SchOSet$, it holds that $\mtcFun(\scheFun, \schoFun) \in \PSet$.

To do this, consider the even scheme $\scheFun \in \SchESet$ defined as
follows: $\scheFun(\trkElm) \!\defeq\! (\lst{\trkElm},
\adj{\spcFun}(\trkElm))$, for all $\trkElm \in \TrkSet(\sElm)$.
Observe that, by Lemma <ref> on adjoint dependence maps, the
definition is well-formed.

Moreover, let $\schoFun \in \SchOSet$ be a generic odd scheme and consider
a derived assignment $\asgFun \in \AsgSet(\QPAVSet{\qpElm}, \sElm)$
satisfying the following property: $\flip{\asgFun}(\trkElm) \in \set{
\valFun \in \ValSet[\AcSet](\QPAVSet{\qpElm}) }{ \schoFun(\trkElm \cdot
(\lst{\trkElm}, \adj{\spcFun}(\trkElm))) = \trnFun(\lst{\trkElm},
\adj{\spcFun}(\valFun) \cmp \bndFun[\bpElm]) }$, for all $\trkElm \in
\TrkSet(\sElm)$.

At this point, it remains only to prove that $\playElm = \mtcElm$, where
$\playElm \defeq \playFun(\spcFun(\asgFun) \cmp \bndFun[\bpElm], \sElm)$
and $\mtcElm \defeq \mtcFun(\scheFun, \schoFun)$.
To do this, we proceed by induction on the prefixes of both the play and
the match, i.e., we show that $(\playElm)_{\leq i} = (\mtcElm)_{\leq i}$,
for all $i \in \SetN$.

The base case is immediate by definition, since we have that
$(\playElm)_{\leq 0} = \sElm = (\mtcElm)_{\leq 0}$.

Now, as inductive case, suppose that $(\playElm)_{\leq i} =
(\mtcElm)_{\leq i}$, for $i \in \SetN$.
On one hand, by the definition of match, we have that $(\mtcElm)_{i + 1} =
\schoFun((\mtcElm)_{\leq i} \cdot \scheFun((\mtcElm)_{\leq i}))$, from
which, by the definition of the even scheme $\scheFun$, we derive
$(\mtcElm)_{i + 1} = \schoFun((\mtcElm)_{\leq i} \cdot ((\mtcElm)_{i},
\adj{\spcFun}((\mtcElm)_{\leq i})))$.
On the other hand, by the definition of play, we have that $(\pthElm)_{i +
1} = \trnFun((\pthElm)_{i}, \adj{\spcFun}((\pthElm)_{\leq
i})(\flip{\asgFun}((\pthElm)_{\leq i}))\cmp \bpFun[\bpElm])$, from which,
by the choice of the assignment $\asgFun$, we derive $(\pthElm)_{i + 1} =
\schoFun((\pthElm)_{\leq i} \cdot ((\pthElm)_{i},
\adj{\spcFun}((\pthElm)_{\leq i})))$.
Then, by the inductive hypothesis, we have that $(\mtcElm)_{i + 1} =
\schoFun((\mtcElm)_{\leq i} \cdot ((\mtcElm)_{i},
\adj{\spcFun}((\mtcElm)_{\leq i}))) = \schoFun((\pthElm)_{\leq i} \cdot
((\pthElm)_{i}, \adj{\spcFun}((\pthElm)_{\leq i}))) = (\pthElm)_{i + 1}$,
which implies $(\mtcElm)_{\leq i + 1} = (\pthElm)_{\leq i + 1}$.

[Item <ref>].

If player odd wins the  $\HName(\GName, \sElm, \PSet, \qpElm,
\bpElm)$, we have that player even does not win the same game.
Consequently, by Item <ref>, it holds that $\PSet$ is
not an encasement w.r.t. $\qpElm$ and $\bpElm$.

[Item <ref>].

If $\PSet$ is not an encasement w.r.t. $\qpElm$ and $\bpElm$, by
Item <ref>, we have that player even does not win the
$\HName(\GName, \sElm, \PSet, \qpElm, \bpElm)$.
Now, since $\PSet$ is Borelian, by the determinacy
theorem <cit.>, it holds that player odd wins the same game.

We wish to thank the authors of <cit.> for their helpful comments and
discussions on a preliminary version of the paper.

? 20?? 20?? 20?