Synthesizing Coalitions for Multi-agent Games

  • Wei Ji
  • Farn Wang
  • Peng WuEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


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.


  1. 1.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Brihaye, T., Costa, A., Laroussinie, F., Markey, N.: ATL with strategy contexts and bounded memory. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 92–106. Springer, Heidelberg (2009). doi: 10.1007/978-3-540-92687-0_7 CrossRefGoogle Scholar
  3. 3.
    Bulling, N., Jamroga, W.: Alternating epistemic \(\upmu \)-calculus. In: IJCAI, pp. 109–114 (2011)Google Scholar
  4. 4.
    Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Inf. Comput. 208, 677–693 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999). doi: 10.1007/3-540-48153-2_12 CrossRefGoogle Scholar
  6. 6.
    Huang, C.-H., Schewe, S., Wang, F.: Model-checking iterated games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 154–168. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-36742-7_11 CrossRefGoogle Scholar
  7. 7.
    Jamroga, W., Murano, A.: On module checking and strategies. In: AAMAS, pp. 701–708 (2014)Google Scholar
  8. 8.
    Jamroga, W., Murano, A.: Module checking of strategic ability. In: AAMAS, pp. 227–235 (2015)Google Scholar
  9. 9.
    Jones, A.V., Knapik, M., Penczek, W., Lomuscio, A.: Group synthesis for parametric temporal-epistemic logic. In: AAMAS, pp. 1107–1114 (2012)Google Scholar
  10. 10.
    Kermack, W.O., McKendrick, A.G.: A contribution to the mathematical theory of epidemics. Proc. R. Soc. A Math. Phys. Eng. Sci. 115(772), 700 (1927)CrossRefzbMATHGoogle Scholar
  11. 11.
    Kupferman, O., Vardi, M.Y., Wolper, P.: Module checking. Inf. Comput. 164(2), 322–344 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Laroussinie, F., Markey, N.: Satisfiability of ATL with strategy contexts. In: GANDALF, EPTCS, vol. 119, pp. 208–223 (2013)Google Scholar
  13. 13.
    Lye, K.W., Wing, M.J.: Game strategies in network security. Int. J. Inf. Secur. 4(1), 71–86 (2005)CrossRefGoogle Scholar
  14. 14.
    Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: What makes Atl* decidable? A decidable fragment of strategy logic. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 193–208. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-32940-1_15 CrossRefGoogle Scholar
  15. 15.
    Mogavero, F., Murano, A., Sauro, L.: On the boundary of behavioral strategies. In: LICS, pp. 263–272 (2013)Google Scholar
  16. 16.
    Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: FSTTCS, pp. 133–144 (2010)Google Scholar
  17. 17.
    Pinchinat, S.: A generic constructive solution for concurrent games with expressive constraints on strategies. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 253–267. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-75596-8_19 CrossRefGoogle Scholar
  18. 18.
    Rahwan, T., Michalak, T.P., Wooldridge, M., Jennings, N.R.: Coalition structure generation: a survey. Artif. Intell. 229, 139–174 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Wang, F., Schewe, S., Huang, C.H.: An extension of ATL with strategy interaction. ACM Trans. Program. Lang. Syst. (TOPLAS) 37(3), 9 (2015)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.State Key Laboratory of Computer ScienceInstitute of Software, Chinese Academy of SciencesBeijingChina
  2. 2.University of Chinese Academy of SciencesBeijingChina
  3. 3.Deptartment of Electrical EngineeringNational Taiwan UniversityTaipeiTaiwan

Personalised recommendations