Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources

Several logics for expressing coalitional ability under resource bounds have been proposed andstudied in the literature. Previous work has shown that if only consumption of resources isconsidered or the total amount of resources produced or consumed on any path in the systemis bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic(RB-ATL) is decidable. However, for coalition logics with unbounded resource production andconsumption, only some undecidability results are known. In this paper, we show that the modelcheckingproblem for RB-ATL with unbounded production and consumption of resources isdecidable but EXPSPACE-hard. We also investigate some tractable cases and provide a detailedcomparison to a variant of the resource logic RAL, together with new complexity results.

Publisher Statement: This is an open access article under the CC BY license