Verifying Existence of Resource-Bounded Coalition Uniform Strategies

1 Introduction

We propose a new logical formalism, RB◦ATSEL, for modelling and verifying multi-agent systems where agents execute both ontic actions (actions that change the world) and epistemic actions (actions that change their knowledge). This is a common situation in many multi-agent systems where agents have to explore and change their environment; for example, knowledge-based planning, diagnosis, etc. As an example, we focus on multi-agent systems where some agents monitor the behaviour of other agents to detect norm violations [ ´Alvarez-Napagao et al., 2011]. We would like to be able to automatically verify properties of such systems using model-checking; for example, to check whether monitoring agents have a strategy to detect all norm violations.

There has been considerable work on Alternating Time Temporal Logic (ATL) extended with epistemic operators and on the model-checking problem for the resulting logics, e.g., [van der Hoek and Wooldridge, 2002; Lomuscio et al., 2009]. The motivation of this paper is closer to the work on Dynamic Epistemic Logic (DEL) e.g., [Baltag et al., 1998; van Ditmarsch and Kooi, 2008], and epistemic planning, e.g., [Andersen et al., 2012], where we can reason about how epis-

Brian Logan

University of Nottingham bsl@cs.nott.ac.uk

temic actions change the agents' epistemic states, which is impossible in epistemic ATL.

Our approach differs from previous work in two main respects: the adoption of syntactic knowledge, and considering costs of both ontic and epistemic actions. We interpret epistemic modalities syntactically rather than using an indistinguishability relation. This allows us to use simpler models, and to model different (non-omniscient) reasoning procedures for different agents. We also consider the costs of both ontic and epistemic actions, such as observation and communication. Clearly ontic actions (e.g., moving from one location to another) have costs (e.g., energy). However, observations often have non-trivial costs (e.g., an agent may need to use costly equipment, or pay some authority for verified information [Jamroga and Tabatabaei, 2013; Naumov and Tao, 2015]). Exchanging messages also has costs, for example, energy, or money. This is particularly relevant for norm monitoring scenarios: a successful monitoring strategy may exist, but could be prohibitively expensive and not practically feasible. For this reason, we chose as the basis for our formalism the logic RB◦ATL, where actions produce and consume resources [Alechina et al., 2014]. (If observations have a cost, we need to model resource production if monitoring is to be performed indefinitely.) Using RB◦ATL allows us to check whether a strategy that requires less than a given amount of resources exists. However Alechina et al. [2014] consider only the resource consumption of ontic actions.

The notion of strategies we consider are perfect recall strategies, where the choice of the next action by an agent depends on all previously encountered states. Perfect recall strategies make more sense than memoryless strategies in our setting, as actions both produce and consume resources. (Intuitively, this is because an agent may need to 'loop' several times making some resource in order to execute an action that consumes the resource, e.g., recharging a battery for several timesteps.) In addition, strategies should also be uniform; that is, if an agent has the same knowledge at each point in two histories, then it should chose the same action in both of them. However, model-checking epistemic ATL with uniform perfect recall strategies and more than one agent is undecidable [Dima and Tiplea, 2011]. This result does not change for syntactic epistemics. We therefore propose a notion of coalitionuniform strategies for which the model-checking problem is decidable. A strategy is coalition-uniform for a coalition A if for any two histories indistinguishable for A (wrt some notion of indistinguishability), it chooses the same action. We call the resulting logic Resource-Bounded Alternating Time Syntactic Epistemic Logic (RB◦ATSEL). The main contribution of this paper is a decidable model-checking procedure for RB◦ATSEL with coalition-uniform strategies (wrt any decidable notion of indistinguishability).

2 Syntax and Semantics of RB◦ATSEL

We adopt the approach to epistemic logic that interprets agents' knowledge syntactically, as a (finite) set of formulas, as in, e.g., [Konolige, 1986]. An agent knows that φ if, and only if, φ is in its knowledge base or is derivable from it by some simple terminating procedure (e.g., closure under modus ponens). This approach is very close to the notion of algorithmic knowledge of Fagin et al. [1995]. In what follows, to decide whether the agent knows φ, we simply check whether a formula φ is in agent i's state si, but this can be trivially replaced with a check for alg(si↪ φ) = true, where alg is a terminating procedure that takes a set of formulas si and a formula φ and checks whether φ follows from si.

Syntactic knowledge provides a convenient and compact way of modelling knowledge change, compared to, for example, DEL. In DEL, the update mechanism involves combining models to produce new models, and requires considerably more space to represent and more computation to reason about. In the syntactic approach, we can simply specify postconditions of actions which add and remove formulas from the agent's state. In DEL, we need to essentially associate an automaton with each action that can transform an epistemic model into a new epistemic model. Finally, it is worth noting that many epistemic planners use what are essentially syntactic knowledge bases (and as a result solve a decidable planning problem), e.g., [Petrick and Bacchus, 2004]. This contrasts with the undecidability of DEL-based epistemic planning [Aucher and Bolander, 2013].

The language of RB◦ATSEL is built from the following components: Agt = ¶a1↪ ▷ ▷ ▷ ↪ an♦ a set of n agents; Res = ¶res1↪ ▷ ▷ ▷ ↪ resr♦ a set of r resources; and ⇧ a set of propositions. B = Agt ⇥ Res ! N1 is a set of resource bounds, where N1 = N [ ¶1♦. (Note that the definition of bound and related definitions differ from those in [Alechina et al., 2014] as we assume resources can't be transferred between agents.)

Formulas of the language L of RB◦ATSEL are defined by the following syntax '↪ ::=

where p 2 ⇧ is a proposition, A ✓ Agt, b 2 B is a resource bound and a 2 Agt.

The meaning of RB◦ATSEL formulas is as follows: hhAb ii©' means that a coalition A has a strategy executable within resource bound b to ensure that the next state satisfies '; hhAb ii'U means that A has a strategy executable within resource bound b to ensure while maintaining the truth of '; hhAb ii2' means that A has a strategy executable within resource bound b to ensure that ' is always true; and Ka' means that formula ' is in agent a's knowledge base.

Definition 1. A model of RB◦ATSEL is a structure M = (Φ↪ Agt↪ Res↪ S↪ ⇧↪ Act↪ d↪ c↪ δ) where:

• ÷ Φ is a finite set of formulas of L.
• ÷ Agt is a non-empty set of n agents, Res is a non-empty set of r resources.
• ÷ S is a set of tuples (s1↪ ▷ ▷ ▷ ↪ sn↪ se) where se ✓ ⇧ and for each a 2 Agt, sa ✓ Φ.
• ÷ ⇧ is a finite set of propositional variables; p 2 ⇧ is true in s 2 S iff p 2 se.
• ÷ for every s↪ s0 2 S↪ a 2 Agt, d(s↪ a) = d(s0 ↪ a) if sa = s0a .
• ÷ Act is a non-empty set of actions which includes idle, and d : S ⇥ Agt ! }(Act) ∩ ¶;♦ is a function which assigns to each s 2 S a non-empty set of actions available to each agent a 2 Agt. We assume that for every s 2 S and a 2 Agt, idle 2 d(s↪ a). We denote joint actions by all agents in Agt available at s by D(s) = d(s↪ a1) ⇥ · · · ⇥ d(s↪ an).
• ÷ c : Act ⇥ Res ! Z is the function which models consumption and production of resources by actions (a positive integer means consumption, a negative one production). Let consres(↵) = max(0↪ c(↵↪ res)) and prodres(↵) = -min(0↪ c(↵↪ res)). We stipulate that c(idle↪ res) = 0 for all res 2 Res.
• ÷ δ : S ⇥ Actn ! S is a partial function which for every s 2 S and joint action σ 2 D(s) returns the state resulting from executing σ in s.

We denote by DA(s) the set of all joint actions by agents in coalition A at s. Let σ be a joint action by agents in A. The set of outcomes of this joint action in s is the set of states reached when A executes σ: out(s↪ σ) = ¶s0 2 S ♣ 9σ0 2 D(s) : σ = σ0A ^ s0 = δ(s↪ σ0 )♦ (where s0A is the restriction of σ0 to A). A strategy for a coalition A ✓ Agt is a mapping FA : S+ ! Act♣A♣ (from finite non-empty sequences of states to joint actions by A) such that, for every λs 2 S+, FA(λs) 2 DA(s). A computation λ 2 S! is consistent with a strategy FA iff, for all i ≥ 0, λ[i+1] 2 out(λ[i]↪ FA(λ[0↪ i])). Overloading notation, we denote the set of all computations λ consistent with FA that start from s by out(s↪ FA). Given a bound b 2 B, a computation λ 2 out(s↪ FA) is b-consistent with FA iff, for every i ≥ 0, for every a 2 A,

where Fa(λ[0↪ j]) is a's action as part of the joint action returned by FA for the sequence of states λ[0↪ j]; tot(σ) = prod(σ) - cons(σ) is the (vector) difference between the vector prod(σ) = (prod1(σ)↪ ▷ ▷ ▷ ↪ prodr(σ)) of resource amounts action σ produces and the vector of resource amounts cons(σ) it consumes; ba is a0 s resource bound in b. This condition requires that the amount of resources a accumulated on the path so far, plus the original bound, is greater than or equal to the cost of executing the next action by a in the strategy. FA is a b-strategy if all λ 2 out(s↪ FA) are b-consistent.

In the presence of imperfect information, it makes sense to consider only uniform strategies rather than arbitrary ones.

A strategy is uniform if after epistemically indistinguishable histories, agents select the same actions. Two states s and t are epistemically indistinguishable by agent a, denoted by s ⇠a t, if a has the same local state (knows the same formulas) in s and t: s ⇠a t iff sa = ta. For a coalition A, indistinguishability s ⇠A s0 means that A as a whole has the same knowledge in the two states. Various notions of coalitional knowledge can be used to define ⇠A. For example, s ⇠A t iff Sa2A sa = Sa2A ta (the distributed knowledge of A in s and t is the same). Another possible definition of s ⇠A t is 8a 2 A(sa = ta). ⇠A can be lifted to histories in the obvious way: s1↪ ▷ ▷ ▷ ↪ sk ⇠A t1↪ ▷ ▷ ▷ ↪ tk iff for all j 2 [1↪ k], sj ⇠A tj.

Definition 2. A strategy FA for A is coalition-uniform with respect to ⇠A if for all ¯ s ⇠A ¯ t, FA(¯ s) = FA(¯ t).

Note that any notion of action choice based on coalition knowledge presupposes that agents in the coalition share knowledge for the purpose of action selection. In other words, there is a 'silent step' before action selection when agents in the coalition can communicate with each other instantaneously and without any cost. The only explicit and potentially resource consuming communication actions which may be necessary for a successful strategy are actions communicating with agents outside of the coalition.

The truth definition for RB◦ATSEL with coalitionuniform strategies (parameterised by ⇠A) is as follows:

• ÷ boolean connectives have standard truth definitions
• ÷ M↪ s ♣= p iff p 2 se
• ÷ M↪ s ♣= hhAb ii©φ iff 9 coalition-uniform b-strategy FA such that for all λ 2 out(s↪ FA): M↪ λ[1] ♣= φ
• ÷ M↪ s ♣= hhAb ii2φ iff 9 coalition-uniform b-strategy FA such that for all λ 2 out(s↪ FA) and i ≥ 0: M↪ λ[i] ♣= φ.
• ÷ M↪ s ♣= hhAb iiφU iff 9 coalition-uniform b-strategy FA such that for all λ 2 out(s↪ FA), 9i ≥ 0: M↪ λ[i] ♣= and M↪ λ[j] ♣= φ for all j 2 ¶0↪ ▷ ▷ ▷ ↪ i - 1♦
• ÷ M↪ s ♣= Kaφ iff φ 2 sa

Note that we do not impose any conditions on the syntactic knowledge (not consistency, not veracity etc.). Of course, in a particular modelling scenario such conditions may be imposed. The general results for decidability of model-checking stated below hold for such special cases too. They also hold for strong coalition uniformity where the truth definition for coalition modalities requires the existence of a coalitionuniform strategy from every indistinguishable state. For example, for M↪ s ♣= hhAb ii©φ strong coalition uniformity requires that 8s0 ⇠A s, 9 coalition-uniform b-strategy FA such that for all λ 2 out(s0 ↪ FA): M↪ λ[1] ♣= φ.

3 Model-Checking RB◦ATSEL

In this section, we prove the following general result:

Theorem 1. The model-checking problem for RB◦ATSEL with coalition-uniform strategies, with respect to any decidable notion of ⇠A, is decidable.

To prove decidability we give an algorithm which, given a structure M = (Φ↪Agt↪Res↪ S↪⇧↪Act↪ d↪ c↪ δ) and a formula φ0, returns the set of states [φ0]M satisfying φ0:

[φ0]M = ¶s ♣ M↪ s ♣= φ0♦. The theorem follows from Lemmas 1 and 2 which establish termination and correctness of the algorithm respectively.

Algorithm 1 Labelling φ0

The algorithm is shown in Algorithm 1. Given φ0, we produce a set of subformulas Sub(φ0) of φ0 in the usual way (but excluding subformulas in the scope of a knowledge modality), ordered in increasing order of complexity. We then proceed by cases. For all formulas in Sub(φ) apart from Kaφ, hhAb ii©φ, hhAb iiφU and hhAb ii2φ (where b may contain 1) we essentially run the standard ATL model-checking algorithm [Alur et al., 2002]. Labelling states with hhAb ii©φ makes use of a function Pre(A↪ ⇢↪ b) which, given a coalition A, a set ⇢ ✓ S and a bound b, returns a set of states s in which A has a joint action σA with cons(σA)  b such that out(s↪ σA) ✓ ⇢. Labelling states with hhAb iiφU and hhAb ii2φ is more complex, and in the interests of readability we provide separate functions: UNTIL for hhAb iiφU formulas is shown in Algorithm 2, and BOX for hhAb ii2φ formulas is shown in Algorithm 3.

Both algorithms proceed by depth-first and-or search on M. Information about the state of the search is recorded in a search tree of nodes. A node is a structure which consists of a state of M (including the epistemic states of the agents), the resources available to the agents A in that state (if any), and a finite path of nodes leading to this node from the root node. Edges in the tree correspond to joint actions by agents in A and are labelled with the action taken. Note that the resources available to the agents in a state s on a path constrain the edges from the corresponding node to be those actions σA where cons(σA) is less than or equal to the available resources. For each node n in the tree, we have a function s(n) which returns its state, p(n) which returns the nodes on the path to n, and a(n) which returns the joint action taken by A to reach s(n) (i.e., the label of the edge to n from its predecessor). The function ei↪k(n) returns the resource availability on the i-th resource in s(n) for agent k 2 A as a result of following p(n). The function node0(s↪ b) returns the root node, i.e., a node n0 such that s(n0) = s, p(n0) = [ ], a(n0) = no-op, and ei↪k(n0) = bi↪k for all resources i and agents k 2 A. The function node(n↪ σ↪ s0 ) returns a node n0 where s(n0 ) = s0 , p(n0 ) = [p(n) · n], a(n0 ) = σ, and for all resources i and agents k 2 A, ei↪k(n0 ) = ei↪k(n) + prodi(σk) - consi(σk). In addition, we assume functions hd(u), tl(u) which return the head and tail of a list u, and u ◦ v which concatenates the lists u and v. (We abuse notation slightly, and treat sets as lists, e.g., use hd(u) where u is a set, to return an arbitrary element of u, and use ◦ between a set and a list.)

Algorithm 2 Labelling hhAb iiφU 1: function UNTIL(B↪C↪ hhAb iiφU ) 2: if B = [ ] then 3: return true 4: n hd(B) 5: if 9n0 2 p(n) : s(n0 ) = s(n) ^ (8i↪ k : ei↪k(n0 ) ≥ ei↪k(n)) then 6: return false 7: for i↪ k 2 ¶i 2 Res↪ k 2 A ♣ 9n0 2 p(n) : s(n0 ) = s(n) ^ ei↪k(n0 ) < ei↪k(n) ^ (8j↪ m : ej↪m(n0 )  ej↪m(n))♦ do 8: ei↪k(n) 1 9: if s(n) 2 [ ]M then 10: return UNTIL(tl(B)↪C [ ¶n♦↪ hhAb iiφU ) 11: if s(n) 62 [φ]M then 12: return false 13: if 9n0 2 C : p(n) · n ⇠A p(n0 )[1↪ ♣p(n) · n♣] then 14: σ a(p(n0 )[♣p(n) · n♣ +1] 15: if σ 2 DA(s(n)) ^ cons(σ)  e(n) then 16: P ¶node(n↪ σ↪ s0 ) ♣ s0 2 out(s(n)↪ σ)♦ 17: return UNTIL(P ◦ tl(B)↪C↪ hhAb iiφU ) 18: else 19: ActA ¶σ 2 DA(s(n)) ♣ cons(σ)  e(n)♦ 20: for σ 2 ActA do 21: P ¶node(n↪ σ↪ s0 ) ♣ s0 2 out(s(n)↪ σ)♦ 22: if UNTIL(P ◦ tl(B)↪C↪ hhAb iiφU ) then 23: return true 24: return false

UNTIL (Algorithm 2) takes a stack (list) of 'open' nodes B, a set of 'closed' nodes C, and a formula φ0 = hhAb iiφU 2 Sub(φ0) as input. If there are no more open nodes to consider, UNTIL returns true, indicating that a strategy exists to enforce hhAb iiφU . Otherwise we check whether the state s(n) has been encountered before on p(n), i.e., p(n) ends in a loop. If the loop is unproductive (i.e., resource availability has not increased since the previous occurrence of s(n) on the path p(n)), then the loop is not necessary for a successful strategy, and search on this branch is terminated. If, on the other hand, the loop strictly increases the availability of at least one resource i for some agent k and does not decrease the availability of other resources, then ei↪k(n) is replaced with 1 as a shorthand denoting that any finite amount of i can be produced by repeating the loop sufficiently many times. We then check if the second argument of φ0 is true in s(n). If so, search terminates on the current branch, and continues on a different branch by expanding the next open node in B and adding the current node n to the set of closed nodes. Note that we only add 'successful' branches to the closed set rather than all visited nodes, as search proceeds depth-first. Coalition uniformity is ensured if action choices are consistent with those taken in ⇠A states on all successful paths explored to date (n1↪ ▷ ▷ ▷ ↪ nk ⇠A n01 ↪ ▷ ▷ ▷ ↪ n0k iff s(n1)↪ ▷ ▷ ▷ ↪ s(nk) ⇠A s(n01 )↪ ▷ ▷ ▷ ↪ s(n0k )). If the current branch is not closed (i.e., the second argument of φ0 is not true in s(n), but φ is true in s(n)), search continues on this branch. First we check if the current path (including the current node) is epistemically indistinguishable from a (prefix of) a path to a closed node ⇢. If so, for a coalition-uniform strategy, the same action, σ, should be selected in the current state as in the corresponding state in ⇢. (We use p(n0 )[i] to denote the i-th node in the path p(n0 ), and p(n0 )[1↪ j] to denote the prefix of p(n0 ) up to the j-th node.) If the cost of the action σ is less than the resource availability in the current state, we generate a new node for each possible outcome state of the action, and call UNTIL recursively to continue the search, pushing the nodes corresponding to the successor states onto the stack of open paths. If the cost of the required action is greater than the current resource availability, search terminates on the current branch with false. If no action is required at the current state for coalition uniformity, then for each action that is possible in the current state given the current resource availability, we attempt to find a strategy for each of the outcome states of that action. If a strategy cannot be found for any action possible in s(n), UNTIL returns false.

Algorithm 3 Labelling hhAb ii2φ 1: function BOX(B↪C↪ hhAb ii2φ) 2: if B = [ ] then 3: return true 4: n hd(B) 5: if s(n) 62 [φ]M then 6: return false 7: if 9n0 2 p(n) : s(n0 ) = s(n) ^ (8j↪ k : ej↪k(n0 ) ≥ ej↪k(n)) ^ (9j↪ k : ej↪k(n0 ) > ej↪k(n)) then 8: return false 9: if 9n0 2 p(n) : s(n0 ) = s(n) ^ (8j↪ k : ej↪k(n0 )  ej↪k(n)) then 10: return BOX(tl (B)↪ C [ ¶n♦↪ hhAb ii2φ) 11: if 9n0 2 C : p(n) · n ⇠A p(n0 )[1↪ ♣p(n) · n♣] then 12: σ a(p(n0 )[♣p(n) · n♣ +1] 13: if σ 2 DA(s(n)) ^ cons(σ)  e(n) then 14: P ¶node(n↪ σ↪ s0 ) ♣ s0 2 out(s(n)↪ σ)♦ 15: return BOX(P ◦ tl (B)↪ C↪ hhAb ii2φ) 16: else 17: ActA ¶σ 2 DA(s(n)) ♣ cons(σ)  e(n)♦ 18: for σ 2 ActA do 19: P ¶node(n↪ σ↪ s0 ) ♣ s0 2 out(s(n)↪ σ)♦ 20: if BOX(P ◦ tl (B)↪ C↪ hhAb ii2φ) then 21: return true 22: return false

BOX (Algorithm 3) takes a stack (list) of 'open' nodes B, a set of 'closed' nodes C, and a formula φ0 = hhAb ii2φ 2 Sub(φ0) as input. If there are no more open nodes to consider, BOX returns true. It then checks if φ is false in the state s(n). If so, it returns false immediately, terminating search of the current branch of the search tree. Otherwise we check whether the state s(n) has been encountered before on p(n), i.e., p(n) ends in a loop. For BOX the loop check is slightly different. If the loop decreases the amount of at least one resource for one agent without increasing the availability of any other resource, it cannot form part of a successful strategy, and the search terminates returning false. If a non-decreasing loop is found, then it is possible to maintain the invariant formula φ forever without expending any resources, and the search terminates on the current branch and continues on a different branch by expanding the next open node in B and adding the current node n to the set of closed nodes. The remaining cases are similar to UNTIL. If the current branch is not closed, search continues on the branch, first checking whether an action is required for the strategy to be coalitionuniform, and, if not, for each action that is possible in the current state given the current resource availability.

Lemma 1 (Termination). Algorithm 1 terminates.

Proof. All the cases in Algorithm 1 apart from the calls to Algorithms 2 and 3 clearly terminate. It therefore suffices to show that the calls to Algorithms 2 and 3 terminate.

In order to prove termination, we first show (Claim 1) that on each path explored by Algorithm 2 or Algorithm 3 there is no infinite loop where nodes with the same state and incomparable e(n) occur. This implies that the tree explored for each element of B is of finite depth, since the number of states is finite and repeated states will necessarily occur in the search, and if the resource availability vectors are comparable the search will terminate for that node. Algorithm 2 returns false for a non-increasing loop on line 6, and resets resource availability to 1 on line 8 for an increasing loop; if the same resource-increasing loop is encountered again with all resources set to1or unchanged, the algorithmwill return false on line 6. Algorithm 3 terminates returning false on line 8 if the loop is decreasing, and calls itself on the next member of B on line 10 if the loop is non-decreasing. Second, we show that (Claim 2) there cannot be infinitely many recursive calls generated by calls on line 10 of Algorithm 2 and of Algorithm 3. We do this by showing that the list B containing paths that must be checked with respect to a currently successful strategy, will eventually become empty. Together, these two claims provide the proof of the lemma, because they guarantee that after a finite number of recursive calls both algorithms terminate.

Claim 1: Algorithm 2 and Algorithm 3 cannot generate a path where nodes with the same state and incomparable e(n) occur infinitely often.

This part of the termination proof is similar to that in [Alechina et al., 2014] which in turn is similar to the proof of Lemma f in [Reisig, 1985, p.70], and proceeds by induction on the number of resource/agent pairs m. For m = 1, since e(n) is always positive, the claim is immediate. Assume the claim holds for m and let us show it for m+ 1. In other words, the first m positions in e(n) will eventually become comparable. Then the m + 1 position will become comparable since there are only finitely many positive integers which are smaller than a given em+1(n).

Claim 2. There can be only finitely many calls generated by the coalition uniformity check (line 13 of Algorithm 2 and line 11 of Algorithm 3).

Here we need to show that the open list B is used to explore a finite tree, hence B will eventually become empty. The depth of this tree is bounded by the depth of the longest possible path. Since the relation ⇠A only holds between the paths of the same length, Claim 1 is sufficient to limit the depth of the tree. The finite branching factor of the tree follows from the fact that the set out(s↪ σA) is always finite.

Lemma 2 (Correctness). Given a model M, a state s in M and a formula φ, Algorithm 1 labels s with φ iff M↪ s ♣= φ.

Proof. The proof for all the cases in Algorithm 1 apart from the calls to Algorithms 2 and 3 is straightforward.

Let us look at the case for hhAb iiφU . We need to show that a call to UNTIL([node0(s↪ b)]↪ ¶ ♦↪ hhAb iiφU ) returns true if, and only if, M↪ s ♣= hhAb iiφU and similarly for hhAb ii2φ. By inductive hypothesis, the algorithm only explores paths where φ holds (line 11) until is encountered (line 9), so the pure temporal semantics of U is respected. Note that it is enough to find a finite strategy which is guaranteed to achieve a state where is true. After that, the agents can select the idle action in all subsequent histories, which both ensures coalition uniformity and does not require any resources. The proof as regards resource bounds (and whether it is safe to reset a bound to 1when a productive loop is encountered, and explore a productive loop only once) is similar to the one for RB◦ATL [Alechina et al., 2014]. However, in addition we need to show that the algorithms return true if and only if there is a satisfying coalition-uniform strategy. Assume that the algorithm returns true. We need to show that the strategy found is coalition-uniform. This is ensured by the check on line 13. A current successful strategy is kept in the closed set C, and for all coalition-indistinguishable paths we check whether the same strategy returns true, and only then return true, otherwise we backtrack and try another strategy. For the other direction, assume that there is a coalitionuniform strategy for A to enforce hhAb iiφU . An inspection of Algorithm 2 shows that if such a strategy exists, then there exists a sequence of recursive calls by the algorithm (corresponding to the choice of actions given by the strategy) which results in the algorithm returning true.

The case of hhAb ii2φ is similar. We ensure that Algorithm 3 returns a coalition-uniform strategy by an identical check on line 11.

4 Verifying NormMonitoring Strategies

In this section, we show how RB◦ATSEL can be used to reason about knowledge-based resource bounded strategies in a simple norm monitoring scenario. In the scenario, agents monitor and enforce a norm that visitors to a museum are prohibited from getting too close to the artwork on display: if a visitor approaches the artwork, s/he is warned; if s/he approaches again after being warned, s/he is required to leave the museum. For simplicity, we assume the museum has a single exhibition room, there are two monitoring agents 1 and 2, and one visitor 3. At each timestep, the visitor can perform an idle action or approach the artwork, app. Agents 1 and 2 can perform an idle action, an observation action, obs, issue a warning warn, escort the visitor out of the museum rem, or recharge their battery gen. The agents require a single resource, energy. The gen action produces energy; all other actions apart from idle consume energy.

We use propositions a to denote that the visitor has approached the artwork, ci (i 2 ¶1↪ 2♦) to denote that agent i has just charged their battery, w to denote that the visitor has been warned, and r to denote that the visitor has been removed from the museum. The global system state is represented by s = (s1↪ s2↪ s3↪ se), where si (i = ¶1↪ 2↪ 3♦) is the local state of i, and se is the state of the environment. The set of formulas Φ which constitute possible contents of agents' states includes information on whether the agents have (just) charged, whether the visitor has approached the artwork, been warned, or removed from the museum.

The museum scenario can be modelled by the structure M = (Φ↪ Agt↪ Res↪ S↪ ⇧↪ Act↪ d↪ c↪ δ), where Φ = ¶a↪ c1↪ c2↪ r↪ w♦, Agt = ¶1↪ 2↪ 3♦, Res = ¶energy♦, S = 2¶a↪c1↪w♦ ⇥ 2¶a↪c2↪w♦ ⇥ 2¶r↪w♦ ⇥ 2⇧, ⇧ = ¶a↪ c1↪ c2↪ w↪ r♦, Act = ¶idle↪ app↪ obs↪ warn↪ rem↪ gen♦.

d is defined for all s 2 S as follows:

1. idle 2 d(s↪ i) for all i 2 ¶1↪ 2↪ 3♦
2. obs 2 d(s↪ i) for all i 2 ¶1↪ 2♦
3. app 2 d(s↪ 3) iff r 62 s3
4. gen 2 d(s↪ i) for all i 2 ¶1↪ 2♦
5. warn 2 d(s↪ i) for all i 2 ¶1↪ 2♦ iff a 2 si (a warning is only issued if a monitor knows the visitor has approached the artwork)
6. rem 2 d(s↪ i) for all i 2 ¶1↪ 2♦ iff a↪ w 2 si (the visitor is only removed if s/he approaches the artwork and a warning has been issued)

δ is defined based on the following post conditions of actions (action preconditions are given by d):

1. idle performed by agent i 2 ¶1↪ 2♦ removes ci from si and se; idle performed by agent 3 removes a from se
2. app performed by agent 3 adds a to the state of the environment
3. obs performed by agent i 2 ¶1↪ 2♦ removes ci from si and se, and, if performed in a state where a is true (false), adds (removes) a to (from) i's local state
4. warn performed by agent i 2 ¶1↪ 2♦ removes ci from si and se, and adds w to s1↪ s2↪ s3 and se
5. rem performed by agent i 2 ¶1↪ 2♦ removes ci from si and se, and adds r to s3↪ se
6. gen performed by agent i 2 ¶1↪ 2♦ adds ci to si and se

The following property states that if the visitor approaches the artwork, then this will be known by one of the monitoring agents in the next state:

This formula is true for a notion of coalition uniformity based on distributed knowledge of the coalition. The strategy is as follows: agents take turns charging and observing; agent 1

chooses obs in the state where both agents's states don't contain ci, hence it needs 1 unit of energy to start with. The following properties state that the monitoring agents are able to warn the visitor in two steps after the visitor's approach, and that after being warned, the visitor will be removed directly after another approach. They are true under the same notion of coalition uniformity.

5 RelatedWork

The motivation of work on epistemic logics where acquiring information requires resources [Jamroga and Tabatabaei, 2013; Naumov and Tao, 2015] is very similar to ours, however the technical approach is very different. In [Jamroga and Tabatabaei, 2013], a set of states an agent considers possible is updated by observations (which eliminate some states), and observations have resource costs. The logic introduced in the paper can express statements such as 'i can potentially achieve knowledge of whether φ is true under resource bound b'. In [Naumov and Tao, 2015], edges in an epistemic indistinguishability relation have weights corresponding to the costs of removing them (obtaining information which would distinguish the states). This allows the authors to define weighted knowledge operators which represent the costs of coming to know whether some proposition is true.

Other related work falls broadly into three categories: work on model-checking resource logics (without epistemics), work on model-checking epistemic ATL (under standard semantics for epistemics and without knowledge change), and work on model-checking DEL and epistemic planning. There exist several formalisms that extend Alternating Time Temporal Logic (ATL), [Alur et al., 2002] with reasoning about resources available to agents and production and consumption of resources by actions. When the production of resources is allowed, the model-checking problem for many (but not all) of these logics is undecidable (for a survey, see [Alechina et al., 2015]). Epistemic ATL has been studied extensively, see e.g., [van der Hoek and Wooldridge, 2002; ˚Agotnes, 2006; Lomuscio et al., 2009; Guelev et al., 2011; Dima and Tiplea, 2011]. Its model-checking problem with perfect recall and uniform strategies was shown to be undecidable in the case of more than one agent in [Dima and Tiplea, 2011]. In [Guelev et al., 2011], it was shown that if uniform strategies are defined in terms of distributed knowledge of the coalition, the model-checking problem becomes decidable. The technique used to prove this is very different from the one used in this paper. Various notions of coalition uniformity were studied in [van Ditmarsch and Knight, 2014], and justified for a setting where agents in a coalition share their information; the model-checking problem for the resulting logic was not considered. There is a large body of work on DEL. The modelchecking problem for full DEL was shown to be undecidable in [Aucher and Bolander, 2013] and decidable for a fragment of DEL in [Aucher and Schwarzentruber, 2013]. DEL-based epistemic planning is also undecidable in general, but is tractable for some special cases [Yu et al., 2013; Bolander et al., 2015].

Acknowledgement. This work was supported by the Engineering and Physical Sciences Research Council [grant EP/K033905/1].