No Cover Image

Journal article 467 views 30 downloads

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

Natasha Alechina, Brian Logan, Hoang Nguyen Orcid Logo, Franco Raimondi

Journal of Computer and System Sciences, Volume: 88, Pages: 126 - 144

Swansea University Author: Hoang Nguyen Orcid Logo

  • 61979.pdf

    PDF | Version of Record

    © 2017 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license

    Download (633.3KB)

Check full text

DOI (Published version): 10.1016/j.jcss.2017.03.008

Abstract

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

Full description

Published in: Journal of Computer and System Sciences
ISSN: 0022-0000
Published: Elsevier BV 2017
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa61979
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2022-12-15T16:15:02Z
last_indexed 2023-01-13T19:23:07Z
id cronfa61979
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2022-12-15T16:59:33.7166477</datestamp><bib-version>v2</bib-version><id>61979</id><entry>2022-11-22</entry><title>Model-checking for Resource-Bounded ATL with production and consumption of resources</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>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.</abstract><type>Journal Article</type><journal>Journal of Computer and System Sciences</journal><volume>88</volume><journalNumber/><paginationStart>126</paginationStart><paginationEnd>144</paginationEnd><publisher>Elsevier BV</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>0022-0000</issnPrint><issnElectronic/><keywords>Model-checking; Resources; Coalitional ability; Verification of multi-agent systems</keywords><publishedDay>1</publishedDay><publishedMonth>9</publishedMonth><publishedYear>2017</publishedYear><publishedDate>2017-09-01</publishedDate><doi>10.1016/j.jcss.2017.03.008</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:59:33.7166477</lastEdited><Created>2022-11-22T12:11:06.3861135</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><order>1</order></author><author><firstname>Brian</firstname><surname>Logan</surname><order>2</order></author><author><firstname>Hoang</firstname><surname>Nguyen</surname><orcid>0000-0003-0260-1697</orcid><order>3</order></author><author><firstname>Franco</firstname><surname>Raimondi</surname><order>4</order></author></authors><documents><document><filename>61979__26093__ca5183d99a8044d69c6d34379788e3c5.pdf</filename><originalFilename>61979.pdf</originalFilename><uploaded>2022-12-15T16:15:27.9004107</uploaded><type>Output</type><contentLength>648497</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>&#xA9; 2017 The Authors. Published by Elsevier Inc. 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:59:33.7166477 v2 61979 2022-11-22 Model-checking for Resource-Bounded ATL with production and consumption of resources cb24d5c5080534dc5b5e3390f24dd422 0000-0003-0260-1697 Hoang Nguyen Hoang Nguyen true false 2022-11-22 SCS 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. Journal Article Journal of Computer and System Sciences 88 126 144 Elsevier BV 0022-0000 Model-checking; Resources; Coalitional ability; Verification of multi-agent systems 1 9 2017 2017-09-01 10.1016/j.jcss.2017.03.008 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2022-12-15T16:59:33.7166477 2022-11-22T12:11:06.3861135 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Natasha Alechina 1 Brian Logan 2 Hoang Nguyen 0000-0003-0260-1697 3 Franco Raimondi 4 61979__26093__ca5183d99a8044d69c6d34379788e3c5.pdf 61979.pdf 2022-12-15T16:15:27.9004107 Output 648497 application/pdf Version of Record true © 2017 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license true eng http://creativecommons.org/licenses/by/4.0/
title Model-checking for Resource-Bounded ATL with production and consumption of resources
spellingShingle Model-checking for Resource-Bounded ATL with production and consumption of resources
Hoang Nguyen
title_short 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_sort Model-checking for Resource-Bounded ATL with production and consumption of resources
author_id_str_mv cb24d5c5080534dc5b5e3390f24dd422
author_id_fullname_str_mv cb24d5c5080534dc5b5e3390f24dd422_***_Hoang Nguyen
author Hoang Nguyen
author2 Natasha Alechina
Brian Logan
Hoang Nguyen
Franco Raimondi
format Journal article
container_title Journal of Computer and System Sciences
container_volume 88
container_start_page 126
publishDate 2017
institution Swansea University
issn 0022-0000
doi_str_mv 10.1016/j.jcss.2017.03.008
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 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.
published_date 2017-09-01T04:21:14Z
_version_ 1763754402839003136
score 11.013148

Similar Items