Advertisement

State of the Art in Logics for Verification of Resource-Bounded Multi-Agent Systems

  • Natasha AlechinaEmail author
  • Brian Logan
Conference paper
  • 35 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12180)

Abstract

Approaches to the verification of multi-agent systems are typically based on games or transition systems defined in terms of states and actions. However such approaches often ignore a key aspect of multi-agent systems, namely that the agents’ actions require (and sometimes produce) resources. We survey previous work on the verification of multi-agent systems that takes resources into account, extending substantially a survey from 2016 [9].

Notes

Acknowledgements

The authors thank Stéphane Demri for helpful discussions.

References

  1. 1.
    Abdulla, P.A., Mayr, R., Sangnier, A., Sproston, J.: Solving parity games on integer vectors. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 106–120. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40184-8_9CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Bouajjani, A., d’Orso, J.: Deciding monotonic games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 1–14. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-45220-1_1CrossRefGoogle Scholar
  3. 3.
    Alechina, N., Logan, B., Nguyen, H.N., Rakib, A.: A logic for coalitions with bounded resources. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, vol. 2, pp. 659–664. IJCAI/AAAI, AAAI Press (2009)Google Scholar
  4. 4.
    Alechina, N., Logan, B., Nguyen, H.N., Rakib, A.: Resource-bounded alternating-time temporal logic. In: Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2010, pp. 481–488. IFAAMAS (2010)Google Scholar
  5. 5.
    Alechina, N., Bulling, N., Demri, S., Logan, B.: On the complexity of resource-bounded logics. Theor. Comput. Sci. 750, 69–100 (2018).  https://doi.org/10.1016/j.tcs.2018.01.019MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Alechina, N., Bulling, N., Logan, B., Nguyen, H.N.: On the boundary of (un)decidability: decidable model-checking for a fragment of resource agent logic. In: Yang, Q. (ed.) Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI 2015. IJCAI, AAAI Press, Buenos Aires, Argentina, July 2015Google Scholar
  7. 7.
    Alechina, N., Bulling, N., Logan, B., Nguyen, H.N.: The virtues of idleness: a decidable fragment of resource agent logic. Artif. Intell. 245, 56–85 (2017).  https://doi.org/10.1016/j.artint.2016.12.005MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Alechina, N., Dastani, M., Logan, B.: Verifying existence of resource-bounded coalition uniform strategies. In: Rossi, F. (ed.) IJCAI 2016, Proceedings of the 25th International Joint Conference on Artificial Intelligence. IJCAI/AAAI (2016)Google Scholar
  9. 9.
    Alechina, N., Logan, B.: Verifying systems of resource-bounded agents. In: Beckmann, A., Bienvenu, L., Jonoska, N. (eds.) CiE 2016. LNCS, vol. 9709, pp. 3–12. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-40189-8_1CrossRefzbMATHGoogle Scholar
  10. 10.
    Alechina, N., Logan, B.: Resource logics with a diminishing resource (extended abstract). In: Dastani, M., Sukthankar, G., Andre, E., Koenig, S. (eds.) Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2018, pp. 1847–1849. IFAAMAS (2018)Google Scholar
  11. 11.
    Alechina, N., Logan, B., Nga, N.H., Rakib, A.: Logic for coalitions with bounded resources. J. Logic Comput. 21(6), 907–937 (2011)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Alechina, N., Logan, B., Nguyen, H.N., Raimondi, F.: Decidable model-checking for a resource logic with production of resources. In: Proceedings of the 21st European Conference on Artificial Intelligence, ECAI-2014, pp. 9–14. ECCAI, IOS Press, Prague, Czech Republic, August 2014Google Scholar
  13. 13.
    Alechina, N., Logan, B., Nguyen, H.N., Raimondi, F.: Symbolic model-checking for one-resource RB+-ATL. In: Yang, Q. (ed.) Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI 2015. IJCAI, AAAI Press, Buenos Aires, Argentina, July 2015Google Scholar
  14. 14.
    Alechina, N., Logan, B., Nguyen, H.N., Raimondi, F.: Model-checking for resource-bounded ATL with production and consumption of resources. J. Comput. Syst. Sci. 88, 126–144 (2017)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Alechina, N., Logan, B., Nguyen, H.N., Raimondi, F., Mostarda, L.: Symbolic model-checking for resource-bounded ATL. In: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, pp. 1809–1810. ACM (2015)Google Scholar
  16. 16.
    Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0028774CrossRefGoogle Scholar
  18. 18.
    Belardinelli, F.: Verification of non-uniform and unbounded artifact-centric systems: decidability through abstraction. In: Bazzan, A.L.C., Huhns, M.N., Lomuscio, A., Scerri, P. (eds.) International Conference on Autonomous Agents and Multi-Agent Systems, AAMAS 2014, pp. 717–724. IFAAMAS/ACM (2014)Google Scholar
  19. 19.
    Belardinelli, F., Demri, S.: Resource-bounded ATL: the quest for tractable fragments. In: Elkind, E., Veloso, M., Agmon, N., Taylor, M.E. (eds.) Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2019, pp. 206–214. International Foundation for Autonomous Agents and MultiAgent Systems (2019)Google Scholar
  20. 20.
    Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Model checking rational agents. IEEE Intell. Syst. 19(5), 46–52 (2004)CrossRefGoogle Scholar
  21. 21.
    Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. J. Auton. Agents Multi-Agent Syst. 12(2), 239–256 (2006). http://dro.dur.ac.uk/622/CrossRefGoogle Scholar
  22. 22.
    Brázdil, T., Jančar, P., Kučera, A.: Reachability games on extended vector addition systems with states. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 478–489. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14162-1_40CrossRefGoogle Scholar
  23. 23.
    Bulling, N., Farwer, B.: On the (un-)decidability of model checking resource-bounded agents. In: Proceedings of the 19th European Conference on Artificial Intelligence, ECAI 2010. Frontiers in Artificial Intelligence and Applications, vol. 215, pp. 567–572. IOS Press (2010)Google Scholar
  24. 24.
    Bulling, N., Farwer, B.: On the (un-)decidability of model checking resource-bounded agents. Technical report IfI-10-05. Clausthal University of Technology (2010)Google Scholar
  25. 25.
    Bulling, N., Farwer, B.: Expressing properties of resource-bounded systems: the logics RTL* and RTL. In: Dix, J., Fisher, M., Novák, P. (eds.) CLIMA 2009. LNCS (LNAI), vol. 6214, pp. 22–45. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16867-3_2CrossRefzbMATHGoogle Scholar
  26. 26.
    Bulling, N., Goranko, V.: How to be both rich and happy: combining quantitative and qualitative strategic reasoning about multi-player games (extended abstract). In: Mogavero, F., Murano, A., Vardi, M.Y. (eds.) Proceedings 1st International Workshop on Strategic Reasoning, SR 2013. EPTCS, vol. 112, pp. 33–41 (2013)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Bulling, N., Nguyen, H.N.: Model checking resource bounded systems with shared resources via alternating Büchi pushdown systems. In: Chen, Q., Torroni, P., Villata, S., Hsu, J., Omicini, A. (eds.) PRIMA 2015. LNCS (LNAI), vol. 9387, pp. 640–649. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-25524-8_47CrossRefGoogle Scholar
  28. 28.
    Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.: Generalized mean-payoff and energy games. In: Lodaya, K., Mahajan, M. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, 15–18 December 2010, Chennai, India. LIPIcs, vol. 8, pp. 505–516. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)Google Scholar
  29. 29.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)CrossRefGoogle Scholar
  30. 30.
    Courtois, J.-B., Schmitz, S.: Alternating vector addition systems with states. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 220–231. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44522-8_19CrossRefGoogle Scholar
  31. 31.
    Della Monica, D., Napoli, M., Parente, M.: On a logic for coalitional games with priced-resource agents. Electron. Notes Theor. Comput. Sci. 278, 215–228 (2011)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Della Monica, D., Napoli, M., Parente, M.: Model checking coalitional games in shortage resource scenarios. In: Proceedings of the 4th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2013. EPTCS, vol. 119, pp. 240–255 (2013)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Dennis, L.A., Fisher, M., Webster, M.P., Bordini, R.H.: Model checking agent programming languages. Autom. Softw. Eng. 19(1), 5–63 (2012)CrossRefGoogle Scholar
  34. 34.
    Dima, C., Tiplea, F.L.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR abs/1102.4225 (2011). http://arxiv.org/abs/1102.4225
  35. 35.
    Fisher, M., Dennis, L.A., Webster, M.P.: Verifying autonomous systems. Commun. ACM 56(9), 84–93 (2013)CrossRefGoogle Scholar
  36. 36.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Boston (1979)zbMATHGoogle Scholar
  37. 37.
    Jurdziński, M., Lazić, R., Schmitz, S.: Fixed-dimensional energy games are in pseudo-polynomial time. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 260–272. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-47666-6_21CrossRefGoogle Scholar
  38. 38.
    Kanovich, M.I.: Petri nets, horn programs, linear logic and vector games. Ann. Pure Appl. Logic 75(1–2), 107–135 (1995)MathSciNetCrossRefGoogle Scholar
  39. 39.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  40. 40.
    Lincoln, P., Mitchell, J.C., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. Ann. Pure Appl. Logic 56(1–3), 239–311 (1992)MathSciNetCrossRefGoogle Scholar
  41. 41.
    Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_55CrossRefGoogle Scholar
  42. 42.
    Nguyen, H.N., Rakib, A.: A probabilistic logic for resource-bounded multi-agent systems. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, 10–16 August 2019, pp. 521–527. ijcai.org (2019)Google Scholar
  43. 43.
    Raskin, J., Samuelides, M., Begin, L.V.: Games for counting abstractions. Electron. Notes Theor. Comput. Sci. 128(6), 69–85 (2005)CrossRefGoogle Scholar
  44. 44.
    Shapiro, S., Lespérance, Y., Levesque, H.J.: The cognitive agents specification language and verification environment for multiagent systems. In: Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2002, pp. 19–26. ACM Press, New York (2002)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Utrecht UniversityUtrechtThe Netherlands
  2. 2.University of NottinghamNottinghamUK

Personalised recommendations