Model-checking for resource-bounded ATL with production and consumption of resources
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 m...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Published: |
Elsevier
2017
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/37147/ |
| _version_ | 1848795401277145088 |
|---|---|
| author | Alechina, Natasha Logan, Brian Nguyen, Hoang Nga Raimondi, Franco |
| author_facet | Alechina, Natasha Logan, Brian Nguyen, Hoang Nga Raimondi, Franco |
| author_sort | Alechina, Natasha |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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 modelchecking 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. |
| first_indexed | 2025-11-14T19:31:30Z |
| format | Article |
| id | nottingham-37147 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:31:30Z |
| publishDate | 2017 |
| publisher | Elsevier |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-371472020-05-04T19:55:31Z https://eprints.nottingham.ac.uk/37147/ Model-checking for resource-bounded ATL with production and consumption of resources Alechina, Natasha Logan, Brian Nguyen, Hoang Nga Raimondi, Franco 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 modelchecking 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. Elsevier 2017-09 Article PeerReviewed Alechina, Natasha, Logan, Brian, Nguyen, Hoang Nga and Raimondi, Franco (2017) Model-checking for resource-bounded ATL with production and consumption of resources. Journal of Computer and System Sciences, 88 . pp. 126-144. ISSN 1090-2724 model-checking resources coalitional ability verification of multi-agent systems http://www.sciencedirect.com/science/article/pii/S0022000017300363 doi:10.1016/j.jcss.2017.03.008 doi:10.1016/j.jcss.2017.03.008 |
| spellingShingle | model-checking resources coalitional ability verification of multi-agent systems Alechina, Natasha Logan, Brian Nguyen, Hoang Nga Raimondi, Franco Model-checking for resource-bounded ATL with production and consumption of resources |
| title | Model-checking for resource-bounded ATL with production and
consumption of resources |
| title_full | Model-checking for resource-bounded ATL with production and
consumption of resources |
| title_fullStr | Model-checking for resource-bounded ATL with production and
consumption of resources |
| title_full_unstemmed | Model-checking for resource-bounded ATL with production and
consumption of resources |
| title_short | Model-checking for resource-bounded ATL with production and
consumption of resources |
| title_sort | model-checking for resource-bounded atl with production and
consumption of resources |
| topic | model-checking resources coalitional ability verification of multi-agent systems |
| url | https://eprints.nottingham.ac.uk/37147/ https://eprints.nottingham.ac.uk/37147/ https://eprints.nottingham.ac.uk/37147/ |