Decidable model-checking for a resource logic with production of resources

Alechina, Natasha; Logan, Brian; Nguyen, Hoang; Raimondi, Franco

doi:10.3233/978-1-61499-419-0-9

Conference Paper/Proceeding/Abstract 16401 views 24 downloads

Decidable model-checking for a resource logic with production of resources

Natasha Alechina, Brian Logan, Hoang Nguyen

, Franco Raimondi

ECAI 2014 : 21st European Conference on Artificial Intelligence

Swansea University Author: Hoang Nguyen

PDF | Version of Record

© 2014 The Authors and IOS Press. This article is published online with Open Access by IOS Press and distributed under the terms of the Creative Commons Attribution Non-Commercial License
Download (259.44KB)

Check full text

DOI (Published version): 10.3233/978-1-61499-419-0-9

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:	ECAI 2014 : 21st European Conference on Artificial Intelligence
ISBN:	978-1-61499-418-3 978-1-61499-419-0
ISSN:	0922-6389 1879-8314
Published:	IOS Press 2014
Online Access:	Check full text
URI:	https://cronfa.swan.ac.uk/Record/cronfa61993
Tags:	Add Tag No Tags, Be the first to tag this record!

first_indexed	2022-12-07T10:32:30Z
last_indexed	2023-01-13T19:23:09Z
id	cronfa61993
recordtype	SURis
fullrecord	<?xml version="1.0"?><rfc1807><datestamp>2022-12-07T10:34:14.3690625</datestamp><bib-version>v2</bib-version><id>61993</id><entry>2022-11-22</entry><title>Decidable model-checking for a resource logic with production 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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>ECAI 2014 : 21st European Conference on Artificial Intelligence</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher>IOS Press</publisher><placeOfPublication/><isbnPrint>978-1-61499-418-3</isbnPrint><isbnElectronic>978-1-61499-419-0</isbnElectronic><issnPrint>0922-6389</issnPrint><issnElectronic>1879-8314</issnElectronic><keywords/><publishedDay>18</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-08-18</publishedDate><doi>10.3233/978-1-61499-419-0-9</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-07T10:34:14.3690625</lastEdited><Created>2022-11-22T12:17:38.5888904</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>61993__26025__e76b72fcfb0742a986590e838319e650.pdf</filename><originalFilename>61993.pdf</originalFilename><uploaded>2022-12-07T10:32:58.4736264</uploaded><type>Output</type><contentLength>265669</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>© 2014 The Authors and IOS Press. This article is published online with Open Access by IOS Press and distributed under the terms of the Creative Commons Attribution Non-Commercial License</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by-nc/3.0/deed.en_US</licence></document></documents><OutputDurs/></rfc1807>
spelling	2022-12-07T10:34:14.3690625 v2 61993 2022-11-22 Decidable model-checking for a resource logic with production 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. Conference Paper/Proceeding/Abstract ECAI 2014 : 21st European Conference on Artificial Intelligence IOS Press 978-1-61499-418-3 978-1-61499-419-0 0922-6389 1879-8314 18 8 2014 2014-08-18 10.3233/978-1-61499-419-0-9 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2022-12-07T10:34:14.3690625 2022-11-22T12:17:38.5888904 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 61993__26025__e76b72fcfb0742a986590e838319e650.pdf 61993.pdf 2022-12-07T10:32:58.4736264 Output 265669 application/pdf Version of Record true © 2014 The Authors and IOS Press. This article is published online with Open Access by IOS Press and distributed under the terms of the Creative Commons Attribution Non-Commercial License true eng https://creativecommons.org/licenses/by-nc/3.0/deed.en_US
title	Decidable model-checking for a resource logic with production of resources
spellingShingle	Decidable model-checking for a resource logic with production of resources Hoang Nguyen
title_short	Decidable model-checking for a resource logic with production of resources
title_full	Decidable model-checking for a resource logic with production of resources
title_fullStr	Decidable model-checking for a resource logic with production of resources
title_full_unstemmed	Decidable model-checking for a resource logic with production of resources
title_sort	Decidable model-checking for a resource logic with production 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	Conference Paper/Proceeding/Abstract
container_title	ECAI 2014 : 21st European Conference on Artificial Intelligence
publishDate	2014
institution	Swansea University
isbn	978-1-61499-418-3 978-1-61499-419-0
issn	0922-6389 1879-8314
doi_str_mv	10.3233/978-1-61499-419-0-9
publisher	IOS Press
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.
published_date	2014-08-18T04:21:15Z
_version_	1763754404404527104
score	11.012678

Decidable model-checking for a resource logic with production of resources

Similar Items