Model-checking for Resource-Bounded ATL with production and consumption of resources

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