Probabilistic Model Checking Multi-agent Behaviors in Dispersion Games Using Counter Abstraction

  • Jianye Hao
  • Songzheng Song
  • Yang Liu
  • Jun Sun
  • Lin Gui
  • Jin Song Dong
  • Ho-fung Leung
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7455)


Accurate analysis of the stochastic dynamics of multi-agent system is important but challenging. Probabilistic model checking, a formal technique for analysing a system which exhibits stochastic behaviors, can be a natural solution to analyse multi-agent systems. In this paper, we investigate this problem in the context of dispersion games focusing on two strategies: basic simple strategy (BSS) and extended simple strategies (ESS). We model the system using discrete-time Markov chain (DTMC) and reduce the state space of the models by applying counter abstraction technique. Two important properties of the system are considered: convergence and convergence rate. We show that these kinds of properties can be automatically analysed and verified using probabilistic model checking techniques. Better understanding of the dynamics of the strategies can be obtained compared with empirical evaluations in previous work. Through the analysis, we are able to demonstrate that probabilistic model checking technique is applicable, and indeed useful for automatic analysis and verification of multi-agent dynamics.


Model Check Multiagent System Model Check Technique Vickrey Auction Statistical Model Check 
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.
    Alpern, S.: Spatial dispersion as a dynamic coordination problem. Tech. rep., The London School of Economics (2001)Google Scholar
  2. 2.
    Baier, C., Katoen, J.: Principles of Model Checking, ch. 10, pp. 866–883. The MIT Press (2008)Google Scholar
  3. 3.
    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 (LNAI), vol. 4324, pp. 162–174. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  4. 4.
    Arthur, B.: Inductive reasoning and bounded rationality. American Economic Association Papers 84, 406–411 (1994)Google Scholar
  5. 5.
    Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. AAMAS 12, 239–256 (2006)Google Scholar
  6. 6.
    Claus, C., Boutilier, C.: The dynamics of reinforcement learning in cooperative multiagent systems. In: AAAI 1998, pp. 746–752 (1998)Google Scholar
  7. 7.
    Challet, D., Zhang, Y.: Emergence of cooperation and organization in an evolutionary game. Physica A 246, 407 (1994)CrossRefGoogle Scholar
  8. 8.
    Holzmann, G.: The spin model checker. TSE 23(5), 279–295 (1997)MathSciNetGoogle Scholar
  9. 9.
    Gomes, E.R., Kowalczyk, R.: Dynamic analysis of multiagent-learning with e-greedy exploration. In: ICML 2009 (2009)Google Scholar
  10. 10.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 102–111 (1994)CrossRefGoogle Scholar
  11. 11.
    Hao, J.Y., Song, S.Z., Liu, Y., Sun, J., Dong, J.S., Leung, H.F.: Online Technical Report,
  12. 12.
    Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical Model Checking: An Overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  14. 14.
    Osborne, M.J., Rubinstein, A.: A Course in Game Theory. MIT Press, Cambridge (1994)zbMATHGoogle Scholar
  15. 15.
    Stone, P., Veloso, M.: Multiagent systems: A survey from a machine learning perspective. Autonomous Robots 8, 345–383 (2000)CrossRefGoogle Scholar
  16. 16.
    Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1, ∞ )-Counter Abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Rao, A.S.: Agentspeak(l): Bdi Agents Speak Out in a Logical Computable Language. In: Van de Velde, W., Perram, J.W. (eds.) MAAMAW 1996. LNCS, vol. 1038, pp. 42–55. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  18. 18.
    Song, S.Z., Hao, J.Y., Liu, Y., Sun, J., Leung, H.F., Dong, J.S.: Analyzing multi-agent systems with probabilistic model checking approach. In: ICSE 2012. NIER (2012)Google Scholar
  19. 19.
    Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  20. 20.
    Sun, J., Liu, Y., Roychoudhury, A., Liu, S., Dong, J.S.: Fair Model Checking with Process Counter Abstraction. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 123–139. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  21. 21.
    Sun, J., Song, S., Liu, Y.: Model Checking Hierarchical Probabilistic Systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 388–403. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  22. 22.
    Grenager, T., Powers, R., Shoham, Y.: Dispersion games: general definitions and some specific learning results. In: AAAI 2002, pp. 398–403 (2002)Google Scholar
  23. 23.
    Tadjouddine, E.M., Guerin, F., Vasconcelos, W.: Abstraction for model checking game-theoretical properties of auction (short paper). In: AAMAS 2008, pp. 1613–1616 (2008)Google Scholar
  24. 24.
    Tuyls, K., Verbeeck, K., Lenaerts, T.: A selection-mutation model for q-learning in multi-agent systems. In: AAMAS 2003, pp. 693–700 (2003)Google Scholar
  25. 25.
    Vidal, J.M., Durfee, E.H.: Predicting the expected behavior of agents that learn about agents: The clri framework. AAMAS 6, 77–107 (2003)Google Scholar
  26. 26.
    Wooldridge, M., Fisher, M., Huget, M.P., Parsons, S.: Model checking multi-agent systems with mable. In: AAMAS 2002, pp. 952–959 (2002)Google Scholar
  27. 27.
    Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: ASE 2000, pp. 3–12 (2000)Google Scholar
  28. 28.
    Azar, Y., Broder, A.Z., Karlin, A.R., Upfa, E.: Balanced allocations. SIAM Journal on Computing 29(1), 190–200 (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Jianye Hao
    • 1
  • Songzheng Song
    • 2
  • Yang Liu
    • 2
  • Jun Sun
    • 3
  • Lin Gui
    • 2
  • Jin Song Dong
    • 2
  • Ho-fung Leung
    • 1
  1. 1.The Chinese University of Hong KongHong Kong
  2. 2.National University of SingaporeSingapore
  3. 3.Singapore University of Technology and DesignSingapore

Personalised recommendations