Formal Modelling and Verification of Probabilistic Resource Bounded Agents

An increasingly important field of AI is autonomous agents and multi-agent systems, where agents are entities that can interact with their environment or other agents in pursuit of their goals. In general, multi-agent systems research refers to software agents. However, the agents in a Multi-agent System (MAS) could also be for example humans or robots. A key feature of a MAS is that agents in the system are concurrent. The primary aims of such systems are modularity, scalability, flexibility, robustness, and distributed computing (Jennings & Wooldridge, 1998). In multi-agent systems, there are many problems which also require coalition formation among the agents and such problems can only be usefully analysed in terms of the combined abilities of groups of agents. For example, it may be that no single agent, a potential home buyer having some financial deposit constraint, has a strategy to reach a particular state, buying a home, on its own, but two agents, perhaps husband and wife, cooperating with each other are capable of achieving this outcome. Similarly, in the prisoners dilemma (Rapoport, 1989), a single prisoner cannot ensure the optimal outcome, while a coalition of two prisoners can. The Alternating-time Temporal Logic (ATL) (Alur et al., 2002) was introduced as a logical formalism for analysing the strategic abilities of coalitions with temporal winning conditions. The semantics of ATL is usually given by a transition system specification based on concurrent game structures. In ATL, various interesting properties of coalitions and strategies such as reachability and controllability can be formulated. One can then encode a system and verify its desired properties expressed in ATL using standard ATL model-checking tools, such as jMocha (Alur et al., 2001) and MCMAS (Lomuscio et al., 2017). Coalition Logic (CL) (Pauly, 2002) is another logical formalism similar to ATL, intended to describe the ability of groups of agents to achieve a goal in a strategic game. It can specify what a group of agents can (not) achieve through choices of their actions. In the literature, several variants of ATL and CL have been proposed (see e.g., (Goranko, 2001; Ågotnes et al., 2009; Herzig et al., 2013)). These logics allow us to express many interesting properties of coalitions and strategies, such as “a coalition of agents A(\(\subseteq N\), the set of all agents) has a strategy to reach a state satisfying \(\varphi \) no matter what the other agents and/or environment (\(N\setminus A\)) in the system do”, where \(\varphi \) characterises, e.g., lifting a heavy weight by a group of robots A, saving a building from fire by a group of fire extinguisher robots A or simply a solution to a problem. In fact, these logics can be used to state various qualitative properties of real-world concurrent systems. However, analysing quantitative properties of systems, such as reliability and uncertainty, which can not be expressed trivially in the logics described above, is equally or even more important. Reliability is the probability that a system will perform its specified function over a given period of time under defined environmental conditions. For example, a reliability property could be “if a fire is detected in a building, then the probability of it being put out and the building being saved by a coalition of robotic agents A within k time steps is at least p”.

Many real-world systems, such as 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 paradigm offers an excellent framework which can be used to model and implement such systems (Leitao et al., 2016). Such systems usually 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). These systems therefore often require rigorous analysis and verification to ensure their designs are correct (Kwiatkowska, 2016). Thus, working together across theory and practice is fundamental to address real-world challenges and develop novel formal frameworks in tandem with the theory and tools required to ensure desired systems’ reliability and correctness. In conventional verification via model-checking, given a model of a system, and a specification, a model checker determines if the system satisfies the specification by returning a yes or no answer. However, when considering stochasticity in the environment, agents in the system should be formalised in a way so that they exhibit probabilistic behaviour. PRISM (Kwiatkowska et al., 2002) is a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. A system model in PRISM can be developed using its own modelling language similar to reactive modules (Alur et al., 2001), and the properties can be written in an appropriate property specification language, including PCTL (Bianco & de Alfaro, 1995), CSL (Baier et al., 1999), PLTL (Baier, 1998), PCTL\(^*\) (Baier, 1998), and rPATL (Chen et al., 2013). These are fundamentally probabilistic temporal logics. The logic rPATL allows to reason 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 neither be expressed in rPATL nor in any other probabilistic temporal logics mentioned above in a straightforward way. In this paper, we propose a logic pRB-ATL  for reasoning about coalitional ability under resource constraints in the probabilistic setting, which allows us to express such properties. The significance and novelty of the proposed logical framework, based on probabilistic reasoning and decision-theoretic principles, is that it allows us to analyse the implications of uncertainty and limited computational, communication, or any other resources on the design of autonomous agents in a more realistic and simple manner. This article is a revised and extended version of Nguyen and Rakib (2019). The main differences from Nguyen and Rakib (2019) are a complete literature review, addition of the complete proofs of the lemmas and theorems, development of the model-checking toolkit, and modeling a more complex example system with comprehensive experimental analysis and verification results.

The rest of this paper is organised as follows. In Sect. 2, we review related work and discuss how our proposed logic pRB-ATL  differs from other logics suggested in the literature. In Sect. 3, we discuss the basic notions of probability distribution, and the underlying probabilistic formalisms of our logic such as Discrete-time Markov chains and Markov Decision Processes. In Sect. 4 we present the syntax and semantics of pRB-ATL. In Sect. 5, we give a model-checking algorithm for pRB-ATL. In Sect. 6, we outline an implementation of our model-checking prototyping tool. In Sect. 7, we model, analyse, and present experimental results applying our techniques and tool. Finally, in Sect. 8 we conclude the paper and outline directions for future work.

In this section, we outline recent important developments on ATL and its extensions considering conventional, resource-bounded, and probabilistic reasoning by discussing important features, such as (un)decidability results, expressiveness, and model-checking problems.

A large number of existing studies in the multi-agent coalition literature have formulated reasoning about the abilities of coalitions of agents in terms of games (Pauly, 2002; Goranko, 2001; Wooldridge & Dunne, 2004; Ågotnes et al., 2009). The coalition logic basically generalises the notion of a strategic game, and its semantics is given in terms of state transition systems where each state has an associated strategic game. The logic ATL (Alur et al., 2002) was originally developed to reason about distributed processes in adversarial environments, and CL (Pauly, 2002) can be regarded as the one-step fragment of ATL (Goranko & Drimmelen, 2006; Goranko, 2001). That is, in CL, the outcome of a strategic game is realised in the next state, but in ATL, properties can be expressed holding in arbitrary future states. These logics allow us to express many interesting properties of coalitions and strategies, as mentioned previously, such as \(\langle \!\langle A \rangle \!\rangle \varphi \), which states that coalition A has a strategy to reach a state satisfying \(\varphi \). The exact semantics of the modalities of the coalition varies depending on whether or not the knowledge that each agent has about the current state of the game is complete (in modal logic it’s attributed as complete/incomplete information), and whether agents can use past game state knowledge when deciding on their next move or not (in modal logic it’s attributed as perfect/imperfect recall). It is shown in Alur et al. (2002) that the model-checking problem for complete information is decidable in polynomial time, and it’s undecidable for the incomplete information and perfect recall case (Dima and Tiplea, 2011).

Recently, there has been growing interest in formal models of resource-bounded agents (Alechina et al., 2009; Alechina et al., 2010; Bulling & Farwer, 2010; Della Monica et al., 2011; Alechina et al., 2010; Nguyen et al., 2015). In resource-bounded reasoning agent research work, the emphasis is on the behavior of agents constrained by fixed resource bounds. For example, the authors of Alechina et al. (2009) introduced Coalition Logic for Resource Games (CLRG), an extension of Coalition Logic that allows explicit reasoning about the resource endowments of coalitions of agents and the resource bounds on strategies. Similarly, the Resource-bounded Alternating-time Temporal Logic (RB-ATL) (Alechina et al., 2010) was developed for reasoning about coalitional ability under resource bounds. The logic RB-ATL   allows us to express various resource-bounded properties, such as \(\langle \!\langle A^b \rangle \!\rangle \varphi \) which expresses that coalition A has a strategy to reach a state satisfying \(\varphi \) under the resource bound b. The model-checking problem for RB-ATL is decidable and if resource bounds are encoded in unary, the model-checking algorithm for RB-ATL runs in time polynomial in the size of the formula and the structure, and exponential in the number of resources. There also exist other works on extensions of temporal logics and logics of coalitional ability that are capable of expressing resource bounds (Bulling & Farwer, 2010; Della Monica et al., 2011). In Bulling and Farwer (2010) Resource-bounded Tree Logics RTL and RTL\(^*\) were introduced. The logic RTL\(^*\), which extends CTL\(^*\) with quantifiers representing the cost of paths, can allow only to analyse single-agent systems. RTL is a fragment of RTL\(^*\) in which each temporal operator is immediately preceded by a path quantifier. Fundamentally, in their proposed language the existential path quantifier \(E\varphi \) of CTL has been replaced by \(\langle \rho \rangle \varphi \), where \(\rho \) represents a set of available resources. Intuitively, the formula \(\langle \rho \rangle \varphi \) states that there exists a computation feasible with the given resources \(\rho \) that satisfies \(\varphi \). It has been shown that the model-checking problem for RTL and some sub-classes of RTL\(^*\) is decidable.

The Price Resource-bounded ATL (PRB-ATL) logic proposed in Della Monica et al. (2011) has introduced its model-checking problem and its syntax and semantics consider resource endowment of the whole system when evaluating a formula pertaining to a coalition of agents. In their model the resources are convertible to money and its amount is bounded. Example properties that can be expressed in PRB-ATL includes \(\langle \!\langle A^\$ \rangle \!\rangle \varphi \), which states that the coalition A has a strategy such that, no matter what the opponent agents do, \(\varphi \) can be achieved under the expenses \(\$\). Similar to the RB-ATL, \(\$\) can be \(\infty \) in the general case. That is, the meaning of \(\langle \!\langle A^\$ \rangle \!\rangle \varphi \) when \(\$=\infty \) is the same as its counterpart in ATL. The model-checking problem for PRB-ATL is decidable and its complexity similar to that of RB-ATL.

In Alechina et al. (2010), the authors proposed a sound and complete logic RBCL that allows us to express the costs of strategies under resource bounds. They have demonstrated how to verify properties expressed in RBCL and provided a decision procedure for the satisfiability problem of RBCL as well as a model-checking algorithm. However, RBCL has some limitations. For example, properties like "coalition C has a strategy to maintain the property \(\varphi \) with resources b", or "coalition C can maintain \(\varphi \) until \(\psi \) becomes true provided C has resources b" cannot be expressed in RBCL. We can express and verify such properties using RB-ATL (Alechina et al., 2010; Nguyen et al., 2015).

In a more recent work (Belardinelli & Demri, 2021), the authors studied model-checking problem complexity of RB±ATL\(^{+}\), a variant of RB±ATL (Alechina et al., 2018). The authors investigated the RB±ATL\(^{+}\) version, which allows Boolean combinations of path formulas starting with single temporal operators, but is only able to analyse a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. Its model-checking problem complexity is \(\Delta ^P_2\)-complete when taking into account just one agent and one resource, which is similar to that of the standard CTL\(^{+}\) logic. Additionally, they have demonstrated that the model-checking problem for RB±ATL\(^{+}\) can be solved in EXPTIME with an arbitrary number of agents and a fixed number of resources by using a sophisticated Turing reduction to the parity game problem for alternating vector addition systems with states. Overall, the paper provides a thorough and rigorous treatment of the model-checking problem complexities of strategic reasoning in resource-bounded agents considering both the production and consumption of resources.

A large number of multi-agent application domains, such as IoT and CPS in general and disaster rescue and military operations in particular, require not only the reasoning about the team behavior of agents but also require that the agents and/or the environment may have random or unreliable behaviors. In such domains, the behaviour of an agent has to be described in terms of a distribution of probability over a set of possibilities. There has recently been increasing interest in developing logics with a probabilistic component and to link logical and probabilistic reasoning (see e.g., (Chen and Lu, 2007; Bulling & Jamroga, 2009; Forejt et al., 2011; Huang et al., 2012; Chen et al., 2013; Song et al., 2019; Fu et al., 2018; Wan et al., 2013)). These logics are essentially extensions of CTL or ATL which allow for probabilistic quantification of described properties. In general, probabilistic systems exhibit a combination of probabilistic and nondeterministic behaviour, and the semantics of the system models are defined in terms of probabilistic transition systems. For example, the semantics of the probabilistic ATL logics are defined over probabilistic extension of concurrent game structure (Alur et al., 2002), for which a commonly used underlying formalism is Markov Decision Processes (MDPs). Probabilistic model-checking is also a well-established technique, and a well-known tool PRISM exists based on Markov chains (MCs) and MDPs probabilistic models (Kwiatkowska et al., 2002). In Chen and Lu (2007), PATL/PATL\(^*\) logics have been developed by extending ATL and interpreting over the probabilistic concurrent game structures. Interesting properties that can be expressed in PATL include \(\langle \!\langle A \rangle \!\rangle [\varphi _p]{\bowtie v}\); it can be read as: a coalition A has a strategy such that for all strategies of agents not in A, the probability that the path formula \(\varphi \) is satisfied is \(\bowtie v\) (\(\bowtie \in \{\le ,<,>,\ge \}\)). It was then further extended to develop the logics rPATL/rPATL\(^*\) (Chen et al., 2013) for expressing quantitative properties of stochastic multi-player games. The logics rPATL/rPATL\(^*\) extend PATL/PATL\(^*\) with operators that can enforce an expected reward \(\bowtie v\). The logic rPATL\(^*\) can express cumulative rewards given by the transition system. It is know that model-checking problem for rPATL\(^*\) is 2EXPTME-complete.

Similar to rPATL, strategies of the agents in our proposed pRB-ATL  logic are randomised. An agent uses a randomised strategy by selecting a probability distribution over moves; and the move to be played is then chosen at random, according to the distribution. However, the reasoning problem considered in our work differs from rPATL in two important ways. First, and most importantly, properties in rPATL related to rewards are of 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. That is, using pRB-ATL, it is possible to ask whether a strategy (a sequence of actions) exists to achieve some goal with probability 0.99 if the agents start with e.g., 100 units of energy. Second, semantics for rPATL is based on turn-based systems while ours is based on concurrent systems. However, recently developed PRISM-games 3.0 (Kwiatkowska et al., 2020) supports modelling concurrent games. We are aware that properties of resource-bounded systems can be verified by expressing them using rPATL. However, to encode a system using rPATL, we have to expand the model to incorporate the resource information into the states of the model. For different formulas with different resource bounds we have to then induce a new model to perform the model-checking algorithms. Our proposed approach allows model-checking algorithms to work directly with the original model. This opens up the possibility of future research including not only agents consume but also produce resources. In the resource production case, verifying resource-bounded properties by encoding resource-bounded system using rPATL is no longer feasible. Furthermore, we do not mention anything about optimal strategies in our framework. Our aim is to check existence of a strategy (which may not be optimal), where the resources each agent is prepared to commit to a goal are bounded.

The approach proposed by Huang et al. (2012) in developing probabilistic ATL logic relies on interpreted system semantics. The resulting logic PATL\(^*\) essentially generalises the interpreted system (Fagin et al., 1995) by adding probabilistic modality and explicit local actions taken by the agents. An example property that can be expressed in PATL\(^*\) is \(\langle \!\langle A \rangle \!\rangle ^{\bowtie v}\varphi \) which expresses that coalition A has a strategy to enforce \(\varphi \) with a probability \(\bowtie v\). However, since the semantics is based on incomplete information and synchronous perfect recall, model-checking problem for PATL\(^*\) is undecidable even for a single agent system.

In Bulling and Jamroga (2009), another alternative semantics for a probabilistic logic PATL has been proposed using the notion of prediction denotation operator. In PATL the reasoning about probabilistic success studied over complete information games. The success of the strategy of a coalition is measured according to a probability measure describing the potential actions of the rest of the agents in the system. An example property that can be expressed in PATL is \(\langle \!\langle A \rangle \!\rangle ^{p}_{\omega }\varphi \) which expresses that coalition A has a strategy to enforce \(\varphi \) with probability p when agents not in A behave according to \(\omega \). The model-checking problem for PATL with mixed strategies is bounded between Probabilistic polynomial time and PSPACE.

In Guan and Yu (2022), the authors presented a probabilistic continuous-time linear logic (CLL), to reason about the probability distribution execution of continuous-time Markov chains (CTMCs). In CLL, multiphase timed until formulas are allowed and the semantics of the formulas focuses on relative time intervals, meaning that time can be reset just like in timed automata. The model-checking problem is reduced to a reachability problem of absolute time intervals.

In Wang et al. (2021), the authors proposed a new concept of probabilistic conformance for Cyber-Physical Systems (CSP). This idea is based on approximately equal satisfaction probability for a given (infinite) set of signal temporal logic (STL) formulas. They have presented a verification algorithm for the probabilistic compliance of grey-box CPS, described by probabilistic uncertain systems. Their proposed statistical verification method is based on a statistical test that can determine if two probability distributions are equal at any chosen level of confidence. It is shown that statistically confirming compliance is possible when the STL formula is monotonically parameterized, meaning that the satisfaction probability of the formula changes monotonically with the parameters.

We must say that after ATL (Alur et al., 2002) was introduced a remarkably rich literature has been developed. Here we have discussed only an overview of the works that are closely related to the topic of the paper. However, in all the approaches, at least in the probabilistic setting, the basic idea of agents acting in an environment according to a set of rules in the pursuit of goals does not take into account resources. In real life, many actions that an agent may perform to achieve a goal can only be accomplished in the availability of certain resources. Certain actions are not possible without sufficient resources, which will lead to a plan failure. To the best of our knowledge, there are no existing works in the literature that address probabilistic variants of ATL for modeling and verifying resource-bounded agents explicitly.

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 \(\mu : Q\rightarrow [0,1]\) be a probability distribution function over Q such that \(\sum _{q\in Q} \mu (q) = 1\). We denote by \(\mathcal {D}(Q)\) the set of all such distributions over Q. For a given \(\mu \in \mathcal {D}(Q)\), \(\textsf{supp}(\mu )=\{q\in Q\mid \mu (q)>0\}\) is called the support of \(\mu \). A probability space is a measure space with total measure 1. The standard notation of a probability space is a triple (\(\Omega , \mathcal {F}, Pr)\), where \(\Omega \) is a sample space which represents all possible outcomes, \(\mathcal {F}\subseteq \mathcal {P}(\Omega )\) is a \(\sigma \)-algebra over \(\Omega \), i.e., it includes the empty subset and it is closed under countable unions and complement, and \(Pr: \mathcal {F}\rightarrow [0,1]\) is a probability measure over \((\Omega , \mathcal {F})\). The interested reader is referred to Billingsley (1986) 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^\omega \), respectively.

In this section, we provide the syntax and semantics of pRB-ATL. Let us consider a multi-agent system consisting of a set \(N=\{1,2,\ldots n\}\) of \(n(\ge 1)\) concurrently executing agents. In order to reason about resources, we assume that the actions performed by the agents have costs. Let \(R = \{res_1, res_2,\ldots , res_r\}\) be a finite set of \(r\ge 1\) 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 \(\mathbb {B}\) over R is defined as \(\mathbb {B}= (\mathbb {N}\cup \{\infty \})^{r}\), where \(r=|R|\). We denote by \(\vec {0}\) the smallest resource bound \((0,\ldots ,0)\) and by \(\vec {\infty }\) the greatest resource bound \((\infty ,\ldots ,\infty )\).

In probabilistic model-checking, the most elementary class of properties for probabilistic models is reachability. Given a state \(q\in Q\), the probabilistic reachability problem computes the probability to reach some state in a specified target set of states in the model. That is, the basic reachability question is: “can we reach a given target state from a given initial state with some given probability v?". More formally, given a state \(q\in Q\), and a set of target states \(T\subseteq Q\), the reachability probability is the measure of paths starting in q and containing a state from T, i.e., \(Pr(\{\lambda \in \Omega _{M,q}\mid \lambda (i)\in T\) for some \(i\in \mathbb {N}\})\). The property of probabilistic reachability actually refers to the minimum or maximum probability. In practice, many model-checking problems can be reduced to reachability problem; therefore, it is considered as one of the most fundamental properties in probabilistic model-checking. For an in-depth discussion on this topic, we refer the interested reader to Forejt et al. (2011).

Here, we present an algorithm for the model-checking problem of pRB-ATL. In particular, given a pRCGS \(S = (n,r,Q,\Pi ,\pi ,d,c,\delta )\) and a pRB-ATL  formula \(\varphi \), the algorithm produces the set of states \(Sat(\varphi )\) of S that satisfy \(\varphi \), i.e., \(Sat(\varphi ) = \{ q \in Q \mid S,q \models \varphi \}\). Similar to ATL   and its descendants, the algorithm generally processes \(\varphi \) recursively by computing the set of states satisfying sub-formulae of \(\varphi \) before combining them to produce \(Sat(\varphi )\). For the propositional cases, the algorithm can be summarised as follows:Let us focus on the last cases \(Sat(\langle \!\langle A^b \rangle \!\rangle \textsf{P}_{\bowtie v}[\psi ])\) where \(\psi =\bigcirc \varphi _1\) and \(\psi =\varphi _1 \mathbin {\mathcal {U}}^{k} \varphi _2\) with \(k\in \mathbb {N}\cup \{\infty \}\). Notice that the case \(Sat(\langle \!\langle A^b \rangle \!\rangle \textsf{P}_{\bowtie v}[\lnot \psi ])\) can be reduced to \(Sat(\langle \!\langle A^b \rangle \!\rangle \textsf{P}_{\bowtie ^{-1} 1-v}[\psi ])\) 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 \(\textsf{Pr}_{S,q}^{F_{A}\cup F_{\bar{A}}} (\psi )\) is a shorthand forThen, computing states satisfying \(\langle \!\langle A^b \rangle \!\rangle \textsf{P}_{\bowtie v}[\psi ]\) is reduced to comparing these min/max values with v as follows:where \(\triangleleft \in \{<,\le \}\) and \(\triangleright \in \{>,\ge \}\). To this end, we can formulate a simple recursive algorithm, as presented in Algorithm 1, to compute the set of states satisfying a formula \(\varphi \). It still remains to show how to compute \(\textsf{Pr}_{S,q}^{\max }(A^b,\psi )\) and \(\textsf{Pr}_{S,q}^{\min }(A^b,\psi )\). Based on the structure of \(\psi \), these values can be computed according to the following three cases:

Case (a): \(\psi = \bigcirc \varphi _1\). Assume that \(Sat(\varphi _1)\) has been computed. Then the maximal probability to arrive at a state in \(Sat(\varphi _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 \(\bar{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 (b): \(\psi = \varphi _1 \mathbin {\mathcal {U}}^{\le k} \varphi _2\). Assume that \(Sat(\varphi _1)\) and \(Sat(\varphi _2)\) are computed. For convenience, we denote \(\textsf{Pr}_{S,q}^{\max }(A^b,\varphi _1 \mathbin {\mathcal {U}}^k \varphi _2)\) and \(\textsf{Pr}_{S,q}^{\min }(A^b,\varphi _1 \mathbin {\mathcal {U}}^k \varphi _2)\) by \(X^{b}_{q,k}\) and \(Y^{b}_{q,k}\), respectively. Then, there are three trivial sub-cases: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 \(\psi \) 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 \(X^b_{q,k}\) and \(Y^b_{q,k}\), respectively, for each k. 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 \(X^b_{q,0}\) and \(Y^b_{q,0}\) saturate to either 0 or 1 regardless of b and q by definition.

Case (c): \(\psi = \varphi _1 \mathbin {\mathcal {U}}\varphi _2\). Assume that \(Sat(\varphi _1)\) and \(Sat(\varphi _2)\) are computed. Again for convenience, we denote \(\textsf{Pr}_{S,q}^{\max }(A^b,\varphi _1 \mathbin {\mathcal {U}}\varphi _2)\) and \(\textsf{Pr}_{S,q}^{\min }(A^b,\varphi _1 \mathbin {\mathcal {U}}\varphi _2)\) by \(X^{b}_{q}\) and \(Y^{b}_{q}\), respectively. Similar to the approach in Chen et al. (2013), variables \(X^{b}_{q}\) can be computed by iterating the computation of variables \(X^{b}_{q,k}\) as defined in case (b) for \(k \rightarrow \infty \). In practice, this computation can be terminated up to a large enough k such that \(\max \limits _{b,q}\vert X^{b}_{q,k}-X^{b}_{q,k+1}\vert \) is less than some \(\epsilon \), a pre-specified convergence threshold. This is based on the fact that \(X^{b}_{q,k}\) is a non-decreasing sequence that converges to \(X^{b}_{q}\) (Raghavan & Filar, 1991).

In the following, we show the termination and the correctness of Algorithm 1.

Assuming that the natural numbers occurring in a pRB-ATL formula \(\varphi \) are encoded in unary, we have the following result.

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.

We have developed a prototype probabilistic model-checking tool for resource-bounded stochastic multiplayer games based on the techniques proposed in this paper .¹ The tool is implemented in Python. It takes two input, a pRCGS model and a pRB-ATL formula. The model input is then interpreted by a parser into an instance of the class Model. Similarly, the formula is interpreted by an another parser into an instance of the class Formula. This formula instance may recursively include further formula instances of the sub formulas of the input formula. Finally, the implementation of the model-checking procedure \(Sat(\varphi )\), introduced in Sect. 5, is executed to compute the set of states of the input model satisfying the input formula. The whole described process is depicted in Fig. 2.

The class Formula has five sub-classes corresponding to the five cases of state formulas \(\varphi \) defined in Sect. 4.1. For the last case \(\langle \!\langle A^b \rangle \!\rangle \textsf{P}_{\bowtie v}[\psi ]\), an auxiliary class, named PathFormula, is introduced to represent path formulae (next, until and negation). Similar to the class Formula, PathFormula has three sub-classes corresponding to the three cases of the path formulae \(\psi \).

The two parsers have been implemented based on Antlr4 (ANTLR, 2020). They interpret pRCGS models and pRB-ATL formulae in a specification language, respectively, defined as close to the syntaxes of pRCGS and pRB-ATL as possible. The syntax of the specification language for pRCGS models is as follow:

where agents is a positive number indicating the number of agents in the model, resources is a number indicating the number of resources. The remainders describe the set of their corresponding elements. In particular, sets such as gstates are defined by the syntax diagram depicted in Fig. 3 where gstate are simply names of states.

The syntax diagram for propositions is similar. Functions such as availables are defined as sets of mappings. Each mapping follows the syntax diagram in Fig. 4 from a pair consisting of a state and a number (identifying an agent) to the number of available actions.

The syntaxes are similar for labellings, costings, transitions where elements of labellings are mapping to a set, costings to a cost (a tuple of numbers) and transitions to a state distribution. A state distribution is simply a set of pairs consisting of a state and a natural number. The probability of a state in a distribution is the division of its corresponding number by the sum of all the numbers in the distribution. The syntax diagram for such a pair is depicted in Fig. 5.

The underlying implementation technique of the model-checking procedure \(Sat(\varphi )\) is an explicit-state model-checking. The procedure of \(Sat(\varphi )\) is implemented by a member method, named \(\texttt {sat}\), of the class Formula. This method is overridden for each of the five sub-classes corresponding to the five cases of \(Sat(\varphi )\) described in Sect. 5. The method \(\texttt {sat}\) takes only one parameter, an instance of the input model, and recursively calls the same method of instances representing the sub-formulae of \(\varphi \).

Let us illustrate the use of the pRB-ATL and quantitatively verify the system presented in Example 1 via our model-checking tool. We generalise the properties described in Example 2 as follows “Can a coalition from \(q_0\), equipped with e units of electricity and w units of water, make sure that the building is at least v low-burnt safe?”. This is formalised in pRB-ATL by \(\varphi _A = \langle \!\langle A^{(e,w)} \rangle \!\rangle \textsf{P}_{\ge v} \Diamond \hbox {low-burnt}\). To this end, we need to check whether \(S_{ff},q_0 \models \varphi _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 saved with low-burnt 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)\le (2,1)\) and for \(A=\{1,2\}\) those are bounded by \((e,w)\le (4,2)\). For each case of A and (e, w), the model-checking results 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 with low-burnt. 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 \(q_1\) from \(q_0\) where the chance to arrive at \(q_3\), the low-burnt safe state, is at least \(25\%\). That is, choosing the following actions: 21 in \(q_0\), 21 in \(q_1\), and 11 in \(q_3\). Note that any resource bound greater than (2, 1) will also not increase the chance of making sure the building is low-burnt safe with a higher probability. 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 with low-burnt increases to \(74\%\) as more and more resources are given. This is because from \(q_0\) both the agents can force the arrival at \(q_2\) instead of \(q_1\). Eventually, the maximal chance of making the building safe with low-burnt reaches \(99\%\) as both the agents have enough resources to follow the same best strategy. That is, choosing the following actions: 22 in \(q_0\), 22 in \(q_2\), and 11 in \(q_3\).

As we mentioned earlier, if a fire occurs in the building, there are possibilities that the building fire intensity can be increased from low (at \(q_1\) or \(q_2\)) to medium (at \(q_4\)), and eventually to high (at \(q_6\)) severity. If the fire intensity reaches from low to medium, then for a single agent with resource bound (2, 1) the maximum probability for which the building can be saved with medium-burnt is \(5.7\%\), choosing the following actions: 22 in \(q_0\), 12 in \(q_2\), 21 in \(q_4\), and 11 in \(q_5\). Since agent 2 is not required to cooperate, it will try to minimize the probability. Basically, there are two paths from \(q_0\) to \(q_5\) where agent 1 performs action 2 at \(q_0\), namely \(q_0 \xrightarrow {22} q_2 \xrightarrow {12} q_4 \xrightarrow {21} q_5\) with probability 0.057 and \(q_0 \xrightarrow {21} q_1 \xrightarrow {12} q_4 \xrightarrow {21} q_5\) with probability 0.165, and obviously the first path will be chosen. An interesting point to note here is that increasing resource bound from (2, 1) to (3, 2) for agent 1 will not increase the probability of saving the building anymore with medium-burnt. For example, with resource bound (3, 2) if agent 1 senses the fire and then pumps water twice, then agent 2, being uncooperative and its objective is the opposite, will sense the fire and pump the water once, and ultimately will lead through a path ending up with probability 0.002. That is, choosing the following actions: 22 in \(q_0\), 22 in \(q_2\), 21 in \(q_4\), and 11 in \(q_5\). Tables 1 and 2 demonstrate the self-explanatory results for the coalition, as well as other situations such as high-burnt.

In this paper, we have designed and developed a framework for automatic verification of systems with both resource limitations and probabilistic behaviour. We proposed a novel temporal logic pRB-ATL  for reasoning about coalitional abilities of systems under resource constraints that exhibit both probabilistic and non-deterministic behaviour. The novelty of our approach lies in complex logical combinations that tackles the problem of more comprehensive resource-bounded probabilistic multi-agent system specification and verification. To model multi-agent systems where the actions of agents consume resources, we have modified probabilistic strategy logics in two ways. Firstly, we added resource annotations to the actions in the transition system. For each individual action and each resource type, we have specified how many units of this resource type the action consumes. Secondly, we have extended the logical language so that we can express properties related to resources and probability. The model-checking problem for standard strategy logics is a special case of the model-checking problem for the corresponding resource logics. We have investigated how much harder does the model-checking problem become when resources are added explicitly. We have designed model-checking algorithms for the resulting logic pRB-ATL, implemented them in a prototype tool, and used our techniques to solve simple multi-agent model-checking problems of increasing complexity. Algorithm 1 returns a set of states satisfying a  pRB-ATL  formula \(\varphi \) and its complexity is \(O(\vert \varphi \vert ^{3r+1} \cdot \vert S\vert ^3)\). To the best of the authors’ knowledge, this is the first work on an approach that provides a straightforward way to express and verify the properties of resource-bounded probabilistic multi-agent problems commonly found in real-world settings.

There are a number of interesting directions in this area for future research. First of all, we would like to investigate extensions of our logical framework and techniques to incorporate agent’s behaviour with production of resources, and analyse a wider class of properties for the resulting logic. Secondly, we would like to study alternative semantics of the logics, including Interpreted Systems and Strategy Logic, implement them and report the expressivity and performance among alternative approaches. In this paper, we have used the example system just to explain the definitions/concepts used in Sect. 4 and in the rest of the paper in terms of the example. However, construction of a model considering a more realistic scenario is a non-trivial work. In future work, we have a plan to investigate the use of pRBATL logic for the analysis and verification of collaborative systems, by means of several use-cases. For example, in the domain of smart production system or similar other domains where a group of robots work collaboratively to achieve some goals.