Concurrent Games in Dynamic Epistemic Logic

1 Introduction

The discipline of distributed synthesis seeks solutions for automating the design of artificial agents that interact and make decisions in order to achieve some service. The main challenge is to synthesize strategies for each agent of a team collaborating towards a common goal, against opponents, usually in an imperfect information setting.

As advocated in the Dynamic Epistemic Logic (DEL) approach to epistemic planning, we consider multi-agent systems described symbolically by DEL presentations, which consist in an initial epistemic state (actual world and worlds considered possible by some agents), and epistemic actions that agents may perform. An epistemic action, besides the standard precondition and effects of the action, also describes the agents' ability to perceive its execution. Synthesising strategies was studied in the single-agent case [Bolander and Andersen, 2011; Aucher and Bolander, 2013; Bolander et al., 2015; Bolander, 2017], and in a multi-player turn-based game setting [Maubert et al., 2019; Maubert et al., 2020].

However, concurrent execution of actions has not been considered so far in epistemic planning. Some works consider concurrent execution of abstract actions (as in concurrent game structures [de Alfaro and Henzinger, 2000]), or concurrent execution of purely epistemic actions without effects on the world [van Eijck et al., 2011; ˚Agotnes and van Ditmarsch, 2011; Benevides and Lima, 2019] or only public [Lima, 2014]. But to our knowledge, concurrent execution of arbitrary epistemic actions with explicit effects has never been studied. And yet they are essential for modelling realistic situations.

Consider the two-robot coordination example of Figure 1. Some container can be placed either left or right. Two robots (or agents), i and j, can either wait or push the container, which incidentally is energy-consuming. Both agents waiting, the container stays in place. Otherwise, if i pushes while j waits, the container moves right (if not already there), and, symmetrically, if j pushes while i waits, it moves left (if not already there). Agents pushing concurrently results in a conflict. To determine the effect of such conflicting actions, one solution is to consider that they are blocking, as done for instance in [Fox and Long, 2003] for in temporal planning, or facts involved in conflifcts are just maintained [Lima, 2014]. Another option consists in selecting a maximal subset of non-conflicting actions, as done for instance in [Eshuis and Wieringa, 2001] in UML work-flow modelling.

In this paper, we adopt the latter solution, which is more challenging. A major additional difficulty with respect to this latter UML setting arises from epistemic features of actions of the DEL framework. In our robot example, while robots i and j perfectly perceive pushing and waiting actions, the two other agents k and ℓ cannot distinguish them. Note that this issue is not tackled in [Lima, 2014] since actions are public.

Our first contribution is to define a DEL concurrent update product that provides the dynamics of concurrent epistemic actions. This new product yields a non-deterministic dynamics controlled by a scheduler, whose role is to resolve conflicts. On the basis of this product we show how finite DEL presentations can generate infinite concurrent game arenas.

Our second contribution is a proof that distributed synthesis can be solved for such games for two cases: the case where all actions are public (perfectly observed by everyone), and the case where all actions have propositional pre- and postconditions and information among the agents is hierarchical (Theorems 4 and 7). To prove this we extend to the concurrent setting some results from [Maubert et al., 2019; Maubert et al., 2020], namely, that the infinite concurrent game arenas arising from DEL game presentations can be finitely represented when actions are all public or all propositional. We then transfer existing results on the model-checking problem for the epistemic strategic logic ATL∗K [Van der Hoek and Wooldridge, 2003] to obtain, in particular, decidability of distributed synthesis for rich temporal epistemic objectives.

Remark that our work is unrelated to the concurrent dynamic logic from [van Benthem et al., 2007], where several games are played concurrently. Our work also differs from concurrent dynamic epistemic logic [van Ditmarsch et al., 2003], where concurrency represents some form of alternation [Chandra and Stockmeyer, 1976].

Outline: In Section 2, we provide all the necessary material on DEL presentations. In Section 3 we present the concurrent update product, and we use it in Section 4 to define DEL games and establish our main results.

2 Background on DEL

We fix a finite set of agents Ag = {1, . . . ,N} and a countable set of atomic propositions AP. The language of epistemic logic, noted LK, is defined by the grammar ϕ ::= true | p | ¬ϕ | ϕ ∧ ϕ | Kiϕ where p ∈ AP and i ∈ Ag. Formula Kiϕ reads as "agent i knows that ϕ". Ruling out modality Ki yields propositional logic.

2.1 Epistemic Models and States

Epistemic models are relational structures that represent agents' knowledge.

Definition 1 (Epistemic models). An epistemic model is a structure M = (W, (≈i)i∈Ag , λ) where W is a finite nonempty set of worlds, for each agent i ∈ Ag, the equivalence relation ≈i ⊆ W × W is an epistemic relation that reflects agents i's information (or knowledge), and λ : W → 2AP is a valuation function. An epistemic state is a pair (M, w) where M is an epistemic model and w is a world of M representing the actual world.

An epistemic state (M,w) will often be written w when the model M is clear from the context.

Example 1. The epistemic state of Figure 2 represents the situation of Figure 1. Proposition left holds when the container is on the left. In the actual world w, left is false since the container is on the right and we assume that agents i, j and k know this fact, but that ℓ does not: he does not distinguish between world w and the world u where the container is on the left.

The semantics of LK is based on epistemic states.

Definition 2 (Semantics of LK). Let (M, w) be an epistemic state. We define the sentence "Formula ϕ holds in (M, w)", written (M,w) |= ϕ or w |= ϕ, by induction on ϕ: w |= true; w |= p whenever p ∈ λ(w); w |= ¬ϕ whenever w ̸|= ϕ; w |= ϕ1 ∧ϕ2 whenever w |= ϕ1 and w |= ϕ2; and w |= Kiψ whenever (M, u) |= ψ, for all worlds u such that w ≈i u.

2.2 ActionModels and Epistemic Actions

Action models ([Baltag et al., 1998], [Van Ditmarsch et al., 2007]) gather several "concrete" actions (with preconditions and effects [van Ditmarsch and Kooi, 2006]) with epistemic relations describing how the concrete actions are perceived.

Definition 3 (Action models). An action model is a structure A = (A, (≈i)i∈Ag , pre, post) where A is a nonempty finite set of actions, ≈i ⊆ A × A is the epistemic relation of agent i ∈ Ag, the precondition function pre : A → LK specifies the guard for an action to be executable, and the postcondition is a partial function post : A × AP ⇀ LK that describes the effect of actions over atomic propositions; when post(a, p) is undefined, p is not affected by a. An epistemic action is a pair (A, a) where a ∈ A denotes the action actually executed.

Example 2. Figure 3 describes the action model for the tworobot coordination example. Action pushi represents agent i pushing the container to the right. Agent i can execute pushi whenever its energy is high, i.e., when proposition lowEi is false (lowEi and lowEj are initially false); this action consumes energy if it is effective (i.e., the container was not already on the right): in that case the postcondition makes proposition lowEi true. Action pushj for agent j is defined similarly. Finally, the waiting action of robots, represented by waiti and waitj respectively, have the true precondition and the effect of refilling energy (i.e. turning lowEi to false). To keep our example simple, we suppose that all agents but ℓ distinguish between pushi and waiti even if the box is on the right, and similarly for pushj and waitj.

We exhibit two particular kinds of epistemic actions.

Definition 4 (Propositional, public action). An action model A is propositional if for every concrete action a of A and each proposition p, formulas pre(a) and post(a)(p) are propositional. An epistemic action (A, a) is public if for all agents i, a ≈i a′ if and only if a′ = a.

2.3 Update Product

Execution of epistemic actions may change the world but also agents' information. It is formalised by the update product between epistemic models and action models.

Definition 5 (Update product). The update product of epistemic model M = (W, (≈i)i∈Ag , λ) with action model A = (A, (≈i)i∈Ag , pre, post) is the epistemic model M⊗ A := (W⊗, (≈⊗i )i∈Ag, λ⊗), where:

• W⊗ = {(w, a) ∈ W × A | (M, w) |= pre(a)};
• (w, a) ≈⊗i (u, b) whenever w ≈i u and a ≈i b;
• p ∈ λ⊗(w, a) whenever (M,w) |= post(a, p).

We lift the product to epistemic states and epistemic actions: whenever M, w |= pre(a), we let (M, w) ⊗ (A, a) be the epistemic state (M⊗ A, (w, a)).

Example 3. Figure 4 shows (M⊗A, (w, pushi)), that describes the epistemic state after execution of action pushi from the epistemic state of Figure 1 (strictly speaking, it only displays worlds connected to the actual one). The physical situation has not changed: the container is still on the right. However agent ℓ, who initially considered it possible that the container is on the left, and cannot distinguish between pushi and waiti, still considers it possible that the container is on the left. Some information has changed though: initially, agent ℓ knew that robots had energy, but now he considers it possible that robot i's energy has become low.

3 Concurrent Actions

Fix an epistemic state (M,w) and an action model A. From now on, atomic propositions are partitioned into shared propositions (AP s ) that all agents can modify, and private ones: AP pi is the set of private propositions of agent i. As a result, AP = AP s ⊎ ⊎i∈Ag AP pi , where ⊎ is the disjoint union. An agent can play any action that does not modify private propositions of others. We gather in set Ai those actions, namely those whose postconditions are undefined on ∪j̸=iAP pj . A joint action is a tuple ⃗a = 〈a1, . . . , aN〉 ∈ ∏i∈Ag Ai, and we let ⃗aj denote action aj. Finally, a joint action ⃗a is available in w when every individual action ⃗aj can be executed in w: (M, w) |= pre(⃗a1) ∧ · · · ∧ pre(⃗an).

3.1 Conflicts

We define a formula noconflict(⃗a)(p) expressing that all individual actions of a joint action ⃗a agree on their effect (if any)

on proposition p. We first introduce the set Ag(⃗a, p) of agents whose individual action in ⃗a has an effect on p. Formally, Ag(⃗a, p) is the set {i = 1..N | post(⃗ai)(p) is defined}. We then let noconflict(⃗a)(p) be the formula

Now, in a situation where all individual actions of the joint action ⃗a agree on their effect on each proposition, the effect of executing them concurrently can be determined unambiguously. Such a situation is expressed by the formula noconflict(⃗a) := ∧p∈AP noconflict(⃗a)(p).

Definition 6. A joint action ⃗a is non-conflicting in w if M, w |= noconflict(⃗a). Otherwise ⃗a is conflicting in w.

Example 4. In our running example, 〈pushi, pushj〉 is conflicting in both worlds w and u.

To resolve conflicts, we resort to a scheduler.

3.2 The Role of the Scheduler

Given a conflicting available joint action, the scheduler selects a maximal subset of consistent individual actions, and inhibits the remaining actions by "cancelling" their effects on shared variables. An inhibited action of agent i may still have effects on AP pi , which may differ from the original ones. The inhibiting mechanism is implemented by a ghost mapping ◦ : A → A with the following properties: for every agent i ∈ Ag and every action a ∈ Ai, the ghost ◦(a) (written a◦) must be in Ai and post(a◦) is undefined on AP s . This assumption ensures that no conflict arises when inhibiting actions. We also assume that ◦(a) is executable as long as a is, i.e., that pre(a◦) is a logical consequence of pre(a).

Example 5. For the robots, AP s = {left}, AP pi = {lowEi}, AP pj = {lowEj}, and AP pk = AP pℓ = ∅. Facing the conflicting joint action 〈pushi, pushj〉, the scheduler can choose between 〈pushi◦ , pushj〉 and 〈pushi, pushj◦ 〉, and we set pushi◦ := waiti and pushj◦ := waitj.

The epistemic relations from a ghost can be set in many different ways, and the choice is a design matter. For example, assume that ghost actions are distinct from those that can be played by agents, and that ghosts are not epistemically related to those playable actions. Then the scheduler's selection is public: indeed, when for joint action ⃗a scheduler inhibits the action of agent i, all agents are implicitly informed that agent i is discarded.

Definition 7. If A = A·⊎A◦ is split between playable actions A· and ghosts ones A◦, and A· and A◦ are not related by any ≈i, we say that the scheduler is public.

In the sequel, we consider that action models A are implicitly equipped with a ghost mapping.

3.3 Concurrent Update Product

To define the concurrent execution of possibly conflicting actions, we introduce a concurrent update product ⊞ that generalises the classic update product ⊗ (Definition 5).

Before defining this product, we formalise the possible choices for the scheduler. We say that joint action⃗b is a subaction of joint action ⃗a, written⃗b ⪯ ⃗a, whenever ⃗b is obtained from ⃗a by replacing some individual actions by their ghosts. Formally, ⃗b ⪯ ⃗a if⃗bi ∈ {⃗ai, (⃗ai)◦ }, for every 1 ≤ i ≤ N. Remark that, by definition of the ghost mapping, if ⃗a is available in w, so are its sub-actions.

Given a joint action ⃗a, we let Max(⃗a,w) be the set of joint actions composed of the ⪯-maximal sub-actions of ⃗a nonconflicting in w. Elements of Max(⃗a,w) are therefore joint actions non-conflicting in w where a minimal number of actions are inhibited. Notice that Max(⃗a, w) = {⃗a} as soon as ⃗a is non-conflicting in w.

Example 6. The set Max(〈pushi, pushj〉,w) is {〈waiti, pushj 〉, 〈pushi, waitj 〉}.

We now define the concurrent update product, that implements the execution of joint actions.

Definition 8 (Concurrent update product). The concurrent update product of M and A is the Kripke model M⊞ A = (W⊞, (≈⊞i )i∈Ag, λ⊞), where:

• W⊞ = {(w,⃗b) ∈ W × AN | ⃗b ∈ Max(⃗a, u)

for some joint action ⃗a available in w};

• (w,⃗b) ≈⊞i (u,⃗c) if w ≈i u and⃗bj ≈i ⃗cj for all j;
• p ∈ λ⊞(u,⃗b) if (M, u) |= ∧i∈Ag(⃗b,p) post(bi, p).

We can now define the set of epistemic states that may result from executing a joint action ⃗a in (M, w):

This set is a singleton when ⃗a is non-conflicting in w. Remark that the component-wise definition of concurrent epistemic relations ≈⊞i in Definition 8 makes the identity of who performs an action common knowledge.

Example 7. The pointed concurrent update product (M⊞ A, 〈w, (pushi, waitj)〉) of Figure 5 belongs to (M,w) ⊞ (pushi, pushj). Action pushj was inhibited, but agent ℓ considers it possible that lowEj is now true.

4 Concurrent DELGames

In this section, we show how DEL can represent infinite concurrent game arenas, in which players act simultaneously. We then show how, as for turn-based games [Maubert et al., 2019; Maubert et al., 2020] these infinite game arenas can in some cases be folded back into finite ones, when actions are all public, or when they are all propositional. Finally, we show that in these cases, one can model check the epistemic strategic logic ATL∗K on DEL-represented concurrent games.

4.1 Concurrent Game Arenas

Here we recall (nondeterministic) concurrent game arenas with imperfect information and related notions.

Definition 9. A concurrent game arena is a tuple G = (Act, V, vini, (Acti)i∈Ag , ∆, (≈i)i∈Ag , λ), where

• Act is a non-empty set of actions,
• V is a non-empty set of positions,
• vini ∈ V is an initial position,
• Acti : V → 2Act \ {∅} is a repertoire function for i,
• ∆⊆ V ×ActN ×V is a transition relation,
• ≈i ⊆ V ×V is an indistinguishability equivalence relation for agent i, and
• λ : V → 2AP is a valuation function.

In a position v each agent i chooses an available action ai ∈ Acti(v), yielding a joint action ⃗a = 〈a1, . . . , aN〉. The set of joint actions available in v is written JAct(v). The game then moves nondeterministically to some position v′ ∈ ∆(v,⃗a). If, for every position v and joint action⃗a, {v′ | (v,⃗a, v′ ) ∈ ∆} is a singleton, then G is deterministic and we may represent the transition relation as a function δ : V ×ActN → V .

A play π = v0v1v2 . . . is an infinite sequence of positions such that for all k ∈ N, there exists ⃗a ∈ ActN such that vk+1 ∈ ∆(vk,⃗a). We let πk = vk and π≤k = v0v1 . . . vk. A history h = v0v1 . . . vn is a finite non-empty prefix of a play, last(h) = vn is the last position in h, |h| = n+ 1 is its length, and HistG is the set of histories in G. We write λ(h) for λ(last(h)).

As usual for agents with synchronous perfect recall (see for instance [Fagin et al., 1995]), the indistinguishability relation of each agent i is lifted to histories as follows: h ≈i h′ if |h| = |h′ | and hk ≈i h′k for every k < |h|.

A (uniform) strategy σ for an agent i is a function σi that associates an action to any history and such that, for every pair of indistinguishable histories h ≈i h′ , σ(h) = σ(h′ ). Classically, we assume that Acti(v) = Acti(v′ ) whenever v ≈i v′ . A strategy profile for a coalition of agents C ⊆ Ag is a tuple σC = 〈σi〉i∈C, and ΣC is the set of strategy profiles for coalition C. Finally, an outcome of a strategy profile σC from a position v0 is a play starting in position v0 and in which agents in C follow the strategies in ΣC: formally, a play π = v0v1 . . . is an outcome of 〈σi〉i∈C from v0 if, for every k ∈ N, there is a joint action ⃗a such that vk+1 ∈ ∆(vk,⃗a) and (⃗a)i = σi(v0 . . . vk), for all i ∈ C. We let out(h, σC) be the set of outcomes of σC from position v.

Definition 10. Given a concurrent game arena G = (Act, V, vini, (Acti)i∈Ag,∆, (≈i)i∈Ag, λ), we define the unfolding of G as the game arena Gunf = (Act, V ′ , v′ini , (Act′i )i∈Ag,∆′ , (≈′i )i∈Ag, λ′ ) where V ′ = HistG, v′ini = vini, for every h ∈ HistG, Act′i (h) = Acti(last(h)), λ′ (h) = λ(last(h)), ≈′i is the synchronous perfect-recall lifting of ≈i to histories, and ∆′ = {(h,⃗a, h · v) | (last(h),⃗a, v) ∈ ∆}.

We say that two game structures G and G ′ are equivalent whenever their unfoldings are isomorphic.

4.2 DEL Presentations of Game Arenas

We use DEL models to define infinite concurrent arenas:

Definition 11. A DEL game presentation, or DEL game, is a tuple G = 〈M,w,A〉 where (M,w) is an initial epistemic state and A is an action model.

The game starts in the initial epistemic state (M,w). In each round, each agent i chooses an action a ∈ Ai available in the current state (M′ , w′ ), resulting in a joint action ⃗a (we assume that each agent always has at least one available action; if needed we may add a dummy action in the model). The next epistemic state is nondeterministically chosen by the scheduler among (M′ ,w′ ) ⊞⃗a (this choice is nontrivial if ⃗a is conflicting), and the game goes on.

After n rounds in which the players chose joint actions ⃗a1, . . . ,⃗an, the epistemic state is of the form MAn , (w,⃗b1, . . . ,⃗bn), where MAn is defined by letting MA0 = M and MAn+1 = MAn ⊞ A, and each ⃗bk+1 is a maximal sub-action of ⃗ak+1 consistent in MAk , (w,⃗b1, . . . ,⃗bk). In the following we may write w⃗b1 . . .⃗bn instead of (w,⃗b1, . . . ,⃗bn), and call it a history. The length of a history inMAn is defined as |w⃗b1 . . .⃗bn| = n. Since the length of a history determines the epistemic model to which it belongs, we may omit it and write w⃗b1 . . .⃗bn |= ϕ instead of MAn ,w⃗b1 . . .⃗bn |= ϕ. We require that players know their available actions: if w⃗b1 . . .⃗bn ≈i u⃗c1 . . .⃗cn, then the same actions are available to i in both worlds.

A DEL presentation denotes a concurrent game arena, where positions are epistemic states attainable from the initial one,and moves are obtained by applying the concurrent update product of Definition 8. Because this product yields several epistemic states, this concurrent game arena is nondeterministic.

Definition 12. Given a DEL game presentation G = 〈M,w,A〉 we define the concurrent game arena GG = (A, V, vini, (Acti)i∈Ag,∆, (≈i)i∈Ag, λ) where, writing MAn = (Wn , (≈ni )i∈Ag , λn ) for every n:

• A is the set of actions in A,
• the set of positions is V = ∪n∈NWn ,
• the initial position is vini = w,
• Acti(v) = {a ∈ Ai | v |= pre(a)},
• ∆= {(v,⃗a, v′ ) | v′ ∈ v⊞⃗a},
• v ≈i v′ if |v| = |v′ | = n and v ≈ni v′ , and
• λ(v) = λ|v| (v).

We want to reason about strategic abilities and knowledge on infinite concurrent games given as DEL game presentations. To do so we consider the logic ATL∗K .

Definition 13. The syntax of ATL∗K is given by the following grammar:

with p ∈ AP, C ⊆ Ag and i ∈ Ag.

Formula 〈C〉ψ reads as "coalition C has a strategy profile to ensure ψ", and the meaning of other operators is as usual. We let ≈C = ∪i∈C ≈i, and define the semantics of ATL∗K .

Definition 14. Let G be a concurrent game arena, v a position and π a play. The semantics of ATL∗K is defined as follows, where h is a history in G, π is a play and i ∈ N is a point in time (we omit boolean cases):

Remark 1. We use the uninformed semantics for the knowledge operators, which does not depend on the strategies used by the agents, and is the usual one used in epistemic planning (see [Puchala, 2010; Maubert, 2014; Maubert et al., 2020] for more details). Also, we use the subjective semantics for strategic operators, in contrast with the objective one that only asks strategies to be winning from the actual current history (see [Bulling and Jamroga, 2014]).

Given a game arena G with initial position vini, we write G |= ϕ if G, vini |= ϕ. We study the following modelchecking problem: given a DEL game presentation G and a formula ϕ ∈ ATL∗K , do we have GG |= ϕ?

4.3 Decidability for Public Actions

A deterministic game arena with transition function δ is said to have only public actions if, for all positions v, v′ and joint actions ⃗a,⃗a′ such that ⃗a ̸= ⃗a′ , we have δ(v,⃗a) ̸≈i δ(v′ ,⃗a′ ). The following is known for ATL∗K on such arenas:

Theorem 1 ([Belardinelli et al., 2017]). Model checking ATL∗K on finite deterministic concurrent game structures with only public actions is 2-EXPTIME-complete.

First we prove that DEL games with public actions can be finitely represented. Our proof yields nondeterministic game arenas, that we will then transform into deterministic ones that have only public actions in the sense of [Belardinelli et al., 2017]. We will need the following result on the concurrent update product with public action models and a public scheduler (see Definition 7):

Lemma 2. Let M be an epistemic model and A an event model. If the scheduler is public, A has only public actions and its ghost mapping ◦ : A· → A◦ is injective, then for all worlds w,w′ ∈ M, all joint actions ⃗a,⃗a′ , if ⃗a ̸= ⃗a′ then for all (w,⃗b) ∈ (M, w) ⊞⃗a and (w′ ,⃗b′ ) ∈ (M, w′ ) ⊞⃗a′ , for all agents i, (w,⃗b) ̸≈i (w′ ,⃗b′ ).

The injectivity assumption means that two different played actions cannot become the same after being inhibited, in which case the actions of DEL games could not be public in the sense of [Belardinelli et al., 2017].

The proof that the infinite game arena GG induced by a DEL game G with public actions can be finitely represented is very similar to that in [Maubert et al., 2020]. It relies on the fact that updating an epistemic state with a joint action made of public actions can only decrease the size of the obtained epistemic states (when removing their disconnected components) as long as their ghosts are public too. It follows that only finitely many different epistemic models can be generated from a given initial state, up to isomorphism.

Proposition 3. Given a DEL game G = 〈M, w, A〉 with only public actions, one can build a finite game arena G equivalent to GG and of size exponential in |G|.

Because of the scheduler, the resulting arena is nondeterministic. To obtain Theorem 4 below it essentially remains to show that we can transform these nondeterministic arenas into deterministic ones that have only public actions in the sense of [Belardinelli et al., 2017].

Theorem 4. Model checking ATL∗K on DEL concurrent games with public actions, public scheduler and injective ghost mapping is 2-EXPTIME-complete.

Proof sketch. The lower bound comes from LTL synthesis [Pnueli and Rosner, 1989]. For the upper bounds, let G be a DEL presentation and Φ an ATL∗K formula. First, by Proposition 3 we build in exponential time a finite nondeterministic game arena G = (Act, V, vini, (Acti)i∈Ag,∆, (≈i)i∈Ag, λ) equivalent to GG. We build a deterministic game arena Gd by adding a special agent, the scheduler s, who has perfect information and whose possible actions Acts allow him to resolve the non-determinism. The agents choose their actions, and then the scheduler resolves nondeterminism. To do so we introduce intermediary positions of the form (v,⃗a): in each round, in a position v, the agents in Ag choose a joint action ⃗a (the scheduler can only play some dummy action), and the game moves deterministically to (v,⃗a). Now all "normal" agents can only choose the dummy move, and the scheduler can choose a maximal consistent sub-action ⃗b of ⃗a, which determines the new position v′ . Indistinguihability relations for all normal agents are as in G for positions v, and we let (v,⃗a) ≈i (v′ ,⃗a′ ) iff v ≈i v′ and ⃗a = ⃗a′ . This definition is correct because, by Lemma 2, when the agents choose different joint actions, they distinguish the resulting epistemic states no matter the choices of the scheduler. One can check that Gd has only public actions in the sense of [Belardinelli et al., 2017]. We then duplicate all next operators in Φ to skip artificial positions of the form (v,⃗a). To check Φ on Gd , the procedure from [Belardinelli et al., 2017] takes time doubly exponential in the size of Φ and exponential in the size of Gd , which is itself of size exponential in the size of the original DEL game presentation G.

4.4 Decidability for Propositional Actions

A DEL game presentation presents hierarchical information if the set of agents Ag can be totally ordered (i1 < . . . < iN) so that ≈ii ⊆ ≈ii+1 for each 1 ≤ i < N, and similarly for concurrent game arenas. We prove that when, in a DEL game presentation, all actions are propositional actions and information is hierarchical, model checking ATL∗K is decidable.

We first generalise to the concurrent setting a result from [Maubert et al., 2019] which states that infinite turnbased DEL games induced by propositional models can be finitely represented. As for public actions, the game arena that we obtain is nondeterministic.

Proposition 5. Let G = 〈M,w,A〉 be a DEL game where A is propositional. One can build a finite nondeterministic game arena G equivalent to GG, of size exponential in |G|.

We will invoke the following result, that was stated for deterministic game arenas:

Theorem 6 ([Berthon et al., 2017]). Model checking ATL∗K with uninformed semantics is decidable on deterministic game arenas with hierarchical information.

The result in [Berthon et al., 2017] is for ATL∗ without knowledge operators, and for the objective semantics of strategic operators. But their bottom-up algorithm can be easily extended to deal with knowledge operators and subjective semantics: one first performs a powerset construction on the game arena to include sufficient information to evaluate knowledge operators positionally (for instance using ktrees [van der Meyden, 1998]), and then one evaluates knowledge and strategic modalities in a bottom-up fashion.

Thanks to Proposition 5 and a reduction to deterministic arenas similar to the one presented in the proof of Theorem 4, we can use Theorem 6 and obtain that:

Theorem 7. Model checking ATL∗K on DEL game presentations with propositional actions and hierarchical information is decidable.

However the complexity is nonelementary, as it is already the case for multiplayer reachability games with hierarchical information [Peterson et al., 2001]. The number of exponentials will be the maximum between the number of agents with different observation power and the alternation of knowledge operators in the formula.

5 Conclusion

We proposed a setting that permits the succinct specification of concurrent game arenas with epistemic actions. Conflicts are resolved by a scheduler that nondeterministically selects consistent subsets of actions, and inhibits the discarded ones. We established that on such games one can perform strategic reasoning, or more precisely one can model check the strategic epistemic logic ATL∗K , in two cases: when actions are public (Theorem 4) and when actions are propositional and information is hierarchical among the agents (Theorem 7).

Note that we could tune the scheduler differently: in our robot example, a third choice for 〈pushi, pushj〉 could be 〈waiti, waitj〉, which would capture blocking conflicts. Technically, we could relax the selection to other sub-actions than ⪯-maximal ones, and the complexities established in our main theorems would still hold for such different schedulers.

One could also consider fairness requirements to ensure that the scheduler does not favor some agents in resolving conflicts, for instance requiring that if an agent infinitely often enters a conflict, then infinitely often his action is selected by the scheduler. Fairness constraints can often be expressed directly in ATL∗K , in which case our main results still hold.