Skip to main content
SpringerLink
Log in
Book cover

Conference on Computability in Europe

CiE 2016: Pursuit of the Universal pp 3–12Cite as

Verifying Systems of Resource-Bounded Agents

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9709))

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 briefly survey previous work on the verification of multi-agent systems that takes resources into account, and outline some key challenges for future work.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Another strand of work focusses on theorem proving, e.g., [28], but such approaches typically require user interaction to guide the search for a proof.

  2. 2.

    There is work on model-checking infinite state transition systems, see, for example, [11], but in this paper we concentrate on the finite case.

  3. 3.

    CL is a fragment of ATL with only the next time \(\langle \!\langle A \rangle \!\rangle \bigcirc \) modality.

  4. 4.

    Here, (0, 1) is the allocation of 0 units of \(r_1\) and 1 unit of \(r_2\) to agent 1. We only show resource bound for the proponent agents, \(\{1 \}\) in this case. Versions of resource logic where opponents are also resource-bounded all have an undecidable model-checking problem, see [14].

References

  1. 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 

  2. 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 

  3. 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). AAAI Press, Buenos Aires, July 2015

    Google Scholar 

  4. 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 

  5. Alechina, N., Logan, B., Nga, N.H., Rakib, A.: Logic for coalitions with bounded resources. J. Logic Comput. 21(6), 907–937 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  6. 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. IOS Press, Prague, August 2014

    Google Scholar 

  7. Alechina, N., Logan, B., Nguyen, H.N., Raimondi, F.: Symbolic model-checking for oneresource RB+-ATL. In: Yang, Q. (ed.) Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015). AAAI Press, Buenos Aires, July 2015

    Google Scholar 

  8. 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 

  9. Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  10. 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.) Computer Aided Verification. LNCS, vol. 1247, pp. 521–525. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  11. 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 

  12. Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Model checking rational agents. IEEE Intell. Syst. 19(5), 46–52 (2004)

    Article  Google Scholar 

  13. 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/

    Article  Google Scholar 

  14. 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 

  15. 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 

  16. Bulling, N., Farwer, B.: Expressing Properties of Resource-Bounded Systems: The Logics RTL\(^{*}\) and RTL. In: Fisher, M., Novák, P., Dix, J. (eds.) CLIMA X. LNCS, vol. 6214, pp. 22–45. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  17. 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)

    Google Scholar 

  18. 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: Principles and Practice of Multi-Agent Systems. LNCS, vol. 9387, pp. 640–649. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  19. 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)

    Article  MATH  Google Scholar 

  20. Monica, D.D., Napoli, M., Parente, M.: On a logic for coalitional games with priced-resource agents. Electr. Notes. Theor. Comput. Sci. 278, 215–228 (2011)

    Article  MathSciNet  Google Scholar 

  21. 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)

    Google Scholar 

  22. Dennis, L.A., Fisher, M., Webster, M.P., Bordini, R.H.: Model checking agent programming languages. Autom. Softw. Eng. 19(1), 5–63 (2012)

    Article  Google Scholar 

  23. 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

  24. Fisher, M., Dennis, L.A., Webster, M.P.: Verifying autonomous systems. Commun. ACM 56(9), 84–93 (2013)

    Article  Google Scholar 

  25. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory. Addison-Wesley, Languages and Computation (1979)

    Google Scholar 

  26. 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)

    Chapter  Google Scholar 

  27. 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)

    Chapter  Google Scholar 

  28. 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, New York (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Nottingham, Nottingham, UK

    Natasha Alechina & Brian Logan

Authors
  1. Natasha Alechina
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Brian Logan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Natasha Alechina .

Editor information

Editors and Affiliations

  1. Swansea University, Swansea, United Kingdom

    Arnold Beckmann

  2. Université Paris-Diderot - Paris 7, Paris, France

    Laurent Bienvenu

  3. University of South Florida, Tampa, Florida, USA

    Nataša Jonoska

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Alechina, N., Logan, B. (2016). Verifying Systems of Resource-Bounded Agents. In: Beckmann, A., Bienvenu, L., Jonoska, N. (eds) Pursuit of the Universal. CiE 2016. Lecture Notes in Computer Science(), vol 9709. Springer, Cham. https://doi.org/10.1007/978-3-319-40189-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40189-8_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40188-1

  • Online ISBN: 978-3-319-40189-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation