Abstract
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.
Supported by the National Natural Science Foundation of China (61672229, 61832015).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Continuing the tradition in multi-agent systems with the exception of the initial paper on alternating refinement relations [3].
References
de Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: Proceedings of LICS 2000 (2000)
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). https://doi.org/10.1007/3-540-49213-5_2
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). https://doi.org/10.1007/BFb0055622
Baskar, A., Ramanujam, R., Suresh, S.P.: Knowledge-based modelling of voting protocols. In: Proceedings of TARK 2007 (2007)
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)
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)
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)
Berwanger, D., Mathew, A.B., van den Bogaard, M.: Hierarchical information and the synthesis of distributed strategies. Acta Informatica 55, 669–701 (2018)
Blackburn, P., Rijke, M.D., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)
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). https://doi.org/10.1007/978-3-642-16242-8_1
Dima, C., Tiplea, F.L.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR (2011)
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). https://doi.org/10.1007/BFb0084794
Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of alternating-time temporal logic. Theor. Comput. Sci. 353, 93–117 (2006)
Jamroga, W., Dix, J.: Model checking abilities under incomplete information is indeed delta2-complete. In: Proceedings of EUMAS 2006 (2006)
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). https://doi.org/10.1007/978-3-540-71389-0_18
Laroussinie, F., Markey, N., Sangnier, A.: ATLsc with partial observation. In: Proceedings of GandALF 2015 (2015)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)
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)
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). https://doi.org/10.1007/BFb0055614
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). https://doi.org/10.1007/11539452_42
Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: Proceedings of FOCS 1979 (1979)
Strauss, C.: A critical review of the triple ballot voting system, part2: cracking the triple ballot encryption (2006)
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)
VAS-Group. In: Imperial college of London. https://vas.doc.ic.ac.uk/software/mcmas/
Wikipedia: Three ballot voting system. https://en.wikipedia.org/wiki/threeballot
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). https://doi.org/10.1007/978-3-642-15240-5_6
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Gardy, P., Deng, Y. (2019). Simulations for Multi-Agent Systems with Imperfect Information. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-32409-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32408-7
Online ISBN: 978-3-030-32409-4
eBook Packages: Computer ScienceComputer Science (R0)