Coalitional Planning in Game-like Domains via ATL Model Checking

Based on the planning via model checking paradigm, we address the problem of coalitional planning in this paper. Informally, coalitional planning is the problem of planning for a subset of agents in a multi-agent system to force the whole multi-agent system to satisfy some goals. We use the language of ATL as the goal language and the semantic structure of ATL, i.e., concurrent game structure, to formalize the planning domain. We separate the concept of goal and planning object and use execution structures to interpret the goals. And then, we define a algorithm for coalitional planning and formally prove its correctness. Distinguished from the previous work, in coalitional planning all the ATL formulas can be considered as goals, thus the expressive power of ATL is sufficiently applied.