Model-checking for Resource-Bounded ATL with production and consumption of resources

Alechina, Natasha; Logan, Brian; Nguyen, Hoang Nga; Raimondi, Franco

Abstract

© 2017 The Authors Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic (RB-ATL) is decidable. However, for coalition logics with unbounded resource production and consumption, only some undecidability results are known. In this paper, we show that the model-checking problem for RB-ATL with unbounded production and consumption of resources is decidable but EXPSPACE-hard. We also investigate some tractable cases and provide a detailed comparison to a variant of the resource logic RAL, together with new complexity results.

Citation

Alechina, N., Logan, B., Nguyen, H. N., & Raimondi, F. (2017). Model-checking for Resource-Bounded ATL with production and consumption of resources. Journal of Computer and System Sciences, 88, 126-144. https://doi.org/10.1016/j.jcss.2017.03.008

• Journal Article Type: Article
• Acceptance Date: Aug 19, 2016
• Online Publication Date: Apr 4, 2017
• Publication Date: 2017-09
• Deposit Date: Sep 26, 2016
• Publicly Available Date: Apr 4, 2017
• Journal: Journal of Computer and System Sciences
• Print ISSN: 0022-0000
• Electronic ISSN: 1090-2724
• Publisher: Elsevier
• Peer Reviewed: Peer Reviewed
• Volume: 88
• Pages: 126-144
• DOI: https://doi.org/10.1016/j.jcss.2017.03.008
• Keywords: model-checking, resources, coalitional ability, verification of multi-agent systems
• Public URL: https://nottingham-repository.worktribe.com/output/966494
• Publisher URL: http://www.sciencedirect.com/science/article/pii/S0022000017300363