Verifying Team Formation Protocols with Probabilistic Model Checking

  • Taolue Chen
  • Marta Kwiatkowska
  • David Parker
  • Aistis Simaitis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6814)


Multi-agent systems are an increasingly important software paradigm and in many of its applications agents cooperate to achieve a particular goal. This requires the design of efficient collaboration protocols, a typical example of which is team formation. In this paper, we illustrate how probabilistic model checking, a technique for formal verification of probabilistic systems, can be applied to the analysis, design and verification of such protocols. We start by analysing the performance of an existing team formation protocol modelled as a discrete-time Markov chain. Then, using a Markov decision process model, we construct optimal algorithms for team formation. Finally, we use stochastic two-player games to analyse the competitive coalitional setting, in which agents are split into cooperative and hostile classes. We present experimental results from these models using the probabilistic model checking tool PRISM, which we have extended with support for stochastic games.


Coalition Formation Stochastic Game Reward Structure Agent Organisation Total Reward 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdallah, S., Lesser, V.R.: Organization-based cooperative coalition formation. In: IAT, pp. 162–168. IEEE, Los Alamitos (2004)Google Scholar
  2. 2.
    Ågotnes, T., van der Hoek, W., Wooldridge, M.: Reasoning about coalitional games. Artificial Intelligence 173(1), 45–79 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Ballarini, P., Fisher, M., Wooldridge, M.: Uncertain agent verification through probabilistic model-checking. In: Barley, M., Mouratidis, H., Unruh, A., Spears, D., Scerri, P., Massacci, F. (eds.) SASEMAS 2004-2006. LNCS, vol. 4324, pp. 162–174. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  5. 5.
    Bonzon, E., Lagasquie-Schiex, M.-C., Lang, J.: Efficient coalitions in Boolean games. In: Texts in Logic and Games, vol. 5, pp. 293–297 (2008)Google Scholar
  6. 6.
    Chatterjee, K., Henzinger, T., Piterman, N.: Strategy logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 59–73. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203–224 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Dunne, P.E., van der Hoek, W., Kraus, S., Wooldridge, M.: Cooperative boolean games. In: Proc. of AAMAS 2008, pp. 1015–1022. ACM, New York (2008)Google Scholar
  9. 9.
    Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated Verification Techniques for Probabilistic Systems. In: Proc. SFM 2011. Springer, Heidelberg (to appear, 2011)Google Scholar
  10. 10.
    Gaston, M.E., des Jardins, M.: Agent-organized networks for dynamic team formation. In: Proc. of AAMAS 2005, pp. 230–237. ACM, New York (2005)Google Scholar
  11. 11.
    Glinton, R., Scerri, P., Sycara, K.: Agent-based sensor coalition formation. In: Proc. Fusion 2008, pp. 1–7. IEEE, Los Alamitos (2008)Google Scholar
  12. 12.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)CrossRefzbMATHGoogle Scholar
  13. 13.
    Kraus, S., Shehory, O., Taase, G.: Coalition formation with uncertain heterogeneous information. In: Proc. of AAMAS 2003, pp. 1–8. ACM, New York (2003)Google Scholar
  14. 14.
    Kwiatkowska, M., Norman, G.: Verifying randomized Byzantine agreement. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 194–209. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  15. 15.
    Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Proc. of CAV 2011. LNCS. Springer, Heidelberg (to appear, 2011)Google Scholar
  17. 17.
    Lomuscio, A., Raimondi, F.: mcmas: A model checker for multi-agent systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Manisterski, E., David, E., Kraus, S., Jennings, N.R.: Forming efficient agent groups for completing complex tasks. In: Proc. of AAMAS 2006, pp. 834–841. ACM, New York (2006)Google Scholar
  19. 19.
    Osborne, M.J., Rubinstein, A.: A course in game theory. The MIT press, Cambridge (1994)zbMATHGoogle Scholar
  20. 20.
    Shehory, O., Kraus, S.: Methods for task allocation via agent coalition formation. Artificial Intelligence 101(1-2), 165–200 (1998)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Taolue Chen
    • 1
  • Marta Kwiatkowska
    • 1
  • David Parker
    • 1
  • Aistis Simaitis
    • 1
  1. 1.Computing LaboratoryUniversity of OxfordOxfordUK

Personalised recommendations