Simulations for Multi-Agent Systems with Imperfect Information

  • Patrick GardyEmail author
  • Yuxin Deng
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)


Equivalence-checking and simulations are well-known methods used to reduce the size of a system in order to verify it more efficiently. While Alur et al. proposed a notion of simulation sound and complete for ATL as early as 1998, there have been very few works on equivalence-checking performed on extensions of ATL* with probabilities, imperfect information, counters etc. In the case of multi-agent systems (MASs) with imperfect information, the lack of sound and complete algorithm mostly follows from the undecidability of ATL model-checking. However, while ATL is undecidable overall, there exist sub-classes of MASs for which ATL becomes decidable. In this paper, we propose a notion of simulation sound for ATL/ATL* on any MASs and complete on naive MASs. Using our simulations we design an equivalence-checking algorithm sound and complete for MASs with public actions.


  1. 1.
    de Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: Proceedings of LICS 2000 (2000)Google Scholar
  2. 2.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 23–60. Springer, Heidelberg (1998). Scholar
  3. 3.
    Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998). Scholar
  4. 4.
    Baskar, A., Ramanujam, R., Suresh, S.P.: Knowledge-based modelling of voting protocols. In: Proceedings of TARK 2007 (2007)Google Scholar
  5. 5.
    Belardinelli, F., Condurache, R., Dima, C., Jamroga, W., Jones, A.V.: Bisimulations for verifying strategic abilities with an application to ThreeBallot. In: Proceedings of AAMAS 2017 (2017)Google Scholar
  6. 6.
    Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Verification of multi-agent systems with imperfect information and public actions. In: Proceedings AAMAS 2017. International Foundation for Autonomous Agents and Multiagent Systems (2017)Google Scholar
  7. 7.
    Berthon, R., Maubert, B., Murano, A., Rubin, S., Vardi, M.Y.: Strategy logic with imperfect information. In: Proceedings of LICS 2017, pp. 1–12 (2017)Google Scholar
  8. 8.
    Berwanger, D., Mathew, A.B., van den Bogaard, M.: Hierarchical information and the synthesis of distributed strategies. Acta Informatica 55, 669–701 (2018)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Blackburn, P., Rijke, M.D., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  10. 10.
    Chatterjee, K., Doyen, L.: The complexity of partial-observation parity games. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 1–14. Springer, Heidelberg (2010). Scholar
  11. 11.
    Dima, C., Tiplea, F.L.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR (2011)Google Scholar
  12. 12.
    Goltz, U., Kuiper, R., Penczek, W.: Propositional temporal logics and equivalences. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 222–236. Springer, Heidelberg (1992). Scholar
  13. 13.
    Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of alternating-time temporal logic. Theor. Comput. Sci. 353, 93–117 (2006)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Jamroga, W., Dix, J.: Model checking abilities under incomplete information is indeed delta2-complete. In: Proceedings of EUMAS 2006 (2006)Google Scholar
  15. 15.
    Laroussinie, F., Markey, N., Oreiby, G.: On the expressiveness and complexity of ATL. In: Seidl, H. (ed.) FoSSaCS 2007. LNCS, vol. 4423, pp. 243–257. Springer, Heidelberg (2007). Scholar
  16. 16.
    Laroussinie, F., Markey, N., Sangnier, A.: ATLsc with partial observation. In: Proceedings of GandALF 2015 (2015)Google Scholar
  17. 17.
    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19, 9–30 (2017)CrossRefGoogle Scholar
  19. 19.
    van der Meyden, R., Vardi, M.Y.: Synthesis from knowledge-based specifications. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 34–49. Springer, Heidelberg (1998). Scholar
  20. 20.
    van der Meyden, R., Wilke, T.: Synthesis of distributed systems from knowledge-based specifications. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 562–576. Springer, Heidelberg (2005). Scholar
  21. 21.
    Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: Proceedings of FOCS 1979 (1979)Google Scholar
  22. 22.
    Strauss, C.: A critical review of the triple ballot voting system, part2: cracking the triple ballot encryption (2006)Google Scholar
  23. 23.
    Tabatabaei, M., Jamroga, W., Ryan, P.Y.: Expressing receipt freeness and coercion-resistance in logics of strategic ability preliminary attempt. In: Proceedings of PrAISe 2016 (2016)Google Scholar
  24. 24.
    VAS-Group. In: Imperial college of London.
  25. 25.
    Wikipedia: Three ballot voting system.
  26. 26.
    Zhang, C., Pang, J.: On probabilistic alternating simulations. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IAICT, vol. 323, pp. 71–85. Springer, Heidelberg (2010). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Shanghai Key Laboratory of Trustworthy ComputingEast China Normal UniversityShanghaiChina

Personalised recommendations