Strategy Representation and Reasoning for Incomplete Information Concurrent Games in the Situation Calculus

1 Introduction

Strategy representation and reasoning has recently received much attention in multi-agent system and AI communities. Many strategic logics have been established, and most of them are built upon Alternating-time Temporal Logic (ATL) [Alur et al., 2002] where formula hhGiiφ expresses that coalition G has a group strategy to ensure temporal goal φ holds no matter what the other agents do.

Many extensions of ATL have been proposed, mainly along two lines. On one hand, in reality, players often have incomplete information about the game states, e.g., in poker games. Although they may have strategies to ensure a goal holds, they may not know what these strategies are or how to execute strategies where the prescribed actions for indistinguishable states are not the same. Extensions of ATL are proposed to deal with such games [van der Hoek and Wooldridge, 2003; Jamroga and van der Hoek, 2004; Jamroga and ˚Agotnes,

2007]. On the other hand, strategies are treated implicitly in ATL, and extensions of ATL are proposed to reason about strategies explicitly, that is, treat strategies as first-order objects [Walther et al., 2007; Mogavero et al., 2010].

However, the above extensions suffer from other limitations. Firstly, the extensions are mainly propositional, hence lacking expressiveness to compactly specify game structures or indistinguishable states. Secondly, as pointed out by [Ramanujam and Simon, 2008; van Eijck, 2013], these extensions treat strategies as abstract objects rather than considering the internal structure of strategies, that is, the combination of basic strategies to form complex ones. Thirdly, most extensions ignore the coordination problem. As discussed in [Ghaderi et al., 2007], a coalition may have many group strategies to ensure a goal, yet a player may not know other players' choices, hence the coalition may end up with a group strategy which may not ensure the goal.

Other than modal logics, another main family of logics in AI is action formalisms. A prominent example of action formalisms is the situation calculus [Reiter, 2001], which is a first-order language with some second-order ingredients suitable for reasoning about actions and change. Based on the situation calculus, a logic programming language Golog [Levesque et al., 1997] has been designed for high-level agent control. There have been a few works studying strategic reasoning in the situation calculus [Schulte and Delgrande, 2004; Farinelli et al., 2007; De Giacomo et al., 2010; Ghaderi et al., 2007]. The first one deals with von Neumann Morgenstern games, while the second one focuses on Markov games, using Golog to specify agent behavior. The third work studies complete information turn-based games, where ConGolog [De Giacomo et al., 2000], a concurrent version of Golog, is also used to specify game structures. However, these works either focus on solution concepts like Nash equilibria rather than ATL-like properties, or cannot reason about strategies explicitly. Lastly, Ghaderi et al. study the coordination problem and present a formalization of joint ability of coalitions based on the idea of iterated elimination of dominated strategies [Osborne and Rubinstein, 1999]. Nonetheless, it is desirable to have a more general account of joint ability of a coalition under constraints, which maybe a rough collective strategy which the coalition commits to, or a protocol that the players must comply with, such as traffic rules.

In this paper, we propose a framework based on the situation calculus for strategy representation and reasoning for incomplete information concurrent games. We first propose a simple extension with a strategy sort of a concurrent variant of multi-agent epistemic situation calculus, which can be used to compactly represent possibly infinite concurrent games, and reason about strategies explicitly. Then we propose a strategy programming language based on Golog, which can be used to specify collective strategies of coalitions. We emphasize that in this paper, by the word "collective strategy", we mean group strategy which is common knowledge of the coalition. Next, we adapt the approach of Ghaderi et al. to formalize joint ability of coalitions under commitments to strategy programs. We illustrate our logical framework with a variant of Levesque's Squirrels World.

2 Preliminaries

In this section, we introduce the situation calculus and Golog.

The situation calculus [Reiter, 2001] is a many-sorted first-order logic language (with some second-order elements) specifically designed for representing dynamically changing worlds. There are three disjoint sorts: situation for situations, action for actions, and object for everything else. In this language, the constant S0 is used to denote the initial situation; the binary function do(a↪ s) is used to denote the successor situation of s resulting from performing action a, and do([a1↪ a2↪ ▷▷▷↪ ak]↪ s) is used as a shorthand for do(ak↪ ▷ ▷ ▷ ↪ do(a2↪ do(a1↪ s))); the binary predicate Poss(a↪ s) means that action a is possible in situation s. Actions can be parameterized, e.g., pick(r↪ x) represents robot r picking up object x. There are relational and functional fluents whose values vary from situation to situation. These fluents are denoted by symbols that take a situation term as their last argument. There are also situation-independent predicates and functions. Finally, there is a binary predicate @ on situations: s @ s0 means that s is a proper subhistory of s0 . We use s v s0 as a shorthand for s @ s0 _s = s0 , and we let s  s0 abbreviate for s v s0 ^ 8a8s⇤ (s @ do(a↪ s⇤ ) v s0 ⊃ poss(a↪ s⇤ )), meaning that s is a subhistory of s0 and every action on the way from s to s0 is possible. We say that a situation s is executable if it is possible to perform the actions in s one by one: Exec(s) ▷= 8a↪ s0 ▷do(a↪ s0 ) v s ⊃ Poss(a↪ s0 )▷

In this language, an application domain is specified by a basic action theory (BAT) which describes how the world changes as the result of the available actions. Each BAT D consists of the following five disjoint parts:

1. ⌃, the foundational axioms of the situation calculus;
2. Dap, a precondition axiom for each action specifying when the action can be legally performed;
3. Dss, a successor state axiom (SSA) for each fluent which describes how fluent values change between situations;
4. Duna, unique name axioms for actions;
5. DS0 , axioms describing the initial situation S0.

Liu and Levesque [2014] propose a multi-agent extension of the situation calculus. They use a special fluent B(i↪ s0 ↪ s), which means that agent i considers situation s0 accessible from situation s, and introduce a special predicate A(i↪ a0 ↪ a↪ s), meaning that in situation s, agent i considers action a0 as a possible alternative of action a. The following is their successor state axiom for the B fluent:

Intuitively, for agent i, situation s0 is accessible after action a is performed in situation s iff it is the result of doing some alternative a⇤ of a in some s⇤ accessible from s, and executability of a in s implies that of a⇤ in s⇤ . Then beliefs are defined as follows. Let φ(s) be a formula with a single situation variable s.

• ÷ Agent i believes φ:

• ÷ Agent i truly believes φ:

Based on the situation calculus, Golog [Levesque et al., 1997] has been proposed to represent complex actions obtained by the combinations of primitive actions. Golog programs are defined by the following constructs:

1. ↵, primitive action;
2. δ1; δ2, action sequence;
3. '?, test;
4. δ1 ♣δ2, nondeterministic choice of actions;
5. ⇡x▷δ, nondeterministic choice of arguments;
6. δ⇤ , nondeterministic iteration.

Conditionals and loops are defined as abbreviations. The formal semantics of Golog is usually specified by an abbreviation Do(δ↪ s↪ s0 ), which intuitively means that executing δ brings us from situation s to s0 . Another form of semantics for Golog is the transition semantics, which is based on the important concept of a configuration, denoted as a pair (δ↪ σ), where δ is a program (that remains to be executed) and σ a situation (of actions that have been performed). As presented in [De Giacomo et al., 2000], the transition semantics for Golog programs is defined by two predicates Trans(δ↪ s↪ δ0 ↪ s0 ) and F inal(δ↪ s).

3 A concurrent epistemic situation calculus

In this section, we present a concurrent epistemic situation calculus with a strategy sort, which can be used to compactly represent incomplete information games where a fixed finite set of agents act simultaneously and instantly at each game step, and to reason about strategies explicitly.

We fix a set of agents AG = ¶1↪ ▷ ▷ ▷ ↪ n♦; we introduce an agent sort and n agent constants, for which unique names and domain closure hold. We introduce two additional sorts: an action profile sort and a second-order strategy sort. Intuitively, an action profile is an n-ary vector of actions, one action for each agent. A strategy is a function from situations to actions. Let G ✓ AG, a group strategy of coalition G is a function from G to strategies. A strategy profile is a group strategy of AG. We use variables d, d0 , ▷ ▷ ▷ for action profiles, f, f 0 , ▷ ▷ ▷ for strategies, fG, f 0G, ▷ ▷ ▷ for group strategies of G, and G to represent AG∩G. We treat fG the same as the set of variables ¶fi ♣ i 2 G♦. When G is a singleton ¶i♦, we simply write i.

We introduce a function joint(a1↪ ▷ ▷ ▷ ↪ an) which maps n actions into an action profile, and n projection functions pri(d), 1  i  n, which maps an action profile into its ith component. For simplicity, we write joint(a1↪ ▷ ▷ ▷ ↪ an) as ha1↪ ▷ ▷ ▷ ↪ ani, and write pri(d) as di. Situations are now sequences of action profiles; so the first argument of the function do and the predicate Poss is of the action profile sort.

The set ⌃ of foundational axioms for situations is the same as before except that we replace each action variable with an action profile variable. We also add to ⌃ the following axioms concerning action profiles:

• ÷ 8d9a1↪ ▷ ▷ ▷ ↪ an▷d = ha1↪ ▷ ▷ ▷ ↪ ani;
• ÷ ha1↪ ▷ ▷ ▷ ↪ ani=ha01 ↪ ▷ ▷ ▷ ↪ a0n i⊃a1 = a01 ^ ▷ ▷ ▷ ^an = a0n ;
• ÷ pri(ha1↪ ▷ ▷ ▷ ↪ ani) = ai, i = 1↪ ▷ ▷ ▷ ↪ n.

Reiter [2001] presents an account of true concurrency where a concurrent action is modeled as a possibly infinite set of simple actions. Our account of concurrent actions as action profiles can be viewed as a special case of Reiter's account.

To specify the precondition axioms for action profiles, we introduce n predicates Possi(a↪ s), meaning that it is possible for agent i to perform action a in situation s. In general, the following holds: Poss(ha1↪ ▷▷▷↪ ani↪ s) ⊃ Vni=1Possi(ai↪ s)▷ However, the converse does not necessarily hold: two simple actions may each be possible, their preconditions may be jointly consistent, yet intuitively they should not be concurrently possible. This is the precondition interaction problem as discussed in [Reiter, 2001].

To model turn-based games, we introduce an action wait, and n fluents turni(s), meaning that it is agent i's turn to make a move. We have P ossi(wait↪ s) ⌘ ≻turni(s).

Let fG be a group strategy of coalition G. The abbreviation s vfG s0 is used to represent the formula

To model agents' observability about action profiles, we introduce a special predicate A0 (i↪ j↪ a0 ↪ a↪ s), meaning that when agent j performs action a in situation s, agent i considers it possible that agent j does action a0 . In general, we let A(i↪ d0 ↪ d↪ s) ⌘ Vnj=1A0 (i↪ j↪ d0j ↪ dj ↪ s)▷

Intuitively, this means that s is a subhistory of s0 , and on the way from s to s0 , each agent i in G performs actions according to strategy fi. Further, we introduce the abbreviation:

Let φ(fAG↪ s) be a situation calculus formula. We introduce the following abbreviations, where we use fAG(s) to represent the action profile at situation s, i.e., hf1(s)↪ ▷ ▷ ▷ ↪ fn(s)i.

• ÷ Eventually φ: ⌃φ ▷= 9s0 ▷s vfAG s0 ^ φ(fAG↪ s0 ).
• ÷ Next φ: ©φ ▷= φ(fAG↪ do(fAG(s)↪ s));

We say that a strategy f is an executable strategy of agent i, if in any situation, i knows the action required by f and its executability. Formally, we have:

For a coalition G, we let EX(G↪ fG) ▷= Vi2G EX(i↪ fi). In fact, the notion of executable strategy coincides with that of uniform strategy in the literature, say [Jamroga and van der Hoek, 2004]: a strategy f is uniform if for any situations s and s0 indistinguishable for agent i, the values of f at s and s0 are the same. Formally, we have:

In the following, we illustrate the use of our situation calculus language with a variant of Levesque's Squirrels World.

Example 1 Squirrels and acorns live in a plane, and there is a fixed set of squirrels acting simultaneously at any time. Each squirrel and acorn is located at a cell (p↪ q), where p↪ q 2 Z, the set of integers, and each cell can contain any number of acorns and squirrels.

Each squirrel can do actions below: pick up an acorn if he is located at the same cell as this acorn and does not hold any acorn in the current situation; drop an acorn that he is holding; move up, down, right and left a cell; also stay at the current location and do nothing (nil). A squirrel can observe the action of another squirrel within a distance of one, but if the action is a sensing action, the result is not observable.

There are only two squirrels 1 and 2. As shown in Figure 1, initially, squirrel 1 is located at the cell (-1↪-1) and 2 is located at the cell (1↪ 1), and any squirrel knows the location of the other one; there is only one acorn in each of the cell (-1↪ 1) and (1↪ -1), and in other cells there are no acorns.

We use four ordinary fluents: in situation s, squirrel i is holding an acorn (hold(i↪ s)); squirrel i is at cell (p↪ q) (cell(i↪ p↪ q↪ s)); there are n acorns at cell (p↪ q) (acorn(p↪ q↪ n↪ s)); the situation s will be achieved after m steps from the initial situation S0 (step(s) = m).

For illustration purpose, we only present some axioms of the BAT of this game, denoted by Dsq:

Finally, we show that our situation calculus can be used to reason about games described by GDL-II [2014]. For the purpose of General Game Playing, GDL (Game Description Language) has been developed as a high-level language for the specification of complete information games. GDL is based on the standard syntax and semantics of logic programming, characterized by a number of special keywords. GDL-II is an extension of GDL for describing imperfect/incomplete information games. It has two extra keywords: sees, which specifies the information that each player gets, and random, which denotes a special player who chooses moves randomly.

Schiffel and Thielscher present a full embedding of GDLII into a multi-agent epistemic situation calculus, and formally prove that this provides a sound and complete reasoning method for players' knowledge about game states as well as about the knowledge of the other players. In fact, the situation calculus they use is essentially our extended situation calculus without the strategy sort. If we let A(i↪ d↪ d0 ↪ s) ▷=

which intuitively means that agent i cannot distinguish between two joint actions d and d0 if their own actions are the same and the information i gets about d is the same as that about d0 , then their SSA for the knowledge fluent K coincides with the SSA for our B fluent. Therefore, using their embedding, we get that GDL-II can be embedded into the concurrent epistemic situation calculus.

4 Individual strategic ability

In this section, we show that in our situation calculus, we can distinguish between different kinds of individual strategic abilities, including that studied by [Lesp´erance et al., 2000].

As discussed in the literature, say [Jamroga and ˚Agotnes, 2007], by considering whether the strategies of agent i or other agents are executable, and whether agent i knows which strategy to ensure his goal, there are different notions of strategic abilities of agent i. We can formalize these different abilities in our situation calculus as follows. Let φ(fAG↪ s) be a situation calculus formula which serves as the goal for agent i. Note that by our notation, f¯i represents a group strategy of agents other than i.

1. Can1(φ↪ s) ▷= 9fi▷Bel(i↪ 8f¯i▷φ(fi↪ f¯i↪ now)↪ s);
2. Can3(φ↪ s) ▷= 9fi▷EX(i↪ fi) ^ Bel(i↪ 8f¯i▷φ(fi↪ f¯i↪ now)↪ s);
3. Can2(φ↪ s) ▷= Bel(i↪ 9fi8f¯i▷φ(fi↪ f¯i↪ now)↪ s);
4. Can4(φ↪ s) ▷= Bel(i↪ 9fi▷EX(i↪ fi) ^ 8f¯i▷φ(gi↪ g¯i↪ now)↪ s).
5. In (1), i knows which strategy to ensure φ. In (2), i knows there exists a strategy to ensure φ. But in both (1) and (2), the strategy of agent i may not be executable. In (3), agent i knows which strategy to ensure the goal φ and this strategy is executable for him, but other agents' strategies may not be executable; in this case, agent i considers the worst case. In (4), i knows there exists an executable strategy to ensure φ, but does not know which strategy.

Example 1 Cont'd. We first give an abbreviation meaning that the distance between agents 1 and 2 in s is not more than k:

Also, we let S1 = do(hright↪ lefti↪ S0). Since in S0, any agent cannot see the action of the other one, in S1, he no longer knows the location of the other one.

1. Let φ1 =©dist(1↪ 2)  4. ThenDsq ♣= Can3(φ1↪ S1). This is because when agent 1 moves up, no matter what action agent 2 does, agent 1 believes that their distance is no more than 4.
2. Let φ2 = ©9p↪ q↪ p0 ↪ q0 ▷cell(2↪ p↪ q) ^ cell(1↪ p0 ↪ q0 ) ^ [q < 3^≻(p = 2^q = 2) ⊃ ♣p-p0 ♣  2^♣q-q0 ♣  2]. Then Dsq ♣= Can1(φ2↪ S1) ^ ≻Can3(φ2↪ S1) ^ Can4(φ2↪ S1). In S1, after agent 1 does the same action as agent 2 does in S0, he believes that φ2 holds. Thus we have Can1(φ2↪ S1). However, since agent 1 cannot observe agent 2's action in S0, this strategy is not executable. In fact, we cannot find an executable strategy of agent 1 which ensures φ2, hence Can3(φ2↪ S1) does not hold. On the other hand, for each possible action of agent 2 in S0, when agent 1 does the same action in S1, φ2 holds; thus we have Can4(φ2↪ S1).

Now we show that we can represent in our framework the notion of ability Can('↪ s) defined by Lesp´erance et al. (2000) in the single-agent case, where '(s) is a formula about situation s:

• ÷ CanGet('↪ f↪ s) ▷=9s0 (OnPath(f↪ s↪ s0 )^Bel('↪ s0 )^ 8s⇤ [s v s⇤ @ s0 ⊃ 9aBel(f(now) = a↪ s⇤ )]);
• ÷ OnPath(f↪ s↪ s0 ) ▷= s  s0 ^ 8a8s⇤ (s @ do(a↪ s⇤ ) v s0 ⊃ f(s⇤ ) = a); This is the same as our s f s0 .

Here the second line requires that g be uniform on the way from s to s0 .

Recall that we use ⌃ to denote the set of foundational axioms for our extended situation calculus. Then we get

• ÷ Can('↪ s) ▷= 9f▷Bel(CanGet('↪ f↪ now)↪ s).

5 A strategy programming language: SGolog

In this section, we propose a strategy programming language SGolog for specifying collective strategies of coalitions.

We first consider a single-step fragment (SSF) of Golog, which is used to specify an agent's possible choice to perform in one step. A situation-suppressed formula ' is a situation calculus formula with all situation arguments suppressed, and '[s] denotes the formula obtained from ' by taking s as the situation arguments of all fluents mentioned in '.

Definition 1 SSF programs are defined inductively as follows: δ ::= ('?; ↵) ♣ (δ1 ♣ δ2) ♣ (⇡x▷δ(x)), where ' is a situation-suppressed formula, and ↵ is an action term.

The formal semantics of SSF programs is defined by an abbreviation Does(δ↪ a↪ s), which intuitively means action a forms a legal execution of δ in situation s.

Definition 2 Does(δ↪ a↪ s) is defined inductively as:

• ÷ Does(δ1 ♣ δ2↪ a↪ s) ▷=Does(δ1↪ a↪ s) _Does(δ2↪ a↪ s);
• ÷ Does('?; ↵↪ a↪ s) ▷= '[s] ^ a = ↵;
• ÷ Does(⇡x▷δ(x)↪ a↪ s) ▷= 9x▷Does(δ(x)↪ a↪ s).

We use > (resp. ?) to represent true (resp. false). For convenience, we let ⇤ be an extra SSF program, which intuitively means taking an arbitrary action, and define Does(⇤↪ s↪ a) ▷= >. Next, we define SGolog programs, which can be used to represent the collective behavior/strategy of a coalition or the protocol of a multi-agent game. A primitive SGolog program is an n-ary vector of SSF programs. We use ⇤ to denote the n-ary vector of ⇤'s. For a primitive program ✓, we use ✓i to denote its i-th component.

Definition 3 SGolog programs are defined as follows:

while ' do ⇢ ♣ ⇢1O⇢2O▷▷▷O⇢m ♣ ⇢1M⇢2M ▷▷▷M⇢m↪ where ✓ is a primitive program, and ' is a situation suppressed formula.

A conditional [if ' then ⇢1 else ⇢2] is defined as abbreviation for the program ['?; ⇢1 ♣ ≻'?; ⇢2]. The prioritized disjunction and conjunction operators O and M are inspired by the work of Zhang and Thielscher (2015). Intuitively, ⇢1O⇢2O▷▷▷O⇢m means that if the program ⇢1 can be executed in situation s, then only ⇢1 is executed and the other programs are discarded, else if ⇢2 can be executed, then execute ⇢2, ..., i.e., ⇢i has higher priority than ⇢i+1. The program ⇢1 M ⇢2 M ▷▷▷ M ⇢m means that if all of ⇢1, ..., and ⇢m can be applied together in s, then all of them are applied, else we discard ⇢m and consider whether the remaining ⇢i's can be applied together.

The formal semantics of SGolog programs is defined by two predicates: Trans(⇢↪ s↪ ⇢0 ↪ s0 ), which holds if executing one step of program ⇢ in situation s may lead to situation s0 with ⇢0 remaining to be executed; and Final(⇢↪ s), which holds if program ⇢ may legally terminate in situation s. The two predicates are inductively defined as follows.

1. Trans(✓↪ s↪ ⇢0 ↪ s0 ) ⌘ 9d▷Poss(d↪ s) ^ s0 = do(d↪ s) ^ [Vni=1 Does(✓i↪ di↪ s)] ^ ⇢0 = >?;
2. Trans('?↪ s↪ ⇢0 ↪ s0 ) ⌘ ?;
3. Trans(⇢1; ⇢2↪ s↪ ⇢0 ↪ s0 ) ⌘ (9⇢01 ▷T rans(⇢1↪ s↪ ⇢01 ↪ s0 ) ^ ⇢0 = ⇢01 ; ⇢2) _ F inal(⇢1↪ s) ^ T rans(⇢2↪ s↪ ⇢0 ↪ s0 );
4. Trans(⇢1 ♣ ⇢2↪ s↪ ⇢0 ↪ s0 ) ⌘ T rans(⇢1↪ s↪ ⇢0 ↪ s0 ) _ T rans(⇢2↪ s↪ ⇢0 ↪ s0 );
5. Trans(⇡x▷⇢↪ s↪ ⇢0 ↪ s0 ) ⌘ 9x▷Trans(⇢↪ s↪ ⇢0 ↪ s0 );
6. Trans(⇢⇤ ↪ s↪ ⇢0 ↪ s0 ) ⌘ 9⇢00 ▷T rans(⇢↪ s↪ ⇢00 ↪ s0 ) ^ ⇢0 = ⇢00 ; ⇢⇤ ;
7. Trans(while ' do ⇢↪ s↪ ⇢0 ↪ s0 ) ⌘ 9⇢00 ▷ '[s] ^ T rans(⇢↪ s↪ ⇢00 ↪ s0 ) ^ ⇢0 = ⇢00 ; (while ' do ⇢);
8. Trans(⇢1 M ▷▷▷ M ⇢m↪ s↪ ⇢0 ↪ s0 ) ⌘ (Vmk=1 9⇢0k ▷Trans(⇢k↪ s↪ ⇢0k ↪ s0 )^⇢0 = ⇢01 M ▷▷▷ M ⇢0m)_ ¶≻[Vmk=1 9⇢0k ▷T rans(⇢k↪ s↪ ⇢0k ↪ s0 )] ^ T rans(⇢1 M ▷▷▷ M ⇢m-1↪ s↪ ⇢0 ↪ s0 )♦.
9. Trans(⇢1O▷▷▷O⇢m↪ s↪ ⇢0 ↪ s0 )⌘Trans(⇢1↪ s↪ ⇢0 ↪ s0 ) _ ¶≻9⇢01 ↪ s00 ▷T rans(⇢1↪ s↪ ⇢01 ↪ s00 ) ^ T rans(⇢2O▷▷▷O⇢m↪ s↪ ⇢0 ↪ s0 )♦;
10. Final(✓↪ s) ⌘ ?;
11. Final('?↪ s) ⌘ '[s];
12. Final(⇢1; ⇢2↪ s) ⌘ Final(⇢1↪ s) ^Final(⇢2↪ s);
13. Final(⇢1 ♣ ⇢2↪ s) ⌘ Final(⇢1↪ s) _Final(⇢2↪ s);
14. Final(⇡x▷⇢↪ s) ⌘ 9x▷Final(⇢↪ s);
15. Final(while ' do ⇢↪ s↪ ⇢0 ↪ s0 ) ⌘ '[s] ^ F inal(⇢↪ s) _ ≻'[s];
16. Final(⇢⇤ ↪ s) ⌘ >;
17. Final(⇢1O▷▷▷O⇢m)↪ s) ⌘ Vmk=1 Final(⇢k↪ s);

Example 1 Cont'd.

1. Final(⇢1 M ▷▷▷ M ⇢m↪ s) ⌘ Final(⇢1↪ s).
2. ÷ Let ⇢1 = (hup↪ ⇤i; hup↪ ⇤i; hpick↪ ⇤i)O(hright↪ ⇤i; hright↪ ⇤i; hpick↪ ⇤i). Then ⇢1 is a strategy for agent 1 in situation S0 such that he prefers the acorn in position (-1↪ 1).
3. ÷ Let ⇢2 = (hup ♣ left↪ ⇤i; hup↪ ⇤i) M (hup ♣ right↪ ⇤i; hdown↪ ⇤i). Since this is a prioritized conjunction, when ⇢2 is performed in S0, agent 1 should move up twice.
4. ÷ Let ⇢3 = hup↪ downi; hright↪ lefti. Then ⇢3 is a group strategy for the two agents in situation S0 to achieve the goal of meeting at (0↪ 0).

We now formally define the notion that a group strategy satisfies an SGolog program. First, we introduce an abbreviation Sat1(fG↪ ⇢↪ s), which intuitively means that group strategy fG complies with program ⇢ in one step from s. It is inductively defined as follows:

1. Sat1(fG↪ '?↪ s) ▷=?;
2. Sat1(fG↪ ✓↪ s) ▷= Vi2G Does(✓i↪ fi(s)↪ s);
3. Sat1(fG↪ ⇢1 ♣ ⇢2↪ s) ▷= Sat1(fG↪ ⇢1↪ s) _ Sat1(fG↪ ⇢2↪ s);
4. Sat1(fG↪ ⇢1; ⇢2↪ s) ▷= Sat1(fG↪ ⇢1↪ s) _ F inal(⇢1↪ s) ^ Sat1(fG↪ ⇢2↪ s);
5. Sat1(fG↪ ⇡x▷⇢↪ s) ▷= 9x▷Sat1(fG↪ ⇢↪ s);
6. Sat1(fG↪ ⇢⇤ ↪ s) ▷=Sat1(fG↪ ⇢↪ s);
7. Sat1(fG↪while ' do ⇢↪ s) ⌘ '[s] ^Sat1(fG↪ ⇢↪ s);
8. Sat1(fG↪ ⇢1 M ▷▷▷ M ⇢m↪ s) ▷= 9s0 ↪ d▷[Vmk=1 9⇢0k T rans(⇢k↪ s↪ ⇢0k ↪ s0 ) ^ s0 = do(d↪ s) ^ dG = fG(s)] _ ≻[9s0 Vmk=1 9⇢0k T rans(⇢k↪ s↪ ⇢0k ↪ s0 )] ^ Sat1(fG↪ ⇢1 M ▷▷▷ M ⇢m-1↪ s).
9. Sat1(fG↪ ⇢1O▷▷▷O⇢m↪ s) ▷= 9⇢0 ↪ s0 ▷T rans(⇢1↪ s↪ ⇢0 ↪ s0 ) ^ Sat1(fG↪ ⇢1↪ s) _ 8⇢0 ↪ s0≻T rans(⇢1↪ s↪ ⇢0 ↪ s0 ) ^ Sat1(fG↪ ⇢2O▷▷▷O⇢m↪ s);

As for Sat1(fG↪ ⇢↪ s), we only consider one step from situation s. To represent a collective strategy of a coalition by an SGolog program, we specify how a group strategy completely complies with this program from a situation.

Here Trans+ is the transitive closure of Trans. Intuitively, Sat(fG↪ ⇢↪ s) means that any situation s0 reachable from s following fG is either a situation resulting from the execution of ⇢, or an situation following a final situation of ⇢.

Obviously, we can prove that ⌃ ♣= Sat(fG↪ ⇢↪ s) ⊃ Sat1(fG↪ ⇢↪ s), that is, if fG complies with ⇢ from s on, then it must comply with ⇢ in one step. In fact, any non-final configuration (⇢0 ↪ s0 ) which comes from configuration (⇢↪ s) according to fG will conform with the remaining ⇢0 in s0 at the next situation. That is,

Therefore, we can say that program ⇢ completely determines a collective strategy fG from a situation s, if we have Sat(fG↪ ⇢↪ s) ^ 8f 0G↪ s0 ▷Sat(f 0G↪ ⇢↪ s) ^ s fG s0 ⊃ fG(s0 ) = f 0G(s0 ). According to the above results, we can also have:

Proposition 2

• ÷ ⌃ ♣= Sat(fG↪ '?; ⇢↪ s) ⌘ '[s] ^ Sat(fG↪ ⇢↪ s).
• ÷ ⌃ ♣= [Vi2G Possi(fi(s)↪ s)] ⊃ Sat(fG↪ ⇢↪ s), where ⇢ = while > do ¯⇤.

6 Joint ability under an SGolog program

In this section, we adapt the approach of [Ghaderi et al., 2007] to formalize joint ability of coalitions under commitments to strategy programs.

We first define the preferred strategies of agent i under an SGolog program ⇢ in situation s by the approach of iterated elimination of dominated strategies. Given an agent i, a group G, a strategy fi, a program ⇢, a situation s, and a goal φ,

So agent i prefers strategy fi for goal φ under the program ⇢ if it is kept for all levels n, where n is a natural number.

There are two cases for the definition of Keep:

So for agents outside the coalition, we keep those executable strategies satisfying ⇢.

(2) i 2 G: Keep is inductively defined as follows:

Keep(i↪G↪ n+1↪ fi↪ ⇢↪ φ↪ s) ▷=Keep(i↪G↪ n↪ fi↪ ⇢↪ φ↪ s) ^

Keep(i↪G↪ 0↪ fi↪ ⇢↪ φ↪ s) ▷= EX(i↪ fi) ^Sat(fi↪ ⇢↪ s);

i ▷[Keep(i↪ G↪ n↪ f 0

≻9f 0

i ↪ fi↪ ⇢↪ φ↪ s)

i ↪ ⇢↪ φ↪ s)^GT E(i↪ G↪ n↪ f 0

For agent i, the strategies kept at level n+1 are those kept at level n for which there is not a better one at level n.

^ ≻GT E(i↪ G↪ n↪ fi↪ f 0

GTE is defined as follows:

i ↪ ⇢↪ φ↪ s)]▷

Strategy fi is as good as f 0 i for agent i to achieve the goal φ under ⇢ if i believes that whenever f 0 i works with strategies kept by the rest of the agents so does fi.

If we omit ⇢, then Pref(i↪ AG↪ fi↪ φ↪ s) is exactly what is defined by Ghaderi et al. If i ◁2 G, then we have P ref (i↪ G↪ fi↪ ⇢↪ s)⌘EX(i↪ fi)^Sat(fi↪ ⇢↪ s)▷

We now define the joint ability of a coalition to achieve a goal under commitments to an SGolog program.

Definition 5 The joint ability of coalition G to achieve goal φ under SGolog program ⇢ in situation s is defined as:

Intuitively, the meaning of SA(G↪ ⇢↪ φ↪ s) is that first, coalition G has a group strategy that complies with the program, such that no matter which strategies complying with ⇢ other agents choose, φ holds under the strategy profile; second, all combinations of agents' preferred strategies which satisfy ⇢ can achieve φ.

The definition of joint ability depends on the infinite process of iterated elimination. However, for agents with bounded rationality, we can define the concept of bounded joint ability as follows: For n ≥ 0, if in the above definition of SA(G↪ ⇢↪ φ↪ s), we replace P ref (i↪ G↪ fi↪ ⇢↪ φ↪ s) with Keep(i↪G↪ n↪ fi↪ ⇢↪ φ↪ s), we get the definition of the n-th level joint ability, which we denote by SAn(G↪ ⇢↪ φ↪ s).

Now we give some properties about SA(G↪ ⇢↪ φ↪ s):

Proposition 3 1. If ⇢ =while > do ✓, then for any ⇢0 , ⌃ ♣= SA(G↪ ⇢; ⇢0 ↪ φ↪ s) ⌘ SA(G↪ ⇢↪ φ↪ s);

In fact, those specifications of abilities defined by Ghaderi et al. (2007) and in ATL can be viewed as joint abilities under some special SGolog programs. First, we formalize them in our framework with minor differences:

• ÷ JCan(φ↪ s) ▷=9fG8fG[EX(AG↪ fAG)⊃⌃φ(fAG↪ s)] ^ 8fAG[Vi2AG P ref (i↪ AG↪ fi↪ φ↪ s) ⊃ ⌃φ(fAG↪ s)];

Theorem 2 1. Let ⇢ =while > do ¯⇤, then ⌃ ♣= JCan(φ↪ s) ⌘ SA(AG↪ ⇢↪ ⌃φ↪ s)▷

• ÷ hhGiiφ ▷= 9fG▷EX(G↪ fG) ^ 8fG▷EX(G↪ fG) ⊃ φ(fAG↪ s).
• Given fG, there exists a corresponding SGolog program ⇢0 : while > do ✓, where ✓i = fi(now) for each i 2 G and ✓i = ⇤ for i 62 G. We have

Intuitively, the above two cases are two extremes of SGolog programs. For the former, no agent has any knowledge about the other agents' strategies. For the latter, the group strategy fG is the common knowledge of group G.

From our definition of joint ability, we can see that SGolog programs serve as the common knowledge of all agents. Thus we can use SGolog programs to specify rough collective strategies, protocols, conventions, or social laws.

Example 1 Cont'd. Suppose the goal of the two squirrels is that each squirrel will hold an acorn in at most 4 steps from S0. This can be represented with φsq : ⌃(step  4 ^ hold(1) ^ hold(2)). We now consider whether the two squirrels have joint abilities to achieve the goal under different SGolog programs:

• ÷ Let ⇢1 = while > do h⇤↪ ⇤i. Then Dsq 2 SA(¶1↪ 2♦↪ ⇢1↪ φsq↪ S0). Under this program, for squirrel 1 (resp. 2), any of his preferred strategies should move up (resp. down) or right (resp. left) in the first step. However, if squirrel 1 moves up and squirrel 2 moves left in the first step, no matter how they will act in the later steps, their goal cannot be achieved.
• ÷ Let ✓1 = hright↪ lefti, ✓2 = hup↪ downi, and ⇢2 be ✓1 or ✓2. Then Dsq ♣= SA(¶1↪ 2♦↪ ⇢2↪ φsq↪ S0). We explain using the example of ✓1. Under this program, the preferred strategy for squirrel 1 must be right; right; pick; and for squirrel 2 it must be left; left; pick. Therefore, any combination of the preferred strategies of the two squirrels can ensure the goal.
• ÷ Let ⇢3 = ✓1O✓2. Then Dsq ♣= SA(¶1↪ 2♦↪ ⇢3↪ φsq↪ S0). Since ✓1 can be executed in S0, it will be executed due to higher priority.
• ÷ Let ⇢4 = h⇤↪ downi; h⇤↪ downi. Then Dsq ♣= SA1(¶1↪ 2♦↪ ⇢↪ φsq ↪ S0) ^ ≻SA0(¶1↪ 2♦↪ ⇢↪ φsq ↪ S0). For goal φsq, initially, agent 1 keeps all those executable strategies, and agent 2 keeps those executable strategies whose first two steps both are down. When agent 1 moves right in the first step, the two agents cannot achieve their goal. However, at level 1, agent 1 should consider those kept strategies of agent 2 at level 0, then he only keeps those strategies whose first 3 steps are up↪ up↪ pick. Then any combination of the preferred strategies of the two agents can achieve the goal.

Example 2 We now consider a traffic rule example. As shown in Figure 2, there are two cars (1 and 2) driving in opposite directions on a road in which there are four lanes numbered as 1↪ 2↪ 3↪ 4. There is only one action move(k) which is always possible, here k is a lane. For simplicity, we assume the velocities of the two cars are the same, that is, when a car executes move(k), then it moves one unit forward. For i = 1↪ 2, there is a fluent loci(m↪ k↪ s), which means car i is on lane k with coordinate m in situation s. Two cars collide when they are at the same location. In this game, we assume that neither car can see the other car (for instance, when two cars are driving in the night with broken lights).

We have the following axioms:

P ossi(move(k)↪ s) ⌘ >↪ i = 1↪ 2; loc1(m↪ k↪ do(d↪ s)) ⌘ 9k0 ▷loc1(m - 1↪ k0 ↪ s) ^ d1 = move(k); loc2(m↪ k↪ do(d↪ s)) ⌘ 9k0 ▷loc2(m + 1↪ k0 ↪ s) ^ d2 = move(k); 9k▷loc1(0↪ k↪ S0) ^ 9k0 ▷loc2(n↪ k0 ↪ S0)▷

We denote the BAT of this game as Dtr, and the goal formula is ' = ≻⌃9m↪ k▷loc1(m↪ k) ^ loc2(m↪ k), meaning that two cars will never collide.

Let ⇢ = while > do ¯⇤. Under ⇢, for any agent i, any strategy is a preferred strategy. However, if both agents choose to always performmove(1), they must collide. Thus Dtr 2 SA(¶1↪ 2♦↪ ⇢↪ '↪ S0). However, consider ⇢0 = while > do hmove(1) ♣move(2)↪move(3) ♣move(4)i. Intuitively, ⇢0 requires that both agents should always drive on the right. It is easy to see that under ⇢0 , the two cars have joint ability to avoid collision. Thus Dtr ♣= SA(¶1↪ 2♦↪ ⇢0 ↪ '↪ S0).

7 Conclusions

In this paper, by a simple extension of a variant of multi-agent epistemic situation calculus with a strategy sort, we have developed a general framework for strategy representation and reasoning for incomplete information concurrent games. The framework can be used to compactly represent the structure of such games, distinguish between different kinds of individual strategic abilities, specify collective strategies of coalitions, and reason about joint abilities of coalitions under commitments to collective strategy specifications. Both strategic abilities in ATL and joint abilities of Ghaderi et al. can be considered as joint abilities under special strategy specifications in our framework.

In our current framework, a strategy of an agent is a function from situations to actions, thus we have made the assumption that all agents have perfect recall. But in reality, agents may have limited memory, and are even memory-free. In the future, we would like to extend our framework to accommodate bounded-memory agents. Another future work is to identify decidable fragments of our framework based on existing work, e.g., [De Giacomo et al., 2013].

Acknowledgments

We thank the anonymous reviewers for helpful comments. This work received support from the Natural Science Foundation of China under Grant Nos. 61572535 and 61463044.