A Probabilistic Logic for Resource-Bounded Multi-Agent Systems

1 Introduction

The Alternating-time temporal logic (ATL) [Alur et al., 2002] and Coalition logic (CL) [Pauly, 2002] were introduced as logical formalisms for analysing the strategic abilities of coalitions with temporal winning conditions. In the literature, several variants of ATL and CL have been proposed (see e.g., [Goranko, 2001; ˚Agotnes et al., 2009; Wooldridge and Dunne, 2004]). These logics allow the specification of system behaviour in terms of logical formulae, and they can be used to express many interesting properties of coalitions and strategies. However, there is no straightforward way of expressing resource requirements for systems of reasoning agents in these logics. Recently, there has been growing interest in formal models of resource-bounded agents [Bulling and Farwer, 2010; Alechina et al., 2010; Monica et al., 2011]. In works on reasoning about resourcebounded agents, the main emphasis is on the behaviour of agents constrained by fixed resource bounds. For example, RB-ATL [Alechina et al., 2010] was developed for reasoning about coalitional ability under resource bounds, which allows expressing various resource-bounded properties, including "coalition A has a strategy to reach a state satisfying ϕ under the resource bound b, but they cannot enforce ϕ under a tighter resource bound b′ (< b)".

Many real-world distributed systems, such as the Internet of Things (IoT) and Cyber-Physical Systems (CPS), are deeply rooted in activities of our daily living [Calvaresi et al., 2017]. The Multi-Agent Systems (MAS) paradigm offers an ideal method to model and implement such systems [Leit˜ao et al., 2016]. These systems often operate in unpredictable and/or uncertain environments [Faza et al., 2009; Zhang et al., 2016]. Their applications encompass many safety-critical domains, and many such applications run in resource-constrained devices and environments [Abbas et al., 2015; Laszka et al., 2015]. They require not only the reasoning about the coalitional behaviour of agents but also that the agents and/or the environment may have random or unreliable behaviours. A rigorous analysis and verification approach can ensure the correctness of their designs [Kwiatkowska, 2016]. There has recently been increasing interest in developing logics with a probabilistic component in order to link logical and probabilistic reasoning [Forejt et al., 2011; Huang et al., 2012; Chen et al., 2013]. These logics are essentially extensions of CTL or ATL which allow for probabilistic quantification of described properties. Research in this area includes developing a model-based verification tool PRISM by Kwiatkowska et. al [Kwiatkowska et al., 2002]. Among other PRISM property specification languages, the logic rPATL [Chen et al., 2013] allows reasoning quantitatively about a system's use of resources and emphasises on expected reward-related measures. In rPATL, we can express that a coalition of agents has a strategy which can ensure that either the probability of an event's occurrence or an expected reward measure meets some threshold. However, probabilistic resource-bounded properties such as

• "can coalition A have a strategy so that the probability of reaching a state satisfying ϕ under the resource bound b is at least v?",
• "a coalition of agents A has a strategy to achieve a property ϕ with probability v provided they have resources b, but they cannot enforce ϕ under a tighter resource bound b′ (< b) with probability v", and
• "a coalition of agents A can maintain ϕ until ψ becomes true with probability v provided they have resources b"

can neither be expressed in rPATL nor in any other probabilistic temporal logics mentioned above. The problem discussed in this paper can be identified as a probabilistic resourceconstrained multi-agent coalition structure formation problem, where the coalitions perform actions towards specific goals, provided they have enough resources. We propose a logic, Probabilistic Resource-Bounded ATL (pRB-ATL), for reasoning about coalitional power under resource constraints in the probabilistic setting. pRB-ATL allows us to express various interesting properties of probabilistic systems where abilities of agents are constrained by available resources. The logic rPATL is one of the approaches most closely related to the work presented in this paper. However, the reasoning problem considered in our work is different in two important aspects. First, and most importantly, properties in rPATL related to rewards are of a statistical nature. They are expressed and computed as constraints on expected values for rewards. In contrast, resource-bounded properties in our pRB-ATL logic lie within the realm of crisp values and constraints; actions and strategies are allowed if and only if they satisfy the resource-bounded constraints. Second, the semantics of rPATL is based on turn-based systems while ours is based on concurrent systems.

The rest of this paper is structured as follows. In Section 2, we discuss the basic notions of probability distributions and the underlying probabilistic formalisms of our logic. In Section 3, we present the syntax and semantics of pRB-ATL. In Section 4, we provide a model-checking algorithm for pRBATL, and conclude the paper in Section 5.

2 Background and Preliminaries

In this section, we discuss the basic notions that are used in the technical part of the proposed logic. Let Q be a finite set and µ : Q → [0, 1] be a probability distribution function over Q such that ∑q∈Q µ(q) = 1. We denote by D(Q) the set of all such distributions over Q. For a given µ ∈ D(Q), supp(µ) = {q ∈ Q | µ(q) > 0} is called the support of µ. A probability space is a measure space with total measure 1. The standard notation of a probability space is a triple (Ω,F, Pr), where Ω is a sample space which represents all possible outcomes, F ⊆ P(Ω) is a σ-algebra over Ω which includes the empty subset and it is closed under countable unions and complement, and Pr : F → [0, 1] is a probability measure over (Ω,F). The interested reader is referred to [Billingsley, 2012] for a complete description relating to probability distributions and measures. We also denote the set of all finite, non-empty finite and infinite sequences of elements of Q by Q∗ , Q+ and Qω , respectively.

2.1 DTMC andMDP

Discrete-time Markov chains (DTMCs) are the simplest probabilistic models in which the systems evolve through discrete time steps.

Definition 1. A DTMC is a tuple Mc = (Q, q0,Π, π, δ), where Q is a set of states, q0 ∈ Q is the initial state, Π is a finite set of propositional variables, π : Q → ℘(Π) is a labelling function, and δ : Q × Q → [0, 1] is a probability transition matrix such that ∑q′∈S δ(q, q′ ) = 1 for all q ∈ Q. Here, δ(q, q′ ) denotes the probability that the chain, whenever in state q, moves into next state q′ .

Markov decision processes (MDPs), an extension to ordinary DTMCs, are a widely used formalism for modelling systems that exhibit both probabilistic and non-deterministic behaviour [Forejt et al., 2011].

Definition 2. An MDP is a tuple Md = (Q, q0,Π, π,A, δ), where A is a set of actions, δ : Q×A → D(Q) is a (partial) probabilistic transition function, and all the other components are the same as their counterparts in a DTMC.

The set of available actions at a state q is defined by A(q) = {α ∈ A | ∃q′ · δ(q, α)(q′ ) > 0}. Unlike DTMCs, in MDPs, the transitions between states occur in two steps. Firstly, an action α is selected from a set of actions A(q) available at a given state q. Secondly, a successor state q′ is chosen randomly, according to the probability distribution δ(q, α). Thus, for a given state q and α ∈ A(q), δ(q, α) : Q → [0, 1] is a function such that ∑q′∈Q δ(q, α)(q′ ) = 1.

Definition 3. A path λ in an MDP Md is an (infinite) alternating sequence of states and actions λ = q0 α0 -→ q1 α1 -→ . . . ∈ (Q×A)ω where αi ∈ A(qi) and δ(qi, αi)(qi+1) > 0 for all i ≥ 0. A finite path λ = q0 α0 -→ q1 α1 -→ . . . αn-1 ---→ qn is defined as usual as a prefix of an infinite path ending at a state qn. The set of finite paths is denoted by (Q×A)∗Q.

Definition 4. A strategy in an MDP Md is a function f : (Q×A)∗Q → D(A) that assigns each finite path λ = q0 α0 -→ q1 α1 -→ . . . αn-1 ---→ qn a probability distribution over the enabled actions A(qn) such that f(λ)(α) > 0 if α ∈ A(qn).

An MDP reduces to a DTMC if the player's strategy is fixed. That is, given an MDP Md, any strategy induces a Markov chain Mc by resolving non-determinism.

3 Syntax and Semantics of pRB-ATL

In this section, we provide the syntax and semantics of pRBATL. Let us consider a multi-agent system consisting of a set N = {1, 2, . . . n} of n(≥ 1) concurrently executing agents. In order to reason about resources, we assume that the actions performed by the agents have costs. Let R be a finite set of resources (such as money, energy, or anything else which may be required by an agent for performing an action). Without loss of generality, we assume that the cost of an action, for each of the resources, is a natural number. The set of resource bounds B over R is defined as B = (N ∪ {∞})r , where r = |R|. We denote by ⃗0 the smallest resource bound (0, . . . , 0) and by ⃗∞ the greatest resource bound (∞, . . . ,∞).

3.1 Syntax of pRB-ATL

Let Π be a finite set of atomic propositions, N be the set of agents, A be a subset of N, and b ∈ B. The syntax of pRB-ATL is defined as follows:

where p ∈ Π, ▷◁∈ {<, ≤, ≥, >}, v ∈ Q∩[0, 1], k ∈ N∪{∞}.

The two temporal operators have a standard meaning, © for "next" and U ≤k for "bounded until" if k < ∞ or "until" otherwise. When k = ∞, we shall simply write U instead of U ∞. Here, 〈〈Ab 〉〉P▷◁v[©ϕ] means that a coalition A has a strategy to make sure that the next state satisfies ϕ under resource bound b with a probability in relation ▷◁ with constant v, regardless of the strategies of other players. The formula

〈〈Ab 〉〉P▷◁v[ϕ1 U ϕ2] means that A has a strategy to enforce ϕ2 while maintaining the truth of ϕ1, and the cost of this strategy is at most b with a probability in relation ▷◁ with constant v, regardless of the strategies of other players. Other temporal operators are defined as abbreviations in a standard way. Particularly, "eventually" is defined as ✸ϕ ≡ ⊤ U ϕ, and "always" as ✷ ≡ ¬✸¬ϕ. Notice that these operators when b = ⃗∞mean the same as their counterparts in ATL, i.e., the ATL operator 〈〈A〉〉 corresponds to 〈〈A ⃗∞〉〉. Other classical abbreviations for ⊥, ∨, → and ↔ are defined as usual.

3.2 Semantics of pRB-ATL

To interpret this language, we extend the definition of resource-bounded concurrent game structures (RBCGS)) [Alechina et al., 2010] with probabilistic behaviours of agents. For consistency with [Alur et al., 2002], in what follows the terms 'agents' and 'players' and the terms 'actions' and 'moves' have been used interchangeably.

Definition 5. A Probabilistic Resource Concurrent Game Structure (pRCGS) is a tuple S = (n, r,Q,Π, π, d, c, δ) where:

• n ≥ 1 is the number of players (agents);
• r ≥ 0 is the number of resources;
• Q is a non-empty finite set of states;
• Π is a finite set of propositional variables;
• π : Π → ℘(Q) is a function which assigns a subset of Q to each variable in Π;
• d : Q × N → N+ is a function which indicates the number of moves (actions) available at a state for each agent, where N+ = N \ {0};
• c : Q × N × N+ → B is a partial function which indicates a resource cost for each move by an agent at a state; and c(q, a, 1) = ⃗0 for any q ∈ Q and a ∈ N;
• δ : Q× (N → N+) → D(Q) is a partial probabilistic transition function.

Given a pRCGS S = (n, r,Q,Π, π, d, c, δ), we identify available moves at a state q ∈ Q of an agent i ∈ N by 1, . . . , d(q, i); then Di(q) = {1, . . . , d(q, i)} denotes the set of available moves; move 1 specifies idling which is always available with cost ⃗0 by definition. Similar to ATL and RBATL, the zero-cost move 1 is required to avoid deadlock and, therefore, maintain totality.

A pRCGS is closely related to MDPs (Definition 2, Section 2.1), where abilities of individual agents and coalitions of agents are constrained by available resources in a nontrivial way. Given A ⊆ N, a joint move m of A is a function m : A → N+. Let D denote the set of all joint actions for N, i.e., D = N → N+. Given q ∈ Q, the set of available joint moves of A at q is denoted by DA(q) = {m : A → N+ | ∀a ∈ A : m(a) ∈ Da(q)}. Given q, q′ ∈ Q and m ∈ D(q), δ(q,m)(q′ ) is the conditional probability of a transition from q to q′ if every agent i ∈ N performs m(i). Then, q′ is called a successor of q if ∃m ∈ D(q) such that q′ ∈ supp(δ(q,m)). To this end, pRCGS is different from RB-CGS in defining the transition function δ. While the δ of a RB-CGS is deterministic, that of a pRCGS is a mapping to a distribution function over states and, hence, specifies non-determinism.

Example 1. Let us consider the design of a system consisting of two firefighter agents N = {1, 2} in a building. Each agent is equipped with two resources: electricity and water. Agents can perform three possible actions, namely, sense, pump water, and idle. They can sense to detect if there is a fire in the building and pump the water to stop the fire. Sensing the fire requires one unit of electricity, pumping water requires one unit of electricity and one unit of water, and idle costs nothing. This scenario is formalised by a pRCGS Sff as depicted in Figure 1. Here, n = 2, r = 2, Q = {q0, q1, q2, q3, q4}, and Π = {safe, destroyed}. For convenience, the transition function δ is written in terms of labels on transitions. Each transition from a state qi to a state qj is annotated with one or more labels of the form (x, y)/z where (x, y) denotes the joint move, x by agent 1's move and y by agent 2's move performed at state qi, and z denotes the probability of arriving at the next state qj.

At the initial state q0, each agent can either stay idle 1 or perform sense action 2. Therefore, the possible joint moves at q0 are (1, 1), (1, 2), (2, 1), and (2, 2). At the states q1 (only one agent detected the fire) and q2 (both detected the fire), each agent can either stay idle 1 or pump water 2. Thus, possible joint moves at q1 and q2 are (1,1), (2,1), (1,2), and (2,2). At the "blue" state q3, the building is saved from the fire and is labelled with a proposition "safe", while at the "red" state q4, the building is destroyed and is labelled with a proposition "destroyed". If a fire does occur in the building, each agent autonomously decides to detect it or stay idle. When only one of the agents detects the fire, the chance of stopping it is 80% if only one of them acts. However, the chance of stopping it increases to 90% if both of them act. The effectiveness of stopping the fire could be improved if both the agents detect the fire jointly. The chance of stopping it then would be 90% if only one of them acts, while it would be 99% if both of them act. If both the agents stay idle (i.e., neither of them detects the fire nor pumps the water to extinguish the fire), the building will be destroyed.

To compare costs and resource bounds, we use the usual point wise vector comparison, that is, (b1, . . . , br) ≤ (d1, . . . , dr) iff bi ≤ di for i ∈ {1, . . . , r} where n ≤ ∞ for all n ∈ N. We also use pointwise vector addition:

(b1, . . . , br) + (d1, . . . , dr) = (b1 + d1, . . . , br + dr) where n + ∞ = ∞ for all n ∈ N ∪ {∞}. Given b ∈ B, B≤b denotes the set of bounds less or equal to b without taking into account ∞ components, i.e., B≤b = {b′ ∈ B | ∀i ∈ {1, . . . , r} : b′i = bi = ∞ ∨ b′i ≤ bi < ∞}. Note that |B≤b| = ∏i∈{1,...,r},bi̸=∞(bi + 1).

Given a joint move m ∈ DA(q), the cost of m is defined as cost(q,m) = ∑a∈A c(q, a,m(a)), i.e., the total cost of the actions performed by the agents in the coalition A.

Given a pRCGS S, we adopt the Definition 3 to define runs (computations). A infinite run is an infinite sequence λ = q0 m0 --→ q1 m1 --→ . . . ∈ (Q×D)ω where mi ∈ D(qi) and qi+1 is as successor of qi by mi, i.e., (qi+1) ∈ supp(δ(qi,mi)) for all i ≥ 0. We denote the set of all infinite computations by ΩS ⊆ (Q×D)ω . A finite computation is a finite prefix λ = q0 m0 --→ q1 m1 --→ q2 . . . mn-1 ----→ qn ∈ (Q × D)∗Q of some infinite sequence in ΩS. We denote the set of all finite computations by Ω+S . For convenience, we denote (Q×D)ω and (Q×D)∗Q by (QD)ω and (QD)∗Q, respectively. The length of a computation λ, denoted by |λ|, is defined as the number of transitions in λ. For a finite computation λ = q0 m0 --→ q1 m1 --→ q2 . . . mn-1 ----→ qn ∈ Ω+S , |λ| = n; for an infinite computation λ ∈ q0 m0 --→ q1 m1 --→ . . .ΩS, |λ| = ∞. Given a computation λ ∈ Ω+S , λ(i) = qi for all i ∈ {0, . . . , |λ|}; λ(i, j) = qi . . . qj for all i, j ∈ {0, . . . , |λ|} and i ≤ j; mλ = m0m1 . . . as the projection of moves in λ and mλ(i) = mi for i ∈ {0, . . . , |λ| - 1}. Note that λ(|λ|) is the last state in λ. Finally, Ω+S,q = {λ ∈ Ω+S | λ(0) = q} denotes the set of (finite) computations starting from q ∈ Q. Given a finite computation λ ∈ Ω+S and a coalition A, the cost of joint actions by A is defined as costA(λ) = ∑|λ|-1 i=0 cost(λ(i),mλ(i)). We adopt Definition 4 (Section 2.1) to define strategies:

Definition 6. Given a pRCGS S, a strategy of a player a ∈ N is a mapping fa : (QD)∗Q → D(N+) which associates each sequence λ ∈ (QD)∗Q to a distribution µa ∈ D({1, . . . , d(λ(|λ|), a)}).

Definition 7. A strategy is called memoryless (or Markovian) if its choice of moves depends only on the current state, i.e., fa(λ) = fa(λ(|λ|)) for all λ ∈ (QD)∗Q. It is called deterministic if it always selects a move with probability 1, i.e., fa(λ) is a Dirac distribution.

Definition 8. Given a pRCGS S, a coalition strategy FA : A → ((QD)∗Q → D(N+)) is a function which associates each player a in A with a strategy.

Given a coalition strategy FA, we show that each finite sequence λ ∈ (QD)∗Q gives rise to a distribution µFA λ ∈ D(DA(λ(|λ|))) over joint actions m ∈ DA(λ(|λ|)) where µFA λ (m) = ∏a∈A fa(λ)(m(a)) and fa = FA(a) for all a ∈ A.

Lemma 1. Given a sequence λ ∈ (QD)∗Q and a coalition strategy FA, µFA λ is a distribution over DA(λ(|λ|)).

Given two coalition strategies FA and FB of two disjoint coalitions A and B, i.e., A ∩ B = ∅, their union is also a coalition strategy, denoted by FA ∪ FB, for A ∪ B.

Definition 9. Given a bound b ∈ B, and a strategy FA, FA is b-bounded iff for all λ ∈ Ω+S such that costA(λ) ≤ b, it holds that supp(µFA λ ) ⊆ {m ∈ DA(λ(|λ|)) | cost(λ(|λ|),m) ≤ b - cost(λ)}.

In other words, all executions of a b-bounded strategy cost at most b resources. In order to reason about probabilistic behaviour of S, we need to determine the probability that certain computations are taken. To do this, we construct for each state q ∈ Q, a probability space over the set of infinite computations ΩS,q starting from q. The basis of the construction is the probability of individual finite computations induced by the transition probability function δ. Given a state q0 ∈ Q, we can determine the probability of every finite computation λ = q0 m0 --→ q1 m1 --→ q2 . . . mn-1 ----→ qn ∈ Ω+S,q consistent with FA as follows:

For each finite computation λ ∈ Ω+S , we can then define a cylinder set Cλ that consists of all infinite computations prefixed by λ. Given an initial state q ∈ Q, it is then standard [Kwiatkowska et al., 2007; Billingsley, 2012] to define a measurable space over ΩS,q, infinite runs of S from q, as (ΩS,q, FS,q) where FS,q ⊆ ℘(ΩS,q) is the least σ-algebra on ΩS,q generated by the family of all cylinder sets Cλ where λ ∈ Ω+S that starts from q, i.e., λ(0) = q. Given a strategy FN, a strategy for all players in the game, the behaviour of S is fully probabilistic. It then gives rise to a probability measure (ΩS,q,FS,q, PrFN S,q ) where PrFN S,q : FS,q → [0, 1] uniquely extends PrFN S,q : Ω+S,q → [0, 1] such that PrFN S,q (Cλ) = PrFN S,q (λ) for all finite computations λ ∈ Ω+S,q starting from q.

3.3 Truth Definition for pRB-ATL

Given a pRCGS S = (n, r, Q, Π, π, d, c, δ), the truth definition for pRB-ATL is given inductively as follows:

• S, q |= ⊤;
• S, q |= p iff q ∈ π(p);
• S, q |= ¬ϕ iff S, q ̸|= ϕ;
• S, q |= ϕ1 ∨ ϕ2 iff S, q |= ϕ1 or S, q |= ϕ2;
• S, q |= 〈〈Ab 〉〉P▷◁v[ψ] iff ∃ b-bounded FA such that ∀F ¯ A, PrFA∪F ¯A S,q ({λ ∈ ΩS,q | S, λ |= ψ}) ▷◁ v;
• S, λ |=©ϕ iff S, λ(1) |= ϕ;
• S, λ |= ϕ1 U k ϕ2 iff ∃i ∈ N such that i ≤ k, ∀j < i : S, λ(j) |= ϕ1, and S, λ(i) |= ϕ2;
• S, λ |= ¬ψ iff S, λ ̸|= ψ.

This definition is a combination of pATL and RB-ATL. In particular, the case of 〈〈Ab 〉〉P▷◁zψ requires the existence of a strategy FA which must be b-bounded while there is no restriction on the strategies of the remaining players ¯ A = N \A.

From the truth definition, the following result directly inherits the complement rule for probability where ≥-1≡≤, >-1≡<, ≤-1≡≥ and <-1≡>:

Example 2. Let us continue with the running Example 1. Consider a question (property): "Can agent 1 from q0, equipped with 2 units of electricity and 1 unit of water, make sure that the building is at least 90% safe?". This means to check if ϕ{1} = 〈〈{1}(2,1) 〉〉P≥0.9✸safe is true at q0. Unfortunately, there is no such strategy for agent 1, i.e., Sff , q0 ̸|= ϕ{1}. Consider another question (property): "Can agents 1 and 2 jointly from q0, equipped with 4 units of electricity and 2 unit of water, make sure that the building is at least 90% safe?". Similar to the previous question, we need to check if ϕ{1,2} = 〈〈{1, 2}(4,2) 〉〉P≥0.9✸safe is true at q0. This is true, for example, when employing a strategy where both the agents perform sensing at q0 and pumping the water at q2. In fact, this strategy can guarantee the safety of the building by up to 99%. Hence, Sff , q0 |= ϕ{1,2}.

4 Model Checking

In this section, we present an algorithm for the model checking problem of pRB-ATL. In particular, given a pRCGS S = (n, r,Q,Π, π, d, c, δ) and a pRB-ATL formula ϕ, the algorithm produces the set of states Sat(ϕ) of S that satisfy ϕ, i.e., Sat(ϕ) = {q ∈ Q | S, q |= ϕ}. Similar to ATL and its descendants, the algorithm generally processes ϕ recursively by computing the set of states satisfying sub-formulae of ϕ before combining them to produce Sat(ϕ). For the propositional cases, the algorithm can be summarised as follows:

Let us focus on the last cases Sat(〈〈Ab 〉〉P▷◁v[ψ]) where ψ = ©ϕ1 and ψ = ϕ1 U k ϕ2 with k ∈ N ∪ {∞}. Notice that the case Sat(〈〈Ab 〉〉P▷◁v[¬ψ]) can be reduced to Sat(〈〈Ab 〉〉P▷◁-1 1-v[ψ]) due to Lemma 2. Instead of following the semantics definition, i.e., determining the existence of a b-strategy for A to achieve a certain probability v from a state s, we compute the min and max values over all possible b-strategies for A. In particular:

where PrFA∪F ¯A S,q (ψ) is a shorthand for

Then, computing states satisfying 〈〈Ab 〉〉P▷◁v[ψ] is reduced to comparing these min/max values with v as follows:

where ◁ ∈ {<,≤} and ▷ ∈ {>,≥}. In the following, we show how to compute Prmax S,q (Ab , ψ) and Prmin S,q (Ab , ψ) recursively on the structure of ψ.

Case (4a): ψ = ©ϕ1. Assume that Sat(ϕ1) has been computed. Then the maximal probability to arrive at a state in Sat(ϕ1) is obtained by players in A selecting an allowed move (costing at most b) to maximise the probability while players outside A, i.e., in ¯ A, select an arbitrary move to minimise it. Conversely, the minimal probability is obtained by players in A selecting an allowed move to minimise it while those outside select one to maximise it. Therefore, we have:

Case (4b): ψ = ϕ1 U ≤k ϕ2. Assume that Sat(ϕ1) and Sat(ϕ2) are computed. For convenience, we denote Prmax S,q (Ab , ϕ1 U k ϕ2) and Prmin S,q (Ab , ϕ1 U k ϕ2) by Xb q,k and Y b q,k , respectively. Then, there are three trivial sub-cases:

• q ∈ Sat(ϕ2): any computation from q satisfies ψ, hence Xb q,k = Y b q,k = 1.
• q /∈ Sat(ϕ1) ∪ Sat(ϕ2): any computation from q does not satisfy ψ, hence Xb q,k = Y b q,k = 0.
• q /∈ Sat(ϕ2) & k = 0: any computation from q does not satisfy ψ before 0 transition, hence Xb q,k = Y b q,k = 0.

Otherwise, players in A try to choose an allowed move m from q with cost at most b that maximises the probability to arrive at a state that can satisfy ψ with the remaining resource b′ = b - cost(q,m) and within k′ = k - 1 transitions. Formally, this can be defined as follows:

Overall, one can form two linear equation systems with variables Xb q,k and Y b q,k , respectively. They can be solved by direct methods such as Gaussian elimination or iterative methods such as Jacobi and Gauss-Seidel [Kwiatkowska et al., 2007]. In general, iterative methods suit the two linear equation systems best. It should not iterate more than k + 1 times as Xb q,0 and Y b q,0 saturate to either 0 or 1 regardless of b and q by definition.

Case (4c): ψ = ϕ1 U ϕ2. Assume that Sat(ϕ1) and Sat(ϕ2) are computed. Again for convenience, we denote Prmax S,q (Ab , ϕ1 U ϕ2) and Prmin S,q (Ab , ϕ1 U ′ ϕ2) by Xb q and Y b q , respectively. We now have two trivial cases:

• If q ∈ Sat(ϕ2), any computation from q satisfies ψ, hence Xb q = Y b q = 1.
• If q /∈ Sat(ϕ1)∪Sat(ϕ2), any computation from q does not satisfy ψ, hence Xb q = Y b q = 0.

Otherwise, players in A try to choose an allowed move m from q with cost at most b that maximises the probability to arrive at a state that can satisfy ψ with the remaining resource b′ = b-cost(q,m). Formally, this can be defined as follows:

Then, one can form two linear equation systems with variables Xb q and Y b q , respectively. Once again, they can be solved via existing methods.

Lemma 3. Given a pRCGS S and a pRB-ATL formula ϕ, (i) Sat(ϕ) terminates and (ii) q ∈ Sat(ϕ) iff S, q |= ϕ.

Sketch of proof. Since recursive calls within Sat(ϕ) are always applied to strictly sub-formulas of ϕ, termination of (i) is straightforward. Correctness of (ii) can be proved by induction on the structure of ϕ. Consider ϕ = ¬ϕ1, q ∈ Sat(ϕ) ⇔ q ∈ S \ Sat(ϕ1) ⇔ q /∈ Sat(ϕ1) ⇔ S, q ̸|= ϕ1 (by I.H.) ⇔ S, q |= ¬ϕ1. Other propositional cases (ϕ = ⊤; p; ϕ1 ∨ϕ2) are similar. Finally, from (1) and (2), the correctness of Sat(〈〈Ab 〉〉P▷◁v[ψ]) follows from the correctness of computing Prmax S,q (Ab , ψ) and Prmin S,q (Ab , ψ). This is immediate from the arguments of the cases (4a), (4b) and (4c).

Assuming that the natural numbers occurring in a pRBATL formula ϕ are encoded in unary, we have the following result.

Lemma 4. The upper bound of the time complexity for Sat(ϕ) is O(|ϕ|3r+4 · |S|3 ).

Sketch of proof. ϕ has at most O(|ϕ|) sub-formulae. The cases (4b) and (4c) are the most computationally complex. In case (4b), the numbers of b and k are bounded by O(|ϕ|r ) and O(|ϕ|), respectively. Therefore, the number of variables, also that of equations, in each corresponding linear equation system is bounded by O(|ϕ|r · |S| · |ϕ|) = O(|ϕ|r+1 · |S|). Similarly, in case (4c), the number of variables and also equations in each corresponding linear equation system is bounded by O(|ϕ|r · |S|). It is well-known that the time complexity of solving such a linear equation system is at most O(n3 ) [Golub and Van Loan, 1996], where n is the number of equations. Therefore, the complexity of computing Sat(ϕ) is O(|ϕ| · (|ϕ|r+1 · |S|)3 ) = O(|ϕ|3r+4 · |S|3 ).

Furthermore, the lower bound is given by that of the ATL, i.e., linear to the size of the input model and the input formula.

Example 3. Let us illustrate the use of the pRB-ATL and quantitatively verify the system presented in Example 1 via model checking. We generalise the properties described in Example 2 as follows "Can a coalition from q0, equipped with e units of electricity and w units of water, make sure that the building is at least v safe?". This is formalised in pRB-ATL by ϕA = 〈〈A(e,w) 〉〉P≥v✸safe. To this end, we need to check whether Sff , q0 |= ϕA. As mentioned in the previous section, this can be reduced to determine the maximal probability:

Intuitively, the best strategy for one agent to help the building to be safe is to sense and then to pump the water. In total, this costs two units of electricity and one unit of water. Similarly, while cooperating, the best strategy for both the agents would be to choose their best strategies concurrently, which will cost together four units of electricity and two units of water. Therefore, for A = {1}, we consider the resources bounded by (e,w) ≤ (2, 1) and for A = {1, 2} those are bounded by (e,w) ≤ (4, 2). For each case of A and (e, w), the corresponding equation system from case (4c) can be solved by, for example, the iterative method as applied in [Kwiatkowska et al., 2007]. The solutions of these linear equation systems are summarised in Table 1 for A = {1} and in Table 2 for A = {1, 2}. In particular, Table 1 shows that any resource bound less than (2, 1) is not helpful for agent 1 as it has no strategy to make sure that the building is safe. In the best case, with resource bound (2, 1), the only vital strategy is to sense the fire and then pump the water. In this case, since agent 2 is not required to cooperate, the worst case is to end up in q1 from q0 where the chance to arrive at q3, the safe state, is at least 80%. That is, choosing the following actions: (2, 1) in q0, (2, 1) in q1 and (1, 1) in q3. Similarly, Table 2 shows that any resource bound less than (2, 1) will not be enough for both the agents while cooperating. However, the chance of making the building safe increases to 90% as more and more resources are given. This is because from q0 both the agents can force the arrival at q2 instead of q1, where there are at least three units of electricity are available at q0. Eventually, the maximal chance of making the building safe reaches 99% as both the agents have enough resources to follow the same best strategy. That is, choosing the following actions: (2, 2) in q0, (2, 2) in q2 and (1, 1) in q3. Due to the small size of the illustrative example system, the time taken for the verification was less than 1 second.

5 Conclusions and FutureWork

In this paper, we proposed a logic pRB-ATL for reasoning about coalitional abilities of systems under resource constraints that exhibit both probabilistic and non-deterministic behaviour, and provided a standard model-checking algorithm for it. pRB-ATL allows us to express various interesting properties of coalitions of agents involving resource limitations and probabilistic behaviour. For example, it can express that "a coalition of agents A has a strategy to achieve a property ϕ with probability ▷◁ v (▷◁∈ {<,≤,≥,>}) provided they have resources b, but they cannot enforce ϕ under a tighter resource bound b′ with probability ▷◁ v".

In future work, we would like to explore the real world applicability of the proposed logic as an underlying solution framework for more complex analyses of resource-bounded systems. The example scenario presented in this paper is a very simple case. If we model a more realistic scenario and increase the problem size, the analysis and verification task would be hard to do by hand. Therefore, it would be more convenient to use an automatic method to encode and verify them, for example using a model checking tool [Kwiatkowska et al., 2002].