On a Logic for Coalitional Games with Priced-Resource Agents

Abstract

Alternating-time Temporal Logic (ATL) and Coalition Logic (CL) are well-established logical formalisms particularly suitable to model games between dynamic coalitions of agents (like e.g. the system and the environment). Recently, the ATL formalism has been extended in order to take into account boundedness of the resources needed for a task to be performed. The resulting logic, called Resource-Bounded ATL (RB-ATL), has been presented in quite a variety of scenarios. Even if the model checking problem for extensions of ATL dealing with resource bounds is usually undecidable, a model checking procedure for RB-ATL has been proposed. In this paper, we introduce a new formalism, called PRB-ATL, based on a different notion of resource bounds and we show that its model checking problem remains in EXPTIME and has a PSPACE lower bound. Then, we tackle the problem of coalition formation. How and why agents should aggregate is not a new issue and has been deeply investigated, in past and recent years, in various frameworks, as for example in algorithmic game theory, argumentation settings, and logic-based knowledge representation. We face this problem in the setting of priced resource-bounded agents with the goal specified by an ATL formula. In particular we solve the problem of determining the minimal cost coalitions of agents acting in accordance to rules expressed by a priced game arena and satisfying a given formula. We show that such problem is computationally not harder than verifying the satisfaction of the same formula with fixed coalitions.