Synthesizing Coalitions for Multi-agent Games

摘要

We present Temporal Cooperation Logic with Coalition Variables (TCLX), for the synthesis of coalitions of unknown sizes to achieve temporal objectives in multi-agent games. TCLX extends Temporal Cooperation Logic (TCL) by allowing existentially quantified variables for agent sets and operators for set relations. Even though TCLX is shown more expressive than TCL and incomparable with AMC, GL, and ATL* in expressiveness, the verification complexities of TCLX are still maintained as those of TCL, i.e., EXPTIME-complete for model-checking and 2-EXPTIME-complete for satisfiability checking. We then extend the on-the-fly model-checking algorithm of TCL for implementing a TCLX model-checker. Our implementation is experimented with three benchmark models in the context of network security, software development, and marketing promotion. The experiment results show the broad applicability and promises of TCLX in synthesizing coalitions for multi-agent systems.