Skip to main content

Research Repository

See what's under the surface

Advanced Search

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

Alechina, Natasha; Bulling, Nils; Logan, Brian; Nguyen, Hoang Nga

Authors

Natasha Alechina

Nils Bulling

Brian Logan

Hoang Nga Nguyen



Abstract

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.

Journal Article Type Article
Journal Artificial Intelligence
Print ISSN 0004-3702
Electronic ISSN 0004-3702
Publisher Elsevier
Peer Reviewed Peer Reviewed
APA6 Citation Alechina, N., Bulling, N., Logan, B., & Nguyen, H. N. (in press). The virtues of idleness: a decidable fragment of resource agent logic. Artificial Intelligence, https://doi.org/10.1016/j.artint.2016.12.005
DOI https://doi.org/10.1016/j.artint.2016.12.005
Publisher URL http://www.sciencedirect.com/science/article/pii/S0004370217300012
Copyright Statement Copyright information regarding this work can be found at the following address: http://creativecommons.org/licenses/by/4.0

Files

author-version.pdf (592 Kb)
PDF

Copyright Statement
Copyright information regarding this work can be found at the following address: http://creativecommons.org/licenses/by/4.0





You might also like



Downloadable Citations

;