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

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

doi:10.1016/j.artint.2016.12.005

Journal article 596 views 58 downloads

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

Natasha Alechina

, Nils Bulling, Brian Logan

, Hoang Nguyen

Artificial Intelligence, Volume: 245, Pages: 56 - 85

Swansea University Author: Hoang Nguyen

PDF | Version of Record

© 2017 The Authors. This is an open access article under the CC BY license
Download (1.13MB)

Check full text

DOI (Published version): 10.1016/j.artint.2016.12.005

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 unbounde...

Full description

Published in:	Artificial Intelligence
ISSN:	0004-3702
Published:	Elsevier BV 2017
Online Access:	Check full text
URI:	https://cronfa.swan.ac.uk/Record/cronfa61980
Tags:	Add Tag No Tags, Be the first to tag this record!

first_indexed	2022-12-15T16:11:02Z
last_indexed	2023-01-13T19:23:07Z
id	cronfa61980
recordtype	SURis
fullrecord	<?xml version="1.0"?><rfc1807><datestamp>2022-12-15T16:12:44.7971633</datestamp><bib-version>v2</bib-version><id>61980</id><entry>2022-11-22</entry><title>The virtues of idleness: A decidable fragment of resource agent logic</title><swanseaauthors><author><sid>cb24d5c5080534dc5b5e3390f24dd422</sid><ORCID>0000-0003-0260-1697</ORCID><firstname>Hoang</firstname><surname>Nguyen</surname><name>Hoang Nguyen</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2022-11-22</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Artificial Intelligence</journal><volume>245</volume><journalNumber/><paginationStart>56</paginationStart><paginationEnd>85</paginationEnd><publisher>Elsevier BV</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>0004-3702</issnPrint><issnElectronic/><keywords>Strategy logics; Resource constraints; Model checking</keywords><publishedDay>1</publishedDay><publishedMonth>4</publishedMonth><publishedYear>2017</publishedYear><publishedDate>2017-04-01</publishedDate><doi>10.1016/j.artint.2016.12.005</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2022-12-15T16:12:44.7971633</lastEdited><Created>2022-11-22T12:11:15.1837791</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Natasha</firstname><surname>Alechina</surname><orcid>0000-0003-3306-9891</orcid><order>1</order></author><author><firstname>Nils</firstname><surname>Bulling</surname><order>2</order></author><author><firstname>Brian</firstname><surname>Logan</surname><orcid>0000-0003-0648-7107</orcid><order>3</order></author><author><firstname>Hoang</firstname><surname>Nguyen</surname><orcid>0000-0003-0260-1697</orcid><order>4</order></author></authors><documents><document><filename>61980__26092__8b495e53340c434e8ecffaccbc315176.pdf</filename><originalFilename>61980.pdf</originalFilename><uploaded>2022-12-15T16:11:30.5952990</uploaded><type>Output</type><contentLength>1185614</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>© 2017 The Authors. This is an open access article under the CC BY license</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>http://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling	2022-12-15T16:12:44.7971633 v2 61980 2022-11-22 The virtues of idleness: A decidable fragment of resource agent logic cb24d5c5080534dc5b5e3390f24dd422 0000-0003-0260-1697 Hoang Nguyen Hoang Nguyen true false 2022-11-22 SCS 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 Artificial Intelligence 245 56 85 Elsevier BV 0004-3702 Strategy logics; Resource constraints; Model checking 1 4 2017 2017-04-01 10.1016/j.artint.2016.12.005 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2022-12-15T16:12:44.7971633 2022-11-22T12:11:15.1837791 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Natasha Alechina 0000-0003-3306-9891 1 Nils Bulling 2 Brian Logan 0000-0003-0648-7107 3 Hoang Nguyen 0000-0003-0260-1697 4 61980__26092__8b495e53340c434e8ecffaccbc315176.pdf 61980.pdf 2022-12-15T16:11:30.5952990 Output 1185614 application/pdf Version of Record true © 2017 The Authors. This is an open access article under the CC BY license true eng http://creativecommons.org/licenses/by/4.0/
title	The virtues of idleness: A decidable fragment of resource agent logic
spellingShingle	The virtues of idleness: A decidable fragment of resource agent logic Hoang Nguyen
title_short	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_sort	The virtues of idleness: A decidable fragment of resource agent logic
author_id_str_mv	cb24d5c5080534dc5b5e3390f24dd422
author_id_fullname_str_mv	cb24d5c5080534dc5b5e3390f24dd422_***_Hoang Nguyen
author	Hoang Nguyen
author2	Natasha Alechina Nils Bulling Brian Logan Hoang Nguyen
format	Journal article
container_title	Artificial Intelligence
container_volume	245
container_start_page	56
publishDate	2017
institution	Swansea University
issn	0004-3702
doi_str_mv	10.1016/j.artint.2016.12.005
publisher	Elsevier BV
college_str	Faculty of Science and Engineering
hierarchytype
hierarchy_top_id	facultyofscienceandengineering
hierarchy_top_title	Faculty of Science and Engineering
hierarchy_parent_id	facultyofscienceandengineering
hierarchy_parent_title	Faculty of Science and Engineering
department_str	School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str	1
active_str	0
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.
published_date	2017-04-01T04:21:14Z
_version_	1763754402960637952
score	11.037603

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

Similar Items