This work is partially based on the paper <cit.>, which appeared in

In system design, model checking is a well-established formal method
that allows to automatically check for global system
correctness <cit.>.
In such a framework, in order to check whether a system satisfies a required
property, we describe its structure in a mathematical model (such as
Kripke structures <cit.> or labeled transition
systems <cit.>), specify the property with a formula of a temporal
logic (such as  <cit.>,  <cit.>, or  <cit.>), and
check formally that the model satisfies the formula.
In the last decade, interest has arisen in analyzing the behavior of
individual components or sets of them in systems with several entities.
This interest has started in reactive systems, which are systems that interact
continually with their environments.
In module checking <cit.>, the system is modeled as a module that
interacts with its environment and correctness means that a desired property
holds with respect to all such interactions.

Starting from the study of module checking, researchers have looked for logics
focusing on the strategic behavior of agents in multi-agent
systems <cit.>.
One of the most important development in this field is Alternating-Time
Temporal Logic (, for short), introduced by Alur, Henzinger, and
Kupferman <cit.>.
allows reasoning about strategies of agents with temporal goals.
Formally, it is obtained as a generalization of  in which the path
quantifiers, there exists “$\E$” and for all “$\A$”, are
replaced with strategic modalities of the form “$\EExs{\ASet}$” and
“$\AAll{\ASet}$”, where $\ASet$ is a set of agents (a.k.a.
Strategic modalities over agent sets are used to express cooperation and
competition among them in order to achieve certain goals.
In particular, these modalities express selective quantifications over those
paths that are the result of infinite games between a coalition and its

formulas are interpreted over concurrent game structures (,
for short) <cit.>, which model interacting processes.
Given a  $\GName$ and a set $\ASet$ of agents, the  formula
$\EExs{\ASet} \psi$ is satisfied at a state $\sElm$ of $\GName$ if there is a
set of strategies for agents in $\ASet$ such that, no matter strategies are
executed by agents not in $\ASet$, the resulting outcome of the interaction in
$\GName$ satisfies $\psi$ at $\sElm$.
Thus,  can express properties related to the interaction among
components, while  can only express property of the global system.
As an example, consider	the property “processes $\alpha$ and $\beta$
cooperate to ensure that a system (having more than two processes) never
enters a failure state”.
This can be expressed by the  formula $\EExs{\{ \alpha, \beta \}} \G
\neg \mathit{fail}$, where $\G$ is the classical  temporal operators
, in contrast, cannot express this property <cit.>.
Indeed, it can only assert whether the set of all agents may or may not
prevent the system from entering a failure state.

The price that one has to pay for the greater expressiveness of  is the
increased complexity of model checking.
Indeed, both its model-checking and satisfiability problems are
2 <cit.>.

Despite its powerful expressiveness,  suffers from a strong limitation,
due to the fact that strategies are treated only implicitly, through
modalities that refer to games between competing coalitions.
To overcome this problem, Chatterjee, Henzinger, and Piterman introduced
Strategy Logic (, for short) <cit.>, a logic that treats
strategies in two-player turn-based games as explicit first-order
In , the  formula $\EExs{\{ \alpha \}} \psi$, for a system modeled
by a  with agents $\alpha$ and $\beta$, becomes $\exists \xSym. \forall
\ySym. \psi(\xSym, \ySym)$, i.e., “there exists a player-$\alpha$ strategy
$\xSym$ such that for all player-$\beta$ strategies $\ySym$, the unique
infinite path resulting from the two players following the strategies $\xSym$
and $\ySym$ satisfies the property $\psi$”.
The explicit treatment of strategies in this logic allows to state many
properties not expressible in .
In particular, it is shown in <cit.> that , in the restricted case
of two-agent turn-based games, corresponds to a proper one-alternation
fragment of .
The authors of that work have also shown that the model-checking problem for
is decidable, although only a non-elementary algorithm for it, both in
the size of system and formula, has been provided, leaving as open question
whether an algorithm with a better complexity exists or not.
The complementary question about the decidability of the satisfiability
problem for  was also left open and, as far as we known, it is not
addressed in other papers apart our preliminary work <cit.>.

While the basic idea exploited in <cit.> to quantify over strategies and
then to commit agents explicitly to certain of these strategies turns to be
very powerful and useful <cit.>,  still presents severe
Among the others, it needs to be extended to the more general concurrent
multi-agent setting.
Also, the specific syntax considered there allows only a weak kind of strategy
For example,  does not allow different players to share the same
strategy, suggesting that strategies have yet to become first-class objects in
this logic.
Moreover, an agent cannot change his strategy during a play without forcing
the other to do the same.

These considerations, as well as all questions left open about decision
problems, led us to introduce and investigate a new Strategy
Logic, denoted , as a more general framework than , for explicit
reasoning about strategies in multi-agent concurrent games.

Syntactically,  extends  by means of two strategy quantifiers,
the existential $\EExs{\xElm}$ and the universal $\AAll{\xElm}$, as well as
agent binding $(\aElm, \xElm)$, where $\aElm$ is an agent and $\xElm$ a
Intuitively, these elements can be respectively read as “there exists a
strategy $\xElm$”, “for all strategies $\xElm$”, and “bind
agent $\aElm$ to the strategy associated with $\xElm$”.

For example, in a  with the three agents $\alpha$, $\beta$, $\gamma$, the
previous  formula $\EExs{\{ \alpha, \beta \}} \G \neg \mathit{fail}$ can
be translated in the  formula $\EExs{\xSym} \EExs{\ySym} \AAll{\zSym}
(\alpha, \xSym) (\beta, \ySym) (\gamma, \zSym) (\G \neg \mathit{fail})$.
The variables $\xSym$ and $\ySym$ are used to select two strategies for the
agents $\alpha$ and $\beta$, respectively, while $\zSym$ is used to select one
for the agent $\gamma$ such that their composition, after the binding, results
in a play where $\mathit{fail}$ is never met.
Note that we can also require, by means of an appropriate choice of agent
bindings, that agents $\alpha$ and $\beta$ share the same strategy, using the
formula $\EExs{\xSym} \AAll{\zSym} (\alpha, \xSym) (\beta, \xSym) (\gamma,
\zSym) (\G \neg \mathit{fail})$.
Furthermore, we may vary the structure of the game by changing the way the
quantifiers alternate, as in the formula $\EExs{\xSym} \AAll{\zSym}
\EExs{\ySym} (\alpha, \xSym) (\beta, \ySym) (\alpha, \zSym) (\G \neg
\mathit{fail})$.
In this case, $\xSym$ remains uniform w.r.t. $\zSym$, but $\ySym$ becomes
dependent on it.
Finally, we can change the strategy that one agent uses during the play
without changing those of the other agents, by simply using nested bindings,
as in the formula $\EExs{\xSym} \EExs{\ySym} \AAll{\zSym} \EExs{\wSym}
(\alpha, \xSym) (\beta, \ySym) (\gamma, \zSym) (\G (\gamma, \wSym) \G \neg
\mathit{fail})$.
The last examples intuitively show that  is a extension of both  and

It is worth noting that the pattern of modal quantifications over strategies
and binding to agents can be extended to other linear-time temporal logics
than , such as the linear  <cit.>.
In fact, the use of  here is only a matter of simplicity in presenting
our framework, and changing the embedded temporal logic only involves few
side-changes in proofs and decision procedures.

As one of the main results in this paper about , we show that the
model-checking problem is non-elementarily decidable.
To gain this, we use an automata-theoretic approach <cit.>.
Precisely, we reduce the decision problem for our logic to the emptiness
problem of a suitable alternating parity tree automaton, which is an
alternating tree automaton (see <cit.>, for a survey) along with
a parity acceptance condition <cit.>.
Due to the operations of projection required by the elimination of
quantifications on strategies, which induce at any step an exponential
blow-up, the overall size of the required automaton is non-elementary in the
size of the formula, while it is only polynomial in the size of the model.
Thus, together with the complexity of the automata-nonemptiness calculation,
we obtain that the model checking problem is in , w.r.t. the size of the
model, and , w.r.t. the size of the specification.
Hence, the algorithm we propose is computationally not harder than the best
one known for  and even a non-elementary improvement with respect to
the model.
This fact allows for practical applications of  in the field of system
verification just as those done for the monadic second-order logic on infinite
objects <cit.>.
Moreover, we prove that our problem has a non-elementary lower bound.
Specifically, it is $k$- in the alternation number $k$ of
quantifications in the specification.

The contrast between the high complexity of the model-checking problem for our
logic and the elementary one for  has spurred us to investigate
syntactic fragments of , strictly subsuming , with a better
In particular, by means of these sublogics, we would like to understand why
is computationally more difficult than .

The main fragments we study here are Nested-Goal, Boolean-Goal,
and One-Goal Strategy Logic, respectively denoted by , , and
Note that the last, differently from the first two, was introduced
in <cit.>.
They encompass formulas in a special prenex normal form having nested temporal
goals, Boolean combinations of goals, and a single goal at a time,
For goal we mean an  formula of the type $\bpElm \psi$, where $\bpElm$ is
a binding prefix of the form $(\alpha_{1}, \xElm[1]), \ldots, (\alpha_{n},
\xElm[n])$ containing all the involved agents and $\psi$ is an agent-full
With more detail, the idea behind  is that, when in $\psi$ there is a
quantification over a variable, then there are quantifications of all free
variables contained in the inner subformulas.
So, a subgoal of $\psi$ that has a variable quantified in $\psi$ itself cannot
use other variables quantified out of this formula.
Thus, goals can be only nested or combined with Boolean and temporal
and  further restrict the use of goals.
In particular, in , each temporal formula $\psi$ is prefixed by a
quantification-binding prefix $\qpElm \bpElm$ that quantifies over a tuple of
strategies and binds them to all agents.

As main results about these fragments, we prove that the model-checking
problem for  is 2, thus not harder than the one for .
On the contrary, for , it is both  and  and thus we
enforce the corresponding result for .
Finally, we observe that  includes , while the relative
model-checking problem relies between 2 and .

To achieve all positive results about , we use a fundamental property of
the semantics of this logic, called elementariness, which allows us to
strongly simplify the reasoning about strategies by reducing it to a set of
reasonings about actions.

This intrinsic characteristic of , which unfortunately is not shared by
the other fragments, asserts that, in a determined history of the play, the
value of an existential quantified strategy depends only on the values of
strategies, from which the first depends, on the same history.
This means that, to choose an existential strategy, we do not need to know the
entire structure of universal strategies, as for , but only their values on
the histories of interest.
Technically, to describe this property, we make use of the machinery of
dependence map, which defines a Skolemization procedure for ,
inspired by the one in first order logic.

By means of elementariness, we can modify the  model-checking procedure
via alternating tree automata in such a way that we avoid the projection
operations by using a dedicated automaton that makes an action quantification
for each node of the tree model.
Consequently, the resulting automaton is only exponential in the size of the
formula, independently from its alternation number.
Thus, together with the complexity of the automata-nonemptiness calculation,
we get that the model-checking procedure for  is 2.

Clearly, the elementariness property also holds for , as it is included
in .
In particular, although it has not been explicitly stated, this property is
crucial for most of the results achieved in literature about  by means
of automata (see <cit.>, as an example).

Moreover, we believe that our proof techniques are of independent interest and
applicable to other logics as well.

Related works.

Several works have focused on extensions of  to incorporate more
powerful strategic constructs.
Among them, we recall Alternating-Time  (, for
short) <cit.>, Game Logic (, for short) <cit.>,
Quantified Decision Modality  (qD$\mu$, for
short) <cit.>, Coordination Logic (, for short) <cit.>,
and some extensions of  considered in <cit.>.

and qD$\mu$ are intrinsically different from  (as
well as from  and ) as they are obtained by extending the
propositional $\mu$-calculus <cit.> with strategic modalities.
is similar to qD$\mu$ but with  temporal operators
instead of explicit fixpoint constructors.
is strictly included in , in the case of two-player turn-based
games, but it does not use any explicit treatment of strategies, neither it
does the extensions of  introduced in <cit.>.
In particular, the latter work consider restrictions on the memory for
strategy quantifiers.

Thus, all above logics are different from , which we recall it aims
to be a minimal but powerful logic to reason about strategic behavior in
multi-agent systems.

A very recent generalization of , which results to be expressive but
a proper sublogic of , is also proposed in <cit.>.
In this logic, a quantification over strategies does not reset the
strategies previously quantified but allows to maintain them in a particular
context in order to be reused.
This makes the logic much more expressive than .
On the other hand, as it does not allow agents to share the same strategy,
it is not comparable with the fragments we have considered in this paper.

Finally, we want to remark that our non-elementary hardness proof about the
model-checking problem is inspired by and improves a proof proposed for
their logic and communicated to us <cit.> by the authors
of <cit.>.

Note on <cit.>.

Preliminary results on  appeared in <cit.>.
We presented there a 2 algorithm for the model-checking problem.
The described procedure applies only to the  fragment, as model
checking for full  is non-elementary.

The remaining part of this work is structured as follows.
In Section <ref>, we recall the semantic framework based on
concurrent game structures and introduce syntax and semantics of .
Then, in Section <ref>, we show the non-elementary lower bound
for the model-checking problem.
After this, in Section <ref>, we start the study of few syntactic
and semantic  fragments and introduce the concepts of dependence map and
elementary satisfiability.
Finally, in Section <ref>, we describe the model-checking
automata-theoretic procedures for all  fragments.

Note that, in the accompanying Appendix <ref>, we recall standard
mathematical notation and some basic definitions that are used in the paper.
However, for the sake of a simpler understanding of the technical part, we
make a reminder, by means of footnotes, for each first use of a non trivial
or immediate mathematical concept.

The paper is self contained.
All missing proofs in the main body of the work are reported in appendix.

Strategy Logic

In this section, we introduce Strategy Logic, an extension of the
classic linear-time temporal logic  <cit.> along with the concepts
of strategy quantifications and agent binding.

Our aim is to define a formalism that allows to express strategic plans over
temporal goals in a way that separates the part related to the strategic
reasoning from that concerning the tactical one.
This distinctive feature is achieved by decoupling the instantiation of
strategies, done through the quantifications, from their application by means
of bindings.

Our proposal, on the line marked by its precursor  <cit.>
and differently from classical temporal logics <cit.>, turns in a logic
that is not simply propositional but predicative, since we treat strategies as
a first order concept via the use of agents and variables as explicit
syntactic elements.
This fact let us to write Boolean combinations and nesting of complex
predicates, linked together by some common strategic choice, which may
represent each one a different temporal goal.
However, it is worth noting that the technical approach we follow here is
quite different from that used for the definition of , which is based,
on the syntactic side, on the  formula framework <cit.> and,

The section is organized as follows.
In Subsection <ref>, we recall the definition of concurrent
game structure used to interpret Strategy Logic, whose syntax is introduced in
Subsection <ref>.
Then, in Subsection <ref>, we give, among the others, the
notions of strategy and play, which are finally used, in
Subsection <ref>, to define the semantics of the logic.

Underlying framework

As semantic framework for our logic language, we use a graph-based
model for multi-player games named concurrent game
structure <cit.>.
Intuitively, this mathematical formalism provides a generalization of
Kripke structures <cit.> and labeled transition
systems <cit.>, modeling multi-agent systems viewed as games,
in which players perform concurrent actions chosen strategically as a
function on the history of the play.

A concurrent game structure (, for short) is a tuple
$\GName \defeq \CGSStruct$, where $\APSet$ and $\AgSet$ are finite
non-empty sets of atomic propositions and agents, $\AcSet$
and $\StSet$ are enumerable non-empty sets of actions and
states, $\sElm[0] \in \StSet$ is a designated initial state,
and $\labFun : \StSet \to \pow{\APSet}$ is a labeling function that
maps each state to the set of atomic propositions true in that state.
Let $\DecSet \defeq \AcSet^{\AgSet}$ be the set of decisions, i.e.,
functions from $\AgSet$ to $\AcSet$ representing the choices of an action
for each agent. [In the following, we use both $\XSet \to \YSet$
and $\YSet^{\XSet}$ to denote the set of functions from the domain $\XSet$
to the codomain $\YSet$.]
Then, $\trnFun: \StSet \times \DecSet \to \StSet$ is a transition
function mapping a pair of a state and a decision to a state.

Observe that elements in $\StSet$ are not global states of the system, but
states of the environment in which the agents operate.
Thus, they can be viewed as states of the game, which do not include the
local states of the agents.
From a practical point of view, this means that all agents have perfect
information on the whole game, since local states are not taken into account
in the choice of actions <cit.>.

Observe also that, differently from other similar formalizations, each agent
has the same set of possible executable actions, independently of the
current state and of choices made by other agents.
However, as already reported in literature <cit.>, this simplifying
choice does not result in a limitation of our semantics framework and allow
us to give a simpler and clearer explanation of all formal definitions and
techniques we work on.

From now on, apart from the examples and if not differently stated, all s are defined on the same sets of atomic propositions $\APSet$ and agents
$\AgSet$, so, when we introduce a new structure in our reasonings, we do not
make explicit their definition anymore.

In addition, we use the italic letters $\pElm$, $\aElm$, $\cElm$, and
$\sElm$, possibly with indexes, as meta-variables on, respectively, the
atomic propositions $\pSym, \qSym, \ldots$ in $\APSet$, the agents $\alpha,
\beta, \gamma, \ldots$ in $\AgSet$, the actions $0, 1, \ldots$ in $\AcSet$,
and the states $\sSym, \ldots$ in $\StSet$.

Finally, we use the name of a  as a subscript to extract the components
from its tuple-structure.
Accordingly, if $\GName = \CGSStruct$, we have that $\AcSet[\GName] =
\AcSet$, $\labFun[\GName] = \labFun$, $\sElm[0\GName] = \sSym[0]$, and so
Furthermore, we use the same notational concept to make explicit to which
the set $\DecSet$ of decisions is related to.
Note that,

Now, to get attitude to the introduced semantic framework, let us describe
two running examples of simple concurrent games.

In particular, we start by modeling the paper, rock, and scissor

[Paper, Rock, and Scissor]

Consider the classic two-player concurrent game paper, rock, and
scissor (PRS, for short) as represented in Figure fig:exm:prs,
where a play continues until one of the participants catches the move of
the other.

Vertexes are states of the game and labels on edges represent decisions of
agents or sets of them, where the symbol $*$ is used in place of every
possible action.
In this specific case, since there are only two agents, the pair of
symbols $**$ indicates the whole set $\DecSet$ of decisions.

The agents “Alice” and “Bob” in $\AgSet \defeq \{ \ASym, \BSym \}$
have as possible actions those in the set $\AcSet \defeq \{ \PSym, \RSym,
\SSym \}$, which stand for “paper”, “rock”, and “scissor”,
During the play, the game can stay in one of the three states in $\StSet
\defeq \{ \sSym[i], \sSym[\ASym], \sSym[\BSym] \}$, which represent,
respectively, the waiting moment, named idle, and the two winner
The latter ones are labeled with one of the atomic propositions in $\APSet
\defeq \{ \wSym[\ASym], \wSym[\BSym] \}$, in order to represent who is the
The catch of one action over another is described by the relation $\CRel
\defeq \{ (\PSym, \RSym), (\RSym, \SSym), (\SSym, \PSym) \} \subseteq
\AcSet \times \AcSet$.

We can now define the  $\GName[P\!RS] \defeq \CGSStruct[ { \sSym[i] }
]$ for the PRS game, with the labeling given by $\labFun(\sSym[i]) \defeq
\emptyset$, $\labFun(\sSym[\ASym]) \defeq \{ \wSym[\ASym] \}$, and
$\labFun(\sSym[\BSym]) \defeq \{ \wSym[\BSym] \}$ and the transition
function set as follows, where $\DSet[\ASym] \defeq \set{ \decFun \in
\DecSet[ { \GName[P\!RS] } ] }{ (\decFun(\ASym), \decFun(\BSym)) \in \CRel
}$ and $\DSet[\BSym] \defeq \set{ \decFun \in \DecSet[ { \GName[P\!RS] } ]
}{ (\decFun(\BSym), \decFun(\ASym)) \in \CRel }$ are the sets of winning
decisions for the two agents: if $\sElm = \sSym[i]$ and $\decFun \in
\DSet[\ASym]$ then $\trnFun(\sElm, \decFun) \defeq \sSym[\ASym]$, else if
$\sElm = \sSym[i]$ and $\decFun \in \DSet[\BSym]$ then $\trnFun(\sElm,
\decFun) \defeq \sSym[\BSym]$, otherwise $\trnFun(\sElm, \decFun) \defeq
\sElm$.

Note that, when none of the two agents catches the action of the other,
i.e., the used decision is in $\DSet[i] \defeq \DecSet[ { \GName[P\!RS] }
] \setminus (\DSet[\ASym] \cup \DSet[\BSym])$, the play remains in the
idle state to allow another try, otherwise it is stuck in a winning
position forever.

We now describe a non-classic qualitative version of the well-known
prisoner's dilemma.

[Prisoner's Dilemma]

In the prisoner's dilemma (PD, for short), two accomplices are
interrogated in separated rooms by the police, which offers them the same
If one defects, i.e., testifies for the prosecution against the other,
while the other cooperates, i.e., remains silent, the defector goes free
and the silent accomplice goes to jail.
If both cooperate, they remain free, but will be surely interrogated in
the next future waiting for a defection.
On the other hand, if every one defects, both go to jail.
It is ensured that no one will know about the choice made by the other.

This tricky situation can be modeled by the  $\GName[P\!D] \defeq
\CGSStruct[ {\sSym[i]} ]$ depicted in Figure fig:exm:pd, where the
agents “Accomplice-1” and “Accomplice-2” in $\AgSet \defeq \{
\ASym[1], \ASym[2] \}$ can chose an action in $\AcSet \defeq \{ \CSym,
\DSym \}$, which stand for “cooperation” and “defection”,
There are four states in $\StSet \defeq \{ \sSym[i], \sSym[ {\ASym[1]} ],
\sSym[ {\ASym[2]} ], \sSym[j] \}$.
In the idle state $\sSym[i]$ the agents are waiting for the interrogation,
while $\sSym[j]$ represents the jail for both of them.
The remaining states $\sSym[ {\ASym[1]} ]$ and $\sSym[ {\ASym[2]} ]$
indicate, instead, the situations in which only one of the agents become
definitely free.
To characterize the different meaning of these states, we use the atomic
propositions in $\APSet \defeq \{ \fSym[ {\ASym[1]} ], \fSym[ {\ASym[2]} ]
\}$, which denote who is “free”, by defining the following labeling:
$\labFun(\sSym[i]) \defeq \{ \fSym[ {\ASym[1]} ], \fSym[ {\ASym[2]} ] \}$,
$\labFun(\sSym[ {\ASym[1]} ]) \defeq \{ \fSym[ {\ASym[1]} ] \}$,
$\labFun(\sSym[ {\ASym[2]} ]) \defeq \{ \fSym[ {\ASym[2]} ] \}$, and
$\labFun(\sSym[j]) \defeq \emptyset$.

The transition function $\trnFun$ can be easily deduced by the figure.

Strategy Logic (, for short) syntactically extends  by
means of two strategy quantifiers, the existential $\EExs{\xElm}$ and
the universal $\AAll{\xElm}$, and agent binding $(\aElm, \xElm)$,
where $\aElm$ is an agent and $\xElm$ a variable.
Intuitively, these new elements can be respectively read as “there
exists a strategy $\xElm$”, “for all strategies $\xElm$”, and
“bind agent $\aElm$ to the strategy associated with the variable

The formal syntax of  follows.

formulas are built inductively from the sets of atomic
propositions $\APSet$, variables $\VarSet$, and agents $\AgSet$, by using
the following grammar, where $\pElm \in \APSet$, $\xElm \in \VarSet$, and
$\aElm \in \AgSet$:

$\varphi ::= \pElm \mid \neg \varphi \mid \varphi \wedge \varphi \mid
\varphi \vee \varphi \mid \X \varphi \mid \varphi \:\U \varphi \mid
\varphi \:\R \varphi \mid \EExs{\xElm} \varphi \mid \AAll{\xElm} \varphi
\mid (\aElm, \xElm) \varphi$.

denotes the infinite set of formulas generated by the above rules.

Observe that, by construction,  is a proper syntactic fragment of ,
i.e., $\LTL \subset \SL$.

In order to abbreviate the writing of formulas, we use the boolean values
true $\Tt$ and false $\Ff$ and the well-known temporal operators future $\F
\varphi \defeq \Tt\: \U \varphi$ and globally $\G \varphi \defeq \Ff\: \R
\varphi$.

Moreover, we use the italic letters $\xElm, \yElm, \zElm, \ldots$, possibly
with indexes, as meta-variables on the variables $\xSym, \ySym, \zSym,
\ldots$ in $\VarSet$.

A first classic notation related to the  syntax that we need to
introduce is that of subformula, i.e., a syntactic expression that is
part of an a priori given formula.

By $\mthfun{sub} : \SL \to \pow{\SL}$ we formally denote the function
returning the set of subformulas of an  formula.

For instance, consider $\varphi = \EExs{\xSym} (\alpha, \xSym) (\F \pSym)$.
Then, it is immediate to see that $\sub{\varphi} = \{ \varphi, (\alpha,
\xSym) (\F \pSym), (\F \pSym), \pSym, \Tt \}$.

Normally, predicative logics need the concepts of free and bound
placeholders in order to formally define the meaning of their
The placeholders are used to represent particular positions in syntactic
expressions that have to be highlighted, since they have a crucial role in
the definition of the semantics.

In first order logic, for instance, there is only one type of placeholders,
which is represented by the variables.

In , instead, we have both agents and variables as placeholders, as it
can be noted by its syntax, in order to distinguish between the
quantification of a strategy and its application by an agent.
Consequently, we need a way to differentiate if an agent has an associated
strategy via a variable and if a variable is quantified.
To do this, we use the set of free agents/variables as the subset of
$\AgSet \cup \VarSet$ containing (i) all agents for which there is no
binding after the occurrence of a temporal operator and (ii) all
variables for which there is a binding but no quantifications.

The set of free agents/variables of an  formula is given by the
function $\mthfun{free} : \SL \to \pow{\AgSet \cup \VarSet}$ defined as

$\free{\pElm} \defeq \emptyset$, where $\pElm \in \APSet$;

$\free{\neg \varphi} \defeq \free{\varphi}$;

$\free{\varphi_{1} \Opr \varphi_{2}} \defeq \free{\varphi_{1}} \cup
\free{\varphi_{2}}$, where $\Opr\! \in \{ \wedge, \vee \}$;

$\free{\X \varphi} \defeq \AgSet \cup \free{\varphi}$;

$\free{\varphi_{1} \Opr \varphi_{2}} \defeq \AgSet \cup
\free{\varphi_{1}} \cup \free{\varphi_{2}}$, where $\Opr\! \in \{
\U\!\!, \R\! \}$;

$\free{\Qnt \varphi} \defeq \free{\varphi} \setminus \{ \xElm \}$,
where $\Qnt\! \in \set{ \EExs{\xElm}, \AAll{\xElm} }{ \xElm \in
\VarSet }$;

$\free{(\aElm, \xElm) \varphi} \defeq \free{\varphi}$, if $\aElm
\not\in \free{\varphi}$, where $\aElm \in \AgSet$ and $\xElm \in
\VarSet$;

$\free{(\aElm, \xElm) \varphi} \defeq (\free{\varphi} \setminus \{
\aElm \}) \cup \{ \xElm \}$, if $\aElm \in \free{\varphi}$, where
$\aElm \in \AgSet$ and $\xElm \in \VarSet$.

A formula $\varphi$ without free agents (resp., variables), i.e., with
$\free{\varphi} \cap \AgSet = \emptyset$ (resp., $\free{\varphi} \cap
\VarSet = \emptyset$), is named agent-closed (resp.,
If $\varphi$ is both agent- and variable-closed, it is referred to as a
The function $\mthfun{snt} : \SL \to \pow{\SL}$ returns the set of
subsentences $\snt{\varphi} \defeq \set{ \phi \in \sub{\varphi} }{
\free{\phi} = \emptyset }$ for each  formula $\varphi$.

Observe that, on one hand, free agents are introduced in
Items <ref> and <ref>
and removed in Item <ref>.
On the other hand, free variables are introduced in
Item <ref> and removed in
Item <ref>.

As an example, let $\varphi = \EExs{\xSym} (\alpha, \xSym) (\beta, \ySym)
(\F \pSym)$ be a formula on the agents $\AgSet = \{ \alpha, \beta, \gamma
\}$.
Then, we have $\free{\varphi} = \{ \gamma, \ySym \}$, since $\gamma$ is an
agent without any binding after $\F \pSym$ and $\ySym$ has no quantification
at all.
Consider also the formulas $(\alpha, \zSym) \varphi$ and $(\gamma, \zSym)
\varphi$, where the subformula $\varphi$ is the same as above.
Then, we have $\free{(\alpha, \zSym) \varphi} = \free{\varphi}$ and
$\free{(\gamma, \zSym) \varphi} = \{ \ySym, \zSym \}$, since $\alpha$ is not
free in $\varphi$ but $\gamma$ is, i.e., $\alpha \notin \free{\varphi}$ and
$\gamma \in \free{\varphi}$.
So, $(\gamma, \zSym) \varphi$ is agent-closed while $(\alpha, \zSym)
\varphi$ is not.

Similarly to the case of first order logic, another important concept that
characterizes the syntax of  is that of the alternation number of
quantifiers, i.e., the maximum number of quantifier switches $\EExs{\cdot}
\AAll{\cdot}$, $\AAll{\cdot} \EExs{\cdot}$, $\EExs{\cdot} \neg
\EExs{\cdot}$, or $\AAll{\cdot} \neg \AAll{\cdot}$ that bind a variable in a
subformula that is not a sentence.
The constraint on the kind of subformulas that are considered here means
that, when we evaluate the number of such switches, we consider each
possible subsentence as an atomic proposition, hence, its quantifiers are
not taken into account.
Moreover, it is important to observe that vacuous quantifications, i.e.,
quantifications on variable that are not free in the immediate inner
subformula, need to be not considered at all in the counting of quantifier

This value is crucial when we want to analyze the complexity of the decision
problems of fragments of our logic, since higher alternation can usually
mean higher complexity.

By $\mthfun{alt} : \SL \to \SetN$ we formally denote the function returning
the alternation number of an  formula.
Furthermore, the fragment $\SL[k-\text{alt}] \defeq \set{ \varphi \in \SL }{
\forall \varphi' \in \sub{\varphi} \:.\: \alt{\varphi'} \leq k }$ of ,
for $k \in \SetN$, denotes the subset of formulas having all subformulas
with alternation number bounded by $k$.

For instance, consider the sentence $\varphi = \AAll{\xSym} \EExs{\ySym}
(\alpha, \xSym) (\beta, \ySym) (\F \varphi')$ with $\varphi' = \AAll{\xSym}
\EExs{\ySym} (\alpha, \xSym) (\beta, \ySym) (\X \pSym)$, on the set of
agents $\AgSet = \{ \alpha, \beta \}$.
Then, the alternation number $\alt{\varphi}$ is $1$ and not $3$, as one can
think at a first glance, since $\varphi'$ is a sentence.
Moreover, it holds that $\alt{\varphi'} = 1$.
Hence, $\varphi \in \SL[1-\text{alt}]$.
On the other hand, if we substitute $\varphi'$ with $\varphi'' =
\AAll{\xSym} (\alpha, \xSym) (\X \pSym)$, we have that $\alt{\varphi} = 2$,
since $\varphi''$ is not a sentence.
Thus, it holds that $\varphi \not\in \SL[1-\text{alt}]$ but $\varphi \in
\SL[2-\text{alt}]$.

At this point, in order to practice with the syntax of our logic by
expressing game-theoretic concepts through formulas, we describe two
examples of important properties that are possible to write in , but
neither in  <cit.> nor in .
This is clarified later in the paper.

The first concept we introduce is the well-known deterministic concurrent
multi-player Nash equilibrium for Boolean valued payoffs.

[Nash Equilibrium]

Consider the $n$ agents $\alpha_{1}, \ldots, \alpha_{n}$ of a game, each
of them having, respectively, a possibly different temporal goal described
by one of the  formulas $\psi_{1}, \!\ldots\!, \psi_{n}$.

Then, we can express the existence of a strategy profile $(\xSym[1],
\ldots, \xSym[n])$ that is a Nash equilibrium (NE, for short) for
$\alpha_{1}, \ldots, \alpha_{n}$ w.r.t. $\psi_{1}, \ldots, \psi_{n}$ by
using the [$1$-alt] sentence $\varphi_{\!N\!\!E} \!\defeq\!
\EExs{\xSym[1]} (\alpha_{1}, \xSym[1]) \cdots \EExs{\xSym[n]} (\alpha_{n},
\xSym[n]) \: \psi_{\!N\!\!E}$, where $\psi_{\!N\!\!E} \!\defeq\!
\bigwedge_{i = 1}^{n} (\EExs{\ySym} (\alpha_{i}, \ySym) \psi_{i})
\rightarrow \psi_{i}$ is a variable-closed formula.

Informally, this asserts that every agent $\alpha_{i}$ has $\xSym[i]$ as
one of the best strategy w.r.t. the goal $\psi_{i}$, once all the other
strategies of the remaining agents $\alpha_{j}$, with $j \neq i$, have
been fixed to $\xSym[j]$.
Note that here we are only considering equilibria under deterministic

As in physics, also in game theory an equilibrium is not always stable.
Indeed, there are games like the PD of Example exm:pd having Nash
equilibria that are instable.
One of the simplest concepts of stability that is possible to think is
called stability profile.

[Stability Profile]

Think about the same situation of the above example on NE.
Then, a stability profile (SP, for short) is a strategy profile
$(\xSym[1], \ldots, \xSym[n])$ for $\alpha_{1}, \ldots, \alpha_{n}$
w.r.t. $\psi_{1}, \ldots, \psi_{n}$ such that there is no agent
$\alpha_{i}$ that can choose a different strategy from $\xSym[i]$ without
changing its own payoff and penalizing the payoff of another agent
$\alpha_{j}$, with $j \neq i$.

To represent the existence of such a profile, we can use the [$1$-alt]
sentence $\varphi_{\!S\!P} \defeq \EExs{\xSym[1]} (\alpha_{1}, \xSym[1])
\cdots \EExs{\xSym[n]} (\alpha_{n}, \xSym[n]) \: \psi_{\!S\!P}$, where
$\psi_{\!S\!P} \defeq \bigwedge_{i,j = 1, i \neq j}^{n} \psi_{j}
\rightarrow \AAll{\ySym} ((\psi_{i} \leftrightarrow (\alpha_{i}, \ySym)
\psi_{i}) \rightarrow (\alpha_{i}, \ySym) \psi_{j})$.

Informally, with the $\psi_{\!S\!P}$ subformula, we assert that, if
$\alpha_{j}$ is able to achieve his goal $\psi_{j}$, all strategies
$\ySym$ of $\alpha_{i}$ that left unchanged the payoff related to
$\psi_{i}$, also let $\alpha_{j}$ to maintain his achieved goal.

At this point, it is very easy to ensure the existence of an NE that is
also an SP, by using the [$1$-alt] sentence $\varphi_{\!S\!N\!\!E}
\defeq \EExs{\xSym[1]} (\alpha_{1}, \xSym[1]) \cdots \EExs{\xSym[n]}
(\alpha_{n}, \xSym[n]) \: \psi_{\!S\!P} \wedge \psi_{\!N\!\!E}$.

Basic concepts

Before continuing with the description of our logic, we have to introduce
some basic concepts, regarding a generic , that are at the base of the
semantics formalization.

Remind that a description of used mathematical notation is reported in
Appendix <ref>.

We start with the notions of track and path.

Intuitively, tracks and paths of a  $\GName$ are legal sequences of
reachable states in $\GName$ that can be respectively seen as partial and
complete descriptions of possible outcomes of the game modeled by $\GName$

A track (resp., path) in a  $\GName$ is a finite
(resp., an infinite) sequence of states $\trkElm \in \StSet^{*}$ (resp.,
$\pthElm \in \StSet^{\omega}$) such that, for all $i \in
\numco{0}{\card{\trkElm} - 1}$ (resp., $i \in \SetN$), there exists a
decision $\decFun \in \DecSet$ such that $(\trkElm)_{i + 1} =
\trnFun((\trkElm)_{i}, \decFun)$ (resp., $(\pthElm)_{i + 1} =
\trnFun((\pthElm)_{i}, \decFun)$). [The notation $(\wElm)_{i} \in
\Sigma$ indicates the element of index $i \in
\numco{0}{\card{\wElm}}$ of a non-empty sequence $\wElm \in
\Sigma^{\infty}$.]

A track $\trkElm$ is non-trivial if it has non-zero length, i.e.,
$\card{\trkElm} > 0$ that is $\trkElm \neq \epsilon$. [The
Greek letter $\epsilon$ stands for the empty sequence.]

The set $\TrkSet \subseteq \StSet^{+}$ (resp., $\PthSet \subseteq
\StSet^{\omega}$) contains all non-trivial tracks (resp., paths).
Moreover, $\TrkSet(\sElm) \defeq \set{ \trkElm \in \TrkSet }{
\fst{\trkElm} = \sElm }$ (resp., $\PthSet(\sElm) \defeq \set{ \pthElm \in
\PthSet }{ \fst{\pthElm} = \sElm }$) indicates the subsets of tracks
(resp., paths) starting at a state $\sElm \in \StSet$. [By
$\fst{\wElm} \defeq (\wElm)_{0}$ it is denoted the first element of
a non-empty sequence $\wElm \in \Sigma^{\infty}$.]

For instance, consider the PRS game of Example exm:prs.
Then, $\trkSym = \sSym[i] \cdot \sSym[\ASym] \in \StSet^{+}$ and $\pthSym =
\sSym[i]^{\omega} \in \StSet^{\omega}$ are, respectively, a track and a path
in the  $\GName[P\!RS]$.
Moreover, it holds that $\TrkSet = \sSym[i]^{+} + \sSym[i]^{*} \cdot
(\sSym[\ASym]^{+} + \sSym[\BSym]^{+})$ and $\PthSet = \sSym[i]^{\omega} +
\sSym[i]^{*} \cdot (\sSym[\ASym]^{\omega} + \sSym[\BSym]^{\omega})$.

At this point, we can define the concept of strategy.

Intuitively, a strategy is a scheme for an agent that contains all choices
of actions as a function of the history of the current outcome.
However, observe that here we do not set an a priori connection between a
strategy and an agent, since the same strategy can be used by more than one
agent at the same time.

A strategy in a  $\GName$ is a partial function $\strFun :
\TrkSet \pto \AcSet$ that maps each non-trivial track in its domain to an

For a state $\sElm \in \StSet$, a strategy $\strFun$ is said
$\sElm$-total if it is defined on all tracks starting in $\sElm$,
i.e., $\dom{\strFun} = \TrkSet(\sElm)$.

The set $\StrSet \defeq \TrkSet \pto \AcSet$ (resp., $\StrSet(\sElm)
\defeq \TrkSet(\sElm) \to \AcSet$) contains all (resp., $\sElm$-total)

An example of strategy in the  $\GName[P\!RS]$ is the function
$\strFun[1] \in \StrSet(\sSym[i])$ that maps each track having length
multiple of $3$ to the action $\PSym$, the tracks whose remainder of length
modulo $3$ is $1$ to the action $\RSym$, and the remaining tracks to the
action $\SSym$.
A different strategy is given by the function $\strFun[2] \in
\StrSet(\sSym[i])$ that returns the action $\PSym$, if the tracks ends in
$\sSym[\ASym]$ or $\sSym[\BSym]$ or if its length is neither a second nor a
third power of a positive number, the action $\RSym$, if the length is a
square power, and the action $\SSym$, otherwise.

An important operation on strategies is that of translation along a
given track, which is used to determine which part of a strategy has yet to
be used in the game.

Let $\strFun \in \StrSet$ be a strategy and $\trkElm \in \dom{\strFun}$ a
track in its domain.
Then, $(\strFun)_{\trkElm} \in \StrSet$ denotes the translation of
$\strFun$ along $\trkElm$, i.e., the strategy with
$\dom{(\strFun)_{\trkElm}} \defeq \set{ \trkElm' \in
\TrkSet(\lst{\trkElm}) }{ \trkElm \cdot \trkElm'_{\geq 1} \in
\dom{\strFun} }$ such that $(\strFun)_{\trkElm}(\trkElm') \defeq
\strFun(\trkElm \cdot \trkElm'_{\geq 1})$, for all $\trkElm' \in
\dom{(\strFun)_{\trkElm}}$. [By $\lst{\wElm} \defeq
(\wElm)_{\card{\wElm} - 1}$ it is denoted the last element of a
finite non-empty sequence $\wElm \in \Sigma^{*}$.] [The notation
$(\wElm)_{\geq i} \in \Sigma^{\infty}$ indicates the suffix from
index $i \in \numcc{0}{\card{\wElm}}$ inwards of a non-empty sequence
$\wElm \in \Sigma^{\infty}$.]

Intuitively, the translation $(\strFun)_{\trkElm}$ is the update of the
strategy $\strFun$, once the history of the game becomes $\trkElm$.

It is important to observe that, if $\strFun$ is a $\fst{\trkElm}$-total
strategy then $(\strFun)_{\trkElm}$ is $\lst{\trkElm}$-total.

For instance, consider the two tracks $\trkElm[1] = \sSym[i]^{4} \in
\TrkSet(\sSym[i])$ and $\trkElm[2] = \sSym[i]^{4} \cdot \sSym[\ASym]^{2} \in
\TrkSet(\sSym[i])$ in the  $\GName[P\!RS]$ and the strategy $\strFun[1]
\in \StrSet(\sSym[i])$ previously described.
Then, we have that $(\strFun[1])_{\trkElm[1]} = \strFun[1]$, while
$(\strFun[1])_{\trkElm[2]} \in \StrSet(\sSym[\ASym])$ maps each track having
length multiple of $3$ to the action $\SSym$, each track whose remainder of
length modulo $3$ is $1$ to the action $\PSym$, and the remaining tracks to
the action $\RSym$.

We now introduce the notion of assignment.

Intuitively, an assignment gives a valuation of variables with strategies,
where the latter are used to determine the behavior of agents in the game.
With more detail, as in the case of first order logic, we use this concept
as a technical tool to quantify over strategies associated with variables,
independently of agents to which they are related to.
So, assignments are

An assignment in a  $\GName$ is a partial function $\asgFun :
\VarSet \cup \AgSet \pto \StrSet$ mapping variables and agents in its
domain to a strategy.

An assignment $\asgFun$ is complete if it is defined on all agents,
i.e., $\AgSet \subseteq \dom{\asgFun}$.
For a state $\sElm \in \StSet$, it is said that $\asgFun$ is
$\sElm$-total if all strategies $\asgFun(\lElm)$ are $\sElm$-total,
for $\lElm \in \dom{\asgFun}$.

The set $\AsgSet \defeq \VarSet \cup \AgSet \pto \StrSet$ (resp.,
$\AsgSet(\sElm) \defeq \VarSet \cup \AgSet \pto \StrSet(\sElm)$) contains
all (resp., $\sElm$-total) assignments.
Moreover, $\AsgSet(\XSet) \defeq \XSet \to \StrSet$ (resp.,
$\AsgSet(\XSet, \sElm) \defeq \XSet \to \StrSet(\sElm)$) indicates the
subset of $\XSet$-defined (resp., $\sElm$-total) assignments, i.e.,
(resp., $\sElm$-total) assignments defined on the set $\XSet \subseteq
\VarSet \cup \AgSet$.

As an example of assignment, let us consider the function $\asgFun[1]
\in \AsgSet$ in the  $\GName[P\!RS]$, defined on the set $\{ \ASym,
\xSym \}$, whose values are $\strFun[1]$ on $\ASym$ and $\strFun[2]$ on
$\xSym$, where the strategies $\strFun[1], \strFun[2] \in \StrSet(\sSym[i])$
are those described above.
Another examples is given by the assignment $\asgFun[2] \in \AsgSet$,
defined on the set $\{ \ASym, \BSym \}$, such that $\asgFun[2](\ASym) =
\asgFun[1](\xSym)$ and $\asgFun[2](\BSym) = \asgFun[1](\ASym)$.
Note that both are $\sSym[i]$-total and the latter is also complete while
the former is not.

As in the case of strategies, it is useful to define the operation of
translation along a given track for assignments too.

For a given state $\sElm \in \StSet$, let $\asgFun \in \AsgSet(\sElm)$ be
an $\sElm$-total assignment and $\trkElm \in \TrkSet(\sElm)$ a track.
Then, $(\asgFun)_{\trkElm} \in \AsgSet(\lst{\trkElm})$ denotes the
translation of $\asgFun$ along $\trkElm$, i.e., the
$\lst{\trkElm}$-total assignment, with $\dom{(\asgFun)_{\trkElm}} \defeq
\dom{\asgFun}$, such that $(\asgFun)_{\trkElm}(\lElm) \defeq
(\asgFun(\lElm))_{\trkElm}$, for all $\lElm \in \dom{\asgFun}$.

Intuitively, the translation $(\asgFun)_{\trkElm}$ is the simultaneous
update of all strategies $\asgFun(\lElm)$ defined by the assignment
$\asgFun$, once the history of the game becomes $\trkElm$.

Given an assignment $\asgFun$, an agent or variable $\lElm$, and a strategy
$\strFun$, it is important to define a notation to represent the
redefinition of $\asgFun$, i.e., a new assignment equal to the first
on all elements of its domain but $\lElm$, on which it assumes the value

Let $\asgFun \in \AsgSet$ be an assignment, $\strFun \in \StrSet$ a
strategy and $\lElm \in \VarSet \cup \AgSet$ either an agent or a
Then, $\asgFun[][\lElm \mapsto \strFun] \in \AsgSet$ denotes the new
assignment defined on $\dom{\asgFun[][\lElm \mapsto \strFun]} \defeq
\dom{\asgFun} \cup \{ \lElm \}$ that returns $\strFun$ on $\lElm$ and is
equal to $\asgFun$ on the remaining part of its domain, i.e.,
$\asgFun[][\lElm \mapsto \strFun](\lElm) \defeq \strFun$ and
$\asgFun[][\lElm \mapsto \strFun](\lElm') \defeq \asgFun(\lElm')$, for all
$\lElm' \in \dom{\asgFun} \setminus \{ \lElm \}$.

Intuitively, if we have to add or update a strategy that needs to be bound
by an agent or variable, we can simply take the old assignment and redefine
it by using the above notation.

It is worth to observe that, if $\asgFun$ and $\strFun$ are $\sElm$-total
then $\asgFun[][\lElm \mapsto \strFun]$ is $\sElm$-total too.

Now, we can introduce the concept of play in a game.
Intuitively, a play is the unique outcome of the game determined by all
agent strategies participating to it.

A path $\playElm \in \PthSet(\sElm)$ starting at a state $\sElm \in
\StSet$ is a play w.r.t. a complete $\sElm$-total assignment
$\asgFun \in \AsgSet(\sElm)$ ($(\asgFun, \sElm)$-play, for short)
if, for all $i \in \SetN$, it holds that $(\playElm)_{i + 1} =
\trnFun((\playElm)_{i}, \decFun)$, where $\decFun(\aElm) \defeq
\asgFun(\aElm)((\playElm)_{\leq i})$, for each $\aElm \in
\AgSet$. [The notation $(\wElm)_{\leq i} \in \Sigma^{*}$
indicates the prefix up to index $i \in \numcc{0}{\card{\wElm}}$ of
a non-empty sequence $\wElm \in \Sigma^{\infty}$.]
The partial function $\playFun : \AsgSet \times \StSet \pto \PthSet$, with
$\dom{\playFun} \defeq \set{ (\asgFun, \sElm) }{ \AgSet \subseteq
\dom{\asgFun} \land \asgFun \in \AsgSet(\sElm) \land \sElm \in \StSet }$,
returns the $(\asgFun, \sElm)$-play $\playFun(\asgFun, \sElm) \in
\PthSet(\sElm)$, for all pairs $(\asgFun, \sElm)$ in its domain.

As a last example, consider again the complete $\sSym[i]$-total assignment
$\asgFun[2]$ previously described for the  $\GName[P\!RS]$, which
returns the strategies $\strFun[2]$ and $\strFun[1]$ on the agents $\ASym$
and $\BSym$, respectively.
Then, we have that $\playFun(\asgFun[2], \sSym[i]) = \sSym[i]^{3} \cdot
\sSym[\BSym]^{\omega}$.
This means that the play is won by the agent $\BSym$.

Finally, we give the definition of global translation of a complete
assignment together with a related state, which is used to calculate, at a
certain step of the play, what is the current state and its updated

For a given state $\sElm \in \StSet$ and a complete $\sElm$-total
assignment $\asgFun \in \AsgSet(\sElm)$, the $i$-th global
translation of $(\asgFun, \sElm)$, with $i \in \SetN$, is the pair of a
complete assignment and a state $(\asgFun, \sElm)^{i} \defeq
((\asgFun)_{(\playElm)_{\leq i}}, (\playElm)_{i})$, where $\playElm =
\playFun(\asgFun, \sElm)$.

In order to avoid any ambiguity of interpretation of the described notions,
we may use the name of a  as a subscript of the sets and functions just
introduced to clarify to which structure they are related to, as in the case
of components in the tuple-structure of the  itself.

As already reported at the beginning of this section, just like  and
differently from , the semantics of  is defined w.r.t. concurrent
game structures.

For a  $\GName$, one of its states $\sElm$, and an $\sElm$-total
assignment $\asgFun$ with $\free{\varphi} \subseteq \dom{\asgFun}$, we write
$\GName, \asgFun, \sElm \models \varphi$ to indicate that the formula
$\varphi$ holds at $\sElm$ in $\GName$ under $\asgFun$.

The semantics of  formulas involving the atomic propositions, the
Boolean connectives $\neg$, $\wedge$, and $\vee$, as well as the temporal
operators $\X\!$, $\U\!$, and $\R\!$ is defined as usual in .
The novel part resides in the formalization of the meaning of strategy
quantifications $\EExs{\xElm}$ and $\AAll{\xElm}$ and agent binding $(\aElm,
\xElm)$.

Given a  $\GName$, for all  formulas $\varphi$, states $\sElm \in
\StSet$, and $\sElm$-total assignments $\asgFun \in \AsgSet(\sElm)$ with
$\free{\varphi} \subseteq \dom{\asgFun}$, the modeling relation $\GName,
\asgFun, \sElm \models \varphi$ is inductively defined as follows.

$\GName, \asgFun, \sElm \models \pElm$ if $\pElm \in \labFun(\sElm)$,
with $\pElm \in \APSet$.

For all formulas $\varphi$, $\varphi_{1}$, and $\varphi_{2}$, it holds

$\GName, \asgFun, \sElm \models \neg \varphi$ if not $\GName,
\asgFun, \sElm \models \varphi$, that is $\GName, \asgFun, \sElm
\not\models \varphi$;

$\GName, \asgFun, \sElm \models \varphi_{1} \wedge \varphi_{2}$ if
$\GName, \asgFun, \sElm \models \varphi_{1}$ and $\GName, \asgFun,
\sElm \models \varphi_{2}$;

$\GName, \asgFun, \sElm \models \varphi_{1} \vee \varphi_{2}$ if
$\GName, \asgFun, \sElm \models \varphi_{1}$ or $\GName, \asgFun,
\sElm \models \varphi_{2}$.

For a variable $\xElm \in \VarSet$ and a formula $\varphi$, it holds

$\GName, \asgFun, \sElm \models \EExs{\xElm} \varphi$ if there
exists an $\sElm$-total strategy $\strFun \in \StrSet(\sElm)$ such
that $\GName, \asgFun[][\xElm \mapsto \strFun], \sElm \models
\varphi$;

$\GName, \asgFun, \sElm \models \AAll{\xElm} \varphi$ if for all
$\sElm$-total strategies $\strFun \in \StrSet(\sElm)$ it holds
that $\GName, \asgFun[][\xElm \mapsto \strFun], \sElm \models
\varphi$.

For an agent $\aElm \in \AgSet$, a variable $\xElm \in \VarSet$, and a
formula $\varphi$, it holds that $\GName, \asgFun, \sElm \models
(\aElm, \xElm) \varphi$ if $\GName, \asgFun[][\aElm \mapsto
\asgFun(\xElm)], \sElm \models \varphi$.

Finally, if the assignment $\asgFun$ is also complete, for all
formulas $\varphi$, $\varphi_{1}$, and $\varphi_{2}$, it holds that:

$\GName, \asgFun, \sElm \models \X \varphi$ if $\GName, (\asgFun,
\sElm)^{1} \models \varphi$;

$\GName, \asgFun, \sElm \models \varphi_{1} \U \varphi_{2}$ if
there is an index $i \in \SetN$ with $k \leq i$ such that $\GName,
(\asgFun, \sElm)^{i} \models \varphi_{2}$ and, for all indexes $j
\in \SetN$ with $k \leq j < i$, it holds that $\GName, (\asgFun,
\sElm)^{j} \models \varphi_{1}$;

$\GName, \asgFun, \sElm \models \varphi_{1} \R \varphi_{2}$ if,
for all indexes $i \in \SetN$ with $k \leq i$, it holds that
$\GName, (\asgFun, \sElm)^{i} \models \varphi_{2}$ or there is an
index $j \in \SetN$ with $k \leq j < i$ such that $\GName,
(\asgFun, \sElm)^{j} \models \varphi_{1}$.

Intuitively, at Items <ref>
and <ref>, respectively, we evaluate the existential
$\EExs{\xElm}$ and universal $\AAll{\xElm}$ quantifiers over strategies, by
associating them to the variable $\xElm$.
Moreover, at Item <ref>, by means of an agent binding
$(\aElm, \xElm)$, we commit the agent $\aElm$ to a strategy associated with
the variable $\xElm$.
It is evident that, due to Items <ref>,
<ref>, and <ref>, the
semantics is simply embedded into the  one.

In order to complete the description of the semantics, we now give the
classic notions of model and satisfiability of an 		sentence.

We say that a  $\GName$ is a model of an  sentence
$\varphi$, in symbols $\GName \models \varphi$, if $\GName, \emptyfun,
\sElm[0] \models \varphi$. [The symbol $\emptyfun$ stands for the
empty function.]

In general, we also say that $\GName$ is a model for $\varphi$ on
$\sElm \in \StSet$, in symbols $\GName, \sElm \models \varphi$, if
$\GName, \emptyfun, \sElm \models \varphi$.

An  sentence $\varphi$ is satisfiable if there is a model for

It remains to introduce the concepts of implication and
equivalence between  formulas, which are useful to describe
transformations preserving the meaning of a specification.

Given two  formulas $\varphi_{1}$ and $\varphi_{2}$ with
$\free{\varphi_{1}} = \free{\varphi_{2}}$, we say that $\varphi_{1}$
implies $\varphi_{2}$, in symbols $\varphi_{1} \implies
\varphi_{2}$, if, for all s $\GName$, states $\sElm \in \StSet$, and
$\free{\varphi_{1}}$-defined $\sElm$-total assignments $\asgFun \in
\AsgSet(\free{\varphi_{1}}, \sElm)$, it holds that if $\GName, \asgFun,
\sElm \models \varphi_{1}$ then $\GName, \asgFun, \sElm \models
\varphi_{2}$.
Accordingly, we say that $\varphi_{1}$ is equivalent to
$\varphi_{2}$, in symbols $\varphi_{1} \equiv \varphi_{2}$, if both
$\varphi_{1} \implies \varphi_{2}$ and $\varphi_{2} \implies \varphi_{1}$

In the rest of the paper, especially when we describe a decision procedure,
we may consider formulas in existential normal form (, for
short) and positive normal form (, for short), i.e.,
formulas in which only existential quantifiers appear or in which the
negation is applied only to atomic propositions.
In fact, it is to this aim that we have considered in the syntax of 		both the Boolean connectives $\wedge$ and $\vee$, the temporal operators
$\U\!\!$, and $\R\!\!$, and the strategy quantifiers $\EExs{ \cdot }$ and
$\AAll{ \cdot }$.
Indeed, all formulas can be linearly translated in  by using De
Morgan's laws together with the following equivalences, which directly
follow from the semantics of the logic: $\neg \X \varphi \equiv \X \neg
\varphi$, $\neg (\varphi_{1} \U \varphi_{2}) \equiv (\neg \varphi_{1}) \R
(\neg \varphi_{2})$, $\neg \EExs{x} \varphi \equiv \AAll{x} \neg \varphi$,
and $\neg (\aElm, \xElm) \varphi \equiv (\aElm, \xElm) \neg \varphi$.

At this point, in order to better understand the meaning of our logic, we
discuss two examples in which we describe the evaluation of the semantics of
some formula w.r.t. the a priori given s.

We start by explaining how a strategy can be shared by different agents.

[Shared Variable]

Consider the [$2$-alt] sentence $\varphi = \EExs{\xSym} \AAll{\ySym}
\EExs{\zSym} ((\alpha, \xSym) (\beta, \ySym) (\X \pSym) \wedge (\alpha,
\ySym) (\beta, \zSym) (\X \qSym))$.
It is immediate to note that both agents $\alpha$ and $\beta$ use the
strategy associated with $\ySym$ to achieve simultaneously the 			temporal goals $\X \pSym$ and $\X \qSym$.

A model for $\varphi$ is given by the  $\GName[S\!V] \defeq \CGSTuple
{\{ \pSym, \qSym \}} {\{ \alpha, \beta\}} {\{ 0, 1 \}} {\{ \sSym[0],
\sSym[1], \sSym[2], \sSym[3] \}} {\labFun} {\trnFun} {\sSym[0]}$, where
$\labFun(\sSym[0]) \defeq \emptyset$, $\labFun(\sSym[1]) \defeq \{ \pSym
\}$, $\labFun(\sSym[2]) \defeq \{ \pSym, \qSym \}$, $\labFun(\sSym[3])
\defeq \{ \qSym \}$, $\trnFun(\sSym[0], (0, 0)) \defeq \sSym[1]$,
$\trnFun(\sSym[0], (0, 1)) \defeq \sSym[2]$, $\trnFun(\sSym[0], (1, 0))
\defeq \sSym[3]$, and all the remaining transitions (with any decision) go
to $\sSym[0]$.
In Figure fig:exm:sv, we report a graphical representation of the

Clearly, $\GName[S\!V] \models \varphi$ by letting, on $\sSym[0]$, the
variables $\xSym$ to chose action $0$ (the goal $(\alpha, \xSym) (\beta,
\ySym) (\X \pSym)$ is satisfied for any choice of $\ySym$, since we can
move from $\sSym[0]$ to either $\sSym[1]$ or $\sSym[2]$, both labeled with
$\pSym$) and $\zSym$ to choose action $1$ when $\ySym$ has action $0$ and,
vice versa, $0$ when $\ySym$ has $1$ (in both cases, the goal
$(\alpha, \ySym) (\beta, \zSym) (\X \qSym)$ is satisfied, since one can
move from $\sSym[0]$ to either $\sSym[2]$ or $\sSym[3]$, both labeled with

We now discuss an application of the concepts of Nash equilibrium and
stability profile to both the prisoner's dilemma and the paper, rock, and
scissor game.

[Equilibrium Profiles]

Let us first to consider the  $\GName[P\!D]$ of the prisoner's
dilemma described in the Example exm:pd.

Intuitively, each of the two accomplices $\ASym[1]$ and $\ASym[2]$ want to
avoid the prison.
These goals can be, respectively, represented by the  formulas
$\psi_{\ASym[1]} \defeq \G \fSym[ {\ASym[1]} ]$ and $\psi_{\ASym[2]}
\defeq \G \fSym[ {\ASym[2]} ]$.

The existence of a Nash equilibrium in $\GName[P\!D]$ for the two
accomplices w.r.t. the above goals can be written as $\phi_{\!N\!E}
\defeq \EExs{\xSym[1]} (\ASym[1], \xSym[1]) \EExs{\xSym[2]} (\ASym[2],
\xSym[2]) \: \psi_{\!N\!E}$, where $\psi_{\!N\!E} \defeq ((\EExs{\ySym}
(\ASym[1], \ySym) \psi_{\ASym[1]}) \rightarrow \psi_{\ASym[1]}) \wedge
((\EExs{\ySym} (\ASym[2], \ySym) \psi_{\ASym[2]}) \rightarrow
\psi_{\ASym[2]})$, which results to be an instantiation of the general
sentence $\varphi_{\!N\!E}$ of Example exm:ne.

In the same way, the existence of a stable Nash equilibrium can be
represented with the sentence $\phi_{\!S\!N\!\!E} \defeq \EExs{\xSym[1]}
(\ASym[1], \xSym[1]) \EExs{\xSym[2]} (\ASym[2], \xSym[2]) \: \psi_{\!N\!E}
\wedge \psi_{\!S\!P}$, where $\psi_{\!S\!P} \defeq (\psi_{1} \rightarrow
\AAll{\ySym} ((\psi_{2} \leftrightarrow (\ASym[2], \ySym) \psi_{2})
\rightarrow (\ASym[2], \ySym) \psi_{1})) \wedge (\psi_{2} \rightarrow
\AAll{\ySym} ((\psi_{1} \leftrightarrow (\ASym[1], \ySym) \psi_{1})
\rightarrow (\ASym[1], \ySym) \psi_{2}))$, which is a particular case of
the sentence $\varphi_{\!S\!N\!\!E}$ of Example exm:sp.

Now, it is easy to see that $\GName[P\!D] \models \phi_{\!S\!N\!E}$ and,
so, $\GName[P\!D] \models \phi_{\!N\!E}$.
Indeed, an assignment $\asgFun \in \AsgSet[ {\GName[P\!D]} ](\AgSet,
\sSym[i])$, for which $\asgFun(\ASym[1])(\sSym[i]) =
\asgFun(\ASym[2])(\sSym[i]) = \DSym$, is a stable equilibrium profile,
i.e., it is such that $\GName[P\!D], \asgFun, \sSym[i] \models
\psi_{\!N\!E} \wedge \psi_{\!S\!P}$.
This is due to the fact that, if an agent $\ASym[k]$, for $k \in \{ 1, 2
\}$, choses another strategy $\strFun \in \StrSet[ {\GName[P\!D]}
](\sSym[i])$, he is still unable to achieve his goal $\psi_{k}$, i.e.,
$\GName[P\!D], \asgFun[][\ASym[k] \mapsto \strFun], \sSym[i] \not\models
\psi_{k}$, so, he cannot improve his payoff.
Moreover, this equilibrium is stable, since the payoff of an agent cannot
be made worse by the changing of the strategy of the other agent.

However, it is interesting to note that there are instable equilibria too.
One of these is represented by the assignment $\asgFun' \in \AsgSet[
{\GName[P\!D]} ](\AgSet, \sSym[i])$, for which
$\asgFun'(\ASym[1])(\sSym[i]^{j}) = \asgFun'(\ASym[2])(\sSym[i]^{j}) =
\CSym$, for all $j \in \SetN$.
Indeed, we have that $\GName[P\!D], \asgFun', \sSym[i] \models
\psi_{\!N\!E}$, since $\GName[P\!D], \asgFun', \sSym[i] \models \psi_{1}$
and $\GName[P\!D], \asgFun', \sSym[i] \models \psi_{2}$, but
$\GName[P\!D], \asgFun', \sSym[i] \not\models \psi_{\!S\!P}$.
The latter property holds because, if one of the agents $\ASym[k]$, for $k
\in \{ 1, 2 \}$, choses a different strategy $\strFun' \in \StrSet[
{\GName[P\!D]} ](\sSym[i])$ for which there is a $j \in \SetN$ such that
$\strFun'(\sSym[i]^{j}) = \DSym$, he cannot improve his payoff but makes
surely worse the payoff of the other agent, i.e., $\GName[P\!D],
\asgFun'[\ASym[k] \mapsto \strFun'], \sSym[i] \models \psi_{k}$ but
$\GName[P\!D], \asgFun'[\ASym[k] \mapsto \strFun'], \sSym[i] \not\models
\psi_{3 - k}$.

Finally, consider the  $\GName[P\!RS]$ of the paper, rock, and
scissor game described in the Example exm:prs together with the
associated formula for the Nash equilibrium $\phi_{\!N\!E} \defeq
\EExs{\xSym[1]} (\ASym, \xSym[1]) \EExs{\xSym[2]} (\BSym, \xSym[2]) \:
\psi_{\!N\!E}$, where $\psi_{\!N\!E} \defeq ((\EExs{\ySym} (\ASym, \ySym)
\psi_{\ASym}) \rightarrow \psi_{\ASym}) \wedge ((\EExs{\ySym} (\BSym,
\ySym) \psi_{\BSym}) \rightarrow \psi_{\BSym})$ with $\psi_{\ASym} \defeq
\F \wSym[\ASym]$ and $\psi_{\BSym} \defeq \F \wSym[\BSym]$ representing
the  temporal goals for Alice and Bob, respectively.
Then, it is not hard to see that $\GName[P\!RS] \not\models
\phi_{\!N\!E}$, i.e., there are no Nash equilibria in this game, since
there is necessarily an agent that can improve his/her payoff by changing
his/her strategy.

Finally, we want to remark that our semantics framework, based on concurrent
game structures, is enough expressive to describe turn-based features in the
multi-agent case too.
This is possible by simply allowing the transition function to depend only
on the choice of actions of an a priori given agent for each state.

A  $\GName$ is turn-based if there exists a function $\ownFun
: \StSet \to \AgSet$, named owner function, such that, for all
states $\sElm \in \StSet$ and decisions $\decFun[1], \decFun[2] \in
\DecSet$, it holds that if $\decFun[1](\ownFun(\sElm)) =
\decFun[2](\ownFun(\sElm))$ then $\trnFun(\sElm, \decFun[1]) =
\trnFun(\sElm, \decFun[2])$.

Intuitively, a  is turn-based if it is possible to associate with each
state an agent, i.e., the owner of the state, which is responsible for the
choice of the successor of that state.

It is immediate to observe that $\ownFun$ introduces a partitioning of the
set of states into $\card{\rng{\ownFun}}$ components, each one ruled by a
single agent.
Moreover, observe that a  having just one agent is trivially
turn-based, since this agent is the only possible owner of all states.

In the following, as one can expect, we also consider the case in which 		has its semantics defined on turn-based  only.
In such an eventuality, we name the resulting semantic fragment
Turn-based Strategy Logic (, for short) and refer to the related
satisfiability concept as turn-based satisfiability.

Model-Checking Hardness

In this section, we show the non-elementary lower bound for the model-checking
problem of .
Precisely, we prove that, for sentences having alternation number $k$, this
problem is $k$-.
To this aim, in Subsection <ref>, we first recall syntax and
semantics of  <cit.>.
Then, in Subsection <ref>, we give a reduction from the
satisfiability problem for this logic to the model-checking problem for .

Quantified propositional temporal logic

Quantified Propositional Temporal Logic (, for short)
syntactically extends the old-style temporal logic with the future
$\F\!$ and global $\G\!$ operators by means of two proposition
quantifiers, the existential $\exists \qElm .$ and the universal $\forall
\qElm .$, where $\qElm$ is an atomic proposition.
Intuitively, these elements can be respectively read as “there exists
an evaluation of $\qElm$” and “for all evaluations of $\qElm$”.

The formal syntax of  follows.

formulas are built inductively from the sets of atomic
propositions $\APSet$, by using the following grammar, where $\pElm \in
\APSet$:

$\varphi ::= \pElm \mid \neg \varphi \mid \varphi \wedge \varphi \mid
\varphi \vee \varphi \mid \X \varphi \mid \F \varphi \mid \G \varphi
\mid \exists \pElm . \varphi \mid \forall \pElm . \varphi$.

denotes the infinite set of formulas generated by the above

Similarly to , we use the concepts of subformula, free atomic
proposition, sentence, and alternation number, together with the 		syntactic fragment of bounded alternation [$k$-alt], with $k \in
\SetN$.

In order to define the semantics of , we have first to introduce the
concepts of truth evaluations used to interpret the meaning of atomic
propositions at the passing of time.

A temporal truth evaluation is a function $\tteFun : \SetN \to \{
\Ff, \Tt \}$ that maps each natural number to a Boolean value.

Moreover, a propositional truth evaluation is a partial function
$\pteFun : \APSet \pto \TTESet$ mapping every atomic proposition in its
domain to a temporal truth evaluation.

The sets $\TTESet \defeq \SetN \to \{ \Ff, \Tt \}$ and $\PTESet \defeq
\APSet \pto \TTESet$ contain, respectively, all temporal and propositional
truth evaluations.

At this point, we have the tool to define the interpretation of 		formulas.

For a propositional truth evaluation $\pteFun$ with $\free{\varphi}
\subseteq \dom{\pteFun}$ and a number $k$, we write $\pteFun, k \models
\varphi$ to indicate that the formula $\varphi$ holds at the $k$-th position
of the $\pteFun$.

For all  formulas $\varphi$, propositional truth evaluation $\pteFun
\in \PTESet$ with $\free{\varphi} \subseteq \dom{\pteFun}$, and numbers $k
\in \SetN$, the modeling relation $\pteFun, k \models \varphi$ is
inductively defined as follows.

$\pteFun, k \models \pElm$ iff $\pteFun(\pElm)(k) = \Tt$, with
$\pElm \in \APSet$.

For all formulas $\varphi$, $\varphi_{1}$, and $\varphi_{2}$, it holds

$\pteFun, k \models \neg \varphi$ iff not $\pteFun, k \models
\varphi$, that is $\pteFun, k \not\models \varphi$;

$\pteFun, k \models \varphi_{1} \wedge \varphi_{2}$ iff
$\pteFun, k \models \varphi_{1}$ and $\pteFun, k \models
\varphi_{2}$;

$\pteFun, k \models \varphi_{1} \vee \varphi_{2}$ iff $\pteFun,
k \models \varphi_{1}$ or $\pteFun, k \models \varphi_{2}$;

$\pteFun, k \models \X \varphi$ iff $\pteFun, k + 1 \models
\varphi$;

$\pteFun, k \models \F \varphi$ iff there is an index $i \in
\SetN$ with $k \leq i$ such that $\pteFun, i \models \varphi$;

$\pteFun, k \models \G \varphi$ iff, for all indexes $i \in \SetN$
with $k \leq i$, it holds that $\pteFun, i \models \varphi$.

For an atomic proposition $\qElm \in \APSet$ and a formula $\varphi$,
it holds that:

$\pteFun, k \models \exists \qElm . \varphi$ iff there exists a
temporal truth evaluation $\tteFun \in \TTESet$ such that
$\pteFun[][\qElm \mapsto \tteFun], k \models \varphi$;

$\pteFun, k \models \forall \qElm . \varphi$ iff for all temporal
truth evaluations $\tteFun \in \TTESet$ it holds that
$\pteFun[][\qElm \mapsto \tteFun], k \models \varphi$.

Obviously, a  sentence $\varphi$ is satisfiable if $\emptyfun,
0 \models \varphi$.

Observe that the described semantics is slightly different but completely
equivalent to that proposed and used in <cit.> to prove the
non-elementary hardness result for the satisfiability problem.

Non-elementary lower-bound

We can show how the solution of  satisfiability problem can be reduced
to that of the model-checking problem for , over a turn-based constant
size  with a unique atomic proposition.

In order to do this, we first prove the following auxiliary lemma, which
actually represents the main step of the above mentioned reduction.

There is a one-agent  $\GName[Rdc]$ such that, for each
[$k$-alt] sentence $\varphi$, with $k \in \SetN$, there exists an
[$k$-alt] variable-closed formula $\trn{\varphi}$ such that $\varphi$
is satisfiable iff $\GName[Rdc], \asgFun, \sElm[0] \models \trn{\varphi}$,
for all complete assignments $\asgFun \in \AsgSet(\AgSet, \sElm[0])$.

Consider the one-agent  $\GName[Rdc] \defeq \CGSTuple { \{ \pSym \} }
{ \{ \alpha \} } { \{ \Ff, \Tt \} } { \{ \sSym[0], \sSym[1] \} } {\labFun}
{\trnFun} {\sSym[0]}$ depicted in Figure fig:lmm:qptl(rdc), where
the two actions are the Boolean values false and true and where the
labeling and transition functions $\labFun$ and $\trnFun$ are set as
follows: $\labFun(\sSym[0]) \defeq \emptyset$, $\labFun(\sSym[1]) \defeq
\{ \pSym \}$, and $\trnFun(\sElm, \decFun) = \sSym[0]$ iff
$\decFun(\alpha) = \Ff$, for all $\sElm \in \StSet$ and $\decFun \in
\DecSet$.
It is evident that $\GName[Rdc]$ is a turn-based .

Moreover, consider the transformation function $\trn{\cdot} : \QPTL \to
\SL$ inductively defined as follows:

* $\trn{\qElm} \defeq (\alpha, \xSym[\qElm]) \X \pSym$, for $\qElm \in
\APSet$;

* $\trn{\exists \qElm . \varphi} \defeq \EExs{\xSym[\qElm]}
\trn{\varphi}$;

* $\trn{\forall \qElm . \varphi} \defeq \AAll{\xSym[\qElm]}
\trn{\varphi}$;

* $\trn{\Opr \varphi} \defeq \Opr \trn{\varphi}$, where $\Opr \in \{
\neg, \X\!, \F\!, \G\! \}$;

* $\trn{\varphi_{1} \Opr \varphi_{2}} \defeq \trn{\varphi_{1}} \Opr
\trn{\varphi_{2}}$, where $\Opr \in \{ \wedge, \vee \}$.

It is not hard to see that a  formula $\varphi$ is a sentence iff
$\trn{\varphi}$ is variable-closed.
Furthermore, we have that $\alt{\trn{\varphi}} = \alt{\varphi}$.

At this point, it remains to prove that, a  sentence $\varphi$ is
satisfiable iff $\GName[Rdc], \asgFun, \sSym[0] \! \models \trn{\varphi}$,
for all total assignments $\asgFun \in \AsgSet(\{ \alpha \}, \sSym[0])$.

To do this by induction on the structure of $\varphi$, we actually show a
stronger result asserting that, for all subformulas $\psi \in
\sub{\varphi}$, propositional truth evaluations $\pteFun \in \PTESet$, and
$i \in \SetN$, it holds that $\pteFun, i \models \psi$ iff $\GName[Rdc],
(\asgFun, \sSym[0])^{i} \models \trn{\psi}$, for each total assignment
$\asgFun \in \AsgSet(\{ \alpha \} \cup \set{ \xSym[\qElm] \in \VarSet }{
\qElm \in \free{\psi} }, \sSym[0])$ such that
$\asgFun(\xSym[\qElm])((\playElm)_{\leq n}) = \pteFun(\qElm)(n)$, where
$\playElm \defeq \playFun(\asgFun, \sSym[0])$, for all $\qElm \in
\free{\psi}$ and $n \in \numco{i}{\omega}$.

Here, we only show the base case of atomic propositions and the two
inductive cases regarding the proposition quantifiers.
The remaining cases of Boolean connectives and temporal operators are
straightforward and left to the reader as a simple exercise.

* $\psi = \qElm$.

By Item <ref> of
Definition <ref> of  semantics, we have that
$\pteFun, i \models \qElm$ iff $\pteFun(\qElm)(i) = \Tt$.
Thus, due to the above constraint on the assignment, it follows that
$\pteFun, i \models \qElm$ iff $\asgFun(\xSym[\qElm])((\playElm)_{\leq
i}) = \Tt$.

Now, by applying Items <ref>
and <ref> of Definition <ref>
of  semantics, we have that $\GName[Rdc], (\asgFun, \sSym[0])^{i}
\models (\alpha, \xSym[\qElm]) \X \pSym$ iff $\GName[Rdc],
(\asgFun'[\alpha \mapsto \asgFun'(\xSym[\qElm])], \sElm')^{1} \models
\pSym$, where $(\asgFun', \sElm') = (\asgFun, \sSym[0])^{i}$.

At this point, due to the particular structure of the 					$\GName[Rdc]$, we have that $\GName[Rdc], (\asgFun'[\alpha \mapsto
\asgFun'(\xSym[\qElm])], \sElm')^{1} \models \pSym$ iff
$(\playElm')_{1} = \sSym[1]$, where $\playElm' \defeq
\playFun(\asgFun'[\alpha \mapsto \asgFun'(\xSym[\qElm])], \sElm')$,
which in turn is equivalent to
$\asgFun'(\xSym[\qElm])((\playElm')_{\leq 0}) = \Tt$.
So, $\GName[Rdc], (\asgFun, \sSym[0])^{i} \models (\alpha,
\xSym[\qElm]) \X \pSym$ iff $\asgFun'(\xSym[\qElm])((\playElm')_{\leq
0}) = \Tt$.

Now, by observing that $(\playElm')_{\leq 0} = (\playElm)_{i}$ and
using the above definition of $\asgFun'$, we obtain that
$\asgFun'(\xSym[\qElm])((\playElm')_{\leq 0}) =
\asgFun(\xSym[\qElm])((\playElm)_{\leq i})$.
Hence, $\pteFun, i \models \qElm$ iff $\pteFun(\qElm)(i) =
\asgFun(\xSym[\qElm])((\playElm)_{\leq i}) = \Tt =
\asgFun'(\xSym[\qElm])((\playElm')_{\leq 0})$ iff $\GName[Rdc],
(\asgFun, \sSym[0])^{i} \models (\alpha, \xSym[\qElm]) \X \pSym$.

* $\psi = \exists \qElm. \psi'$.

[Only if].

If $\pteFun, i \models \exists \qElm. \psi'$, by
Item <ref> of
Definition <ref>, there exists a temporal truth
evaluation $\tteFun \in \TTESet$ such that $\pteFun[][\qElm \mapsto
\tteFun], i \models \psi'$.
Now, consider a strategy $\strFun \in \StrSet(\sSym[0])$ such that
$\strFun((\playElm)_{\leq n}) = \tteFun(n)$, for all $n \in
\numco{i}{\omega}$.
Then, it is evident that $\asgFun[][\xSym[\qElm] \mapsto
\strFun](\xSym[\qElm'])((\playElm)_{\leq n}) = \pteFun[][\qElm \mapsto
\tteFun](\qElm')(n)$, for all $\qElm' \in \free{\psi}$ and $n \in
\numco{i}{\omega}$.
So, by the inductive hypothesis, it follows that $\GName[Rdc],
(\asgFun[][\xSym[\qElm] \mapsto \strFun], \sSym[0])^{i} \models
\trn{\psi'}$.
Thus, we have that $\GName[Rdc], (\asgFun, \sSym[0])^{i} \models
\EExs{\xSym[\qElm]} \trn{\psi'}$.

If $\GName[Rdc], (\asgFun, \sSym[0])^{i} \models \EExs{\xSym[\qElm]}
\trn{\psi'}$, there exists a strategy $\strFun \in \StrSet(\sSym[0])$
such that $\GName[Rdc], (\asgFun[][\xSym[\qElm] \mapsto \strFun],
\sSym[0])^{i} \models \trn{\psi'}$.
Now, consider a temporal truth evaluation $\tteFun \in \TTESet$ such
that $\tteFun(n) = \strFun((\playElm)_{\leq n})$, for all $n \in
\numco{i}{\omega}$.
Then, it is evident that $\asgFun[][\xSym[\qElm] \mapsto
\strFun](\xSym[\qElm'])((\playElm)_{\leq n}) = \pteFun[][\qElm \mapsto
\tteFun](\qElm')(n)$, for all $\qElm' \in \free{\psi}$ and $n \in
\numco{i}{\omega}$.
So, by the inductive hypothesis, it follows that $\pteFun[][\qElm
\mapsto \tteFun], i \models \psi'$.
Thus, by Item <ref> of
Definition <ref>, we have that $\pteFun, i \models
\exists \qElm. \psi'$.

* $\psi = \forall \qElm. \psi'$.

[Only if].

For each strategy $\strFun \in \StrSet(\sSym[0])$, consider a temporal
truth evaluation $\tteFun \in \TTESet$ such that $\tteFun(n) =
\strFun((\playElm)_{\leq n})$, for all $n \in \numco{i}{\omega}$.
It is evident that $\asgFun[][\xSym[\qElm] \mapsto
\strFun](\xSym[\qElm'])((\playElm)_{\leq n}) = \pteFun[][\qElm \mapsto
\tteFun](\qElm')(n)$, for all $\qElm' \in \free{\psi}$ and $n \in
\numco{i}{\omega}$.
Now, since $\pteFun, i \models \forall \qElm. \psi'$, by
Item <ref> of
Definition <ref>, it follows that $\pteFun[][\qElm
\mapsto \tteFun], i \models \psi'$.
So, by the inductive hypothesis, for each strategy $\strFun \in
\StrSet(\sSym[0])$, it holds that $\GName[Rdc],
(\asgFun[][\xSym[\qElm] \mapsto \strFun], \sSym[0])^{i} \models
\trn{\psi'}$.
Thus, we have that $\GName[Rdc], (\asgFun, \sSym[0])^{i} \models
\AAll{\xSym[\qElm]} \trn{\psi'}$.

For each temporal truth evaluation $\tteFun \in \TTESet$, consider a
strategy $\strFun \in \StrSet(\sSym[0])$ such that
$\strFun((\playElm)_{\leq n}) = \tteFun(n)$, for all $n \in
\numco{i}{\omega}$.
It is evident that $\asgFun[][\xSym[\qElm] \mapsto
\strFun](\xSym[\qElm'])((\playElm)_{\leq n}) =
\pteFun[][\qElm \mapsto \tteFun](\qElm')(n)$, for all $\qElm' \in
\free{\psi}$ and $n \in \numco{i}{\omega}$.
Now, since $\GName[Rdc], (\asgFun, \sSym[0])^{i} \models
\AAll{\xSym[\qElm]} \trn{\psi'}$, it follows that $\GName[Rdc],
(\asgFun[][\xSym[\qElm] \mapsto \strFun], \sSym[0])^{i} \models
\trn{\psi'}$.
So, by the inductive hypothesis, for each temporal truth evaluation
$\tteFun \in \TTESet$, it holds that $\pteFun[][\qElm \mapsto
\tteFun], i \models \psi'$.
Thus, by Item <ref> of
Definition <ref>, we have that $\pteFun, i \models
\forall \qElm. \psi'$.

Thus, we are done with the proof.

Now, we can show the full reduction that allows us to state the existence of
a non-elementary lower-bound for the model-checking problem of  and,
thus, of .

The model-checking problem for [$k$-alt] is $k$-.

Let $\varphi$ be a [$k$-alt] sentence, $\trn{\varphi}$ the related
[$k$-alt] variable-closed formula, and $\GName[Rdc]$ the turn-based
of Lemma <ref> of  reduction.

Then, by applying the previous mentioned lemma, it is easy to see that
$\varphi$ is satisfiable iff $\GName[Rdc] \models \AAll{\xSym} (\alpha,
\xSym) \trn{\varphi}$ iff $\GName[Rdc] \models \EExs{\xSym} (\alpha,
\xSym) \trn{\varphi}$.

Thus, the satisfiability problem for  can be reduced to the
model-checking problem for .

Now, since the satisfiability problem for [$k$-alt] is
$k$- <cit.>, we have that the model-checking problem for
[$k$-alt] is $k$- as well.

The following corollary is an immediate consequence of the previous theorem.

The model-checking problem for [$k$-alt] is $k$-.

Strategy Quantifications

Since model checking for  is non-elementary hard while the same problem
for  is only 2, a question that naturally arises is whether
there are proper fragments of  of practical interest, still strictly
subsuming , that reside in such a complexity gap.
In this section, we answer positively to this question and go even further.
Precisely, we enlighten a fundamental property that, if satisfied, allows to
retain a 2 model-checking problem.
We refer to such a property as elementariness.
To formally introduce this concept, we use the notion of dependence map
as a machinery.

The remaining part of this section is organized as follows.
In Subsection <ref>, we describe three syntactic fragments of
, named , , and , having the peculiarity to use strategy
quantifications grouped in atomic blocks.
Then, in Subsection <ref>, we define the notion of dependence
map, which is used, in Subsection <ref>, to introduce the
concept of elementariness.
Finally, in Subsection <ref>, we prove a fundamental result,
which is at the base of our elementary model-checking procedure for .

Syntactic fragments

In order to formalize the syntactic fragments of  we want to
investigate, we first need to define the concepts of quantification
and binding prefixes.

A quantification prefix over a set $\VSet \subseteq \VarSet$ of
variables is a finite word $\qpElm \in \set{ \EExs{\xElm}, \AAll{\xElm} }{
\xElm \in \VSet }^{\card{\VSet}}$ of length $\card{\VSet}$ such that each
variable $\xElm \in \VSet$ occurs just once in $\qpElm$, i.e., there is
exactly one index $i \in \numco{0}{\card{\VSet}}$ such that $(\qpElm)_{i}
\in \{ \EExs{\xElm}, \AAll{\xElm} \}$.

A binding prefix over a set of variables $\VSet \subseteq \VarSet$
is a finite word $\bpElm \in \set{ (\aElm, \xElm) }{ \aElm \in \AgSet
\land \xElm \in \VSet }^{\card{\AgSet}}$ of length $\card{\AgSet}$ such
that each agent $\aElm \in \AgSet$ occurs just once in $\bpElm$, i.e.,
there is exactly one index $i \in \numco{0}{\card{\AgSet}}$ for which
$(\bpElm)_{i} \in \set{ (\aElm, \xElm) }{ \xElm \in \VSet }$.

Finally, $\QPSet(\VSet) \subseteq \set{ \EExs{\xElm}, \AAll{\xElm} }{
\xElm \in \VSet }^{\card{\VSet}}$ and $\BPSet(\VSet) \subseteq \set{
(\aElm, \xElm) }{ \aElm \in \AgSet \land \xElm \in \VSet
}^{\card{\AgSet}}$ denote, respectively, the sets of all quantification
and binding prefixes over variables in $\VSet$.

We now have all tools to define the syntactic fragments we want to analyze,
which we name, respectively, Nested-Goal, Boolean-Goal, and
One-Goal Strategy Logic (, , and , for short).

For goal we mean an  agent-closed formula of the kind $\bpElm
\varphi$, with $\AgSet \subseteq \free{\varphi}$, being $\bpElm \in
\BndSet(\VarSet)$ a binding prefix.

The idea behind  is that, when there is a quantification over a
variable used in a goal, we are forced to quantify over all free variables
of the inner subformula containing the goal itself, by using a
quantification prefix.
In this way, the subformula is build only by nesting and Boolean
combinations of goals.
In addition, with  we avoid nested goals sharing the variables of a
same quantification prefix, but allow their Boolean combinations.
Finally,  forces the use of a different quantification prefix for each
single goal in the formula.

The formal syntax of , , and  follows.

formulas are built inductively from the sets of atomic propositions
$\APSet$, quantification prefixes $\QPSet(\VSet)$ for any $\VSet \subseteq
\VarSet$, and binding prefixes $\BPSet(\VarSet)$, by using the following
grammar, with $\pElm \in \APSet$, $\qpElm \in \cup_{\VSet \subseteq
\VarSet} \QPSet(\VSet)$, and $\bpElm \in \BPSet(\VarSet)$:

$\varphi ::= \pElm \mid \neg \varphi \mid \varphi \wedge \varphi \mid
\varphi \vee \varphi \mid \X \varphi \mid \varphi \:\U \varphi \mid
\varphi \:\R \varphi \mid \qpElm \varphi \mid \bpElm \varphi$,

where in the formation rule $\qpElm \varphi$ it is ensured that $\varphi$
is agent-closed and $\qpElm \in \QPSet(\free{\varphi})$.

In addition,  formulas are determined by splitting the above
syntactic class in two different parts, of which the second is dedicated
to build the Boolean combinations of goals avoiding their nesting:

$\varphi ::= \pElm \mid \neg \varphi \mid \varphi \wedge \varphi \mid
\varphi \vee \varphi \mid \X \varphi \mid \varphi \:\U \varphi \mid
\varphi \:\R \varphi \mid \qpElm \psi$,

$\psi ::= \bpElm \varphi \mid \neg \psi \mid \psi \wedge \psi \mid \psi
\vee \psi$,

where in the formation rule $\qpElm \psi$ it is ensured that $\qpElm \in
\QPSet(\free{\psi})$.

Finally, the simpler  formulas are obtained by forcing each goal to
be coupled with a quantification prefix:

$\varphi ::= \pElm \mid \neg \varphi \mid \varphi \wedge \varphi \mid
\varphi \vee \varphi \mid \X \varphi \mid \varphi \:\U \varphi \mid
\varphi \:\R \varphi \mid \qpElm \bpElm \varphi$,

where in the formation rule $\qpElm \bpElm \varphi$ it is ensured that
$\qpElm \in \QPSet(\free{\bpElm \varphi})$.

$\SL \supset \NGSL \supset \BGSL \supset \OGSL$ denotes the syntactic
chain of infinite sets of formulas generated by the respective grammars
with the associated constraints on free variables of goals.

Intuitively, in , , and , we force the writing of formulas to
use atomic blocks of quantifications and bindings, where the related free
variables are strictly coupled with those that are effectively quantified in
the prefix just before the binding.
In a nutshell, we can only write formulas by using sentences of the form
$\qpElm \psi$ belonging to a kind of prenex normal form in which the
quantifications contained into the matrix $\psi$ only belong to the
prefixes $\qpElm'$ of some inner subsentence $\qpElm' \psi' \in \snt{\qpElm
\psi}$.

An  sentence $\phi$ is principal if it is of the form $\phi =
\qpElm \psi$, where $\psi$ is agent-closed and $\qpElm \in
\QPSet(\free{\psi})$.
By $\psnt{\varphi} \subseteq \snt{\varphi}$ we denote the set of all
principal subsentences of the formula $\varphi$.

We now introduce other two general restrictions in which the numbers
$\card{\AgSet}$ of agents and $\card{\VarSet}$ of variables that are used
to write a formula are fixed to the a priori values $n, m \in
\numco{1}{\omega}$, respectively.
Moreover, we can also forbid the sharing of variables, i.e., each variable
is binded to one agent only, so, we cannot force two agents to use the same
We name these three fragments [$n$-ag], [$m$-var], and [fvs],
Note that, in the one agent fragment, the restriction on the sharing of
variables between agents, naturally, does not act, i.e., $\SL[$1$-ag, fvs] =
\SL[$1$-ag]$.

To start to practice with the above fragments, consider again the sentence
$\varphi$ of Example exm:sv.
It is easy to see that it actually belongs to [$2$-ag, $3$-var,
$2$-alt], and so, to , but not to , since it is of the form
$\qpSym (\bpSym[1] \X \pSym \wedge \bpSym[2] \X \qSym)$, where the
quantification prefix is $\qpSym = \EExs{\xSym} \AAll{\ySym} \EExs{\zSym}$
and the binding prefixes of the two goals are $\bpSym[1] = (\alpha, \xSym)
(\beta, \ySym)$ and $\bpSym[2] = (\alpha, \ySym) (\beta, \zSym)$.

Along the paper, sometimes we assert that a given formula $\varphi$ belongs
to an  syntactic fragment also if its syntax does not precisely
correspond to what is described by the relative grammar.
We do this in order to make easier the reading and interpretation of the
formula $\varphi$ itself and only in the case that it is simple to translate
it into an equivalent formula that effectively belongs to the intended
logic, by means of a simple generalization of classic rules used to put a
formula of first order logic in the prenex normal form.

For example, consider the sentence $\varphi_{\!N\!\!E}$ of
Example exm:ne representing the existence of a Nash equilibrium.
This formula is considered to belong to [$n$-ag, $2n$-var, fvs,
$1$-alt], since it can be easily translated in the form $\phi_{\!N\!\!E} =
\qpSym \bigwedge_{i = 1}^{n} \bpSym[i] \psi_{i} \rightarrow \bpSym
\psi_{i}$, where $\qpSym = \EExs{\xSym[1]} \cdots \EExs{\xSym[n]}
\AAll{\ySym[1]} \cdots \AAll{\ySym[n]}$, $\bpSym = (\alpha_{1}, \xSym[1])
\cdots (\alpha_{n}, \xSym[n])$, $\bpSym[i] = (\alpha_{1}, \xSym[1]) \cdots
(\alpha_{i - 1}, \xSym[i - 1]) (\alpha_{i}, \ySym[i]) (\alpha_{i + 1},
\xSym[i + 1]) \cdots (\alpha_{n}, \xSym[n])$, and $\free{\psi_{i}} =
\AgSet$.

As another example, consider the sentence $\varphi_{\!S\!P}$ of
Example exm:sp representing the existence of a stability profile.
Also this formula is considered to belong to [$n$-ag, $2n$-var, fvs,
$1$-alt], since it is equivalent to $\phi_{\!S\!P} = \qpSym \bigwedge_{i, j
= 1, i \neq j}^{n} \bpSym \psi_{j} \rightarrow ((\bpSym \psi_{i}
\leftrightarrow \bpSym[i] \psi_{i}) \rightarrow \bpSym[i] \psi_{j})$.

Note that both $\phi_{\!N\!\!E}$ and $\phi_{\!S\!P}$ are principal

Now, it is interesting to observe that  and  are exactly
equivalent to [fvs, $0$-alt] and [fvs, $1$-alt], respectively.
Moreover,  <cit.> is the very simple fragment of [fvs,
$1$-alt] that forces all goals in a formula to have a common part containing
all variables quantified before the unique possible alternation of the
quantification prefix.
Finally, we have that  is the [$2$-ag, fvs] fragment.

It is well-known that the non-elementary hardness result for the
satisfiability problem of  <cit.> already holds for formulas in
prenex normal form.
Now, it is not hard to see that the transformation described in
Lemma <ref> of  reduction puts [$k$-alt]
sentences $\varphi$ in prenex normal form into [$1$-ag, $k$-alt]
variable-closed formulas $\trn{\varphi} = \qpElm \psi$.
Moreover, the derived [$1$-ag, $k$-alt] sentence $\EExs{\xSym}
(\alpha, \xSym) \qpElm \psi$ used in Theorem <ref> of
model-checking hardness is equivalent to the [$1$-ag,
$k$-alt] principal sentence $\EExs{\xSym} \qpElm (\alpha, \xSym) \psi$,
since $\xSym$ is not used in the quantification prefix $\qpElm$.
Thus, the hardness result for the model-checking problem holds for
[$1$-ag, $k$-alt] and, consequently, for [$1$-ag, $k$-alt] as
However, it is important to observe that, unfortunately, it is not know
if such an hardness result holds for  or  and, in
particular, for .
We leave this problem open here.

At this point, we prove that  is strictly less expressive than 		and, consequently, than  and .
To do this, we show the existence of two structures that result to be
equivalent only w.r.t. sentences having alternation number bounded by $1$.
It can be interesting to note that, we use an ad-hoc technique based on a
brute-force check to verify that all  formulas cannot distinguish
between the two structures.
A possible future line of research is to study variants of the
Ehrenfeucht-Fraïssé game <cit.> for , which allow to
determine whether two structures are or not equivalent w.r.t. a particular

There exists an [$3$-ag, fvs, $2$-alt] sentence having no 			equivalent.

Consider the two s $\GName[1] \defeq \CGSTuple {\{ \pSym \}} {\{
\alpha, \beta, \gamma \}} {\{ 0, 1 \}} {\{ \sSym[0], \sSym[1], \sSym[2]
\}} {\labFun} {\trnFun[1]} {\sSym[0]}$ and $\GName[2] \defeq \CGSTuple {\{
\pSym \}} {\{ \alpha, \beta, \gamma \}} {\{ 0, 1, 2 \}} {\{ \sSym[0],
\sSym[1], \sSym[2] \}} {\labFun} {\trnFun[2]} {\sSym[0]}$ depicted in
Figure fig:thm:ogslvsatls(exp), where $\labFun(\sSym[0]) =
\labFun(\sSym[2]) \defeq \emptyset$, $\labFun(\sSym[1]) \defeq \{ \pSym
\}$, $\DSet[1] \defeq \{ 00*, 11* \}$, and $\DSet[2] \defeq \{ 00*, 11*,
12*, 200, 202, 211 \}$.

Moreover, consider the [$3$-ag, fvs, $2$-alt] sentence $\varphi^{*}
\defeq \qpSym^{*} \bpSym^{*} \X \pSym$, where $\qpSym^{*} \defeq
\AAll{\xSym} \EExs{\ySym} \AAll{\zElm}$ and $\bpSym^{*} \defeq (\alpha,
\xSym) (\beta, \ySym) (\gamma, \zSym)$.

Then, it is easy to see that $\GName[1] \models \varphi^{*}$ but
$\GName[2] \not\models \varphi^{*}$.
Indeed, $\GName[1], \asgFun[1], \sSym[0] \models \bpSym^{*} \X \pSym$, for
all $\asgFun[1] \in \AsgSet[ {\GName[1]} ](\{ \xSym, \ySym, \zSym \},
\sSym[0])$ such that $\asgFun[1](\ySym)(\sSym[0]) =
\asgFun[1](\xSym)(\sSym[0])$, and $\GName[2], \asgFun[2], \sSym[0] \models
\bpSym^{*} \X \neg \pSym$, for all $\asgFun[2] \in \AsgSet[ {\GName[2]}
](\{ \xSym, \ySym, \zSym \}, \sSym[0])$ such that
$\asgFun[2](\xSym)(\sSym[0]) = 2$ and $\asgFun[2](\zSym)(\sSym[0]) =
(\asgFun[2](\ySym)(\sSym[0]) + 1) \bmod 3$.

Now, due to the particular structure of the s $\GName[i]$ under exam,
with $i \in \{ 1, 2 \}$, for each path $\pthElm \in \PthSet[ {\GName[i]}
](\sSym[0])$, we have that either $\labFun((\pthElm)_{j}) = \{ \pSym \}$
or $\labFun((\pthElm)_{j}) = \emptyset$, for all $j \in
\numco{1}{\omega}$, i.e., apart from the initial state, the path is
completely labeled either with $\{ \pSym \}$ or with $\emptyset$.

Thus, it is easy to see that, for each  formula $\qpElm \bpElm
\psi$, there is a literal $\lElm[\psi] \in \{ \pSym, \neg \pSym \}$ such
that $\GName[i] \models \qpElm \bpElm \psi$ iff $\GName[i] \models \qpElm
\bpElm \X \!\lElm[\psi]$, for all $i \in \{ 1, 2 \}$.

W.l.o.g., we can suppose that $\bpElm = \bpSym^{*}$, since we are always
able to uniformly rename the variables of the quantification and binding
prefixes without changing the meaning of the sentence.

At this point, it is easy to see that there exists an index $k \in \{ 1,
2, 3 \}$ for which it holds that either $\qpSym[k] \bpSym^{*} \X
\!\lElm[\psi] \implies \qpElm \bpSym^{*} \X \!\lElm[\psi]$ or $\qpElm
\bpSym^{*} \X \!\lElm[\psi] \implies \dual{\qpElm[k]} \bpSym^{*} \X
\!\lElm[\psi]$, where $\qpSym[1] \defeq \AAll{\xSym} \AAll{\zElm}
\EExs{\ySym}$, $\qpSym[2] \defeq \EExs{\xSym} \EExs{\yElm} \AAll{\zSym}$,
and $\qpSym[3] \defeq \AAll{\ySym} \AAll{\zElm} \EExs{\xSym}$.

Thus, to prove that every  formula cannot distinguish between
$\GName[1]$ and $\GName[2]$, we can simply show that the sentences
$\qpSym[k] \bpSym^{*} \X \!\lElm$, with $k \in \{ 1, 2, 3 \}$ and $\lElm
\in \{ \pSym, \neg \pSym \}$, do the same.

In fact, it holds that $\GName[i] \models \qpSym[k] \bpSym^{*} \X
\!\lElm$, for all $i \in \{ 1, 2 \}$, $k \in \{ 1, 2, 3 \}$, and $\lElm
\in \{ \pSym, \neg \pSym \}$.
Hence, the thesis holds.

The check of the latter fact is trivial and left to the reader as an

Dependence Maps

We now introduce the concept of dependence map of a quantification and show
how any quantification prefix contained into an  formula can be
represented by an adequate choice of a dependence map over strategies.
The main idea here is inspired by what Skolem proposed for the first order
logic in order to eliminate each existential quantification over variables,
by substituting them with second order existential quantifications over
functions, whose choice is uniform w.r.t. the universal variables.

First, we introduce some notation regarding quantification prefixes.

Let $\qpElm \in \QPSet(\VSet)$ be a quantification prefix over a set
$\QPVSet(\qpElm) \defeq \VSet \subseteq \VarSet$ of variables.

By $\QPEVSet{\qpElm} \defeq \set{ \xElm \in \QPVSet(\qpElm) }{ \exists i \in
\numco{0}{\card{\qpElm}} .\: (\qpElm)_{i} = \EExs{\xElm} }$ and
$\QPAVSet{\qpElm} \defeq \QPVSet(\qpElm) \setminus \QPEVSet{\qpElm}$ we
denote, respectively, the sets of existential and universal
variables quantified in $\qpElm$.

For two variables $\xElm, \yElm \in \QPVSet(\qpElm)$, we say that $\xElm$
precedes $\yElm$ in $\qpElm$, in symbols $\xElm \qpordRel[\qpElm]
\yElm$, if $\xElm$ occurs before $\yElm$ in $\qpElm$, i.e., there are two
indexes $i, j \in \numco{0}{\card{\qpElm}}\!$, with $i < j$, such that
$(\qpElm)_{i} \in \{ \EExs{\xElm}, \AAll{\xElm} \}$ and $(\qpElm)_{j} \in \{
\EExs{\yElm}, \AAll{\yElm} \}$.

Moreover, we say that $\yElm$ is functional dependent on $\xElm$, in
symbols $\xElm \qpdepRel[\qpElm] \yElm$, if $\xElm \in \QPAVSet{\qpElm}$,
$\yElm \in \QPEVSet{\qpElm}$, and $\xElm \qpordRel_{\qpElm} \yElm$, i.e.,
$\yElm$ is existentially quantified after that $\xElm$ is universally
quantified, so, there may be a dependence between a value chosen by $\xElm$
and that chosen by $\yElm$.
This definition induces the set $\QPDepSet(\qpElm) \defeq \set{ (\xElm,
\yElm) \in \QPVSet(\qpElm) \times \QPVSet(\qpElm) }{ \xElm \qpdepRel[\qpElm]
\yElm }$ of dependence pairs and its derived version
$\QPDepSet(\qpElm, \yElm) \defeq \set{ \xElm \in \QPVSet(\qpElm) }{ \xElm
\qpdepRel[\qpElm] \yElm }$ containing all variables from which $\yElm$

Finally, we use $\dual{\qpElm} \in \QPSet(\QPVSet(\qpElm))$ to indicate the
quantification derived from $\qpElm$ by dualizing each quantifier
contained in it, i.e., for all indexes $i \in \numco{0}{\card{\qpElm}}\!$,
it holds that $(\dual{\qpElm})_{i} = \EExs{\xElm}$ iff $(\qpElm)_{i} =
\AAll{\xElm}$, with $\xElm \in \QPVSet(\qpElm)$.
It is evident that $\QPEVSet{\dual{\qpElm}} = \QPAVSet{\qpElm}$ and
$\QPAVSet{\dual{\qpElm}} = \QPEVSet{\qpElm}$.

As an example, let $\qpSym = \AAll{\xSym} \EExs{\ySym} \EExs{\zSym}
\AAll{\wSym} \EExs{\vSym}$.
Then, we have $\QPEVSet{\qpSym} = \{ \ySym, \zSym, \vSym \}$,
$\QPAVSet{\qpSym} = \{ \xSym, \wSym \}$, $\QPDepSet(\qpSym, \xSym) =
\QPDepSet(\qpSym, \wSym) = \emptyset$,

Finally, we define the notion of valuation of variables over a
generic set $\DSet$, called domain, i.e., a partial function $\valFun
: \VarSet \pto \DSet$ mapping every variable in its domain to an element in
By $\ValSet[\DSet](\VSet) \defeq \VSet \to \DSet$ we denote the set of all
valuation functions over $\DSet$ defined on $\VSet \subseteq \VarSet$.

At this point, we give a general high-level semantics for the quantification
prefixes by means of the following main definition of dependence map.

Let $\qpElm \in \QPSet(\VSet)$ be a quantification prefix over a set
$\VSet \subseteq \VarSet$ of variables, and $\DSet$ a set.
Then, a dependence map for $\qpElm$ over $\DSet$ is a function
$\spcFun : \ValSet[\DSet](\QPAVSet{\qpElm}) \to \ValSet[\DSet](\VSet)$
satisfying the following properties:

$\spcFun(\valFun)_{\rst \QPAVSet{\qpElm}} \!=\! \valFun$, for all
$\valFun \in \ValSet[\DSet](\QPAVSet{\qpElm})$; [By
$\gFun_{\rst \ZSet} : (\XSet \cap \ZSet) \to \YSet$ we denote the
restriction of a function $\gFun : \XSet \to \YSet$ to the
elements in the set $\ZSet$.]

$\spcFun(\valFun[1])(\xElm) \!=\! \spcFun(\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)}$.

$\SpcSet[\DSet](\qpElm)$ denotes the set of all dependence maps for
$\qpElm$ over $\DSet$.

Intuitively, Item <ref> asserts that $\spcFun$ takes the
same values of its argument w.r.t. the universal variables in $\qpElm$ and
Item <ref> ensures that the value of $\spcFun$ w.r.t. an
existential variable $\xElm$ in $\qpElm$ does not depend on variables not in
$\QPDepSet(\qpElm, \xElm)$.

To get a better insight into this definition, a dependence map $\spcFun$ for
$\qpElm$ can be considered as a set of Skolem functions that, given a
value for each variable in $\QPVSet(\qpElm)$ that is universally quantified
in $\qpElm$, returns a possible value for all the existential variables in
$\qpElm$, in a way that is consistent w.r.t. the order of quantifications.

Observe that, each $\spcFun \in \SpcSet[\DSet](\qpElm)$ is injective, so,
$\card{\rng{\spcFun}} = \card{\dom{\spcFun}} =
\card{\DSet}^{\card{\QPAVSet{\qpElm}}}$.
Moreover, $\card{\SpcSet[\DSet](\qpElm)} = \prod_{\xElm \in
\QPEVSet{\qpElm}} \card{\DSet}^{\card{\DSet}^{\card{\QPDepSet(\qpElm,
\xElm)}}}$.

As an example, let $\DSet = \{ 0, 1 \}$ and $\qpSym = \AAll{\xSym}
\EExs{\ySym} \AAll{\zSym} \in \QPSet(\VSet)$ be a quantification prefix over
$\VSet = \{ \xSym, \ySym, \zSym \}$.
Then, we have that $\card{\SpcSet[\DSet](\qpSym)} = 4$ and
$\card{\SpcSet[\DSet](\dual{\qpSym})} = 8$.
Moreover, the dependence maps $\spcFun[i] \in \SpcSet[\DSet](\qpSym)$ with
$i \in \numcc{0}{3}$ and $\dual[i]{\spcFun} \in
\SpcSet[\DSet](\dual{\qpSym})$ with $i \in \numcc{0}{7}$, for a particular
fixed order, are such that $\spcFun[0](\valFun)(\ySym) = 0$,
$\spcFun[1](\valFun)(\ySym) = \valFun(\xSym)$, $\spcFun[2](\valFun)(\ySym) =
1 - \valFun(\xSym)$, and $\spcFun[3](\valFun)(\ySym) = 1$, for all $\valFun
\in \ValSet[\DSet](\QPAVSet{\qpSym})$, and
$\dual[i]{\spcFun}(\dual{\valFun})(\xSym) = 0$ with $i \in \numcc{0}{3}$,
$\dual[i]{\spcFun}(\dual{\valFun})(\xSym) = 1$ with $i \in \numcc{4}{7}$,
$\dual[0]{\spcFun}(\dual{\valFun})(\zSym) =
\dual[4]{\spcFun}(\dual{\valFun})(\zSym) = 0$,
$\dual[1]{\spcFun}(\dual{\valFun})(\zSym) =
\dual[5]{\spcFun}(\dual{\valFun})(\zSym) = \dual{\valFun}(\ySym)$,
$\dual[2]{\spcFun}(\dual{\valFun})(\zSym) =
\dual[6]{\spcFun}(\dual{\valFun})(\zSym) = 1 - \dual{\valFun}(\ySym)$, and
$\dual[3]{\spcFun}(\dual{\valFun})(\zSym) =
\dual[7]{\spcFun}(\dual{\valFun})(\zSym) = 1$, for all $\dual{\valFun} \in
\ValSet[\DSet](\QPAVSet{\dual{\qpSym}})$.

We now prove the following fundamental theorem that describes how to
eliminate the strategy quantifications of an  formula via a choice of a
suitable dependence map over strategies.
This procedure can be seen as the equivalent of Skolemization in
first order logic (see <cit.>, for more details).

Let $\GName$ be a  and $\varphi = \qpElm \psi$ an  formula, being
$\qpElm \in \QPSet(\VSet)$ a quantification prefix over a set $\VSet
\subseteq \free{\psi} \cap \VarSet$ of variables.
Then, for all assignments $\asgFun \in \AsgSet(\free{\varphi}, \sElm[0])$,
the following holds: $\GName, \asgFun, \sElm[0] \models \varphi$ iff there
exists a dependence map $\spcFun \in \SpcSet[ {\StrSet(\sElm[0])}
](\qpElm)$ such that $\GName, \asgFun \umrg \spcFun(\asgFun'), \sElm[0]
\models \psi$, for all $\asgFun' \in \AsgSet(\QPAVSet{\qpElm},
\sElm[0])$. [By $\gFun[1] \umrg \gFun[2] : (\XSet[1] \cup
\XSet[2]) \to (\YSet[1] \cup \YSet[2])$ we denote the operation of
union of two functions $\gFun[1] : \XSet[1] \to \YSet[1]$ and
$\gFun[2] : \XSet[2] \to \YSet[2]$ defined on disjoint domains, i.e.,
$\XSet[1] \cap \XSet[2] = \emptyset$.]

The proof proceeds by induction on the length of the quantification prefix
For the base case $\card{\qpElm} = 0$, the thesis immediately follows,
since $\QPAVSet{\qpElm} = \emptyset$ and, consequently, both
$\SpcSet[\StrSet( {\sElm[0]} )](\qpElm)$ and $\AsgSet(\QPAVSet{\qpElm},
\sElm[0])$ contain the empty function only (we are assuming, by
convention, that $\emptyfun(\emptyfun) \defeq \emptyfun$).

We now prove, separately, the two directions of the inductive case.

[Only if].

Suppose that $\GName, \asgFun, \sElm[0] \models \varphi$, where $\qpElm =
\Qnt \cdot \qpElm'$.
Then, two possible cases arise: either $\Qnt = \EExs{\xElm}$ or $\Qnt =
\AAll{\xElm}$.

* $\Qnt = \EExs{\xElm}$.

By Item <ref> of
Definition <ref> of  semantics, there is a
strategy $\strFun \in \StrSet(\sElm[0])$ such that $\GName,
\asgFun[][\xElm \mapsto \strFun], \sElm[0] \models \qpElm' \psi$.
Note that $\QPAVSet{\qpElm} = \QPAVSet{\qpElm'}$.
By the inductive hypothesis, we have that there exists a dependence
map $\spcFun \in \SpcSet[\StrSet( {\sElm[0]} )](\qpElm')$ such that
$\GName, \asgFun[][\xElm \mapsto \strFun] \umrg \spcFun(\asgFun'),
\sElm[0] \models \psi$, for all $\asgFun' \in
\AsgSet(\QPAVSet{\qpElm'}, \sElm[0])$.
Now, consider the function $\spcFun' : \AsgSet(\QPAVSet{\qpElm},
\sElm[0]) \to \AsgSet(\VSet, \sElm[0])$ defined by $\spcFun'(\asgFun')
\defeq \spcFun(\asgFun')[\xElm \mapsto \strFun]$, for all $\asgFun'
\in \AsgSet(\QPAVSet{\qpElm}, \sElm[0])$.
It is easy to check that $\spcFun'$ is a dependence map for $\qpElm$
over $\StrSet(\sElm[0])$, i.e., $\spcFun' \in \SpcSet[\StrSet(
{\sElm[0]} )](\qpElm)$.
Moreover, $\asgFun[][\xElm \mapsto \strFun] \umrg \spcFun(\asgFun') =
\asgFun \umrg \spcFun(\asgFun')[\xElm \mapsto \strFun] = \asgFun \umrg
\spcFun'(\asgFun')$, for $\asgFun' \in \AsgSet(\QPAVSet{\qpElm},
\sElm[0])$.
Hence, $\GName, \asgFun \umrg \spcFun'(\asgFun'), \sElm[0] \models
\psi$, for all $\asgFun' \in \AsgSet(\QPAVSet{\qpElm}, \sElm[0])$.

* $\Qnt = \AAll{\xElm}$.

By Item <ref> of
Definition <ref>, we have that, for all strategies
$\strFun \in \StrSet(\sElm[0])$, it holds that $\GName,
\asgFun[][\xElm \mapsto \strFun], \sElm[0] \models \qpElm' \psi$.
Note that $\QPAVSet{\qpElm} = \QPAVSet{\qpElm'} \cup \{ \xElm \}$.
By the inductive hypothesis, we derive that, for each $\strFun \in
\StrSet(\sElm[0])$, there exists a dependence map $\spcFun[\strFun]
\in \SpcSet[\StrSet( {\sElm[0]} )](\qpElm')$ such that $\GName,
\asgFun[][\xElm \mapsto \strFun] \umrg \spcFun[\strFun](\asgFun'),
\sElm[0] \models \psi$, for all $\asgFun' \in
\AsgSet(\QPAVSet{\qpElm'}, \sElm[0])$.
Now, consider the function $\spcFun' : \AsgSet(\QPAVSet{\qpElm},
\sElm[0]) \to \AsgSet(\VSet, \sElm[0])$ defined by $\spcFun'(\asgFun')
\defeq \spcFun[\asgFun'(\xElm)](\asgFun[|']_{\rst
\QPAVSet{\qpElm'}})[\xElm \mapsto \asgFun'(\xElm)]$, for all $\asgFun'
\in \AsgSet(\QPAVSet{\qpElm}, \sElm[0])$.
It is evident that $\spcFun'$ is a dependence map for $\qpElm$ over
$\StrSet(\sElm[0])$, i.e., $\spcFun' \in \SpcSet[\StrSet( {\sElm[0]}
Moreover, $\asgFun[][\xElm \mapsto \strFun] \umrg
\spcFun[\strFun](\asgFun') = \asgFun \umrg
\spcFun[\strFun](\asgFun')[\xElm \mapsto \strFun] = \asgFun \umrg
\spcFun'(\asgFun'[\xElm \mapsto \strFun])$, for $\strFun \in
\StrSet(\sElm[0])$ and $\asgFun' \in \AsgSet(\QPAVSet{\qpElm'},
\sElm[0])$.
Hence, $\GName, \asgFun \umrg \spcFun'(\asgFun'), \sElm[0] \models
\psi$, for all $\asgFun' \in \AsgSet(\QPAVSet{\qpElm}, \sElm[0])$.

Suppose that there exists a dependence map $\spcFun \in \SpcSet[\StrSet(
{\sElm[0]} )](\qpElm)$ such that $\GName, \asgFun \umrg \spcFun(\asgFun'),
\sElm[0] \models \psi$, for all $\asgFun' \in \AsgSet(\QPAVSet{\qpElm},
\sElm[0])$, where $\qpElm = \Qnt \cdot \qpElm'$.
Then, two possible cases arise: either $\Qnt = \EExs{\xElm}$ or $\Qnt =
\AAll{\xElm}$.

* $\Qnt = \EExs{\xElm}$.

There is a strategy $\strFun \in \StrSet(\sElm[0])$ such that $\strFun
= \spcFun(\asgFun')(\xElm)$, for all $\asgFun' \in
\AsgSet(\QPAVSet{\qpElm}, \sElm[0])$.
Note that $\QPAVSet{\qpElm} = \QPAVSet{\qpElm'}$.
Consider the function $\spcFun' : \AsgSet(\QPAVSet{\qpElm'}, \sElm[0])
\to \AsgSet(\VSet \setminus \{ \xElm \}, \sElm[0])$ defined by
$\spcFun'(\asgFun') \defeq \spcFun(\asgFun')_{\rst (\VSet \setminus \{
\xElm \})}$, for all $\asgFun' \in \AsgSet(\QPAVSet{\qpElm'},
\sElm[0])$.
It is easy to check that $\spcFun'$ is a dependence map for $\qpElm'$
over $\StrSet(\sElm[0])$, i.e., $\spcFun' \in \SpcSet[\StrSet(
{\sElm[0]} )](\qpElm')$.
Moreover, $\asgFun \umrg \spcFun(\asgFun') = \asgFun \umrg
\spcFun'(\asgFun')[\xElm \mapsto \strFun] = \asgFun[][\xElm \mapsto
\strFun] \umrg \spcFun'(\asgFun')$, for $\asgFun' \in
\AsgSet(\QPAVSet{\qpElm'}, \sElm[0])$.
Then, it is evident that $\GName, \asgFun[][\xElm \to \strFun] \umrg
\spcFun'(\asgFun'), \sElm[0] \models \psi$, for all $\asgFun' \in
\AsgSet(\QPAVSet{\qpElm'}, \sElm[0])$.
By the inductive hypothesis, we derive that $\GName, \asgFun[][\xElm
\mapsto \strFun], \sElm[0] \models \qpElm' \psi$, which means that
$\GName, \asgFun, \sElm[0] \models \varphi$, by
Item <ref> of
Definition <ref> of  semantics.

* $\Qnt = \AAll{\xElm}$.

First note that $\QPAVSet{\qpElm} = \QPAVSet{\qpElm'} \cup \{ \xElm
\}$.
Also, consider the functions $\spcFun[\strFun|'] :
\AsgSet(\QPAVSet{\qpElm'}, \sElm[0]) \to \AsgSet(\VSet \setminus \{
\xElm \}, \sElm[0])$ defined by $\spcFun[\strFun|'](\asgFun') \defeq
\spcFun(\asgFun'[\xElm \mapsto \strFun])_{\rst (\VSet \setminus \{
\xElm \})}$, for each $\strFun \in \StrSet(\sElm[0])$ and $\asgFun'
\in \AsgSet(\QPAVSet{\qpElm'}, \sElm[0])$.
It is easy to see that every $\spcFun[\strFun|']$ is a dependence map
for $\qpElm'$ over $\StrSet(\sElm[0])$, i.e.,
$\spcFun[\strFun|'] \in \SpcSet[\StrSet( {\sElm[0]} )](\qpElm')$.
Moreover, $\asgFun \umrg \spcFun(\asgFun') = \asgFun \umrg
\spcFun[\asgFun'(\xElm)|'](\asgFun'_{\rst \QPAVSet{\qpElm'}})[\xElm
\mapsto \asgFun'(\xElm)] = \asgFun[][\xElm \mapsto \asgFun'(\xElm)]
\umrg \spcFun[\asgFun'(\xElm)|'](\asgFun'_{\rst \QPAVSet{\qpElm'}})$,
for $\asgFun' \in \AsgSet(\QPAVSet{\qpElm}, \sElm[0])$.
Then, it is evident that $\GName, \asgFun[][\xElm \to \strFun] \umrg
\spcFun[\strFun|'](\asgFun'), \sElm[0] \models \psi$, for all $\strFun
\in \StrSet(\sElm[0])$ and $\asgFun' \in \AsgSet(\QPAVSet{\qpElm'},
\sElm[0])$.
By the inductive hypothesis, we derive that $\GName, \asgFun[][\xElm
\mapsto \strFun], \sElm[0] \models \qpElm' \psi$, for all $\strFun \in
\StrSet(\sElm[0])$, which means that $\GName, \asgFun, \sElm[0]
\models \varphi$, by Item <ref> of
Definition <ref>.

Thus, the thesis of the theorem holds.

As an immediate consequence of the previous result, we derive the following

Let $\GName$ be a  and $\varphi = \qpElm \psi$ an  sentence,
where $\psi$ is agent-closed and $\qpElm \in \QPSet(\free{\psi})$.
Then, $\GName \models \varphi$ iff there exists a dependence map $\spcFun
\in \SpcSet[ {\StrSet(\sElm[0])} ](\qpElm)$ such that $\GName,
\spcFun(\asgFun), \sElm[0] \models \psi$, for all $\asgFun \in
\AsgSet(\QPAVSet{\qpElm}, \sElm[0])$.

Elementary quantifications

We now have all tools we need to introduce the property of elementariness
for a particular class of dependence maps.

Intuitively, a dependence map over functions from a set $\TSet$ to a set
$\DSet$ is elementary if it can be split into a set of dependence maps over
$\DSet$, one for each element of $\TSet$.

This idea allows us to enormously simplify the reasoning about strategy
quantifications, since we can reduce them to a set of quantifications over
actions, one for each track in their domains.
This means that, under certain conditions, we can transform a dependence map
$\spcFun \in \SpcSet[\StrSet(\sElm)](\qpElm)$ over strategies in a function
$\adj{\spcFun} : \TrkSet(\sElm) \to \SpcSet[\AcSet](\qpElm)$ that associates
with each track a dependence map over actions.

To formally develop the above idea, we have first to introduce the generic
concept of adjoint function and state an auxiliary lemma.

Let $\DSet$, $\TSet$, $\USet$, and $\VSet$ be four sets, and $\mFun :
(\TSet \to \DSet)^{\USet} \to (\TSet \to \DSet)^{\VSet}$ and $\adj{\mFun}
: \TSet \to (\DSet^{\USet} \to \DSet^{\VSet})$ two functions.
Then, $\adj{\mFun}$ is the adjoint of $\mFun$ if
$\adj{\mFun}(\tElm)(\flip{\gFun}(\tElm))(\xElm) =
\mFun(\gFun)(\xElm)(\tElm)$, for all $\gFun \in (\TSet \to
\DSet)^{\USet}$, $\xElm \in \VSet$, and $\tElm \in \TSet$ [By
$\flip{\gFun} : \YSet \to \XSet \to \ZSet$ we denote the operation of
flipping of a function $\gFun : \XSet \to \YSet \to \ZSet$.]

Intuitively, $\adj{\mFun}$ is the adjoint of $\mFun$ if the dependence from
the set $\TSet$ in both domain and codomain of the latter can be extracted
and put as a common factor of the functor given by the former.
This means also that, for every pair of functions  $\gFun[1], \gFun[2] \in
(\TSet \to \DSet)^{\USet}$ such that $\flip{\gFun[1]}(\tElm) =
\flip{\gFun[2]}(\tElm)$ for some $\tElm \in \TSet$, it holds that
$\mFun(\gFun[1])(\xElm)(\tElm) = \mFun(\gFun[2])(\xElm)(\tElm)$, for all
$\xElm \in \VSet$.

It is immediate to observe that if a function has an adjoint then this
adjoint is unique.
At the same way, if one has an adjoint function then it is possible to
determine the original function without any ambiguity.
Thus, it is established a one-to-one correspondence between functions
admitting an adjoint and the adjoint itself.

Next lemma formally states the property briefly described above, i.e., that
each dependence map over a set $\TSet \to \DSet$, admitting an adjoint
function, can be represented as a function, with $\TSet$ as domain, which
returns dependence maps over $\DSet$ as values.

Let $\qpElm \in \QPSet(\VSet)$ be a quantification prefix over a set
$\VSet \subseteq \VarSet$ of variables, $\DSet$ and $\TSet$ two 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)$.

We now define the formal meaning of the elementariness of a dependence map
over functions.

Let $\qpElm \in \QPSet(\VSet)$ be a quantification prefix over a set
$\VSet \subseteq \VarSet$ of variables, $\DSet$ and $\TSet$ two sets, and
$\spcFun \in \SpcSet[\TSet \to \DSet](\qpElm)$ a dependence map for
$\qpElm$ over $\TSet \to \DSet$.
Then, $\spcFun$ is elementary if it admits an adjoint function.
$\ESpcSet[\TSet \to \DSet](\qpElm)$

It is important to observe that, unfortunately, there are dependence maps
that are not elementary.
To easily understand why this is actually the case, it is enough to count
both the number of dependence maps $\SpcSet[\TSet \to \DSet](\qpElm)$ and of
adjoint functions $\TSet \to \SpcSet[\DSet](\qpElm)$, where $\card{\DSet} >
1$, $\card{\TSet} > 1$ and $\qpElm$ is such that there is an $\xElm \in
\QPEVSet{\qpElm}$ for which $\QPDepSet(\qpElm, \xElm) \neq \emptyset$.
Indeed, it holds that $\card{\SpcSet[\TSet \to \DSet](\qpElm)} =
\prod_{\xElm \in \QPEVSet{\qpElm}} \card{\DSet}^{\card{\TSet} \cdot
\card{\DSet}^{\card{\TSet} \cdot \card{\QPDepSet(\qpElm, \xElm)}}} >
\prod_{\xElm \in \QPEVSet{\qpElm}} \card{\DSet}^{\card{\TSet} \cdot
\card{\DSet}^{\card{\QPDepSet(\qpElm, \xElm)}}} = \card{\TSet \to
\SpcSet[\DSet](\qpElm)}$.
So, there are much more dependence maps, a number double exponential in
$\card{\TSet}$, than possible adjoint functions, whose number is only
exponential in this value.

Furthermore, observe that the simple set
$\QPSet[\exists^{*}\forall^{*}](\VSet) \defeq \set{ \qpElm \in \QPSet(\VSet)
}{ \exists i \in \numcc{0}{\card{\qpElm}} \:.\: \QPAVSet{(\qpElm)_{< i}} =
\emptyset \wedge \QPEVSet{(\qpElm)_{\geq i}} = \emptyset }$, for $\VSet
\subseteq \VarSet$, is the maximal class of quantification prefixes that
admits only elementary dependence maps over $\TSet \to \DSet$, i.e., it is
such that each $\spcFun \in \SpcSet[\TSet \to \DSet](\qpElm)$ is elementary,
for all $\qpElm \in \QPSet[\exists^{*}\forall^{*}](\VSet)$.
This is due to the fact that there are no functional dependences between
variables, i.e., for each $\xElm \in \QPEVSet{\qpElm}$, it holds that
$\QPDepSet(\qpElm, \xElm) = \emptyset$.

Finally, we can introduce a new very important semantics for  syntactic
fragments, which is based on the concept of elementary dependence map over
strategies, and we refer to the related satisfiability concept as
elementary satisfiability, in symbols $\emodels$.

Intuitively, such a semantics has the peculiarity that a strategy, used in
an existential quantification in order to satisfy a formula, is only chosen
between those that are elementary w.r.t. the universal quantifications.
In this way, when we have to decide what is its value $\cElm$ on a given
track $\trkElm$, we do it only in dependence of the values on the same track
of the strategies so far quantified, but not on their whole structure, as it
is the case instead of the classic semantics.
This means that $\cElm$ does not depend on the values of the other
strategies on tracks $\trkElm'$ that extend $\trkElm$, i.e., it does not
depend on future choices made on $\trkElm'$.
In addition, we have that $\cElm$ does not depend on values on parallel
tracks $\trkElm'$ that only share a prefix with $\trkElm$, i.e., it is
independent on choices made on the possibly alternative futures $\trkElm'$.

The elementary semantics of  formulas involving atomic propositions,
Boolean connectives, temporal operators, and agent bindings is defined as
for the classic one, where the modeling relation $\models$ is substituted
with $\emodels$, and we omit to report it here.
In the following definition, we only describe the part concerning the
quantification prefixes.

Let $\GName$ be a , $\sElm \in \StSet$ one of its states, and $\qpElm
\psi$ an  formula, where $\psi$ is agent-closed and $\qpElm \in
\QPSet(\free{\psi})$.
Then $\GName, \emptyfun, \sElm \emodels \qpElm \psi$ if there is an
elementary dependence map $\spcFun \in \ESpcSet[\StrSet(\sElm)](\qpElm)$
for $\qpElm$ over $\StrSet(\sElm)$ such that $\GName, \spcFun(\asgFun),
\sElm \emodels \psi$, for all $\asgFun \in \AsgSet(\QPAVSet{\qpElm},
\sElm)$.

It is immediate to see a strong similarity between the statement of
Corollary <ref> of  strategy quantification and the
previous definition.
The only crucial difference resides in the choice of the kind of dependence

Moreover, observe that, differently from the classic semantics, the
quantifications in the prefix are not treated individually but as an atomic
This is due to the necessity of having a strict correlation between the
point-wise structure of the quantified strategies.

It can be interesting to know that we do not define an elementary
semantics for the whole , since we are not able, at the moment, to
easily use the concept of elementary dependence map, when the
quantifications are not necessarily grouped in prefixes, i.e., when the
formula is not in prenex normal form.
In fact, this may represent a challenging problem, whose solution is left
to future works.

Due to the new semantics of , we have to redefine the related concepts
of model and satisfiability, in order to differentiate between the classic
relation $\models$ and the elementary one $\emodels$.
Indeed, as we show later, there are sentences that are satisfiable but not
elementary satisfiable and vice versa.

We say that a  $\GName$ is an elementary model of an 			sentence $\varphi$, in symbols $\GName \emodels \varphi$, if $\GName,
\emptyfun, \sElm[0] \emodels \varphi$.

In general, we also say that $\GName$ is a elementary model for
$\varphi$ on $\sElm \in \StSet$, in symbols $\GName, \sElm \emodels
\varphi$, if $\GName, \emptyfun, \sElm \emodels \varphi$.

An  sentence $\varphi$ is elementarily satisfiable if there
is an elementary model for it.

We have to modify the concepts of implication and equivalence, as well.
Indeed, also in this case we can have pairs of equivalent formulas that are
not elementarily equivalent, and vice versa.
Thus, we have to be careful when we use natural transformation between
formulas, since it can be the case that they preserve the meaning only under
the classic semantics.
An example of this problem can arise when one want to put a formula in .

Given two  formulas $\varphi_{1}$ and $\varphi_{2}$ with
$\free{\varphi_{1}} = \free{\varphi_{2}}$, we say that $\varphi_{1}$
elementarily implies $\varphi_{2}$, in symbols $\varphi_{1}
\eimplies \varphi_{2}$, if, for all s $\GName$, states $\sElm \in
\StSet$, and $\free{\varphi_{1}}$-defined $\sElm$-total assignments
$\asgFun \in \AsgSet(\free{\varphi_{1}}, \sElm)$, it holds that if
$\GName, \asgFun, \sElm \emodels \varphi_{1}$ then $\GName, \asgFun, \sElm
\emodels \varphi_{2}$.
Accordingly, we say that $\varphi_{1}$ is elementarily equivalent
to $\varphi_{2}$, in symbols $\varphi_{1} \!\eequiv\! \varphi_{2}$, if
both $\varphi_{1} \!\eimplies\! \varphi_{2}$ and $\varphi_{2}
\!\eimplies\! \varphi_{1}$ hold.

Elementariness and non-elementariness

Finally, we show that the introduced concept of elementary satisfiability is
relevant to the context of our logic, as its applicability represents a
demarcation line between “easy” and “hard” fragments of .
Moreover, we believe that it is because of this fundamental property that
several well-known temporal logics are so robustly decidable <cit.>.

It is interesting to observe that, for every  $\GName$ and
[$0$-alt] sentence $\varphi$, it holds that $\GName \models \varphi$
iff $\GName \emodels \varphi$.
This is an immediate consequence of the fact that all quantification
prefixes $\qpElm$ used in $\varphi$ belong to
$\QPSet[\exists^{*}\forall^{*}](\VSet)$, for  a given set $\VSet \subseteq
\VarSet$ of variables.
Thus, as already mentioned, the related dependence maps on strategies
$\spcFun \in \SpcSet[\StrSet( {\sElm[0]} )](\qpElm)$ are necessarily

By Corollary <ref> of  strategy quantification, it is
easy to see that the following coherence property about the elementariness
of the  satisfiability holds.
Intuitively, it asserts that every elementarily satisfiable sentence in
is satisfiable too.

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

The proof proceeds by induction on the structure of the formula.
For the sake of succinctness, we only show the crucial case of principal
subsentences $\phi \in \psnt{\varphi}$, i.e., when $\phi$ is of the form
$\qpSym \psi$, where $\qpElm \in \QPSet(\free{\psi})$ is a quantification
prefix, and $\psi$ is an agent-closed formula.

Suppose that $\GName, \emptyfun, \sElm \emodels \qpSym \psi$.
Then, by Definition <ref> of 			elementary semantics, there is 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), \sElm \emodels \psi$.
Now, by the inductive hypothesis, there is a dependence map $\spcFun \in
\SpcSet[ {\StrSet(\sElm)} ](\qpElm)$ such that, for all assignments
$\asgFun \in \AsgSet(\QPAVSet{\qpElm}, \sElm)$, it holds that $\GName,
\spcFun(\asgFun), \sElm \models \psi$.
Hence, by Corollary <ref> of  strategy quantification,
we have that $\GName, \emptyfun, \sElm \models \qpSym \psi$.

However, it is worth noting that the converse property may not hold, as we
show in the next theorem, i.e., there are sentences in  that are
satisfiable but not elementarily satisfiable.

Note that the following results already holds for .

There exists a satisfiable [$1$-ag, $2$-var, $1$-alt] sentence in
that is not elementarily satisfiable.

Consider the [$1$-ag, $2$-var, $1$-alt] sentence $\varphi \defeq
\varphi_{1} \wedge \varphi_{2}$ in   where $\varphi_{1} \defeq \qpSym
(\psi_{1} \wedge \psi_{2})$, with $\qpSym \defeq \AAll{\xSym}
\EExs{\ySym}$, $\psi_{1} \defeq (\alpha, \xSym) \X \pSym \leftrightarrow
(\alpha,\ySym) \X \neg \pSym$, and $\psi_{2} \defeq (\alpha, \xSym) \X \X
\pSym \leftrightarrow (\alpha, \ySym) \X \X \pSym$, and $\varphi_{2}
\defeq \AAll{\xSym} (\alpha, \xSym) \X ((\EExs{\xSym} (\alpha, \xSym) \X
\pSym) \wedge (\EExs{\xSym} (\alpha, \xSym) \X \neg \pSym))$.

Moreover, note that the [$1$-ag, $1$-var, $0$-alt] sentence
$\varphi_{2}$ is equivalent to the  formula $\A \X ((\E \X \pSym)
\wedge (\E \X \neg \pSym))$.

Then, it is easy to see that the turn-based  $\GName[Rdc]$ of
Figure fig:lmm:qptl(rdc) satisfies $\varphi$.
Indeed, $\GName[Rdc], \spcFun(\asgFun), \sSym[0] \models \psi_{1} \wedge
\psi_{2}$, for all assignments $\asgFun \in \AsgSet(\{ \xSym \},
\sSym[0])$, where the non-elementary dependence map $\spcFun \in \SpcSet[
{\StrSet(\sSym[0])} ](\qpSym)$ is such that
$\spcFun(\asgFun)(\ySym)(\sSym[0]) = \neg \asgFun(\xSym)(\sSym[0])$ and
$\spcFun(\asgFun)(\ySym)(\sSym[0] \cdot \sElm[i]) =
\asgFun(\xSym)(\sSym[0] \cdot \sElm[1 - i])$, for all $i \in \{ 0, 1 \}$.

Now, let $\GName$ be a generic .

If $\GName \not\models \varphi$, by Theorem <ref> of
elementary coherence, it holds that $\GName \not\emodels \varphi$.

Otherwise, we have that $\GName \models \varphi$ and, in particular,
$\GName \models \varphi_{1}$, which means that $\GName \models \qpSym
(\psi_{1} \wedge \psi_{2})$.
At this point, to prove that $\GName \not\emodels \varphi$, we show that,
for all elementary dependence maps $\spcFun \in \ESpcSet[
{\StrSet(\sElm[0])} ](\qpSym)$, there exists an assignment $\asgFun \in
\AsgSet(\{ \xSym \}, \sElm[0])$ such that $\GName, \spcFun(\asgFun),
\sElm[0] \not\emodels \psi_{1} \wedge \psi_{2}$.

To do this, let us fix an elementary dependence map $\spcFun$ and an
assignment $\asgFun$.
Also, assume $\sElm[1] \defeq \trnFun(\sElm[0], \allowbreak
\emptyset[\alpha \mapsto \asgFun(\xSym)(\sElm[0])])$ and

* $\pSym \in \labFun(\sElm[1])$ iff $\pSym \in \labFun(\sElm[2])$.

In this case, we can easily observe that $\GName, \spcFun(\asgFun),
\sElm[0] \not\models \psi_{1}$ and consequently, by
Theorem <ref>, it holds that $\GName,
\spcFun(\asgFun), \sElm[0] \not\emodels \psi_{1} \wedge \psi_{2}$.
So, we are done.

* $\pSym \in \labFun(\sElm[1])$ iff $\pSym \not\in \labFun(\sElm[2])$.

If $\GName, \spcFun(\asgFun), \sElm[0] \not\models \psi_{2}$ then, by
Theorem <ref>, it holds that $\GName,
\spcFun(\asgFun), \sElm[0] \not\emodels \psi_{1} \wedge \psi_{2}$.
So, we are done.

Otherwise, let $\sElm[3] \defeq \trnFun(\sElm[1], \emptyset[\alpha
\mapsto \asgFun(\xSym)(\sElm[0] \cdot \sElm[1])])$ and $\sElm[4]
\defeq \trnFun(\sElm[2], \emptyset[\alpha \mapsto
\spcFun(\asgFun)(\ySym)(\sElm[0] \cdot \sElm[2])])$.
Then, it holds that $\pSym \in \labFun(\sElm[3])$ iff $\pSym \in
\labFun(\sElm[4])$.

Now, consider a new assignment $\asgFun' \in \AsgSet(\{ \xSym \},
\sElm[0])$ such that $\asgFun'(\xElm)(\sElm[0] \cdot \sElm[2]) =
\asgFun(\xElm)(\sElm[0] \cdot \sElm[2])$ and $\pSym \in
\labFun(\sElm[3]')$ iff $\pSym \not\in \labFun(\sElm[4])$, where
$\sElm[3]' \defeq \trnFun(\sElm[1], \emptyset[\alpha \mapsto
\asgFun'(\xSym)(\sElm[0] \cdot \sElm[1])])$.
Observe that the existence of such an assignment, with particular
reference to the second condition, is ensured by the fact that $\GName
\models \varphi_{2}$.

At this point, due to the elementariness of the dependence map
$\spcFun$, we have that $\spcFun(\asgFun')(\ySym)(\sElm[0] \cdot
\sElm[2]) = \spcFun(\asgFun)(\ySym)(\sElm[0] \cdot \sElm[2])$.
Consequently, it holds that $\sElm[4] = \trnFun(\sElm[2],
\emptyset[\alpha \mapsto \spcFun(\asgFun')(\ySym)(\sElm[0] \cdot
\sElm[2])])$.
Thus, $\GName, \spcFun(\asgFun'), \sElm[0] \not\models \psi_{2}$,
which implies, by Theorem <ref>, that $\GName,
\spcFun(\asgFun'), \sElm[0] \not\emodels \psi_{1} \wedge \psi_{2}$.
So, we are done.

Thus, the thesis of the theorem holds.

The following corollary is an immediate consequence of the previous theorem.

It is interesting to note that, at the moment, we do not know if such a
result can be extended to the simpler  fragment.

There exists a satisfiable [$1$-ag, $2$-var, $1$-alt] sentence in
that is not elementarily satisfiable.

It is worth remarking that the kind of non-elementariness of the
sentence $\varphi$ shown in the above theorem can be called
essential, i.e., it cannot be eliminated, due to the fact that
$\varphi$ is satisfiable but not elementarily satisfiable.
However, there are different sentences, such as the conjunct
$\varphi_{1}$ in $\varphi$, having both models on which they are
elementarily satisfiable and models, like the  $\GName[Rdc]$, on
which they are only non-elementarily satisfiable.
Such a kind of non-elementariness can be called non-essential,
since it can be eliminated by an opportune choice of the underlying model.
Note that a similar reasoning can be done for the dual concept of
elementariness, which we call essential

Before continuing, we want to show the reason why we have redefined the
concepts of implication and equivalence in the context of elementary

Consider the [$1$-ag, $2$-var, $1$-alt] sentence $\varphi_{1}$ used in
Theorem <ref> of  non-elementariness.
It is not hard to see that it is equivalent to the [$1$-ag, $1$-var,
$0$-alt] $\varphi' \defeq (\EExs{\xSym} (\alpha, \xSym) \psi_{1}
\leftrightarrow \EExs{\xSym} (\alpha, \xSym) \psi_{2}) \wedge (\EExs{\xSym}
(\alpha, \xSym) \psi_{3} \leftrightarrow \EExs{\xSym} (\alpha, \xSym)
\psi_{4})$, where $\psi_{1} \defeq \X (\pSym \wedge \X \pSym)$, $\psi_{2}
\defeq \X (\neg \pSym \wedge \X \pSym)$, $\psi_{3} \defeq \X (\pSym \wedge
\X \neg \pSym)$, and $\psi_{4} \defeq \X (\neg \pSym \wedge \X \neg \pSym)$.
Note that $\varphi'$ is in turn equivalent to the  formula $(\E
\psi_{1} \leftrightarrow \E \psi_{2}) \wedge (\E \psi_{3} \leftrightarrow \E
\psi_{4})$.
However, $\varphi_{1}$ and $\varphi'$ are not elementarily equivalent, since
we have that $\GName[Rdc] \not\emodels \varphi_{1}$ but $\GName[Rdc]
\emodels \varphi'$, where $\GName[Rdc]$ is the  of
Figure fig:lmm:qptl(rdc).

At this point, we can proceed with the proof of the elementariness of
satisfiability for .
It is important to note that there is no gap, in our knowledge, between the
logics that are elementarily satisfiable and those that are not, since the
fragment [$1$-ag, $2$-var, $1$-alt] used in the previous theorem
cannot be further reduced, due to the fact that otherwise it collapses into

Before starting, we have to describe some notation regarding classic
two-player games on infinite words <cit.>, which are used here as a
technical tool.
Note that we introduce the names of scheme and match in place of the more
usual strategy and play, in order to avoid confusion between the concepts
related to a  and those related to the tool.

A two-player arena (, for short) is a tuple $\AName \defeq
\TPAStruct$, where $\NdESet$ and $\NdOSet$ are non-empty non-intersecting
sets of nodes for player even and odd, respectively,
$\EdgRel \defeq \EdgERel \cup \EdgORel$, with $\EdgERel \subseteq \NdESet
\times \NdOSet$ and $\EdgORel \subseteq \NdOSet \times \NdESet$, is the
edge relation between nodes, and $\nElm[0] \in \NdOSet$ is a
designated initial node.

An even position in $\AName$ is a finite non-empty sequence of nodes
$\posElm \in \NdESet^{+}$ such that $(\posElm)_{0} = \nElm[0]$ and, for all
$i \in \numco{0}{\card{\posElm} - 1}\!$, there exists a node $\nElm \in
\NdOSet$ for which $((\posElm)_{i}, \nElm) \in \EdgERel$ and $(\nElm,
(\posElm)_{i + 1}) \in \EdgORel$ hold.
In addition, an odd position in $\AName$ is a finite non-empty
sequence of nodes $\posElm = \posElm' \cdot \nElm \in \NdESet^{+} \cdot
\NdOSet$, with $\nElm \in \NdOSet$, such that $\posElm'$ is an even position
and $(\lst{\posElm'}, \nElm) \in \EdgERel$.

An even (resp., odd) scheme in $\AName$ is a function
$\scheFun : \PosESet \to \NdOSet$ (resp., $\schoFun : \PosOSet \to
\NdESet$) that maps each even (resp., odd) position to an odd (resp., even)
node in a way that is compatible with the edge relation $\EdgERel$ (resp.,
$\EdgORel$), i.e., for all $\posElm \in \PosESet$ (resp., $\posElm \in
\PosOSet$), it holds that $(\lst{\posElm}, \scheFun(\posElm)) \in \EdgERel$
(resp., $(\lst{\posElm}, \schoFun(\posElm)) \in \EdgORel$).

By $\SchESet$ (resp., $\SchOSet$) we indicate the sets of even (resp., odd)

A match in $\AName$ is an infinite sequence of nodes $\mtcElm \in
\NdESet^{\omega}$ such that $(\mtcElm)_{0} = \nElm[0]$ and, for all $i \in
\SetN$, there exists a node $\nElm \in \NdOSet$ such that $((\mtcElm)_{i},
\nElm) \in \EdgERel$ and $(\nElm, (\mtcElm)_{i + 1}) \in \EdgORel$.

By $\MtcSet$ we denote the set of all matches.

A match map $\mtcFun : \SchESet \times \SchOSet \to \MtcSet$ is a
function that, given two schemes $\scheFun \in \SchESet$ and $\schoFun \in
\SchOSet$, returns the unique match $\mtcElm = \mtcFun(\scheFun, \schoFun)$
such that, for all $i \in \SetN$, it holds that $(\mtcElm)_{i + 1} =
\schoFun((\mtcElm)_{\leq i} \cdot \scheFun((\mtcElm)_{\leq i}))$.

A two-player game (, for short) is a tuple $\HName \defeq
\TPGStruct$, where $\AName$ is a  and $\WinSet \subseteq \MtcSet$.

On one hand, we say that player even wins $\HName$ if there exists an even
scheme $\scheFun \in \SchESet$ such that, for all odd schemes $\schoFun \in
\SchOSet$, it holds that $\mtcFun(\scheFun, \schoFun) \in \WinSet$.
On the other hand, we say that player odd wins $\HName$ if there exists an
odd scheme $\schoFun \in \SchOSet$ such that, for all even schemes $\scheFun
\in \SchESet$, it holds that $\mtcFun(\scheFun, \schoFun) \not\in \WinSet$.

In the following, for a given binding prefix $\bpElm \in \BndSet(\VSet)$
with $\VSet \subseteq \VarSet$, we denote by $\bndFun[\bpElm] : \AgSet \to
\VSet$ the function associating with each agent the related variable in
$\bpElm$, i.e., for all $\aElm \in \AgSet$, there is $i \in
\numco{0}{\card{\bpElm}}$ such that $(\bpElm)_{i} = (\aElm,
\bndFun[\bpElm](\aElm))$.

As first step towards the proof of the elementariness of , we have to
give a construction of a two-player game, based on an a priori chosen ,
in which the players are explicitly viewed one as a dependence map and the
other as a valuation, both over actions.
This construction results to be a deep technical evolution of the proof
method used for the dualization of alternating automata on infinite
objects <cit.>.

Let $\GName$ be a , $\sElm \in \StSet$ one of its states, $\PSet
\subseteq \PthSet(\sElm)$ a set of paths, $\qpElm \in \QPSet(\VSet)$ a