A Modal Logic for Joint Abilities under Strategy Commitments

1 Introduction

Representation and reasoning about strategic abilities has been an active research area in AI and multi-agent systems. The foundational work is Alternating-time Temporal Logic ATL/ATL∗ [Alur et al., 2002] where formula ⟪A⟫φ expresses that coalition A has a group strategy to ensure temporal goal φ holds no matter what the other agents do. The formulas are interpreted over concurrent game structures where multiple agents act concurrently and the system transition is determined by the collective behavior of agents.

Many variations and extensions of ATL/ATL∗ have been proposed, e.g., semantic variants about different abilities of agents under perfect vs imperfect information and perfect vs imperfect recall [Schobbens, 2004], explicit quantification over strategies [Chatterjee et al., 2010; Mogavero et al., 2014], probabilistic extensions [Huang et al., 2012], epistemic extensions or variations [van der Hoek and Wooldridge, 2003; Jamroga and van der Hoek, 2004; Naumov and Tao,

∗Corresponding Author

2018], resource bounded variations [Alechina et al., 2010], etc.

However, 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. They studied the coordination problem and present a formalization of joint ability of coalitions based on the idea of iterated elimination of (strictly) dominated strategies [Osborne and Rubinstein, 1999]. Essentially, a coalition has joint ability to achieve a goal if after iterated elimination of dominated strategies, any remaining joint strategy achieves the goal. Further, [Xiong and Liu, 2016] presented a formalization of joint ability of coalitions under commitments to strategy programs. However, both works use the very expressive situation calculus [Reiter, 2001], making it difficult to analyze properties of the logics. Recently, based on coalition logic [Pauly, 2002], [Hawke, 2017] proposed a logic of joint ability in two-player tacit games with a joint ability modality ((A))ϕ: two players have joint ability to achieve a goal if after iterated elimination of punishment strategies, i.e., those strategies that fail to achieve the goal no matter what other agents do, any remaining joint strategy achieves the goal. So they only eliminate punishment strategies, hence their concept of joint ability is much weaker than that of [Ghaderi et al., 2007].

Social rules [Shoham and Tennenholtz, 1995], such as traffic rules, play an important role in coordination. [ ˚Agotnes et al., 2007] used normative systems to describe norms/social rules semantically. As pointed out by [Ramanujam and Simon, 2008; Eijck, 2013], most extensions of ATL treat strategies as abstract objects rather than considering the internal structure of strategies. They proposed to use regular expressions to represent structured strategies. Existing strategic logics are based on various temporal logics such as LTL [Pnueli, 1977] and CTL [Clarke and Emerson, 1981]. [De Giacomo and Vardi, 2013] proposed linear dynamic logic LDL, an extension of LTL with regular expressions. Thus it is valuable to explore strategic logics based on LDL so that structured strategies can be represented.

Moreover, there have been works on specifying strategic abilities under constraints of rationality, by using various solution concepts in game theory. [Huang and Ruan, 2017]

integrated correlated equilibrium (CE) into ATL, taking CE as agents' joint strategy and optimizing over the utilitarian value. [Gutierrez et al., 2014] proposed a logic containing operator [NE]ψ, meaning ψ holds on all Nash equilibrium computations. [Gutierrez et al., 2017] investigated techniques for the characterization and verification of equilibria in multiplay games with goals expressed using logics based on LDL.

In this paper, based on the idea of [Ghaderi et al., 2007], we propose JAADL (meaning Alternating-time Dynamic Logic with Joint Abilities), a modal logic for joint abilities under strategy commitments, which is an extension of ATL∗ . Firstly, we introduce an operator (A)∞ψ ϕ, meaning ϕ holds after iterated elimination of (strictly) dominated strategies w.r.t. group A and goal ψ. Then coalition A has joint ability to achieve ψ can be represented as the formula (A)∞ψ ⟪∅⟫ψ, where ∅ is the empty set, which means that after iterated elimination of (strictly) dominated strategies, any remaining joint strategy achieves ψ. Secondly, our logic is based on LDL, so that we can use regular expressions to represent commitments to structured strategies such as traffic rules, and this can really help eliminate lack of coordination and achieve joint abilities in many cases. For example, the commitment that Car 1 cannot drive in Lane 4 is represented by the regular expression (¬move1(4))∗ . This is similar to Xiong and Liu's work where strategy commitments are described by Golog programs. We present the syntax and semantics of JAADL, analyze valid formulas, give four sufficient/necessary conditions for joint abilities, and apply these conditions to analyze some interesting examples. Finally, we show that model checking memoryless JAADL is in EXPTIME.

2 Preliminaries

In this section, we introduce the concepts of concurrent game structures and strategies.

Let AP be a finite non-empty set of atoms, AC a finite non-empty set of actions, and let AG={1, . . . , n} be a finite non-empty set of agents. We use ∅ to denote the empty set.

• W is a finite non-empty set of states; w0 ∈ W is a designated initial state; L is a labeling function mapping each state to a subset of AP; τ is a transition function mapping a state w and a decision at w to a new state;

Definition 1 (Concurrent Game Structures). A concurrent game structure (CGS) is a tuple G = ⟨W, L, P, τ, w0 ⟩, where

• for each agent i, Pi is a possible action functionmapping each state to a subset of AC; a decision at state w is a function mapping each agent i to an action from Pi(w);
• AG = {a, b, c}, AP = {win}, AC = {R, P, S};

we use D(w) to denote the set of decisions at w; Example 1 (Three-player Collaborative PRS (Paper, Rock, and Scissors)). As shown in Figure 1, three players simultaneously play the actions of Paper, Rock, and Scissors. The group wins if Player a is not beaten by Player b and Player b is not beaten by Player c. We formalize the game as a CGS G as follows:

• W = {si, sw, sl}, w0 = si; · L(si) = L(sl) = ∅, L(sw) = {win};
• Pa(si) = {R, S}, Pb(si) = {P, S}, Pc(si) = {R, P}; · τ(si, d) = sw for d ∈ Dw = {RSP,SPR,SPP,SSP}, τ(si, d) = sl for d ∈ Dl = {RPR,RPP,RSR, SSR}.
• AG = {1, 2}, AP = {crash}, AC = {move(k) ∣ k ∈ {1, 2, 3, 4}}, where move(k) means moving forward one unit while switching to Lane k.

Example 2 (The Traffic Rule Example). As shown in Figure 2, there are 4 lanes, and two cars that drive in opposite directions. We model this example as a CGS where

• W = {(x1, y1,x2, y2) ∣ 1 ≤ x1,x2 ≤ 100, 1 ≤ y1, y2 ≤ 4}, where (xi, yi) represents the position of car i.
• For any i = 1, 2, w ∈ W, if crash /∈ L(w), Pi(w) = AC, otherwise, Pi(w) = ∅.
• w0 = (1, 2, 100, 3). · For any w = (x1, y1,x2, y2) ∈ W, crash ∈ L(w) iff (x1, y1) = (x2, y2).
• τ can be easily given. For example, τ ((5, 3, 2, 4), (move(4), move(2))) = (6, 4, 1, 2).

Definition 2. A track h in a CGS G is a finite state-decision sequence w0d0w1d1...wk s.t. for all i (0 ≤ i < k), di ∈ D(wi), and wi+1 = τ(wi, di). We use last(h) to denote wk.

We now define the concepts of tracks and paths. Tracks are finite state-decision sequences, they are used to define strategies: a strategy is a mapping from tracks to actions. Paths are infinite state-decision sequences, they are used to interpret JAADL path formulas.

Definition 3. A path λ in a CGS G is an infinite state-decision sequence w0d0w1d1... s.t. for all i ≥ 0, di ∈ D(wi), and wi+1 = τ(wi, di).

Definition 4. A strategy for agent i starting from state w is a function mapping each track h beginning from w to an action from Pi(last(h)). We let Stri(w) denote the set of all strategies for agent i starting fromw.

Since we will handle elimination of strategies, we introduce the concept of strategy spaces. A strategy space specifies the set of possible strategies for each agent.

Definition 5. A strategy space s starting from state w is a function mapping each agent i to a subset of Stri(w). The full strategy space fs(w) starting from state w maps each agent i to Stri(w).

Definition 6. A memoryless strategy for agent i is a function mapping each state w to an action from Pi(w). The full memoryless strategy space, denoted by fms, maps each agent i to the set of all memoryless strategies for i.

We use σ to range over strategies. A group strategy of A ⊆ AG is a mapping from A to strategies. We use σA to range over group strategies of A. As a special case, we use σi to range over strategies for agent i. A joint strategy is a group strategy of AG. We use σall to range over joint strategies. For i ∈ AG, we use -i to denote AG - {i}.

3 Syntax and Semantics of JAADL

Definition 7. A state w and a joint strategy σall determine a unique path w0d0w1d1w2d2 . . . as follows: w0 = w0 , and for each j ≥ 0, dj is the decision associated to the track w0 . . .wj, i.e., for each agent i, dj(i) = σi(w0 . . .wj), and wj+1 = τ(wj , dj). We use out(w, σall) to denote this path.

In this section, we introduce the syntax and semantics of JAADL. The logic is an extension of ATL∗ in that it is based on LDL and introduces operators of elimination of dominated strategies (EDS).

We begin with the syntax of JAADL. We use ϕ to denote state formulas, ψ path formulas, φ propositional formulas, and ρ path expressions, which are regular expressions over propositional formulas and tests of path formulas. Other than atomic propositions from AP, we introduce atomic propositions of the form ai where a ∈ AC and i ∈ AG, meaning agent i does action a. We use ⊺ to denote true. Definition 8. JAADL formulas are built as follows:

where p ∈ AP , and A ⊆ AG. Intuitively, ⟨ρ⟩ψ means that from the current state in the path there exists an execution satisfying the path expression ρ such that its last state satisfies ψ. We use [ρ]ψ as abbreviation for ¬⟨ρ⟩¬ψ. It is easy to encode LTL into path formulas as follows: Xϕ translates to ⟨⊺⟩ϕ; Gϕ translates to [⊺∗ ]ϕ;

ϕ1Uϕ2 translates to ⟨(ϕ1?; ⊺)∗ ⟩ϕ2. Intuitively, ⟪A⟫ψ means group A has a strategy to achieve ψ. A special case of ⟪A⟫ψ is ⟪∅⟫ψ, which means ψ always holds no matter how the agents play. We usually write ⟪i1, . . . , ik⟫ instead of ⟪{i1, . . . , ik}⟫ where i1, . . . , ik ∈ AG. (A)ψϕ means ϕ holds after one step of elimination of dominated strategies w.r.t. group A and the goal ψ. (A)∞ψ ϕ

means ϕ holds after iterated elimination of dominated strategies w.r.t. group A and the goal ψ. We use (A)2ψ ϕ to denote

Example 2 cont'd. We are concerned about whether the two cars have joint ability to ensure no crash will ever happen (resp. under the commitment that Car 1 cannot drive in Lane 4). This can be represented by the formula ((1, 2))∞[⊺∗ ]¬crash (resp.

(A)ψ(A)ψϕ, and similarly for (A)kψ ϕ, where k ∈ N. We use ((A))k ψ to abbreviate for (A)kψ ⟪∅⟫ψ. When k = 1, we simply write ((A))ψ. Intuitively, ((A))k ψ means after k-round elimination of dominated strategies, ψ holds no matter how the agents play, and we say group A has stage k joint ability to achieve ψ. We use ((A))∞ψ to abbreviate for (A)∞ψ (⟪A⟫ψ ∧ ⟪∅⟫ψ). The reason we conjoin ⟪A⟫ψ to ⟪∅⟫ψ is that as we will show at the end of this section, the strategy space might become empty after iterated elimination of dominated strategies. We omitted the ⟪A⟫ψ part in the introduction to avoid confusion. Intuitively, ((A))∞ψ means group A has joint ability to ensure ψ.

((1, 2))∞[(¬move1(4))∗ ]¬crash). We now provide the semantics of JAADL. We begin with the semantics of propositional formulas, which are interpreted over state-decision pairs.

• w, d ⊧ p if p ∈ L(w);

Definition 9. Given a CGS G, a state w, and a decision d at w, we interpret propositional formulas inductively:

• w, d ⊧ ai if d(i) = a;
• w, d ⊧ ¬φ if w, d /⊧ φ;

Definition 10 (JAADL Semantics). Given a CGS G, a state w, a strategy space s, and a path λ, we interpret state formulas and path formulas (we omit the cases of ¬ and ∧) and define the operators RA,ψ,w(s) and R∞ A,ψ,w (s) inductively:

· w, d ⊧ φ1 ∧φ2 if w, d ⊧ φ1 and w, d ⊧ φ2. We interpret state formulas and path formulas inductively. The interpretation is wrt a strategy space. When interpreting state formulas, we make use of two operators on strategy spaces: RA,ψ,w(s) and R∞ A,ψ,w (s). Intuitively, RA,ψ,w(s) means the reduction of s via elimination of dominated strategies, and R∞ A,ψ,w (s) means the reduction of s via iterated elimination of dominated strategies.

• w, s ⊧ p if p ∈ L(w). · w, s ⊧ ⟪A⟫ψ if there exists a group strategy σA ∈ sA such that for all strategies σ-A ∈ s-A, we have out(w, (σA, σ-A)), s ⊧ ψ.
• λ, s ⊧ ϕ if w0, s ⊧ ϕ, where λ = w0d0w1 . . .. · λ, s ⊧ ⟨φ⟩ψ if w0, d0 ⊧ φ and λ′ , s ⊧ ψ, where λ = w0d0w1 . . . and λ′ = w1d1 . . ..
• w, s ⊧ (A)ψϕ if w, RA,ψ,w(s) ⊧ ϕ. · w, s ⊧ (A)∞ψ ϕ if w,R∞ A,ψ,w (s) ⊧ ϕ.
• λ, s ⊧ ⟨ψ1?⟩ψ2 if λ, s ⊧ ψ1 and λ, s ⊧ ψ2. · λ, s ⊧ ⟨ρ1 + ρ2⟩ψ if λ, s ⊧ ⟨ρ1⟩ψ or λ, s ⊧ ⟨ρ2⟩ψ.
• λ, s ⊧ ⟨ρ1; ρ2⟩ψ if λ, s ⊧ ⟨ρ1⟩⟨ρ2⟩ψ.

• λ, s ⊧ ⟨ρ0 ⟩ψ if λ, s ⊧ ψ. · λ, s ⊧ ⟨ρk+1 ⟩ψ if λ, s ⊧ ⟨ρk ; ρ⟩ψ for k ∈ N.

For a strategy space s, we define the reduction of s wrt group A, goal ψ and state w as follows: RA,ψ,w(s) = s′ s.t. if i ∉ A, s′i = si; otherwise, s′i = {σi ∈ si ∣ ¬∃σ′i ∈ si.σ′i >ψ,w,s σi}. For k ≥ 2, we define RkA,ψ,w (s) = RA,ψ,w(Rk-1 A,ψ,w (s)). Finally, we define the iterative reduction of s: R∞ A,ψ,w (s) = s′ s.t. for i ∈ AG, s′i = ⋂∞k=0 RkA,ψ,w (s)i.

· λ, s ⊧ ⟨ρ∗ ⟩ψ if there exists k ∈ N such that λ, s ⊧ ⟨ρk ⟩ψ. For σi ∈ si, we define the set of strategies of -i that work with σi to ensure ψ wrt state w and strategy space s as follows: Mψ,w,s(σi) = {σ-i ∈ s-i ∣ out(w, (σi,σ-i)), s ⊧ ψ}. Sometimes when ψ, w and s are clear from the context, we omit them and write M(σi). For σi,σ′i ∈ si, we write σi ≥ψ,w,s σ′i if Mψ,w,s(σi) ⊇ Mψ,w,s(σ′i ); we write σi >ψ,w,s σ′i if Mψ,w,s(σi) ⊃ Mψ,w,s(σ′i ), and we say σi dominates σ′i .

Definition 11. We say a state formula ϕ is valid if for all CGS G, we have G ⊧ ϕ, meaning w0 , fs(w0 ) ⊧ ϕ, where w0 is the initial state of G.

Example 1 cont'd. We have G ⊧ ⟪a, b⟫⟨⊺⟩win, since agents a and b have a group strategy SP to achieve win no matter c plays R or P.

Recall fs(w) is the full strategy space starting from state w. Note that when we write ((A))k ψ, it means that the formula holds from a third-person point of view. Thus the third-person imitates the process of elimination of dominated strategies for each agent in A.

The procedures of iterative EDS for coalitions {a, b, c} and

{a, b} are shown in Figures 3 and 4, respectively. During the procedures, for each agent i in AG, for each available strategies σi of i, we list all the group strategies in M(σi), which is just the set of strategies of -i that work with σi to ensure the goal ⟨⊺⟩win w.r.t. the initial state and the full strategy space. Then we eliminate those strategies σi of agent i, whose M(σi) is a strict subset of some M(σj). Thus G ⊭ ⟪∅⟫⟨⊺⟩win, G ⊧ ((a, b, c))⟨⊺⟩win, G ⊭ ((a, b))⟨⊺⟩win, G ⊧ ((a, b))2 ⟨⊺⟩win. We now introduce some terminology about strategies, which will be used in analyzing properties of our logic.

Definition 12. We say σ is a winning strategy for i wrt ψ, w, s if Mψ,w,s(σ) is s-i. We say σ is a punishment strategy for i wrt ψ, w, s if Mψ,w,s(σ) = ∅. We say σ is an optimal strategy for i wrt ψ,w, s, if for any σ′ ∈ si, σ ≥ψ,w,s σ′ .

Thus σ is a winning strategy for i if σ works with any strategy of -i. The formula ⟪i⟫ψ represents that i has a winning strategy wrt goal ψ. Similarly, σ is a punishment strategy for i if σ works with no strategy of -i. The formula ⟪i⟫¬ψ expresses that i has a punishment strategy wrt goal ψ. An optimal strategy for i is one that weakly dominates all others. Unfortunately, we cannot represent in JAADL that i has an optimal strategy wrt goal ψ.

Definition 13. We say that two strategies σ and σ′ are equivalent wrt ψ,w, s if Mψ,w,s(σ) = Mψ,w,s(σ′ ). We say that two strategies σ and σ′ are incomparable wrt ψ,w, s if Mψ,w,s(σ) ⊈ Mψ,w,s(σ′ ) and Mψ,w,s(σ′ ) ⊈ Mψ,w,s(σ).

Intuitively, in the 0-1 matrix, the payoff for a joint strategy is 1 if it achieves the goal, and 0 otherwise.

Definition 14. Given a CGS G, a state w, a strategy space s, and a goal ψ, the payoff matrix for ψ, denoted Cψ is a 0-1 matrix defined as follows: for each σall ∈ s, Cψ(σall) = 1 iff out(w, σall), s ⊧ ψ.

The definition of payoff matrices clarifies that our definition of elimination of dominated strategies is an instance of the one from game theory [Osborne and Rubinstein, 1999].

Note that different from game theory, when the strategy space is infinite, it might become empty after iterative elimination of dominated strategies. We illustrate with an example.

Example 3. There are two agents 1 and 2. Each agent i has infinitely many strategies σ1 i ,σ2 i , . . .. Figure 5 shows the payoff matrix for the goal ψ: The infinitely many rows and columns show agents 1 and 2's strategies, respectively; for each row j, there are only 1s in columns j and j + 1. This means: for each σj1 , the set of strategies of 2 that work with σj1 to achieve the goal ψ is {σj2 ,σj+1 2 }. At stage 1, Column 1 is eliminated since it is dominated by Column 2; then at stage 2, Row 1 is eliminated since it is dominated by Row 2. Then Column 2 and Row 2 will be eliminated. Eventually, each strategy will be eliminated. By our definitions, neither ((1, 2))k ψ where k ∈ N nor ((1, 2))∞ψ holds.

4 Properties of JAADL

In this section, we analyze valid formulas in JAADL, and give sufficient/necessary conditions for joint abilities, which we use to analyze some interesting examples.

First of all, it is easy to prove the following result. Item 1 says the elimination operators satisfy the K axiom. Item 2 says the negation operator can move inside elimination operators. Item 3 says the absence of stage k joint ability is equivalent to the existence of a joint strategy to achieve the negation of the goal after k round elimination of dominated strategies. Item 4 says stage k joint ability implies stage j joint ability, where j ≥ k or j = ∞. Item 5 says stage k joint ability implies the existence of a group strategy to achieve the goal. Item 6 says a coalition does not have joint ability if the other agents have a strategy to ensure the negation of the goal.

Proposition 1. The following formulas are valid:

1. (A)kψ (ϕ1 →ϕ2) → ((A)kψ ϕ1 → (A)kψ ϕ2), k ∈ N∪{∞}. 2. ¬(A)kψ ϕ ≡ (A)kψ ¬ϕ, k ∈ N∪ {∞}. 3. ¬((A))k ψ ≡ (A)kψ ⟪AG⟫¬ψ, k ∈ N. 4. ((A))k ψ → ((A))j ψ, where j ≥ k or j =∞.
2. Proof. Let G be a CGS, w its initial state, and s = fs(w). 1. Suppose w, s ⊧ (A)kψ (ϕ1 → ϕ2) and w, s ⊧ (A)kψ ϕ1. Then w, RkA,ψ,w (s) ⊧ ϕ1 → ϕ2 and w, RkA,ψ,w (s) ⊧ ϕ1. Thus w, RkA,ψ,w (s) ⊧ ϕ2, so w, s ⊧ (A)kψ ϕ2.
3. w, s ⊧ ¬((A))k ψ iff w, s ⊭ (A)kψ ⟪∅⟫ψ iff w,RkA,ψ,w (s) ⊭ ⟪∅⟫ψ iff w,RkA,ψ,w (s) ⊧ ⟪AG⟫¬ψ iff w, s ⊧ (A)kψ ⟪AG⟫¬ψ.
4. w, s ⊧ ¬(A)kψ ϕ iff w, s ⊭ (A)kψ ϕ iff w,RkA,ψ,w (s) ⊭ ϕ iff w, RkA,ψ,w (s) ⊧ ¬ϕ iff w, s ⊧ (A)kψ ¬ϕ.
5. Suppose w, s ⊧ ((A))k ψ, i.e., w,RkA,ψ,w (s) ⊧ ψ. Since RjA,ψ,w (s) ⊆ RkA,ψ,w (s), where j ≥ k or j = ∞, we have w, RjA,ψ,w (s) ⊧ ψ, so w, s ⊧ ((A))j ψ.
6. Suppose w, s ⊧ ⟪A⟫¬ψ. Then there exists σ-A ∈ s-A such that for all σA ∈ sA, (σA,σ-A) cannot achieve ψ. Thus w, s ⊭ ((A))∞ψ.
7. Suppose w, s ⊧ ((A))k ψ. ThenRkA,ψ,w (s) ≠ ∅ and each σA ∈ RkA,ψ,w (s)A ensures ψ. Thus w, s ⊧ ⟪A⟫ψ.

The following result says that if coalition A has a strategy to achieve ψ, then after elimination of dominated strategies, no agent in A has a punishment strategy. This is because such a strategy is already eliminated.

Proposition 2. ⟪A⟫ψ → (A)ψ⋀a∈A¬⟪a⟫¬ψ is valid.

Proof. Let G be a CGS, w its initial state, and s = fs(w). Suppose w, s ⊧ ¬(A)ψ ⋀a∈A ¬⟪a⟫¬ψ. By Proposition 1(2), w, s ⊧ (A)ψ ⋁a∈A⟪a⟫¬ψ. So w, RA,ψ,w(s) ⊧ ⋁a∈A⟪a⟫¬ψ. Then there exists a ∈ A such that w,RA,ψ,w(s) ⊧ ⟪a⟫¬ψ. Thus w, s ⊧ ¬⟪A⟫ψ, otherwise each σa ∈ sa that ensures ¬ψ will be eliminated and not be in RA,ψ,w(s).

The following result says that coalition A has joint ability iff after iterative EDS, some agent a in A has a winning strategy. This is because if a has a winning strategy, then every remaining strategy is a winning strategy, otherwise, it is already eliminated.

Note that if ψ1 → ψ2 is valid, ((A))k ψ1 → ((A))k ψ2, where k ∈ N ∪ {∞}, may not be valid. In general, the processes of iterated elimination for two different goals might be different, even if there is a logical relationship between them. For example, there are two agents, and each agent has two strategies. The following shows the payoff matrices for the strategies wrt goals ψ1 and ψ2. Since ψ1 → ψ2 is valid, when we have a 1 in Cψ1 , we must have a 1 in the same position in Cψ2 . It is clear that ((A))∞ψ1 holds, but ((A))∞ψ2 does not hold.

Proof. Let G be a CGS, w its initial state, and s = fs(w). Suppose w, s ⊧ ((A))∞ψ. Then w,R∞ A,ψ,w (s) ⊧ ⟪A⟫ψ ∧ ⟪∅⟫ψ. Then for all a ∈ A, w,R∞ A,ψ,w (s) ⊧ ⟪a⟫ψ. So w, s ⊧ (A)∞ψ ⟪a⟫ψ. Now suppose w, s ⊧ (A)∞ψ ⟪a⟫ψ for some a ∈ A. Then some σa ∈ R∞ A,ψ,w (s)a is a winning strategy wrt ψ. Thus any strategy in R∞ A,ψ,w (s)a is a winning strategy. So w, R∞ A,ψ,w (s) ⊧ ⟪A⟫ψ ∧ ⟪∅⟫ψ. Hence w, s ⊧ ((A))∞ψ.

Proof. When A ⊆ B, for each agent a, RB,ψ,w(s)a ⊆ RA,ψ,w(s)a. Let G be a CGS, w its initial state, and s = fs(w). Suppose w, s ⊧ ((A))ψ, i.e., (A)ψ⟪∅⟫ψ. Then w,RA,ψ,w(s) ⊧ ⟪∅⟫ψ. Thus w,RB,ψ,w(s) ⊧ ⟪∅⟫ψ. Hence w, s ⊧ ((B))ψ.

Proposition 4. When A ⊆ B, ((A))ψ → ((B))ψ is valid.

However, when A ⊆ B, ((A))k ψ → ((B))k ψ, where k ∈

N ∪ {∞}, may not be valid. We now give three sufficient conditions for joint abilities. The following result shows that if at stage k, some agent in the coalition has a winning strategy, then there is joint ability at stage k + 1.

Proof. Suppose a has a stage k winning strategy σa. Then σa remains at stage k+1. For every strategy σ′a which remains at stage k+1, it must be a stage k+1 winning strategy, otherwise, σa > σ′a , hence it is already eliminated. Thus there is joint ability at stage k + 1.

Theorem 2. If ⟪A⟫ψ holds, and at stage k, each agent in A has an optimal strategy, then there is joint ability at stage k + 1.

Theorem 3. If ⟪A⟫ψ holds, and at stage k, ∣A∣ -1 agents in A have optimal strategies, then there is joint ability at stage k + 2.

Proof. Suppose ⟪A⟫ψ holds, and at stage k, each agent in A has an optimal strategy. Then for each joint strategy σall where for each a ∈ A, σa is an optimal strategy, σall achieves ψ. At the next stage, each non-optimal strategy will be deleted. Hence, there is joint ability at stage k + 1.

Proof. Suppose ⟪A⟫ψ holds, a ∈ A, and at stage k, each agent in A-{a} have an optimal strategy. Then a has a strategy σa such that for each group strategy σ-a where for each b ∈ A- {a}, σb is an optimal strategy, (σa, σ-a) achieves the goal. At stage k + 1, each non-optimal strategy of each agent in A-{a} will be deleted. Thus a must have a remained strategy which is a winning strategy. By Theorem 1, there is joint ability at stage k + 2. Below, we give a necessary condition for joint abilities.

Theorem 4. Suppose at some stage, no agent in A has a winning strategy, and any two strategies are either equivalent or incomparable, then there is no joint ability.

Proof. When any two strategies are either equivalent or incomparable, no elimination is possible. Since no agent in A has a winning strategy, there is no joint ability.

Finally, we apply the above theorems to analyze the traffic rule example and two more interesting examples. Example 2 cont'd. Clearly, G ⊭ ((1, 2))∞[⊺∗ ]¬crash. This is because any two different strategies are incomparable, by Theorem 4, there is no joint ability.

However, if Car 1 cannot drive in Lane 4, then the two cars will have joint ability to ensure no crash will ever happen, i.e., G ⊧ ((1, 2))[(¬move1(4))∗ ]¬crash. This is because Car 2 can choose to always drive in Lane 4, which is a winning strategy. By Theorem 1, there is stage 1 joint ability.

Example 4 (Autonomous Cars). As shown in Figure 6, two cars move in the same direction. They need to switch lanes to avoid obstacles on the road. The two cars win if both get to the destination without crashing into each other or the obstacles. We can model it as a CGS G where AP = {win, crash}, and AC = {K,W, S}, where K means keeping moving, W means waiting, and S means switching lanes, i.e., moving up or down.

We first consider the situation where there are no obstacles on the road. We model this as the CGS G ′ . We use AK to denote the strategy of always keeping moving. Then G ′ ⊧ ((1, 2))∞[⊺∗ ]¬crash. This is because AK won't make a crash. Thus AK is a winning strategy. By Theorem 1, there is stage 1 joint ability.

Now we consider the case with obstacles. We have G ⊧ ((1, 2))2 ⟨⊺∗ ⟩win. This is because Car 1 has an optimal strategy: keep going, switch lane at position 7, and keep going. By Theorem 3, there is stage 2 joint ability.

We also have G ′ ⊧ ((1, 2))⟨⊺∗ ⟩win. We prove that for each car, AK is an optimal strategy: Let σ′ be a strategy of the other car. Suppose that (σ, σ′ ) achieves the goal, then there is no crash, and the other car gets to the destination. Since AK won't make a crash, (AK, σ′ ) achieves the goal. By Theorem 2, there is stage 1 joint ability.

Example 5 (The Squirrels World). There are two squirrels and two acorns living in a finite grid. Each squirrel can do actions below: pick up an acorn if she is located at the same cell as this acorn and does not hold any acorn; and move up, down, right, and left a cell. As shown in Figure 7, initially, squirrel 1 is located at the cell (-1, -1) and 2 is located at the cell (1, 1); there is only one acorn in each of the cell (-1, 1)

We first consider the formula ψ = ⟨⊺; ⊺; ⊺⟩(hold1 ∧hold2), which means each squirrel will hold an acorn in exactly 3 steps. Clearly, G ⊧ ⟪1, 2⟫ψ. This is because the two squirrels have a strategy to achieve ψ, for example, Squirrel 1 does the action sequence right; right; pick and Squirrel 2 does left; left; pick. However, G ⊭ ((1, 2))∞ψ3. It is easy to show that at stage 1, any two different strategies are incomparable. By Theorem 4, there is no joint ability.

and (1, -1), and in other cells there are no acorns. We can model this squirrels world as a CGS G, and we omit the details here. We use two atoms hold1 and hold2, where holdi means squirrel i holds an acorn.

If we require the first actions of the two squirrels to be (right, left) or (up, down), there is joint ability, i.e., G ⊧ ((1, 2))⟨right1 ∧ left2; ⊺; ⊺⟩(hold1 ∧ hold2) and G ⊧ ((1, 2))⟨up1 ∧ down2; ⊺; ⊺⟩(hold1 ∧ hold2). This is because in each case, each agent has an optimal strategy. By Theorem 2, there is stage 1 joint ability.

5 Model-CheckingMemoryless JAADL

In this section, we explore the computational complexity of model checking JAADL where we consider only memoryless strategies, which are functions from states to actions.

Algorithm 1 Labeling State Space

• 1: Label(G, s,ϕ) 2: for ϕ′ in Sub(ϕ) do
• 8: case ϕ′ = (A)ψϕ1 ∶ [ϕ′ ]s ← [ϕ1]StrS(A,ψ,w,s)
• 3: case ϕ′ = p ∶ [ϕ′ ]s ← {w ∈ W ∣ p ∈ L(w)} 4: case ϕ′ = ¬ϕ ∶ [ϕ′ ]s ←W - [ϕ]s 5: case ϕ′ = ϕ1 ∧ϕ2 ∶ [ϕ′ ]s ← [ϕ1]s ∩ [ϕ2]s 6: case ϕ′ = ⟨⟨A⟩⟩ψ ∶ 7: [ϕ′ ]s ← {w ∣ ∃σA ∈ sA∀σ-A ∈ s-A. P athF (G, w, (σA, σ-A), s, ψ) = true}
• 11: return [ϕ]s
• 9: case ϕ′ = (A)∞ψ ϕ1 ∶ [ϕ′ ]s ← [ϕ1]StrS∞(A,ψ,w,s) 10: end for

Algorithm 2 Model-Checking Path Formulas

• 1: function PathF(G,w,σall, s,ψ)
• 2: Max(ψ) ← the set of maximal state-subformulas in ψ
• 6: replace each occurrence in ψ of ϕ ∈ Max(ψ) by pϕ to get a pure LDL formula ψldl
• 3: for each ϕ ∈Max(ψ) do 4: define a fresh atom pϕ, let w ∈ L(pϕ) iff w ∈ Label(G, s, ϕ) 5: end for
• 7: return whether Kripke(w,σall) ⊧ldl ψldl

We first formally state the model checking problem for memoryless JAADL: Given a CGS G, and a JAADL formula ϕ, decide if w0 , fms ⊧ ϕ, where w0 is the initial state of G.

strategy space, thus the notation [ϕ]s has s as the subscript. Our algorithm proceeds by cases. For case ⟪A⟫ψ, we make use of function PathF shown in Algorithm 2, which is used to decide whether out(w, σall), s ⊧ ψ. A joint strategy σall and a state w in a CGS G uniquely determine an infinite path out(w, σall), which can be viewed as a finite Kripke model with initial state w, we denote it as Kripke(w, σall). Given a pure LDL formula ψldl, we can call the LDL modelchecking algorithm [Faymonville and Zimmermann, 2017] with minor change due to our action atoms, to verify whether Kripke(w,σall) ⊧ldl ψldl. Their algorithm is polynomial in the model size and exponential in the formula size.

Recall fms denotes the full memoryless strategy space of G. Now we give a labeling algorithm (Algorithm 1) which, given a CGS G = ⟨W,L,P, τ,w0 ⟩, a strategy space s, and a state formula ϕ, returns [ϕ]s, denoting the set of all states satisfying ϕ, i.e., [ϕ]s = {w ∈ W ∣ w, s ⊧ ϕ}. Note that different from ATL, JAADL formulas are evaluated w.r.t. a

For case (A)ψϕ1, we call function StrS given in Algorithm 3, which is used to calculate RA,ψ,w(s). For case ϕ′ = (A)∞ψ ϕ1, R∞ A,ψ,w (s) can be computed as follows: repeat s ← StrS(A, ψ, w, s) until there is no change to s. Theorem 5. Model-checking memoryless JAADL can be done in time exponential in the model size and formula size.

Proof. Let n be the model size and l the formula size. Then the number of different memoryless strategies is O(2n ). Calculating the reduction and iterative reduction of a strategy

Algorithm 3 Calculating Reduced Strategy Space

• 1: function StrS(A,ψ,w, s) 2: for each i ∈ A do 3: for each σi ∈ si, compute Mψ,w,s(σi), i.e.,
• {σ-i ∈ s-i ∣ PathF(G,w, (σi,σ-i), s,ψ) = true} 4: for each σi, σ′i ∈ si, if Mψ,w,s(σi) ⊃ Mψ,w,s(σ′i ) then si ← si - {σ′i } 5: end for 6: return s

space takes time O(2n 2l ), and so does processing the case ⟨⟨A⟩⟩ψ. Thus the whole algorithm takes time O(2n 2l ).

The exponential complexity result is due to the fact that the concept of joint abilities is based on elimination of dominated strategies. Model checking strategic logics beyond ATL usually has high complexity. Even restricting to memoryless strategies does not help much. For example, model checking memoryless Strategy Logic (SL) is PSPACE-complete wrt both the model size and the formula size [ ˇCerm´ak et al., 2018]. The paper presents a labeling algorithm for model checking memoryless SL which is exponential time wrt both the model size and the formula size, and gives a symbolic implementation of the labeling algorithm.

6 Conclusions

In this paper, we have proposed JAADL, a modal logic for joint abilities under strategy commitments, which is an extension of ATL∗ . Firstly, we introduce an explicit operator for elimination of dominated strategies so that joint abilities can be expressed. Secondly, the logic is based on LDL, so that regular expressions can be used to represent constraints of structured strategies such as norms/social laws. We analyze valid formulas in the logic, and identify three sufficient conditions and a necessary condition for joint abilities. These conditions make use of the concepts of winning strategies, optimal strategies, equivalent strategies, and incomparable strategies. We use examples to illustrate that we can conveniently apply these conditions to analyze whether there exist joint abilities. Finally, we prove that model checking memoryless JAADL is in EXPTIME.

In the future, we are interested in a thorough investigation of the computational complexity of model-checking JAADL, including the exact complexity of the memoryless case and the general case. Also, we are interested in implementing a symbolic model checker for memoryless JAADL.

Acknowledgments

We thank the anonymous reviewers for helpful comments. We acknowledge support from the Natural Science Foundation of China under Grant Nos. 61572535 and U1811263, and the National Science and Engineering Research Council of Canada.