The virtues of idleness: a decidable fragment of resource agent logic
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 unbounde...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Published: |
Elsevier
2017
|
| Online Access: | https://eprints.nottingham.ac.uk/39849/ |
| _version_ | 1848795928060755968 |
|---|---|
| author | Alechina, Natasha Bulling, Nils Logan, Brian Nguyen, Hoang Nga |
| author_facet | Alechina, Natasha Bulling, Nils Logan, Brian Nguyen, Hoang Nga |
| author_sort | Alechina, Natasha |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T19:39:52Z |
| format | Article |
| id | nottingham-39849 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:39:52Z |
| publishDate | 2017 |
| publisher | Elsevier |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-398492020-05-04T18:31:43Z https://eprints.nottingham.ac.uk/39849/ The virtues of idleness: a decidable fragment of resource agent logic Alechina, Natasha Bulling, Nils Logan, Brian Nguyen, Hoang Nga 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. Elsevier 2017-01-04 Article PeerReviewed Alechina, Natasha, Bulling, Nils, Logan, Brian and Nguyen, Hoang Nga (2017) The virtues of idleness: a decidable fragment of resource agent logic. Artificial Intelligence . ISSN 0004-3702 http://www.sciencedirect.com/science/article/pii/S0004370217300012 doi:10.1016/j.artint.2016.12.005 doi:10.1016/j.artint.2016.12.005 |
| spellingShingle | Alechina, Natasha Bulling, Nils Logan, Brian Nguyen, Hoang Nga The virtues of idleness: a decidable fragment of resource agent logic |
| title | The virtues of idleness: a decidable fragment of resource agent logic |
| title_full | The virtues of idleness: a decidable fragment of resource agent logic |
| title_fullStr | The virtues of idleness: a decidable fragment of resource agent logic |
| title_full_unstemmed | The virtues of idleness: a decidable fragment of resource agent logic |
| title_short | The virtues of idleness: a decidable fragment of resource agent logic |
| title_sort | virtues of idleness: a decidable fragment of resource agent logic |
| url | https://eprints.nottingham.ac.uk/39849/ https://eprints.nottingham.ac.uk/39849/ https://eprints.nottingham.ac.uk/39849/ |