RESUMO
Strategic ability updating relates to establishing some required properties, which can be expressed by strategic abilities, in a multicomponent reactive system. We model such a reactive system as a concurrent game structure (CGS), which is the semantic model of Alternating-time Temporal Logic (ATL). Then, we propose coalitional commitment as a tool for achieving the required strategic ability updating. Intuitively, a coalitional commitment can extend the state space of a CGS by a context function and then delete some transitions by a coalitional normative system (CNS). We propose coordinated ATL (co-ATL) for reasoning about strategic abilities in the structures obtained from a CGS by implementing a CNS. The model-checking problem for co-ATL is proved to be PTIME-complete, just like that of ATL, and is thus tractable. Then, we characterize the limitation of coalitional commitment power by identifying the set of co-ATL formulas whose satisfaction cannot be established and the set of co-ATL formulas whose satisfaction cannot be avoided. Afterward, we show that the effectiveness problem, feasibility problem, and synthesis problem for coalitional commitment are PTIME-complete, NP-complete, and FNP-complete, respectively. Finally, we treat the coalitional commitment synthesis problem as an extended planning problem and present an algorithm based on the planning as model checking paradigm. Our work can be seen as an improvement for both social law research and planning via model checking research.
