Game-Theoretic Semantics for ATL+ with Applications to Model Checking
Valentin Goranko Antti Kuusisto Raine Rönnholm


An SDP-Based Algorithm for

 Linear-Sized Spectral Sparsification
    Yin Tat Lee

Microsoft Research
 Redmond, USA


He Sun

The University of Bristol

Bristol, UK



    
=====================================================================================================





We develop a game-theoretic semantics () for the fragment  of the alternating-time temporal logic 
, thereby extending the recently introduced for .

We show that the game-theoretic semantics is equivalent to the standard compositional semantics of with perfect-recall strategies. 
Based on the new semantics, we provide an analysis of the memory and time resources needed for model checking  and show that strategies of the verifier that use only a very limited amount of memory suffice. Furthermore, using the , we provide a new algorithm for model checking and identify a natural hierarchy of tractable fragments of that substantially extend . 



























§ INTRODUCTION







The full Alternating-time Temporal Logic 
<cit.> is one of the main logical systems used for formalising and verifying strategic reasoning about agents in multi-agent systems. It is very expressive, and that expressiveness comes at a high (2-EXPTIME) price of computational complexity of model checking. Its basic
fragment —which can be regarded as the multi-agent extension of CTL— has, on the other hand, tractable model checking but its expressiveness is rather limited. In particular, only allows expressing strategic objectives of the type AΦ where Φ is a simple temporal goal involving a single temporal operator. The intermediate fragment  naturally emerges as a good alternative, essentially extending to allow  expressing strategic objectives which are Boolean combinations of simple temporal goals. The price for this is a reasonably higher computational complexity of model checking , viz. PSPACE-completeness <cit.>. Still, the PSPACE-completeness result alone gives a rather crude estimate of the amount of computational resources, such as memory, needed for model checking .





Main ideas and contributions. 
In this paper we take an alternative approach to the semantic analysis and model checking of fragments of , concentrating in particular on fragments of . Our analysis is not based on the standard compositional semantics but on a new, game-theoretic semantics (). The main aims and contributions of the paper are three-fold:



  * We introduce an adequate game-theoretic semantics for  equivalent to the standard (perfect-recall) compositional semantics.


  * We propose new model checking algorithms for and some of its fragments, using the developed here, rather than the standard semantics. We also analyse more precisely the use of memory resources in via .




  * We apply the -based approach to model checking in order to identify new tractable fragments of .






The main part of the paper consists of a detailed presentation and analysis of the new for .
In particular, we obtain results similar to those in our earlier work <cit.>, where we defined a for .

We establish, inter alia, the surprising result 
that it is always sufficient to
consider finite paths only when 
formulae are evaluated via , even when considering infinite models.

Since we are dealing with  as
opposed to , a range of new technical ideas and mechanisms are
needed for the correct evaluation of multiple temporal
goals pursued simultaneously by the proponent coalition.



The approach via enables us, inter alia, to perform a more precise analysis on the memory resources needed for evaluating -formulae
than the algorithm from <cit.>  

which employs a mix of a path construction procedure for checking strategic formulae AΦ on one hand, and the standard labelling algorithm

on the other hand.



Our model checking algorithm for follows uniformly a procedure directly based on and also enables us, inter alia, to identify and correct a flaw in the model checking procedure of <cit.> and some of the claims on which it is based. Yet, the PSPACE upper bound result of <cit.> is easily confirmed by our algorithm, and we provide a new  simple proof of that result. Besides new methods, we use some nice ideas from <cit.>.

As a new complexity result obtained via , we identify a

natural hierarchy of fragments of that 
extend and have tractable (PTIME-complete) model checking.
The hierarchy is based on bounding the
Boolean strategic width 



of formulae.

We denote the new fragments in the hierarchy by ^k for different positive integers k.





Here ^k contains those
formulae of  where subformulae AΦ are restricted such that Φ is a
Boolean combination of at most k formulae. Note that thus ^1 corresponds to plain .





The current paper
extends the results in <cit.>, where a for is
considered, in various non-trivial ways. 

Firstly, several new ideas and technical notions, such as the role of a seeker and
the use of a truth function, are introduced here in order to enable the transition
from to in the setting.

Secondly, a useful and generally elucidating link between our and Büchi games is identified. That link applies readily also to the simpler evaluation games in <cit.>.

Thirdly, and most importantly, we show how to use the new upgraded semantics in a model checking procedure for and the fragments ^k. This would not have been possible with the semantics of <cit.>.




The current paper is the journal version of <cit.>. We extend
<cit.> by, inter alia, including a range of new
results on systems of bounded semantics based on finite transducers.
We analyse the amount of memory resources needed for winning strategies and establish tight lower and upper bounds for it.

We notice that in transducer based semantics, an exponential amount of memory with respect to formula size is required.

However, only a linear amount of this is actually used in any concrete single evaluation process of a formula. 

Based on this we argue that the transducer based approach does not give a complete analysis for the requirement of memory resources.








Other, indirectly related works include a series of papers, incl. 
<cit.>, 
<cit.>, 
<cit.>,  
<cit.> 
on a variety of explicit strategy logics, as the development of game-theoretic semantics is a natural challenge arising in the present context.




Structure of the paper.
After the preliminaries in Section <ref>,  we define a bounded, finitely bounded, and unbounded game-theoretic semantics for in Section <ref>. In Section <ref> we analyse the various properties of the novel systems of . In Section <ref> we prove equivalence of the bounded and unbounded versions with the standard compositional semantics of with perfect recall strategies. In Section <ref> we apply the to the model checking problem for and identify a hierarchy of tractable fragments of it.  In Section <ref> we study the transducer-based bounded memory semantics for these fragments. We then conclude in Section <ref>. 











§ PRELIMINARIES






In this section we define concurrent game models and the syntax and the (perfect-recall) semantics for . We also introduce some new terminology and notations that will be used later in this paper.



A concurrent game model 
() 

is a tuple 

    ℳ := (, , , , d, o, v)


which consists of: 
 
– The following non-empty sets:
agents = {a_1,…,a_k}, 

states , 

proposition symbols , 

actions ; 

– The following functions: an action function 
d:×→𝒫()∖{∅} 
which assigns a non-empty set of actions available to each agent at each state; a
transition function o which assigns an outcome state
o(q, )

to each state q∈ and action profile (a 
tuple of actions = (α_1,…,α_k)

such that α_i∈ d(a_i,q) for each a_i∈); 
and finally, a valuation function v:→𝒫(). 



We use symbols p, p_0, p_1, … 
to denote proposition symbols and q, q_0, q_1, …  to denote states.
Sets of agents 

are called coalitions. The complement  
A= ∖ A of a coalition A is the opposing coalition of A. The set (A,q) of action tuples available to  coalition A at state q∈ is defined as 
(A,q):={(α_i)_a_i∈ A|α_i∈ d(a_i,q)  for each  a_i∈ A}.





  

Let ℳ^* = (, , , , d, o, v), where: 

= {a_1,a_2},   = {q_0,q_1,q_2,q_3,q_4},   = {p_1,p_2,p_3},  
 = {α,β},  






and d, o and v defined as shown below:





    = {a_1,a_2},   = {q_0,q_1,q_2,q_3,q_4}
        = {p_1,p_2,p_3},   = {α,β}
       d(a_2,q_0)=d(a_1,q_1)={α,β}  and else   d(a_i,q_i)={α}
       o(q_0,αα)=q_1,   o(q_0,αβ)=q_2,   o(q_1,αα)=q_2, 
       o(q_1,αβ)=q_3,   o(q_2,αα)=q_1   and   o(q_3,αα)=q_3 
       v(p_1)={q_2,q_4},   v(p_2)={q_3}  and  v(p_3)={q_1}.








[scale=1.8]
	at (-0.3,0) [draw, circle] (0) p_1;
	at (1,0) [draw, circle] (1) p_3;
	at (-0.3,1) [draw, circle] (2) p_1;
	at (1,1) [draw, circle] (3) p_2;
	at (2.3,0) [draw, circle] (4) p_1;
	at (-1.5,1.3) ℳ^*:;
	at (-0.6,-0.3) q_0;
	at (1.3,-0.3) q_1;
	at (-0.6,1.3) q_2;
	at (1.3,1.3) q_3;
	at (2.6,0.3) q_4;
	[-latex] (0) to node[below] αα (1);
	[-latex] (0) to node[left] αβ (2);
	[-latex] (2) to node[above] αα (3);
	[-latex, bend left] (1) to node[left] αα (3);
	[-latex, bend left] (3) to node[right] αα (1);
	[-latex] (1) to node[below] βα (4);
	[-latex, loop right] (4) to node αα (4);















Let ℳ = (, , , , d, o, v) be a .

A path
in ℳ is a
sequence Λ:ℕ→ of states 
such that for each n∈ℕ, we have 
Λ[n+1] = o(Λ[n],) for
some admissible action profile 
 in Λ[n]. 

A finite path (aka history)
is a finite prefix sequence of a path in ℳ.

We let (ℳ)
denote the set of all paths in ℳ and _fin(ℳ)
the set of all finite paths in ℳ.[Note that, accordingly this terminology, a “path” always refers to an infinite path. We use this terminology since we mostly consider infinite paths.]



A positional strategy of an agent a∈ is a function s_a: → such that s_a(q)∈ d(a,q) for each q∈. 

A perfect-recall strategy, or hereafter just  strategy, of agent a∈ is a function  s_a: _fin(ℳ)→ such that s_a(λ)∈ d(a,λ[k]) for each λ∈_fin(ℳ) where λ[k] is the last state in λ. 

A collective strategy S_A for A⊆ is a tuple of individual strategies, one for each agent in A. 

With (q,S_A) we denote the set of all paths emerging in plays beginning from q where the agents in A follow the strategy S_A.











The formulae of are defined by the following grammar.





State formulae: ::= p ||∨|A   (p∈)

Path formulae: 
 ::=||∨||

Other Boolean connectives are defined as usual,
and furthermore, ,  and   are
abbreviations for ⊤, (⊤), and 
() respectively.

With Φ and Ψ we denote path formulae only; φ, ψ, and χ denote any formulae.






Let ℳ be a .





Truth of state and path formulae of is
defined, respectively,
with respect to states q∈ St and paths Λ∈(ℳ), inductively as follows, where φ, ψ are state formulae:




  * ℳ,q p  iff  q∈ v(p) (for p∈).


  * ℳ,qφ iff ℳ,qφ.


  * ℳ,qφ∨ψ iff ℳ,qφ or ℳ,qψ.


  * ℳ,qAΦ iff there exists a (perfect-recall) strategy S_A such that ℳ,ΛΦ for each Λ∈(q,S_A).


  * ℳ,Λφ
iff ℳ,Λ[0]φ. 



  * ℳ,Λφ iff ℳ,Λ[1]φ.


  * ℳ,ΛΦ iff ℳ,ΛΦ.


  * ℳ,ΛΦ∨Ψ iff ℳ,ΛΦ or ℳ,ΛΨ.


  * ℳ,Λφψ iff
there exists i∈ℕ such that ℳ,Λ[i]ψ and ℳ,Λ[j]φ  for all j < i.












The set of subformulae, (φ), of a formula φ is defined as usual. Subformulae with a temporal operator as the main connective will be called temporal subformulae, while subformulae with  as the main connective are strategic subformulae. The subformula Ψ of a formula 
φ = AΨ is called the temporal objective of φ. 






We also define the set 𝐴𝑡(Φ) of relative atoms of Φ as follows:








  * 𝐴𝑡(χ∨χ^') = 𝐴𝑡(χ)∪𝐴𝑡(χ^')
and 𝐴𝑡(χ) = 𝐴𝑡(χ).


  * 𝐴𝑡(Aχ) = {Aχ} and 𝐴𝑡(p) = {p}

for p∈Π.


  * 𝐴𝑡(χχ^') = {χχ^'}

and 𝐴𝑡(χ) = {χ}.



We say that χ∈𝐴𝑡(Φ) occurs positively (resp. negatively)   in Φ if χ has an occurrence in the scope of an even (resp. odd) number of negations in Φ.




We denote by SUB_𝐴𝑡(Φ)
the subset of (Φ) containing 
all relative atoms of Φ 
and also all Boolean combinations χ of
these relative atoms such that χ∈SUB(Φ).








Let 
φ^*:= p_2∧ (p_1∨a_1Ψ), 
φ^*:= a_1Ψ, where


    Ψ:= ( p_3∧a_2 p_1)  ∨  ( p_1∧( p_1) p_2).

Written without using abbreviations, Ψ  becomes


    ( p_3 ∨a_2 p_1)∨((⊤ p_1) ∨(( p_1) p_2)).

Here 𝐴𝑡(Ψ)={ p_3,a_2 p_1,⊤ p_1, ( p_1) p_2}, where a_2 p_1 is a state formula and the rest are path formulae. The formula p_3 occurs negatively in Ψ and the rest of the formulae in 𝐴𝑡(Ψ) occur positively in Ψ.








§ GAME-THEORETIC SEMANTICS




In this section we define 
bounded, finitely bounded 
and unbounded evaluation games for .

These games give rise to three different systems of semantics, namely, the bounded, finitely  bounded and unbounded  for .





These systems of semantics were defined for plain already in <cit.>. The principal difference between
the bounded and unbounded is that the bounded variant forces games to 
end after a finite number of steps. This is a significant difference achieved, as we shall see,
via requiring the players to choose ordinal numbers that can intuitively be considered to determine
upper bounds for game durations (see also Example <ref>). In the unbounded semantics, no such ordinals are
used, and the games can continue for infinitely many rounds.



As explained in
<cit.>, the difference between bounded and
unbounded semantics is directly analogous to the difference between for-loops and 
while-loops. Indeed, for-loops require an extra parameter that determines the number of loop iterations, and
while-loops can possibly loop infinitely long.



Having both the bounded and unbounded semantics at our disposal will prove beneficial in
Section <ref> where we discuss model checking. Indeed, we shall need
the unbounded semantics for connecting fragments of to Büchi games and thereby obtaining
novel tractability results. On the other hand, we shall need the
bounded semantics for our proof strategy of Theorem <ref> which
confirms the PSPACE-completeness of model checking.




The unbounded and bounded semantics will be proved equivalent below. 
The finitely bounded semantics is not equivalent to these two. The difference 
between the finitely bounded and bounded semantics is that the parameters 
with which the players force the games to be finite are possibly infinite 
ordinals in bounded semantics and finite ordinals in finitely bounded semantics.
The finitely bounded and bounded semantics are equivalent over finite models but
not over infinite ones. The reason for introducing finitely bounded semantics is that it
provides a novel, interesting perspective on and while still being 
equivalent over finite (but not infinite) models with the standard semantics.





Below we shall use some terminology and notational conventions introduced in 
<cit.>. 



 §.§ Evaluation games: informal description



Given a  ℳ,  a state  and a state formula φ, the 

evaluation game (ℳ, , φ) is, intuitively, 
a formal debate between two opponents, Eloise (E)  and Abelard (A), about whether the
formula φ is true at the state  in the model ℳ. Eloise claims that φ is true, so she  (initially) adopts the role of a verifier in the game,
and Abelard tries to prove the formula false, so he is (initially) the falsifier.

These roles (verifier, falsifier) can swap in the course of the game when negations are encountered in the formula. 

If ∈{ E, A}, 
then  denotes the opponent of ,   
i.e., ∈{ E, A}∖{}.


We now provide an intuitive account of the
bounded evaluation game and the bounded for .

The intuitions underlying the finitely bounded and unbounded  are similar.



A reader unfamiliar with the concept of may find it useful to
consult, for example, <cit.> for in general and 
 <cit.> or <cit.> for -specific . 

The for presented here follows the 
general principles of , with the main original 
feature being the treatment of strategic formulae AΦ.

We first give an informal account of 
the way such formulae are treated in our evaluation games. 

Formal definitions and some concrete examples will be given further, beginning from Section <ref>.



The evaluation of formulae of the type AΦ in a given model is
based on constructing finite paths in that model. 
The following two ideas are central.


Firstly, the path formula Φ in AΦ
can be divided into goals for the verifier (), these being  
the relative atoms ψ∈𝐴𝑡(Φ) that occur positively in Φ,  
and goals for the falsifier (), these being 
the relative atoms ψ∈𝐴𝑡(Φ) that occur negatively in Φ.
(Some formulae may be goals for both players.) 

For simplicity, let us assume for now that Φ is in negation normal form and all the atoms in 𝐴𝑡(Φ)  are temporal formulae of the type p.

Then the verifier's goals are eventuality statements p,
while the falsifier's goals are statements p'
that occur negated; note that the negation of p' is
equivalent to the safety statement p'.




The verifier wishes to verify her/his[The genders of the
players may be assigned randomly below at points when this causes no
ambiguities and streamlines the presentation.] goals.
The falsifier, likewise, wants to verify her/his goals, i.e.,
the falsifier wishes to falsify the related safety statements.










Secondly, every temporal goal associated with AΦ has a unique “finite determination point” 

on any given path where that goal can be verified by 
the player to whom the goal belongs. This means the following.

If a goal p of the verifier is true on an infinite path  π,
then there necessarily exists an earliest point q
on that path where the fact that p 
holds on  π becomes verified simply
because p is true at q. Indeed, the first point of π where p is
true is the finite determination point q of p.

Once p has been verified, it will remain true on π, 
no matter what happens on the path after q.

Similarly, concerning falsifier's goals, if p' is false (and thus p' true) on an infinite path π', there is a unique point where p' first becomes falsified, that point being the first state q' of π'
where p' is true. That point q' is the finite determination point of the goal p' of the falsifier.
Furthermore, p' will
remain false on the path no matter what happens further.

(Note that there is no analogous finite determination point for -formulae such as Ap on a given infinite path. Note also that we discussed only the simple temporal goals  p and p'
for simplicity, but every temporal goal—as long as it can be verified by 
the player to whom the goal belongs—does indeed have a finite determination point. This will
become clear below.) 




Now, the game-theoretic evaluation procedure of an -formula 
AΦ proceeds roughly as follows.

The verifier is controlling the agents in the coalition A and the falsifier controls the agents in the opposing coalition A=∖ A.

The players start constructing a path. (Each transition from one state to another is carried

out according to the process “𝖲𝗍𝖾𝗉  𝗉𝗁𝖺𝗌𝖾"
defined formally in Section <ref>.)


The verifier is first
given a chance to verify some of her/his goals in Φ.

The falsifier tries to prevent this and to possibly verify some of her/his own goals instead.
During this path construction/verification process, the verifier is said to have the role of the seeker. 

A player is allowed to stay as the seeker for only a finite number of rounds. This is ensured by requiring the seeker to announce an ordinal[To see why finite ordinals do not suffice in 
general relates to infinite branching. See, e.g., Example 3.11 of <cit.> for details.], 

called timer[Note that the term “timer” is used here differently from <cit.>.
], 
before the path construction process begins, and then lower the ordinal each time a new state is reached. 

The process ends when the ordinal becomes zero or when the seeker 
is satisfied, having verified some of her goals.

Since ordinals are well-founded, the process must terminate.




After the verifier has ended her/his seeker turn, the falsifier may either end the game or take the role of the seeker.

If (s)he decides to become the seeker, then (s)he sets a new
timer and the path construction 
process continues for some finite number of rounds. 

When the falsifier is satisfied,
having verified some of her/his goals,
the verifier may again take the seeker's role, and so on. 

Thus, the verifier and falsifier take turns 
being the seeker, trying to reach (verify) their goals.

The number of these alternations is bounded by a
seeker turn counter
which is a finite number that equals the total number of goals in Φ.

(The formal description of seeker turn alternation is
given in the clause “𝖣𝖾𝖼𝗂𝖽𝗂𝗇𝗀  𝗐𝗁𝖾𝗍𝗁𝖾𝗋  𝗍𝗈

𝖼𝗈𝗇𝗍𝗂𝗇𝗎𝖾  𝖺𝗇𝖽  𝖺𝖽𝗃𝗎𝗌𝗍𝗂𝗇𝗀  𝗍𝗁𝖾  𝗍𝗂𝗆𝖾𝗋" in Section <ref>.)

Each time a goal in Φ becomes verified, this is recorded in a truth function T.
(The recording of verified goals is described formally in the
process “𝖠𝖽𝗃𝗎𝗌𝗍𝗂𝗇𝗀  𝗍𝗁𝖾  𝗍𝗋𝗎𝗍𝗁  𝖿𝗎𝗇𝖼𝗍𝗂𝗈𝗇" defined
in Section <ref>.)



The truth function carries the following information at any stage of the game:






  * The verifier's goals that have been verified. 


  * The falsifier's goals that have been verified. 


  * All other goals remain open.




When neither of the players wants to become the seeker, or when the seeker turn counter becomes zero, the path construction process ends and the 
players play a standard Boolean evaluation game on Φ by using the values given by T; the open goals are given truth values as follows:





  * The verifier's open goals are (so far) not verified and thus considered false.


  * Likewise, the falsifier's open goals are (so far) not verified and thus considered false. Recall  here that the falsifier's goals occur in the scope of a negation.



Next we consider the conditions when a player is “satisfied” with the current status of the truth function T—and thus wants to end the game—and when (s)he is “unsatisfied” and wants to continue the game as the seeker.

Note that when the path construction ends, then every goal is
given a Boolean truth value based on the truth function T, as
described above. With these values, the formula Φ is either true or false.

If Φ is true with the current values based on T, then the verifier can win the Boolean game for Φ; dually, if Φ is not true with the values based on T, then the falsifier can win the Boolean game for Φ. Hence the players want to take the role of the seeker in order to modify the truth function T in such a way that the truth of Φ with respect to T changes from false to true (whence  is satisfied) or from true to false (whence  is satisfied).


The truth value of Φ with respect to T
can keep changing when T is modified, but only a finite number of changes is possible. 
Indeed, the maximum number of such truth alternations is the total number of goals in Φ.






In the general case, formulae of the type φψ, φ and (state formulae) φ may also occur in 𝐴𝑡(Φ) as goals, and Φ does not have to be in negation normal form. Formulae of the type φψ can be either verified, by showing that ψ is true, or falsified, by showing that φ is not true at related states. State formulae φ can only be verified at the initial state and the next-state-formulae φ can only be verified at the second state on the path traveled.










 §.§ Evaluation games: formal description




Now we will present the bounded evaluation game which uses the bounded transition game as a subgame for evaluating strategic subformulae. 

Interleaved with the definition we will provide, in italics, a running example that uses
ℳ^* and φ^* from Examples <ref> and <ref>
respectively.






  §.§.§ Rules of the bounded evaluation game
 

Let ℳ = (, , , , d, o, v) be a , ∈ a state, φ a state formula and Γ>0 an ordinal called a timer bound.

The -bounded evaluation game 
(ℳ, , φ,Γ) 
between the players A and E  is defined as follows.

A location of the game is a tuple (,q,ψ,T) where 
∈{ A, E},
q∈ is a state, ψ is a subformula of φ

and T is a truth (history) function, mapping some subset of (φ) into {⊤,,}.[We note here that the values of T are only modified during transtion games and that T is always a total function for all subformulae of φ that are relevant for the transition game that is played.]


The initial location of the
game is ( E,,φ,T_in),
where T_in is the empty function.


In every location (,q,ψ,T), the player  is called the verifier
and  the falsifier for that location.

Intuitively, q is the current state of the game and T encodes truth values of formulae on a path that has been constructed earlier in the game.



Each location is associated with exactly one of the rules 1–6 given below.

First we provide the rules for locations (,q,ψ,T) where ψ is
either a proposition symbol or has a Boolean connective as its
main operator:



  1.
A location (,q,p,T), where p∈,
is an ending location of the evaluation game.

If T ≠∅, 

then  wins the game if T(p) = ⊤ and else  wins.

Respectively, if T = ∅, 

then  wins if q∈ v(p) and else  wins.



  2. From a location (,q,ψ,T)
the game moves to the location (,q,ψ,T).



  3. In a location (,q,ψ∨θ,T) the player 
chooses one of the locations (,q,ψ,T) and (,q,θ,T),
which becomes the next location of the game.


We then define the rules of the evaluation game for
locations with strategic formulae as follows.






  4. Suppose a location (,q,AΦ,T) is reached.



  * If 

T ≠∅, then this location is an ending location where  wins if T(AΦ)=⊤ and else  wins. 


  * If 

T  = ∅, 
then the evaluation game enters a transition game
g(,q,AΦ,). The transition game is a
subgame to be defined later on.

The transition game eventually reaches an exit location (',q',ψ,T'),
and the evaluation game continues from that location. Note that an exit location only
ends the transition game, so exit locations of transition games and
ending locations of the evaluation game are different concepts.




The rules corresponding to the temporal connectives are defined using the truth function T
(updated in an earlier transition game) as follows.



  5.
A location (,q,φψ,T) is an ending location of the evaluation game. 

 wins if T(φψ) =⊤ and else  wins.


  6.
Likewise, a location (,q,φ,T) is an ending location. 
 
 wins if T(φ) = ⊤ and otherwise  wins.




These are the rules of the evaluation game. We note that the timer bound
 will be used only in transition games. If =ω, we say that the evaluation game is finitely bounded. 





The  initial location of the finitely bounded evaluation game 
𝒢(ℳ^*,q_0,φ^*,ω) 
(see Examples <ref> and <ref>) is ( E,q_0,a_1Ψ,∅), from where the transition game 
g( E,q_0,a_1Ψ,ω) begins.





Consider the evaluation game 𝒢^*:=𝒢(ℳ^*,q_0,φ^*,ω) (see Examples <ref> and <ref>). The game begins from the initial location ( E,q_0, p_2∧ (p_1∨a_1Ψ),∅). It is easy to see that the rule for the conjunction is that the falsifier gets to choose either of the conjuncts. So, here Abelard may first choose the next location of the game to be ( E,q_0, p_2,∅) or ( E,q_0,p_1∨a_1Ψ,∅). If Abelard chooses the first option, then the next location is ( A,q_0,p_2,∅), where Abelard loses, since q_0∉ v(p_2). 

Suppose now that Abelard chooses the second option. Now Eloise gets to  choose the next location of the game to be ( E,q_0,p_1,∅) or ( E,q_0,a_1Ψ,∅). If Eloise would choose the first, she would lose immediately since q_0∉ v(p_1). So, suppose Eloise chooses the second option. Then the transition game g( E,q_0,a_1Ψ,ω) begins.






  §.§.§ Rules of the transition game


Recall that transition games are subgames of evaluation games. Their purpose is to evaluate the truth of strategic subformulae, in a game-like fashion.  

Now we give a detailed description of transition games.[A transition game for  is similar to the `embedded game'  introduced in <cit.> for the of . The role of the seeker  here is similar to the role of the controller in that embedded game.]

A transition game

g(,q_0,AΦ,), 
where ∈{ A, E},
q_0∈, AΦ∈ and >0 is an ordinal,
is defined as follows.

 is called the verifier in the transition game. 

The game g(,q_0,AΦ,Γ)
is based on configurations, i.e.,

tuples (,q,T,n,γ,x), where  

the player ∈{𝐄,𝐀} is called the seeker; 
q is the current state; 
T:𝐴𝑡(Φ)→{⊤,,𝗈𝗉𝖾𝗇} is a 
truth function; 
n∈ℕ is a seeker turn counter (n≤ |𝐴𝑡(Φ)|);

γ is an ordinal called timer;

and x∈{ i,ii,iii } is
an index showing the current phase of the transition game.




The game g(,q_0,AΦ,) begins
at the initial configuration 
(,q_0,T_0,|𝐴𝑡(Φ)|,,i), 
with T_0(χ) = for all χ∈𝐴𝑡(Φ).




The transition game g( E,q_0,a_1Ψ,ω) begins from the initial configuration ( E,q_0,T_0,4,ω,i), since |𝐴𝑡(Ψ)|=4. (Note that the timer is initially ω in transition games occurring within finitely bounded evaluation games, but the timer will always have a finite value thereafter.)



The transition game then proceeds by iterating the phases i, ii and iii, which we first describe informally; detailed formal definitions are given afterwards.




  i. 𝖠𝖽𝗃𝗎𝗌𝗍𝗂𝗇𝗀  𝗍𝗁𝖾  𝗍𝗋𝗎𝗍𝗁  𝖿𝗎𝗇𝖼𝗍𝗂𝗈𝗇:

In this phase the  players make claims on the truth of state formulae at the current state q. If  makes some claim, then the opponent  may either: 1) accept the claim, whence truth function is updated accordingly, or 2) challenge the claim. In the latter case the transition game ends 
and truth of the claim is verified in a continued evaluation game.


  ii. 𝖣𝖾𝖼𝗂𝖽𝗂𝗇𝗀  𝗐𝗁𝖾𝗍𝗁𝖾𝗋  𝗍𝗈  𝖼𝗈𝗇𝗍𝗂𝗇𝗎𝖾  𝖺𝗇𝖽  𝖺𝖽𝗃𝗎𝗌𝗍𝗂𝗇𝗀  𝗍𝗁𝖾  𝗍𝗂𝗆𝖾𝗋:

Here the current seeker  may either continue her seeker turn and lower the value of the timer, or end her seeker turn. If  chooses the latter option, then the opponent  of the seeker may either 1) take the role of the seeker and announce a new value for the timer or 2) end the transition game, whence the formula Φ is evaluated based on current values of the truth function.


  iii. 𝖲𝗍𝖾𝗉  𝗉𝗁𝖺𝗌𝖾:

Here the verifier  chooses actions for the agents in the coalition in A at the current state q. Then  chooses actions for the agents in the opposing coalition A. After the resulting transition to a new state q' has been made, the game continues again with phase i.



We now describe the phases i, ii and iii in technical detail:



i. 𝖠𝖽𝗃𝗎𝗌𝗍𝗂𝗇𝗀  𝗍𝗁𝖾  𝗍𝗋𝗎𝗍𝗁  𝖿𝗎𝗇𝖼𝗍𝗂𝗈𝗇.

Suppose the current configuration is (,q,T,n,γ,i).

Then the truth function T is updated by considering, one by one, each formula χ∈𝐴𝑡(Φ) in some fixed order[We will see that the order here is irrelevant for the existence of winning strategies in the evaluation game. This is simply because the player with a winning strategy can make all the claims that are true and oppose all the other claims—regardless of the order in which the formulae are considered.]. 

If T(χ)≠, then the value χ cannot be updated. Else the value of χ may be modified according to the rules A – C below.




A. Updating T on temporal formulae with : Suppose

that φψ ∈  At(Φ).
Now first the verifier  may claim that ψ is true at the current state q.

If  makes that claim, then  chooses either of the following: 




  *  accepts the claim of , whence the truth function is updated so that 
φψ is assigned value ⊤ (φψ becomes verified), hereafter indicated by φψ ↦⊤.


  *  challenges the claim of , whence the transition game ends
at the exit location (,q,ψ,∅). 
(We note that, here and further, when a transition game ends, the evaluation game 
continues from the related exit location and the evaluation game will never
return to the same exited transition game again.)



If  does not claim that ψ is true at q,
then  may make that same claim (that ψ is true at q).

If  makes that claim, then the same two steps above concerning
accepting and challenging 
are followed, but with  and  swapped everywhere.



Suppose then that neither of the players claims that ψ is true at q. 

Then first  can claim that φ is false at q. 

If  makes that claim, then  chooses either of the following: 




  *  accepts the claim, whence the truth function is updated so that
φψ↦ (φψ becomes falsified).



  *  challenges the claim, whence the transition game ends
at the exit location (,q,φ,∅).



If  does not claim that φ is false at q, then  may make that claim.
If he does, then the same steps as those above are followed, but with  and  swapped.




B. Updating T on proposition symbols and strategic formulae: The

truth function can be updated on proposition symbols p∈𝐴𝑡(Φ) and formulae A'Ψ∈𝐴𝑡(Φ) only when the phase i is executed for the first time (so, q = q_0). 

In this case, given such a formula χ, first  can claim that χ


is true at q.

Now, if  accepts this claim, 
then the truth function is updated s.t. χ↦⊤. 

If  challenges the claim, 
then the transition game ends at the exit location (,q,χ,∅).

If  does not claim that χ is true at q, then  may make that claim.
If he does, then the same steps are followed, but with  and  swapped.



C. Updating T on formulae with : The

truth function can be updated on formulae of type ψ∈𝐴𝑡(Φ) only when phase i is executed for the second time in the transition game

(so, q is some successor of q_0).

First  can claim that ψ is true at q. 

If  accepts that claim, 
then the truth function is updated s.t. 
ψ↦⊤.

If  challenges the claim, 
then the transition game ends at the exit location (,q,ψ,∅).

If  does not claim that ψ is true at q, then  can make that claim.
If he does, the same steps are followed, but with  and  swapped.



Note that in points B and C, the formulae cannot be mapped to  by the truth function T. But if these formulae are left with the value , then they will be considered false by default if the transition game ends in stage ii (and the boolean game is played). Intuitively this is because if no player has claimed these formulae to be true, then players have agreed that they are indeed false.



If neither player makes any claim which would update
the value of a formula χ∈𝐴𝑡(Φ), then the value of χ is left . Once the values of the truth function T have been updated (or left as they are) for all formulae in 𝐴𝑡(Φ), a new truth function T' is obtained. 

The transition game then moves to the new configuration (,q,T^',n,γ,ii). 



 
In the configuration ( E,q_0,T_0,4,ω,i) the players begin adjusting T_0 for which initially T_0(χ)= for every χ∈𝐴𝑡(Ψ). Since it is the first round of the transition game, the value of p_3 cannot be modified, but the value of a_2 p_1 can be modified. 

Suppose that Eloise claims that a_2 p_1 is true at q_0. Now Abelard could challenge the claim, whence the transition game ends and the evaluation game continues from location ( E,q_0,a_2 p_1,∅) (which leads to a new transition game g( E,q_0,a_2 p_1,ω)). Suppose Abelard does not challenge the claim. Then a_2 p_1 is mapped to ⊤.


 
Since p_1 and ( p_1) p_2 occur positively in Φ, Eloise has interest only to verify them and Abelard has interest only to falsify them. Eloise could verify p_1 by claiming that p_1 is true, or verify ( p_1) p_2 by claiming that p_2 is true. But,  if Eloise makes either of these claims, then Abelard wins the whole evaluation game by challenging, since q_0∉ v(p_1)∪ v(p_2). Suppose that Eloise does not make any claims. 

Now, Abelard could claim that p_1 is not true, in order to falsify ( p_1) p_2. But if he does that, he loses the evaluation game if Eloise challenges, since q_0∉ v(p_1). Suppose that Abelard does not make any claims either. Then the transition game proceeds to configuration ( E,q_0,T,4,ω,ii), where T(a_2 p_1)=⊤ and T(χ)= for the other χ∈𝐴𝑡(Ψ).







ii. 𝖣𝖾𝖼𝗂𝖽𝗂𝗇𝗀  𝗐𝗁𝖾𝗍𝗁𝖾𝗋  𝗍𝗈  𝖼𝗈𝗇𝗍𝗂𝗇𝗎𝖾  𝖺𝗇𝖽  𝖺𝖽𝗃𝗎𝗌𝗍𝗂𝗇𝗀  𝗍𝗁𝖾  𝗍𝗂𝗆𝖾𝗋.

Suppose a configuration (,q,T,n,γ,ii) has been reached.

Assume first that γ≠ 0. Then the seeker  can choose whether to continue the transition game as the seeker.

If yes, then  chooses some ordinal γ'<γ and the transition game continues from (,q,T,n,γ',iii).

If  does not want to continue, or if γ = 0,
then one of the following applies.








  (a)
Suppose that n≠ 0. Then the player  
chooses whether she wishes to continue the transition game.

If yes, then  chooses an ordinal γ'< 
(so,  in fact resets the timer value)
and the transition game continues from (,q,T,n-1,γ',iii).

Otherwise the transition game ends
at the exit location (,q,Φ,T).


  (b)
Suppose that n=0. Then the transition game ends
at the exit location (,q,Φ,T).





 
In ( E,q_0,T,4,ω,ii) Eloise may decide whether to continue the transition game as the seeker. Suppose that Eloise does not continue, whence Abelard may now become the seeker and continue the transition game, or end it. If Abelard ends the transition game, then the evaluation game is continued from ( E,q_0,Ψ,T). But because T( p_3)= and T(a_2 p_1)=⊤, Eloise can then win the evaluation game by choosing the left disjunct of Ψ (recall that with these values of T Eloise is then guaranteed to win). Suppose thus that Abelard decides to become the seeker, whence he chooses some m<ω and the next configuration is ( A,q_0,T,3,m,iii).





iii. 𝖲𝗍𝖾𝗉  𝗉𝗁𝖺𝗌𝖾
[The procedure in this phase is analogous to the step game, 
(,A,q), which was introduced for the for (<cit.>).]

Suppose that the configuration is 
(,q,T,n,γ,iii).



  (a) First,  chooses an action α_i∈ d(a_i,q) for each a_i∈ A.

  (b) Then,  chooses an action α_i∈ d(a_i,q) for each a_i∈A.

The resulting action profile produces a successor state q':=o(q,α_1,…,α_k). 



The transition game then moves to the configuration 
(,q',T,n,γ,i).




 
In the configuration ( A,q_0,T,3,m,iii) Eloise (who is the verifier ) first chooses action for agent a_1, then Abelard chooses action for agent a_2, which produces either successor state  q_1 or q_2. Then the transition game continues from the configuration ( A,q_j,T,3,m,i), where j∈{1,2}.





This concludes the definition of the rules for the phases i, ii and iii in the transition game g(,q_0,AΦ,).



 

Suppose first that the transition game is continued from ( A,q_2,T,3,m,i). 
Since it is the second round, Abelard could now try to verify p_3 by claiming that p_3 is true at q_2. However, then Eloise would win by challenging. But if Abelard does not try to verify p_3 now, then the value of p_3 will stay . In that case Eloise will win the evaluation game simply by not making any more claims in the transition game.



 

Suppose then that the game continues from ( A,q_1,T,3,m,i). 
Suppose that Abelard  verifies p_3 by claiming that p_3 is true and that Eloise does not challenge. If the transition game now ended at ( E,q_1,Ψ,T') with T'( p_3)=⊤, Abelard would win. Thus, suppose that Abelard ends his seeker turn and Eloise chooses some finite timer, say 2. At ( E,q_1,T',2,2,iii) Eloise can force the resulting state q_3 by choosing α for a_1. At ( E,q_3,T',2,2,i) Eloise can verify ( p_1) p_2 by claiming that p_2 is true at q_3. Furthermore, Eloise can move via q_1 to q_4 and verify p_1 there, before timer reaches 0. When the evaluation game is eventually continued, Eloise wins by choosing the right disjunct of Ψ.








Suppose that the transition game continues from the configuration ( A,q_2,T',3,m,i). Since it is the second round of the transition game, Abelard could now try to verify p_3 by claiming that p_3 is true at q_2. However, then Eloise could win by challenging this claim. But if Abelard does not try to verify p_3 at that configuration, then the value of p_3 will stay . Hence, when Abelard decides to end his seeker's  turn or when the timer m is lowered to 0, then Eloise may end the transition game and win the evaluation game from a location of the form ( E,Ψ,q',T”).





Suppose now that the transition game continues from the configuration ( A,q_1,T',3,m,i). Suppose that Abelard verifies p_3 by claiming that p_3 is true and that Eloise does not challenge that claim. If the transition game now ended at location ( E,q_1,Ψ,T”), where T”( p_3)=⊤, Abelard would win. Thus, if Abelard decides to quit the transition game, then Eloise wants to continue as a seeker from configuration ( E,q_1,T”,2,m',iii) for some m'<ω. Then Eloise can choose action α for agent a_1 and lower the timer to 2, whence the next configuration is ( E,q_3,T”,2,2,i). Eloise can then verify ( p_1) p_2 at it by claiming that p_2 is true at q_3.
Furthermore, Eloise can move via q_1 to q_4 and verify p_1 there, before the timer reaches 0. Then Eloise will win when the evaluation game is continued from a location of the form ( E, q_4,Ψ,T”').










  §.§.§ The unbounded evaluation game



Let (ℳ, q, φ,Γ)  be a -bounded evaluation game. We can define a corresponding unbounded evaluation game, (ℳ, q, φ), by replacing transition games g(,q,AΦ,) with unbounded transition games, g(,q,AΦ); these are played with the same rules as g(,q_0,AΦ,Γ)  except that timers γ are not used in them. Instead, the players can keep the role of a seeker for arbitrarily long and thus the game may last for an infinite number of rounds. In the case of an infinite play, the player who took the last seeker turn loses the entire evaluation game. (Recall that the number of seeker alternations is bounded by the number |𝐴𝑡(Φ)|.) 









 §.§ Defining the game theoretic semantics




In this section we define game-theoretic semantics for by equating truth of formulae with the existence of a winning strategy for Eloise in the corresponding evaluation game.

We begin with the following remark which will be relevant for the notion of positional strategies in evaluation games.


The description of transition games above is based on a simplified notion of configurations. The phases i–iii consist of several “subphases” and more information should be encoded into configurations.  The full notion of configuration  should also include:


– In phase i, a counter indicating the relative atom currently under consideration by the players; flags for each player indicating whether and what claim (s)he has made on the truth of the current relative atom; a 3-bit flag indicating if it is the first, second, or some later round in the transition game. 

– For phase ii, a flag whether the current seeker wants to continue,
and for phase iii, a record of the
current choice of actions for the agents in A by .



For technical simplicity, we omit these formal details.


Hereafter a position in an evaluation game will mean either a location of the form (,q,φ,T) or a configuration in the fully extended form described in the remark above. By this definition, at every position only one of the players (Abelard or Eloise) has a move to choose. Thus, the entire evaluation game—including transition games as subgames—is a turn-based game of perfect information. 


By game tree T_𝒢 of an evaluation game 𝒢, we mean the tree whose nodes   correspond to all positions arising in 𝒢, and every branch of which corresponds to a possible play of 𝒢 (including transition games as subgames). Note that some of these plays may be infinite, but only because an embedded transition game does not terminate, in which case a winner in the entire evaluation game is uniquely assigned according to the rules in 
Section <ref>.

The formal definitions of players' memory-based strategies in the evaluation games games are defined as expected, based on histories of positions. As usual, a strategy for a player  is called  winning if, following that strategy,  is guaranteed to win regardless of how  plays. 

A strategy is positional if it depends only on the current position.

We can also define strategies for transition games that arise within evaluation games; note that these are substrategies for the strategies in evaluation games. A strategy τ for a transition game is called winning for  if


  * every exit location that can be reached with τ is a winning location for  in the evaluation game that continues from the exit location, and additionally,

  * in the alternative scenario where the transition game continues infinitely long while τ is followed (which is possible only in unbounded games), the player  is not the player who holds the (necessarily last) seeker's turn that lasts infinitely long.







Let ℳ be a , q∈, φ∈ and  an ordinal. 
Truth of φ in the -bounded 
(⊩_), resp. unbounded  
(⊩)  is defined as follows: 


    ℳ,q⊩_φ 
    		(resp. ℳ,q⊩φ) iff Eloise has a positional
       winning strategy in 𝒢(ℳ,q,φ,) 
    		(resp. 𝒢(ℳ,q,φ)).




We will show later that evaluation games are determined with positional strategies. Hence, if we allowed perfect-recall strategies in the truth definition above, we
would obtain equivalent semantics.





 
 
Consider the  
	
ℳ = (, , , , d, o, v), where:  

    = {1,2},   = {q_0, q_1, q_2},   = {p_1,p_2},   = {α, β}
        d(1,q_0)= d(2,q_1) = {α, β};   d(a,q_i)={α} 
    
    	   o(q_0,βα)=q_0,   o(q_0,αα)= o(q_1,αβ)=q_1,   
    		o(q_1,αα)=o(q_2,αα)=q_2 
       v(p_1)={q_0}  and  v(p_2)={q_2}.

	





[scale=1.5]
	at (-0.3,0) [draw, circle] (0) p_1;
	at (1,0) [draw, circle] (1) p_3;
	at (2.3,0) [draw, circle] (4) p_2;
	at (-1.8,0) ℳ:;
	at (-0.3,-0.45) q_0;
	at (1.05,-0.45) q_1;
	at (2.35,-0.45) q_2;
	at (1.35,0.5) αβ;
	[-latex, loop left] (0) to node βα (0);	
	[-latex] (0) to node[below] αα (1);
	[-latex, loop above] (1) to (1);		
	[-latex] (1) to node[below] αα (4);
	[-latex, loop right] (4) to node αα (4);








Here we have ℳ = (, , , , d, o, v), where  
= {a_1,a_2}, = {p_1,p_2},
= {q_0, q_1, q_2}, = {α, β}, and 
the transition, outcome and valuation functions are defined as above. 





 
Let φ:=a_2( p_1 ∨  p_2) (here p_1 =  p_1). We describe a winning strategy for Eloise in the unbounded evaluation game (ℳ,q_0,φ).

Eloise immediately ends her seeker's turn and does not make claims while being at q_0. If Abelard makes claims at q_0, she challenges those claims. If Abelard ends the transition game at q_0, Eloise wins the evaluation game by choosing p_1, as now the value of p_1 is . 

Suppose that Abelard forces a transition to q_1 by choosing α for a_1. If he claims p_1 is true at q_1, Eloise does not challenge. If Abelard ends his seeker turn at q_1, Eloise becomes the seeker. At q_1 she forces a transition to q_2, by choosing α for a_2. Then she verifies p_2 by claiming that p_2 is true at q_2.

If the transition game ends at q_2, she wins by choosing p_2, whose value is ⊤.

Note that by following this strategy, Eloise cannot stay as a seeker for infinitely long.




We will see later that there is never need for a larger than |At(Φ)| number of seeker alternations in a transition game for a formula AΦ. In Example <ref> we saw that there are cases where exactly |At(Φ)| seeker alternations are needed in the corresponding transition game. The following example generalizes the setting of Example <ref> by showing that no fixed upper bound for the number of seeker alternations suffices for all transitions games.






Let φ_k=a_2Ψ_k, where Ψ_k:= r_0∨⋁_1≤ i≤ k( p_i∧ r_i). Consider the following  ℳ (c.f. the model in Example <ref>).


[
	scale=1.5,
	state/.style=draw, rectangle, rounded corners, font=
	]
	at (0,0) [state] (0) r_0,…, r_n;
	at (1.5,0) [state] (1) r_1,…, r_n;
	at (3.2,0) [state] (2) p_1, r_1,…, r_n;
	at (4.8,0) [state] (3) r_2,…, r_n;
	at (6.5,0) [state] (4) p_2, r_2,…, r_n;
	at (5,-1.5) [state] (5) p_n-1,r_n-1,r_n;
	at (3.4,-1.5) [state] (6) r_n;
	at (2.1,-1.5) [state] (7) p_n,r_n;
	at (0.7,-1.5) [state] (8) p_n;
	[below=4pt of 0] q_0;
	[below=4pt of 1] q_1;
	[below=0pt of 2] q_1';
	[below=4pt of 3] q_2;
	[below=0pt of 4] q_2';
	[below=0pt of 5] q_n-1';
	[below=4pt of 6] q_n;
	[below=0pt of 7] q_n';
	[below=4pt of 8] q_fin;
	[-latex, loop above] (0) to node βα (0);	
	[-latex] (0) to node[below] αα (1);
	[-latex, loop above] (1) to node αβ (1);	
	[-latex] (1) to node[below] αα (2);
	[-latex, loop above] (2) to node βα (2);
	[-latex] (2) to node[below] αα (3);
	[-latex, loop above] (3) to node αβ (3);
	[-latex] (3) to node[below] αα (4);
	[-latex, loop above] (4) to node βα (4);
	[-latex, dashed] (4) to (5);
	[-latex, loop above] (5) to node βα (5);
	[-latex] (5) to node[below] αα (6);
	[-latex, loop above] (6) to node αβ (6);
	[-latex] (6) to node[below] αα (7);
	[-latex, loop above] (7) to node βα (7);
	[-latex] (7) to node[below] αα (8);
	[-latex, loop left] (8) to node αα (8);




At q_0 Eloise wants to end her seeker turn immediately as r_0 “still” true. When Abelard becomes the seeker, he wants to make a transition to q_1 and falsify r_0 there. Since Abelard has then no reason to continue as a seeker, he gives the seeker turn to Eloise. Now Eloise wants to make a transition to q_1' in order to verify p_1; since r_1 is still true, Eloise has then no reason to continue as a seeker. We may suppose that the transition game continues like this, so that the seeker role is swapped after every transition and p_i are verified while r_i are falsified. When Abelard finally becomes the seeker at q_n', the maximum number of |At(Ψ_k)|=2k+1 seeker alternations has been used. Then Abelard makes a transition to q_n', falsifies r_n and wins the “boolean game” for Ψ_k with the values of the (fully updated) truth function.






§ ANALYSING EVALUATION GAMES





In this section we will analyse the properties of the evaluation games of . We first prove positional determinacy of both 
bounded and unbounded evaluation games. Then we find so-called stable timer bounds for bounded evaluation games and show that with them, the bounded becomes equivalent to the unbounded . Finally we present the notion of a regular strategy which will be needed for proving the equivalence of and the standard compositional semantics of in the next section.





 §.§ Positional determinacy




Here we prove positional determinacy of both bounded and unbounded evaluation games. Recall here that positions are either locations in evaluation games or configurations in transition games—in the extended sense which was discussed in Remark <ref>.


Bounded evaluation games 

are determined and the winner has a positional winning strategy.




(Sketch) 
Since ordinals are well-founded and they must decrease during transition games, it is easy to see that the game tree is well-founded. Thus positional determinacy
follows easlily, essentially by backward induction.





Unbounded evaluation games 

are determined and the winner has a positional winning strategy.









(Sketch)


This claim can be proved 
in a similar way as Gale-Stewart theorem.


Another way to prove the claim is to
show that unbounded evaluation games are essentially Büchi-games
(see, e.g., <cit.> for Büchi-games). 

The details of the proof via Büchi-games are in <cit.>,


but the principal idea is to set up a Büchi condition such that Eloise wins the Büchi game if the set of positions visited infinitely often is included in the union of configurations of the transition games where Abelard is the seeker and positions of the evaluation game where Eloise has already won.

 

 

We will show that unbounded evaluation games are essentially Büchi-games
(see, e.g., <cit.>). 

We first discuss the case where the underlying ℳ is finite.
We follow the technicalities for Büchi-games from <cit.>, which gives an
excellently detailed and to-the-point presentation of the related basic notions.



Take a triple (ℳ,q,φ),
where ℳ is a finite , q a state of ℳ, 
and φ a formula of .
We will convert this triple into a Büchi game BG such 
that ℳ,qφ iff player 2
has a winning strategy in BG from a certain
position of BG determined by the state q.

The required Büchi game  BG corresponds almost exactly to
the unbounded evaluation game 𝒢(ℳ,q,φ).
The set of states of BG is the finite set of positions in  
𝒢(ℳ,q,φ).
The states of BG assigned to player 1 (resp., player 2) of BG are
the positions where Abelard (resp., Eloise) is to move.

The edges of the binary transition relation E of BG
correspond to the  changes of positions in 𝒢(ℳ,q,φ).





Also, E is defined such that ending locations in the
evaluation game connect (only) to themselves via E.
This ensures that every state of BG has a successor state.





We set a co-Büchi-objective
such that an infinite play of BG is
winning for player 2 iff the set of states visited 
infinitely often is a subset of the union of the following sets of states of BG:






  * States of BG corresponding to
configurations of the transition games where Abelard is the seeker.


  * States  of BG corresponding to such ending locations in 
the game (ℳ,q,φ)
where Eloise has already won.  





Clearly, Eloise (resp., Abelard) has a 
positional winning strategy in the evaluation game
starting at a position 𝑝𝑜𝑠 of 
the evaluation game iff player 2  (resp., player 1) in BG has a
positional winning strategy from the state of BG
corresponding to 𝑝𝑜𝑠.



Finite Büchi games enjoy positional 
determinacy (see e.g. 

<cit.>), which completes the case of finite s. 

For infinite s, the argument is the same but requires positional determinacy of Büchi games on infinite game graphs. That fact is well-known and follows easily from Theorem 4.3 of <cit.>.

 









Let 𝒢(ℳ,,φ) be an unbounded evaluation game. 
Note that positions of an evaluation game form a tree of a finite depth.
We prove the claim by induction on the positions of 𝒢(ℳ,,φ) in that tree. The only nontrivial case is when a position leads to an unbounded transition game g(,q_0,AΦ). We make the inductive hypothesis that every possible exit position of g(,q_0,AΦ) is a winning position for either of the players.

We now do inner induction proof on the number n=𝐴𝑡(Φ) and show that any configuration in g(,q_0,AΦ) that is of the form c=(,,q,T,n,x) is a winning configuration for either of the players. We suppose that c is not a winning configuration for . Now it is easy to see that  can play in such a way that the next configuration c' is not a winning position for . By induction on the length of the transition game, we can show that  has such a strategy τ, that when (s)he follows τ, one of the following holds:


  * The transition game ends at an exit position that is not a winning position for .

  *  decides to stop being a seeker at some configuration that is not a winning position for .

  * The transition game lasts for infinite number of rounds.

If 1 holds, then by the (outer) inductive hypothesis, the exit position of the game is a winning position for . If 2 holds, then by the (inner) inductive hypothesis, the next configuration is a winning position for . And if 3 holds, then  wins since  was the seeker. Hence the initial configuration c is a winning position for .











By the positional determinacy, we have the following consequence: If Eloise (Abelard) has a perfect recall strategy in a bounded or unbounded evaluation game (or transition game), then she (he) has a positional winning strategy in that game.








 §.§ Finding stable timer bounds




In this section study which timer bounds are “stable” for a given model. Intuitively this means that a timer bound  is stable for a model ℳ if neither of the players can benefit from announcing timers that are higher than (or equal to) . We will see that, by finding stable timer bounds, we can make the bounded equivalent to the unbounded . Moreover, the identification of stable timer bounds for finite models will be necessary for our model checking proofs in Section <ref>. 

We next consider a “semi-bounded” variant of the transition game in which one player must use timers when being the seeker and the other is allowed to play without timers.
A timer bound  is stable for an unbounded transition game g(,q_0,AΦ) if the player with a winning strategy in g(,q_0,AΦ) can, in fact, win using timers below .




We first identify stable timer bounds for finite models.



Let ℳ be a finite , q_0∈ a state and Φ∈ a
path formula. Then k:=||·|𝐴𝑡(Φ)| is a
stable timer bound for g(,q_0,AΦ).



We give a detailed sketch of proof.

Let c=( E,q,T,n,x) be a configuration
(for an unbounded game, so
no timer is listed). Suppose that exit location (,q,Φ,T) is not a
winning location for Eloise. Then she wants to stay as the
seeker until the truth function is modified to T' that makes Φ true.
Since T is updated state-wise, it is not beneficial for Eloise to go in loops
such that T is not updated. Hence, if Eloise has a winning strategy from c, then she has a winning strategy in which T is updated at least once every || rounds. Since T can be updated at most |𝐴𝑡(Φ)| times, we see that a timer greater than k =||·|𝐴𝑡(Φ)| is not needed.










If ℳ is a finite , the unbounded is equivalent on ℳ to the (||·|φ|)-bounded .





In order to find stable timer bounds for infinite models, we give the following definition (cf. Def 4.12 in <cit.>).





Let ℳ be a and let q∈. The branching degree of q, (q), is the cardinality of the set of outcome states from q:

(q):=({o(q,α⃗)|α⃗∈(,q)}).

The regular branching bound of ℳ,
or (ℳ), is the smallest infinite regular cardinal κ
such that κ > (q) for every q∈.

Note that (ℳ)=ω if and only if ℳ is image-finite.




If c=(,q,T,n,x) is a configuration in an unbounded transition game and γ is an ordinal,
we use the notation c[γ]:=(,q,T,n,γ,x).




 
Let ℳ be a , q_0∈ and Φ∈ a path formula. Then (ℳ) is a stable timer bound for g(,q_0,AΦ). 






Suppose first that Eloise has a winning strategy τ in g(ℳ,q_0,AΦ). Let c be any configuration of the form c=(, A,q,T,n,ii) such that


  * c can be reached with τ.

  * If Abelard decides to quit seeking at c, then τ instructs Eloise to become seeker.

We need to find an ordinal γ_0<(ℳ) for Eloise to announce if she needs to become seeker at c and supplement τ with instructions on lowering the ordinal after every transition while she is a seeker. We will use the instructions given by τ for verifications and choices for actions.

Suppose that Abelard quits seeking at c. Let T_g,c be the tree that is formed by all of those paths of confiqurations, starting from c, in which Eloise stays as the seeker and plays according to τ. Since τ is a winning strategy, every path in T_g,c must be finite, and thus T_g,c is well-founded. We prove the following claim by well-founded induction on T_g,c:

    For every  c'∈ T_g,c,  there is an ordinal γ<(ℳ) 
     s.t.  c'[γ]  is a winning position for Eloise.

We choose γ=0 for every leaf on T_g,c. Suppose then that c' is not a leaf. By the inductive hypothesis, the claim holds for every configuration that can be reach with a transition from c'. We now define γ to be the successor of the supremum of these ordinals. Since (ℳ) is regular, we have γ<(ℳ).

Then, there is γ_0<(ℳ) such that c[γ_0] is a winning configuration for Eloise. 




By using Proposition <ref>, it is now easy to show that when the regular branching bound of the given model is used as a timer bound , then the -bounded becomes equivalent to the unbounded . 


Suppose that ≥(ℳ). Then the unbounded is equivalent on ℳ to the -bounded .







Suppose first that ℳ,q⊩φ. By Proposition <ref> Eloise can win the evaluation game using timers smaller than  when being the seeker. Hence clearly ℳ,q⊩_φ. 

Suppose then ℳ,q⊮φ. By Proposition <ref>, Abelard has a winning strategy in (ℳ,q,φ). Thus, by Proposition <ref>, Abelard can win (ℳ,q,φ) using timers smaller than  when being the seeker. Hence, Abelard clearly has a winning strategy in (ℳ,q,φ,) and thus ℳ,q⊮_φ. 



Consequently, finite timers suffice in image-finite models. However, the finitely bounded (with =ω) is not generally equivalent to the unbounded . See the following example.



[C.f. Example 3.7 in <cit.>]
Consider the image infinite concurrent game model ℳ which is displayed in the figure below.






	[
	scale=0.55,
	prestate/.style=rectangle,draw=black!100,fill=black!20,thick,inner sep=3pt,minimum width=5mm,font=,
	state/.style=rectangle,rounded corners,draw=black!50,thick,inner sep=3pt,minimum width=5mm,font=,
	tb/.style=dashed,-latex,
	sb/.style=-latex,
	action/.style=font=,
	label/.style=font=
	]

	at (0,3) [state] (s0) p;
		[label,above= 1pt of s0] s_0;
	at (-6,0) [state] (s10) p;
		[label,below= 1pt of s10] t_0;
	at (-3,0) [state] (s20) p;
		[label,below= 1pt of s20] t_1;
	at (0,0) [state] (s30) p;
		[label,below= 1pt of s30] t_2;
	at (3,0) [state] (s40) p;
		[label,below= 1pt of s40] t_3;
	at (6,0) [state] (s50) p;
		[label,below= 1pt of s50] t_4;

	at (7,1.5) ⋯;

	[sb] (s0) to node [action,left] 0,1 (s10);
	[sb] (s0) to node [action,right] 0,2 (s20);
	[sb] (s0) to node [action,right] 0,3 (s30);
	[sb] (s0) to node [action,right] 0,4 (s40);
	[sb] (s0) to node [action,right] 0,5 (s50);

	[sb] (s20) to node [action,below] 0,0 (s10);
	[sb] (s30) to node [action,below] 0,0 (s20);
	[sb] (s40) to node [action,below] 0,0 (s30);
	[sb] (s50) to node [action,below] 0,0 (s40);
	[sb] (8.5,0) to node [action,below] 0,0 (s50);

	[sb,loop left] (s10) to node [action,left] 0,0 (s10);




Here we clearly have ℳ,s_0⊩1 p since every path from s_0 will eventually reach the state t_0 where p is true. However, ℳ,s_0⊮_ω1 p since for any value n<ω for the timer, chosen by Eloise, Abelard can choose n for the first action of agent 2 and then it will take n+1 rounds to reach t_0.

Because (ℳ)=ℵ_1 (equal to 2^ℵ_0 if we assume the continuum hypothesis), by Corollary <ref> we have ℳ,s_0⊩_ℵ_11 p. However, in this particular model, we also have ℳ,s_0⊩_ω+11 p since Eloise can win the game by first choosing ω for the value of the timer and then lowering its value to n<ω which corresponds the the action which Abelard first chooses for the agent 2. 








 §.§ Regular strategies




Here we define a notion of a regular strategy which will be important for the proofs later in this paper. We only define this concept for Eloise only for the transition games in which Eloise is the verifier. This suffices for our needs, but the definition—and the related Lemma <ref>—could easily be generalized for both players and all kinds of transition games.


A strategy τ for Eloise in a transition game g( E,q,AΦ) is regular, if the following properties hold:


  (i) τ instructs Eloise to make all the claims which are valid (by the respective ). Moreover, τ instructs Eloise to challenge all the claims which Abelard makes. (Note that this latter condition is safe for Eloise since she is given the chance to make every claim first and thus, by the first condition, Abelard can only make claims which are false.)


  (ii) τ instructs Eloise to try to end the game (by ending her seeker turn or by not taking a new seeker turn) always when the truth function T has winning values for Eloise—that is, she would a have a winning strategy from the exit location if Abelard did not want to continue as a seeker. 


  (iii) Actions chosen by τ (for the agents in A) are independent of the current seeker  and seeker turn counter n∈ℕ in configurations.



Note that the conditions (i)-(iii) together imply that all the actions chosen by a regular strategy are independent of the current seeker  and seeker turn counter n∈ℕ in configurations. Hence, the actions chosen by a regular strategy depend only[The parameter x and all the other information that is should be encoded in the configurations (see Remark <ref>) are only used for describing the current sub-phase of the game. Hence, it is easy to see players' strategies cannot depend on these parameters.] on the pairs (q,T), where q is the current state and T is the current truth function. 

Also note that since, by (i), Eloise makes all the valid verifications and falsifications, the truth function T is always determined by the path that has been formed by the transition game.

The following lemma shows that from now on we may assume all winning strategies to be regular. Since regular strategies depend only on the states and the truth function, the additional parameters  and n cannot be used for “signalling” any information for τ.


If Eloise has a winning strategy in a transition game g( E,q,AΦ), then she has a regular winning strategy in that game. 



Suppose that Eloise has winning strategy τ  in g( E,q,AΦ). 

We first note that, for checking the regularity conditions (i)–(iii), it suffices the we only consider the configurations that can be reached with the strategy of Eloise. This is because we can choose arbitrary actions for all the other configurations in order to satisfy the regularity conditions. 

We make the strategy τ regular by doing the following modifications (in the given order).



  * If τ does not satisfy the regularity propety (i), then we simply first modify it so that Eloise makes all the claims which are true by ; it is clear that we end up in Eloise's winning exit location if Abelard challenges these new claims. 

Moreover, we then redefine τ to challenge all the claims made by Abelard; since all of these claims must now by false by , it follows from the determinacy of evaluation games that every challenge by Eloise leads into an exit location which is winning for her.

After these modifications, τ is still a winning strategy and it now satisfies the regularity property (i).


Let c=(,q,T,i) be configuration that can be reached with τ and in which τ does not instruct Eloise to challenge some claim φ that Abelard can make (if Abelard claims that some formula ψ is false, then here φ=ψ). If ( A,q,φ) is a winning location for Eloise, then we can redefine τ such that it instructs Eloise to challenge the claim φ. Suppose then that ( A,q,φ) is not a winning location for Eloise, whence by determinacy, ( E,q,φ) is a winning location for Eloise. We then redefine τ in such a way that Eloise makes the claim φ by herself. If Abelard then challenges this claim, the exit position will be winning location for Eloise. 

We do this modification for all configurations for which τ violates the regularity property (i).



  * Let c=(,q,T,n,ii) be a configuration that can be reached with τ so  that ( E,q,Φ,T) is a winning location for Eloise, but τ does not instruct Eloise to try to end the transition game at c. We then redefine τ to instruct Eloise to try to end the game at c. If Abelard also wants to end the game, then we reach a winning exit location for Eloise. If Abelard does not want to end the game, then the game continues from a configuration c' that must be winning for Eloise. We can then modify τ in such way that it is a winning strategy from c'. Moreover, we can do this while maintaining the regularity conditions (i) and (ii)—we simply do the same modifications as above for all new configurations that violate these regularity conditions.

After doing the the procedure above for all configurations for which τ violates the regularity property (ii), τ satisfies the properties (i) and (ii).


  * In order to satisfy the regularity condition (iii), will first modify τ in various ways and then show that the modified strategy satisfies the condition (iii). Supposing that τ already satisfied the conditions (i) and (ii), it will then be regular. 

Suppose first that c=( A,q,T,n,iii) is a winning configuration for Eloise, but T is not winning for Eloise (in the boolean game that potentially follows). Let c'=( E,q,T,n-1,iii). Since Abelard could have ended his Seeker turn at ( A,q,T,n,ii), it now follows that c' must be a winning configuration for Eloise. We then modify τ in such way that it makes the same choice at c' and c (we can do that while maintaining the regularity conditions (i) and (ii) by doing the modifications above—if necessary). We do these modifications for all configurations c of this type.

We then do the following procedure for every integer n≤|𝐴𝑡(Φ)|, beginning from n=|𝐴𝑡(Φ)|. Let c_n=(,q,T,n,iii) be a configuration that can be reached with τ. Let n'≤|𝐴𝑡(Φ)| be the largest integer such that c_n'=(,q,T,n',iii) can be reached with τ. We redefine τ at c_n in such a way that it selects the same actions as at c_n'. We continue this modification in such a way that, when playing from c_n, we can only reach configurations of the same form as those that can be reached from c_n', the only difference being the value of seeker alternation counter. Now all the exit locations that can be reached by using τ from c_n must be winning for Eloise. Since the truth function can be updated at most |𝐴𝑡(Φ)| many times and, by condition (ii), T gets updated after every seeker alternation, it is impossible that Eloise would now lose the game because the seeker turn counter would become zero. Hence τ is still a winning strategy after these modifications.

We observe that by doing the procedure above for every n≤|𝐴𝑡(Φ)| (starting from the highest values) and for every configuration c_n, we finally obtain a winning strategy that is completely independent of the seeker turn counter. Also note that, by applying this procedure, we also maintain the regularity conditions (i) and (ii) for τ.

To prove that the actions chosen by τ for A are now independent of both the seeker  and the seeker turn counter n, suppose for the sake of contradiction that τ assigns different actions  for A in configurations c=(,q,T,n,iii) and c'=(',q,T,n',iii) such that c≠ c' and both c and c' can be reached with τ. Since τ is independent of the seeker turn counter, we must have ≠'. By symmetry we may assume that = E and '= A.

Suppose first that ( E,q,Φ,T) is a winning position for Eloise. Now, by the condition (ii), τ instructs Eloise to end her seeker turn at ( E,q,T,n,ii), and thus the configuration c cannot be reached with τ.

Suppose then that ( E,q,Φ,T) is not a winning position for Eloise. Recall that we have defined τ to make the same choice at c' as at the configuration c”=( E,q,T,n'-1,iii). But this is impossible since τ is independent of the seeker turn counter and that is the only parameter that separates the configurations c and c”.


By doing all the modifications above, τ becomes a regular strategy. Since it remains a winning strategy for Eloise even after all  these modifications, Eloise thus has a regular winning strategy in g( E,q,AΦ).


Regular strategies will play an important role in the next section where we prove the equivalence of and the standard compositional semantics for . This is because regular strategy of Eloise in a transition game for AΦ can be used in a straightforward way for formulating a collective strategy S_A for the coalition A (and vice versa).





§ GTS VS COMPOSITIONAL SEMANTICS FOR ATL^+





In this section we show that our game-theoretic semantics is equivalent to the standard (perfect-recall) compositional semantics of . From the results of the previous section it follows that this equivalence holds for both unbounded and bounded with a stable timer bound.

We begin with some preliminary definitions. We first define a so-called finite path semantics,
to be used later. See <cit.> for a similar definition.

We define the length (λ) of a finite path λ as the number of transitions in λ (whence the last state of λ is λ[(λ)]).

If λ is a prefix sequence of λ', we write λ≼λ'.







Let ℳ be a  and λ∈_fin(ℳ).
Truth of an ^+ path
formula Φ on the finite path λ is defined as expected,
the non-obvious clauses being as follows:





  * ℳ,λφ iff  (λ)≥ 1 and ℳ,λ[1]φ.


  * ℳ,λφψ iff
there exists some i≤(λ) such that ℳ,λ[i]ψ and ℳ,λ[j]φ  for all j < i.







Let ℳ be a  and λ∈_fin(ℳ).
Truth of a path formula Φ of ^+ on λ is defined as follows:




  * ℳ,λφ
iff ℳ,λ[0]φ (where φ is a 
state formula). 


  * ℳ,λφ iff  (λ)≥ 1 and ℳ,λ[1]φ.


  * ℳ,λΦ iff ℳ,λΦ.


  * ℳ,λΦ∨Ψ iff ℳ,λΦ or ℳ,λΨ.


  * ℳ,λφψ iff
there exists some i≤(λ) such that ℳ,λ[i]ψ and ℳ,λ[j]φ  for all j < i.






Let ℳ be a , Λ∈(ℳ) and Φ a path formula of . 
An index i≥ 1 is a truth-swap point of Φ on Λ if either of the following holds:


  * ℳ,Λ[i-1,∞)Φ and ℳ,Λ[i,∞)Φ.

  * ℳ,Λ[i-1,∞)Φ and ℳ,Λ[i,∞)Φ.

(Above the notation Λ[i,∞) denotes the infinite path (Λ[i],Λ[i+1],…).)

We define the truth-swap number of Φ on Λ to be

    𝑇𝑆𝑁(Φ,Λ) := ({i| i  is a truth-swap point of Φ on Λ}).

 



The claims of the following lemma are
easy to prove. Similar observations have been made in <cit.>.









Let ℳ be a , Λ∈(ℳ) and Φ a path formula of .
Now, the following claims hold:


  * 𝑇𝑆𝑁(Φ,Λ)≤ |{Ψ∈𝐴𝑡(Φ)  | Ψ is a
temporal subformula}|.

  * ℳ,ΛΦ iff there is some k∈ℕ s.t. ℳ,λΦ for every finite λ≼Λ for which (λ)≥ k.





The unbounded is equivalent to the standard (perfect-recall) compositional semantics of .




We prove by induction on  state formulae φ that for any 
CGM ℳ and a state q in ℳ: 

    ℳ,qφ  iff  Eloise has a winning strategy in 𝒢(ℳ,q,φ).

If φ is a proposition symbol, then the claim holds trivially.

Let φ=ψ and suppose first that ℳ,qψ, i.e. ℳ,qψ. By the inductive hypothesis Eloise does not have a winning strategy in 𝒢(ℳ,q,ψ). Since evaluation games are determined, Abelard has a winning strategy in 𝒢(ℳ,q,ψ). Thus, Eloise has a winning strategy in 𝒢(ℳ,q,ψ).

Suppose then that Eloise has a winning strategy in the evaluation game 𝒢(ℳ,q,ψ). Then Eloise cannot have a winning strategy in 𝒢(ℳ,q,ψ). Hence, by the inductive hypothesis, ℳ,qψ, i.e. ℳ,qψ.

Let φ=ψ∨θ and suppose that ℳ,qψ∨θ, i.e. ℳ,qψ or ℳ,qθ. Suppose first that ℳ,qψ, whence by the inductive hypothesis Eloise has a winning strategy in 𝒢(ℳ,q,ψ). Now Eloise can win 𝒢(ℳ,q,ψ∨θ) by choosing ψ on the first move. The case when ℳ,qθ is analoguos. 

Suppose now that Eloise has a winning strategy in the evaluation game 𝒢(ℳ,q,ψ∨θ). Let χ∈{ψ,θ} be disjunct that Eloise chooses when following her winning strategy. Now Eloise must have a winning strategy in 𝒢(ℳ,q,χ) and thus by the inductive hypothesis ℳ,qχ. Therefore ℳ,qψ∨θ.

Finally, let φ=AΦ. It suffices to show that Eloise has winning strategy in the (unbounded) transition game g( E,q,AΦ) if and only if the coalition A has a (perfect recall) strategy S_A such that ℳ,ΛΦ for every Λ∈(q,S_A). The cases (a) and (b) which follow correspond to the two directions of this equivalence.



(a) Suppose first that E has a winning strategy τ in the transition game g( E,q,AΦ). By Lemma <ref> we may assume that τ is regular. Let T_g be the game tree that is formed by all of those configurations that can be encountered with τ. We define S_A by using the actions according to τ for every finite path of states that occurs in consecutive configurations in T_g. The actions for all other finite paths are irrelevant.

In order to show that S_A is well-defined this way, let λ,λ' be finite branches of configurations in T_g such that the states occurring in configurations of λ and λ' are in the same order. Let c=(,q,T,n,iii) and c'=(',q,T',n',iii) be the last configurations in λ and λ', respectively. It suffices to show that τ assigns the same actions for A in both c and c'. Since λ and λ' have visited the same states, by regularity condition (i), we must have T=T'. Therefore, by regularity condition (iii), τ assigns the same actions for c and c'.

Let Λ∈(q,S_A), whence states in Λ occur in some infinite tuple of configurations in T_g.

In the (infinite) play of g( E,q,AΦ), that corresponds to Λ, Eloise does only finitely many verifications and cannot stay as a seeker for infinitely many rounds (since τ is a winning strategy). 
Let k∈ℕ be such that Eloise neither does any further verifications nor becomes a seeker after the state Λ[k].
Let λ_0≼Λ be a finite path such that  |λ_0|≥ k. 

We can show by induction on the formulae in _𝐴𝑡(Φ) that if a position of the form (,λ_0[l],Ψ,T), where Ψ∈_𝐴𝑡(Φ), can be reached by using τ, then the following holds:

    ℳ,λ_0Ψ  iff  =  E.




  * The cases Ψ=φ and Ψ=φ are easy to prove.


  * Let Ψ=ψθ and suppose first that = E. Since τ is a regular winning strategy, there must be i≤ k s.t. Eloise verifies ψθ at λ_0[i]. If Abelard challenged Eloise's claim, the evaluation game would have continued from the position ( E,λ_0[i],θ,T). By the (outer) inductive hypothesis we have ℳ,Λ[i]θ. Let then j<i. Now Abelard could have attempted to falsify ψ at Λ[j], whence Eloise must have challenged since τ is a regular winning strategy. Then the evaluation game would have continued from the position ( E,Λ[j],ψ,T) and thus by the (outer) inductive hypothesis ℳ,Λ[j]ψ. Thus we have shown that ℳ,λ_0ψθ.

Suppose now that = A. We also suppose, for the sake of contradiction, that ℳ,λ_0ψθ. Now there is i≤ k such that  ℳ,λ_0θ. If Abelard would have verified θ at λ_0[i], then Eloise would have lost by the (outer) inductive hypothesis. Hence Eloise should have falsified ψθ at some state λ_0[j], where j<i. But then by the (outer) inductive hypothesis we must have ℳ,λ_0[j]ψ, which is a contradiction. 


  * Suppose that Ψ=Θ. The next position of the evaluation game is (,λ[l],Θ,T) and thus by the (inner) inductive hypothesis, ℳ,λ_0Θ iff = A. Hence,  we have ℳ,λ_0Θ iff = E


  * The case Ψ=Θ_1∨Θ_2 is proven similarly to the previous case.


Abelard is the seeker at the last state λ_0[m] of λ_0 and may attempt to end the transition game at λ_0[m]. By our assumption Eloise does not become a seeker and thus the evaluation game is continued from ( E,λ_0[m],Φ,T) for some T. By the induction proof above, we must have ℳ,λ_0Φ. Hence, by Lemma <ref> we have ℳ,ΛΦ.



(b) Suppose then that there is a joint (perfect recall) strategy S_A such that  ℳ,ΛΦ for every Λ∈(q,S_A). We define a perfect recall strategy τ for Eloise as follows. Suppose that game is at some configuration c that is reached with a finite path λ_0 such that q_0 is the last state of λ_0.


  * If ℳ,q_0θ for some ψθ∈ At(Φ), then Eloise claims that θ is true.

  * If ℳ,q_0ψ for some ψθ∈ At(Φ), then Eloise claims that ψ is false.

  * Suppose that q_0=Λ[0] and ψ∈𝐴𝑡(Φ) is a state formula. If ℳ,q_0ψ, then Eloise claims that ψ is true.

  * Suppose that q_0=Λ[1] and ψ∈𝐴𝑡(Φ). If ℳ,q_0ψ, then Eloise claims that ψ is true.

  * If Abelard makes any claim on the truth of formulae, Eloise always challenges those claims. (Note here that Abelard's claim must be false—according to the compositional truth condition—otherwise Eloise would already have made the same claim by herself.)

  * If Eloise is the seeker in c and ℳ,λ_0Φ, then Eloise decides to end her seeker turn. 

  * If Abelard ends the seeking at c and ℳ,λ_0Φ, then Eloise decides to become seeker. Otherwise, Eloise ends the transition game at c.

  * If Eloise needs to choose actions for agents in coalition A at c, she chooses them according to S_A(λ_0).


We show by (co)-induction on the configurations of the transition game g( E,q,AΦ), that when Eloise uses τ she cannot end up in a losing ending position. 



  * Let c=( E,,q',T,n,i). Since the verifications and challenges are made according to the compositional semantics on the current state, Eloise has a winning strategy from any possible exit position by the (outer) inductive hypothesis.


  * Let c=( E,,q',T,n,ii). By Lemma <ref> and the definition of τ, the transition game can only end when ℳ,λ_0Φ. Hence from the exit position ( E,q',Φ,T), Eloise can play in such a way that for any position (,q',Ψ,T), that is reached, the following condition holds:

    ℳ,λ_0Ψ  iff  =  E,

where Ψ is a subformula of Φ such that there is φ∈𝐴𝑡(Φ) which is a subformula of Ψ. Eventually, a location of the form (,q',φ,T) is reached, where φ∈𝐴𝑡(Φ). Since the verifications by τ are made according to the compositional truth of the relational atoms of Φ, it is quite obvious to see that (,q',φ,T) is a winning position for Eloise.


  * Let c=( E,,q',T,n,iii). This configuration does not lead to any exit locations.


Since Eloise chooses actions for agents in A according to S_A, every path of states that is formed with τ is a prefix sequence of some path Λ∈(q,S_A). Since ℳ,ΛΦ for every Λ∈(q,S_A), by Lemma <ref>, and the definition of τ, Eloise cannot stay as a seeker forever when playing with τ. If Abelard stays as a seeker forever, then Eloise wins. Hence, τ is a (perfect recall) winning strategy for Eloise.

Since unbounded transition games are positionally determined, there is also a positional winning strategy τ' for Eloise.



By combining Theorem <ref> and Corollary <ref>, we immediately obtain the following corollary:


If ≥(ℳ), then the -bounded is equivalent on ℳ with the standard (perfect recall) compositional semantics of .









§ MODEL CHECKING ATL^+ USING GTS






Here we apply the to model checking problems for and its fragments.



 §.§ Revisiting the PSPACE  upper bound proof



As mentioned earlier, the PSPACE upper bound proof
for the model checking of ^+ in <cit.> contains a flaw. Indeed, the claim of Theorem 4 in <cit.> is incorrect and a  counterexample to it can be extracted from our Example <ref>, where ℳ, q_0φ for φ =a_2( p_1 ∨ p_2). In the notation of <cit.>,

since |St_ℳ | = 3 and 𝒜𝒫ℱ(φ) = 2,  by the claim there must be a 6-witness strategy for the agent 2 for 
(ℳ, q_0,  p_1 ∨ p_2). However, this is not the case, since the player 1 can choose to play at q_0 four times β, and then  
α. 

Then ℳ, Λ^6 ( p_1 ∨ p_2) on any resulting path Λ. 

The reason for the problem indicated above is that compositional semantics easily ignores the role and power of the falsifier (Abelard) in the formula evaluation process.
Still, using the introduced above, we will demonstrate in a simple way
that the upper bound result is indeed correct. 



The input to the model checking problem of ^+ is an ^+
formula φ, a finite ℳ and 
a state q in ℳ. 
We assume that ℳ is 
encoded in the standard way (cf. <cit.>)
that provides a full explicit description of the transition function o. 
Unlike <cit.>, we do not assume any bounds on the number of
proposition symbols or agents in the input. 
We only consider here the semantics of ^+ based on perfect information and perfect-recall strategies. 








The ^+ model checking problem is PSPACE-complete.







We get the lower bound directly from <cit.>, so we
only prove the upper bound here.
By Theorem <ref> and Proposition <ref>,
if ℳ is a finite , we
have ℳ,qφ iff

Eloise has a positional winning strategy in 𝒢(ℳ,q,φ,N)
with N = ||·|φ|.

It is routine to construct an alternating Turing machine TM that 
simulates 𝒢(ℳ,q,φ,N) such that the positions for Eloise correspond to existential states of TM and Abelard's positions to universal states. 
Due to the timer bound N, the machine runs in polynomial time.
It is clear that if Eloise has a (positional or not) winning strategy in the evaluation game, then TM accepts. 

Conversely, if TM accepts, we can read a non-positional winning strategy for Eloise from the the computation tree (with only one successful move for existential states
recorded everywhere) which demonstrates 
that TM accepts. By Proposition  <ref>,
Eloise thus also has a positional winning strategy in the evaluation game.




Is the pruning here necessary? Can we shorten this part?
We use s to generate a (finite) pruned game tree T_s such that each position where Eloise makes a choice has a single successor position provided by s, and
each position where Abelard makes a choice has as successors all possible successor states. If some position l of T_s occurs 
more than once on a branch of T_s,

then each subtree whose root is the closest to the root instance of l on
the branch is replaced by a subtree whose root is a last instance of l on the branch.

This process is repeated until the resulting tree encodes a deterministic positional
winning strategy for Eloise.





Since APTIME = PSPACE, the claim follows.












 §.§ A hierarchy of tractable fragments of 




We now identify a natural hierarchy of tractable fragments of ^+.
Let k be a positive integer. Define ^k

to be the fragment of  where all formulae AΦ have the property that 
|𝐴𝑡(Φ)|≤ k. 
Note that ^1 is essentially the same as (with Release).
Note also that the number of non-equivalent formulae of ^k is
not bounded for any k, even in
the special case where the number of propositions and actions is constant,
because nesting of strategic operators A is not limited. 


Still, we will show that the model checking problem for ^k is PTIME-complete for any fixed k.

Again s are encoded explicitly and no
restrictions on the number of propositions or
actions is assumed.



(In fact, a certain implicit
encoding of s leads to  Δ^P_3-completeness <cit.>.)








With the fully developed in place, the following
theorem is now actually straightforward to prove. This demonstrates the
potential advantages of .






We first observe that when φ∈^k and ℳ is finite, the number of all positions in a an
unbounded evaluation game (ℳ,q,φ is polynomial with respect to the size of ℳ and φ (check Remark <ref> for all the information that should be encoded in a position). 
The same holds for bounded evaluation games.
Note that generally for φ'∈, the number positions in an evaluation game could be exponential with respect to φ',
since the total number of truth functions T
grows exponentially with the number of relative atoms.












For any fixed k∈, the model checking problem for 
^k  is PTIME-complete. 







The claim is well-known for  (see <cit.>), so we
have the lower bound for free, for any k. 

One possible proof strategy for the upper bound would involve using
alternating LOGSPACE-machines, but here we argue via Büchi-games instead.




See the details of the reduction of unbounded evaluation
games to Büchi-games in the technical report <cit.> 
(the proof for Proposition <ref>).




Consider a triple (ℳ,q,φ),
where φ∈^k. By the proof of 
Proposition <ref>,  

there exists a Büchi game BG
such that Eloise wins the
unbounded evaluation game 𝒢(ℳ,q,φ) iff
she wins BG from the state of BG that corresponds to the
beginning position of the evaluation game. 

We then observe that
since we are considering ^k 
for a fixed k, the domain size of each truth function T
used in the evaluation game is at most k,
and thus the number of positions in
𝒢(ℳ,q,φ) is polynomial in the 
size of the input (ℳ,q,φ). 
(Cf. Remark <ref> for all the information that should be
encoded in a position in bounded evaluation games;
here we only use the simpler unbounded games.)
Thus also the size of BG is polynomial in the input size. 




We note that, 
in order to avoid blow-ups, it is
essential that the maximum domain size k of
truth functions T is fixed.

We also note—as mentioned already in <cit.>—that the
number of transitions in ℳ is not bounded
by the square of the number of states of ℳ.
In fact, because we impose no limit (other than finiteness) on the 
number of actions in ℳ,
the number of transitions in relation to states is arbitrary. However,
this is no problem to us since an explicit 
encoding of ℳ—which lists all
transitions explicitly—is part of the input to the model checking problem.



Since Büchi games can be solved in PTIME, the claim follows.








Note that the above proof provides more than just a
reduction of unbounded evaluation games on finite models to
Büchi games. It shows that such
evaluation games essentially are Büchi games.











§ BOUNDED MEMORY SEMANTICS FOR ^K







Strategies with bounded memory in concurrent game models 

can be naturally defined using deterministic finite state transducers (or, Mealy machines). For a transducer-based definition of bounded memory strategies, see e.g. <cit.>, and see <cit.> for more on this topic.
Using such strategies, an agent's moves are determined both by the current state in the model and by the current state (memory cell) of the agent's transducer. Then,  transitions take place both in the model and in the state space of the transducer, thus updating the agent's memory.  

So, such strategies are positional with respect to the product of the two state spaces. 

In the compositional m-bounded memory semantics (^m) for ^+, agents are allowed to use at most m memory cells, i.e., strategies defined by transducers with at most  m states.  





 §.§ An upper bound for the number of memory cells


Since the use of the truth function T in our is analogous to the use of memory cells in m-bounded memory semantics, we obtain the following result.





For ^k, the unbounded is equivalent to the m-bounded memory semantics for m = 3^k-2^k.



Let m:=3^k-2^k and φ∈^k. 

We show that 

    ℳ,q⊩φ  iff  ℳ,q^mφ.

 The implication from right to left is immediate by Theorem <ref>. We prove the other direction by induction on φ. The only interesting case is when φ=AΦ. Suppose that Eloise has a winning strategy in g( E,q,AΦ). By Lemma <ref> we may assume that τ is regular.

We define a memory transducer 𝒯 that Eloise can use to define strategies for all agents in A. We fix the set of states C of 𝒯 to be the set of all 

truth functions T for 𝐴𝑡(Φ) such that T(χ)= for at least one χ∈𝐴𝑡(Φ). Since T(χ)∈{,⊤,}, we have |C|≤ 3^k-2^k=m. The initial state of 𝒯 is T_0 

where T_0(χ)= for every χ∈𝐴𝑡(Φ).
The transitions in 𝒯 

 are defined according to how Eloise updates the truth function T during the transition game. However, when T becomes fully updated (i.e. T(χ)≠ for every χ∈𝐴𝑡(Φ)), then no further transitions are made, because in this case all relative atoms have been verified/falsified and the truth of Φ on the path is fixed.

Now, the strategy 

for each agent a∈ A is defined positionally on C×
as follows: At a state T of 𝒯 and 

state q ∈ℳ, the agent a follows the action prescribed by Eloise's winning strategy for the corresponding step phase in the transition game. 

The strategy for A is now well-defined since τ is regular and thus depends only on the current state and the current truth function.

It is now easy to show that ℳ,Λ^mΦ for any path Λ that is consistent with the resulting collective strategy for the coalition A. 


By Theorem <ref>, we obtain the following corollary.

For ^k, the perfect recall compositional semantics is equivalent to the (3^k-2^k)-bounded memory semantics.


This extends the known fact that positional strategies 
(using 1 memory cell) 
suffice for the semantics of (which is essentially the same as ^1).


Moreover, given a formula, there is no need for the full perfect recall semantics, as we may equivalently apply the bounded memory semantics with a bound that is based on the structure of the formula (“the maximum temporal width”).


By _^k we denote the fragment of ^k where all the relative atoms are of the form φ, that is, the “temporal objectives” Φ are
boolean combinations of reachability objectives.




For _^k, the unbounded is equivalent to the m-bounded memory semantics for m = 2^k-1.



In _^k we may modify the rules of the transition games in such a way that relative atoms cannot be falsified by the players (but naturally they can be verified). This is because ψ is interpreted as ⊤ψ and ⊤ is never false: if a player tried to falsify ⊤ψ, that player would immediately lose once the other player challenges the claim.

With this modification of the rules, there are at most 2^k different truth functions that may
appear in the transition games for _^k. Moreover, there is only a single truth function that is fully updated. Hence we may define a memory transducer 𝒯 with 2^k-1 states as in the proof of Theorem <ref> and prove the rest of the claim analogously.


In the next subsection we will show that the result of Theorem <ref> is optimal in the sense that no smaller number of memory cells guarantees an equivalent semantics. Hence, even for _^k, the agents may need exponentially many memory cells with respect to the number of relative atoms. 





 §.§ A lower bound for the number of memory cells


In this section we will investigate the following simple _^k-formula:

    ξ_k:=a_1Φ_k,    where Φ_k :=  p_1∧⋯∧ p_k.

Note that Φ_k is just a conjunction of reachability goals that agent a_1 needs to fulfill (in any order). Since positional strategies suffice for single reachability objectives, it would be intuitive to think that a_1 needs at most k-1 memory cells in order to achieve Φ_k. This is because a_1 needs to change its positional strategy only when completing some of the reachability objectives.[This can be seen by analyzing our for : note that (1) the strategies in transition games may be assumed to be positional with respect to the truth function; and (2) the truth function for Φ_k can be updated at most most k times during the transition game for Φ_k.] However, we will see that the bounded memory strategy of a_1 must potentially use a transducer that has exponentially many states with respect to k. The model that we will use for proving this claim is constructed in the following example.


Let [k]:={1,…, k} and ℳ_k := (, , , , d, o, v) be a , where


  * ={a_1,a_2}, 
={p_1,…,p_k};


  * =[k] ∪ {B| B⊆𝒫([k])∖{∅}}∪{};


  * ={q_0}∪{q_i| i∈[k]}∪{q_B| B∈𝒫([k])∖{∅,[k]}};


  * v(p_i)={q_i}∪{q_B∈| i∈ B} for all p_i∈;


  * d(q_0,a_1)={B| B∈𝒫([k])∖{∅}},   d(q_0,a_2)=[k] 

and d(q,a_i)={} when q∈∖{q_0} and i∈{1,2};


  * o(q_0,(B,i))=q_i   if  i∈ B,
 q_B   else; 

o(q_i,(,))=q_0 when i∈[k] 

and o(q_B,(,))=q_B when B∈𝒫([k])∖{∅,[k]}.


See the following figure for model ℳ_k in the special case when k=3.



[scale=0.9,
	state/.style=draw,circle,inner sep=2pt,minimum width=8mm,font=,
	action/.style=-latex,font=]

	at (-4.2,3.3) ℳ_3:;

	at (0,0) [state] (0) p_4;
	at (0,3) [state] (1r) p_1;
	at (2.9,-1.5) [state] (2r) p_2;
	at (-2.9,-1.5) [state] (3r) p_3;
	at (2.2,2.2) [state] (1) p_1;
	at (1,-2.8) [state] (2) p_2;
	at (-3.2,0.8) [state] (3) p_3;
	at (3.2,0.8) [state] (12) p_1,p_2;
	at (-2.2,2.2) [state] (13) p_1,p_3;
	at (-1,-2.8) [state] (23) p_2,p_3;

	[above=0pt of 0] q_0;
	[above=0pt of 1r] q_1;
	[right=0pt of 2r] q_2;
	[left=0pt of 3r] q_3;
	[right=0pt of 1] q_{1};
	[right=0pt of 2] q_{2};
	[below=0pt of 3] q_{3};
	[below=0pt of 12] q_{1,2};
	[left=0pt of 13] q_{1,3};
	[left=0pt of 23] q_{2,3};

	[action, right, bend right, near end, text width=5mm] (0) to node 
		{1,2,3},1 {1,2},1 {1,3},1 {1},1 (1r);
	[action, left, bend right, near start, text width=3mm] (1r) to node ,  (0);	
	[action, sloped, bend right, text width=7mm] (0) to node 
		{1,2,3},2 {1,2},2 {2,3},2 {2},2 9000 9000 (2r);
	[action, right, bend right, near start] (2r) to node , (0);
	[action, sloped, bend right, text width=11mm] (0) to node 
		90000 90000 {3},3 {1,3},3 {2,3},3 {1,2,3},3 (3r);
	[action, below, bend right, near start] (3r) to node , (0);

	[action, below, near end, text width=1mm] (0) to node {1},2 {1},3 (1);
	[action, left, near end, text width=7mm] (0) to node {2},1 {2},3 (2);
	[action, above, near end, text width=7mm] (0) to node {3},1 {3},2 (3);

	[action, below, sloped, near end] (0) to node {1,2},3 (12);
	[action, above, sloped, near end] (0) to node {2,3},1 (23);
	[action, above, sloped, near end] (0) to node {1,3},2 (13);

	[action, loop above] (1) to node , (1);
	[action, loop below] (2) to node , (2);
	[action, loop left, text width=3mm] (3) to node ,  (3);
	[action, loop right, text width=3mm] (12) to node ,  (12);
	[action, loop above] (13) to node , (13);
	[action, loop below] (23) to node , (23);




The model ℳ_k can be described as follows: At q_0 the agent a_1 gets to “announce” any nonempty set B of (indices of) proposition symbols in . Then, depending on the action chosen by the agent a_2, one of the following happens:



  * Some proposition symbol p_i, for which i∈ B, is reached and then the game returns to q_0. This happens when a_2 chooses i∈ B, whence a transition is made to q_i and then back to q_0. 


  * All proposition symbols p_i with i∈ B are reached, but thereafter no new proposition symbols can be reached. This happens when a_2 chooses some i∉ B, whence a transition is made to q_B, where the game will loop forever.


We will show that agent a_1 has a (2^k-1)-bounded memory strategy σ_a_1 which guarantees the truth of Φ_k on every path in (q_0,σ_a_1). 

We first define a finite state transducer 𝒯_k as follows:



  * The set of states C of 𝒯_k is {c_B| B∈𝒫([k])∖{∅}}. Now |C|=2^k-1. 

  * The initial state of 𝒯_k is c_[k]. 

  * The transitions of 𝒯_k are define as follows: Suppose that the current state of 𝒯_k is c_B for some B∈𝒫([k])∖{∅} and a state q_j is reached for some j∈[k]. Now if j∈ B and B≠{j}, then 𝒯_k changes its state to c_B∖{i}. Else, no transition is made.


See the following picture for the transducer 𝒯_k in the special case when k=3. 



[scale=1,
	state/.style=draw,circle,minimum width=7.7mm,
	action/.style=-latex,font=]

	at (-3.2,0.5) 𝒯_3:;

	at (0,0) [state] (123) ;
		at (0,0) [draw,circle,minimum width=6.3mm] ;
	at (-2,-1.5) [state] (12) ;
	at (0,-1.5) [state] (13) ;
	at (2,-1.5) [state] (23) ;
	at (-2,-3) [state] (1) ;
	at (0,-3) [state] (2) ;
	at (2,-3) [state] (3) ;

	[above=0pt of 0] c_{1,2,3};
	[left=0pt of 12] c_{1,2};
	[right=0pt of 13] c_{1,3};
	[right=0pt of 23] c_{2,3};
	[left=0pt of 1] c_{1};
	[right=0pt of 2] c_{2};
	[right=0pt of 3] c_{3};

	[action, left] (0) to node q_3 (12);
	[action, left] (0) to node q_2 (13);
	[action, right] (0) to node q_1 (23);
	[action, left] (12) to node q_2 (1);
	[action, left, near start] (12) to node q_1 (2);
	[action, right, near start] (13) to node q_3 (1);
	[action, left, near start] (13) to node q_1 (3);
	[action, right] (23) to node q_2 (3);
	[action, right, near start] (23) to node q_3 (2);




Intuitively, the set B, when it is the index of c_B, denotes the set of indices of those proposition symbols p_i that have not yet been reached.

We then define the strategy σ_a_1 simply to select the action B at q_0 when the current state of 𝒯_k is c_B. (The action  is selected elsewhere.) 

It is easy to see that σ_a_1 is a strategy that satisfies Φ_k on every path.

Note that by using 𝒯_k, the agent a_1 essentially remembers which subset of {p_1,…,p_k} of proposition symbols have already been reached. But a_1 does not have to remember in which order these states have been visited; if the order was remembered as well, then the number of states in 𝒯_k would be the number of k-permutations plus the initial  state, resulting in k!+1 states. 


We prove the following lemma for the model ℳ_k constructed in Example <ref>.


ℳ_k^m ξ_k when m<2^k-1.



Let σ_a_1 be a strategy for a_1 using a transducer 𝒯 with less than 2^k-1 states. We will show that there is a path in (q_0,σ_a_1) on which p_i is not reached for some i∈[k].

We first make the following two observations (i) and (ii):














(i) Suppose a_1 chooses some B∈𝒫([k])∖{∅} at q_0 for which i∉ B for some p_i that has not yet been reached. Now the next state may be q_B where it will loop forever. Since q_B∉ v(p_i), the proposition p_i will never be reached.


(ii) Suppose now that a_1 chooses some B at q_0 for which i∈ B for some p_i that has already been reached. Now the next state may be q_i and thereafter the game returns to q_0. Since p_i is the only proposition symbol that is true at q_i, these transitions did not reach any new proposition symbols.





By the points above, we see that in order to reach all p_i, the agent a_1 has to choose such a set B at q_0 which has the indexes of exactly those proposition symbols which have not yet been reached. We denote this behavior of a_1 by (⋆).



Since 𝒯 has less than 2^k-1 states, and |𝒫([k])∖{∅}|=2^k-1, there must be B'∈𝒫([k])∖{∅} which a_1 never chooses at q_0 when following σ_a_1. Supposing that a_1 plays according to (⋆), it may happen that exactly those p_i for which i∈ [k]∖ B are reached (by visiting the corresponding states q_i (i∈ [k]∖ B) and returning to q_0 after every visit). But, in this situation it is no longer possible for a_1 to follow (⋆) and thus impossible to reach all p_i for which i∈ B. 




By Example <ref> and Lemma <ref> we immediately obtain the following corollary.


The perfect recall semantics for _^k  is not equivalent to m-bounded memory semantics for any m<2^k-1.


By this result, agents may need an exponential number of memory cells with respect to the number of relative atoms (in the Boolean combination). Again, this result holds even in the simple case where Φ is just a conjunction of reachability objectives p.

Corollary <ref> also implies that the result of Theorem <ref> is optimal. We leave it open whether the result of Theorem <ref> could be improved.








 §.§ Some remarks on the amount of memory needed for a strategy




There are several ways in which memory resources play a role in strategies.
Besides the read-only memory needed to encode a strategy, for the execution of that strategy one can distinguish the amounts of memory needed: 



(i) to store any possible input of the strategy,

(ii) to compute the value of the strategy function on any given input,

(iii) to execute the strategy in any single play.



Generally, these can be very different. Usually, the first one is taken as the measure of the memory consumption of a strategy in terms of the required input size (i.e., memoryless, bounded memory, unbounded/perfect recall), while the second is usually disregarded and strategies are assumed to be computed by – or even hardwired in – some external devices (“black boxes”). As for the third measure, which involves both the previous two, we are not aware of any explicit consideration of it in the literature. We will make some brief comparing remarks for the case of bounded memory strategies considered here.

From Corollary <ref> we see that agents may need a strategy transducer with 2^k-1 memory cells when there are k reachability objectives. This is because a strategy is a global plan of action—or a look-up table—that must take into account all possible plays.

However, by observing the use of truth function in transition games, we see that in every single play of the game only k-1 memory cells need to be used. That is, the finite state transducer needs to visit only k-1 states on every path (c.f. Example <ref> and the transducer 𝒯_k).
 
Thus, the state space of the transducer has to be exponential with respect to the number of reachability objectives, but only a linearly large section of the transducer is actually used in every single play.

In fact, the latter is to be expected, in the light of the PTIME complexity of model checking of ^k, by Theorem <ref>.   

This observation suggests that the amount of RAM-type of memory needed to use during the play may be a reasonable measure, alternative to the 
number of states in the transducer encoding the agent's strategy in enforcing or refuting a formula  (and for other related logics). Thus, one could argue that agents actually only need to use linear amount of memory in ^k, supposing they can manage their memory in a more dynamical (“on-the-fly”) way[This is also justified from the `human perspective', as people can manage to do, say, 10 tasks by remembering what is already done (by remembering at most 9 pieces of information) without need for exponential memory capacity (which would be 1023 memory cells by Theorem <ref>).].






For a better bound of the required memory it would be sufficient to modify slightly the transition games and consider a bound k not on the number of all relative atoms in strategic subformulae, but only of the temporal objectives occurring in them.











§ CONCLUSION









A natural extension of the present work would be to develop for the full .



In conclusion, we note that the game-theoretic semantics for  developed here has both conceptual and technical importance, as it explains better how the memory-based strategies in the compositional semantics can be generated and thus also provides better insight on the algorithmic aspect of that semantics. 




We note that a for , alternative to the one introduced here, could
be obtained via for coalgebraic fixed point logic
<cit.>. 
However, such a semantics (being designed for more powerful logics) would not directly lead to our that is custom-made for and would thus
not directly enable the complexity analysis that we require.
Also, that alternative approach would not give a semantics where the construction of 
finite paths only suffices. 


One more thing to consider. By analysing our for , it is quite easy to observe that the model checking can be done with alternating linear space machine (this is actually closely related to the discussions on the linear memory of agents in the last section). Do you think that this would be worth mentioning in the paper?




A natural extension of the present work would be to develop for the full . Here the
correspondence with Büchi games could be exploited in full.












 §.§ Acknowledgements

The work of Valentin Goranko was supported by a research grant 2015-04388 of the Swedish Research Council. The work of Antti Kuusisto was supported by the ERC grant 647289 “CODA."






plain




