The virtues of idleness: a decidable fragment of resource agent logic

Article English OPEN
Alechina, Natasha ; Bulling, Nils ; Logan, Brian ; Nguyen, Hoang Nga (2017)
  • Publisher: Elsevier
  • Journal: Artificial Intelligence, volume 245, pages 56-85 (issn: 0004-3702)
  • Related identifiers: doi: 10.1016/j.artint.2016.12.005
  • Subject: Artificial Intelligence
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES

Alternating Time Temporal Logic (ATL) is widely used for the verification of multi-agent systems. We consider Resource Agent Logic (RAL), which extends ATL to allow the verification of properties of systems where agents act under resource constraints. The model checking problem for RAL with unbounded production and consumption of resources is known to be undecidable. We review existing (un)decidability results for fragments of RAL, tighten some existing undecidability results, and identify several aspects which affect decidability of model checking. One of these aspects is the availability of a ‘do nothing’, or idle action, which does not produce or consume resources. Analysis of undecidability results allows us to identify a significant new fragment of RAL for which model checking is decidable.
  • References (35)
    35 references, page 1 of 4

    [1] N. Alechina, B. Logan, H. N. Nguyen, A. Rakib, A logic for coalitions with bounded resources, in: C. Boutilier (Ed.), Proceedings of the Twenty First International Joint Conference on Artificial Intelligence (IJCAI 2009), Vol. 2, AAAI Press, 2009, pp. 659-664.

    [2] N. Bulling, B. Farwer, On the (un-)decidability of model checking resource-bounded agents, in: H. Coelho, R. Studer, M. Wooldridge (Eds.), Proceedings of the 19th European Conference on Artificial Intelligence (ECAI 2010), IOS Press, 2010, pp. 567-572.

    [3] N. Alechina, B. Logan, H. N. Nguyen, A. Rakib, Resource-bounded alternating-time temporal logic, in: W. van der Hoek, G. Kaminka, Y. Lespe´rance, M. Luck, S. Sen (Eds.), Proceedings of the Ninth International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), IFAAMAS, 2010, pp. 481-488.

    [4] D. Della Monica, M. Napoli, M. Parente, Model checking coalitional games in shortage resource scenarios, in: G. Puppis, T. Villa (Eds.), Proceedings of the Fourth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2013), Vol. 119 of Electronic Proceedings in Theoretical Computer Science, 2013, pp. 240-255.

    [5] N. Bulling, V. Goranko, How to be both rich and happy: Combining quantitative and qualitative strategic reasoning about multi-player games (extended abstract), in: F. Mogavero, A. Murano, M. Y. Vardi (Eds.), Proceedings of the 1st International Workshop on Strategic Reasoning (SR 2013), Vol. 112 of Electronic Proceedings in Theoretical Computer Science, 2013, pp. 33-41.

    [6] N. Alechina, B. Logan, H. N. Nguyen, F. Raimondi, Decidable model-checking for a resource logic with production of resources, in: T. Schaub, G. Friedrich, B. O'Sullivan (Eds.), Proceedings of the 21st European Conference on Artificial Intelligence (ECAI-2014), IOS Press, 2014, pp. 9-14.

    [7] N. Alechina, N. Bulling, B. Logan, H. N. Nguyen, On the boundary of (un)decidability: Decidable model-checking for a fragment of resource agent logic, in: Q. Yang (Ed.), Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), AAAI Press, 2015, pp. 1494-1501.

    [8] N. Alechina, B. Logan, H. N. Nguyen, F. Raimondi, Model-checking for resource-bounded ATL with production and consumption of resources, Journal of Computer and System Sciences(in press).

    [9] N. Alechina, B. Logan, H. N. Nguyen, F. Raimondi, Model-checking for Resource-Bounded ATL with production and consumption of resources, Tech. rep., ArXiv e-prints 1504.06766 (2015).

    [10] M. Ghallab, D. S. Nau, P. Traverso, Automated Planning: Theory and Practice, Morgan Kaufmann, 2004.

  • Metrics
    No metrics available
Share - Bookmark