No Cover Image

Conference Paper/Proceeding/Abstract 619 views

Symbolic model-checking for single resource RB+-ATL

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

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)

Swansea University Author: Hoang Nguyen Orcid Logo

Abstract

RB+-ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The model-checking problem for RB+-ATL is known to be decidable. However the only available model-checking algorithm for RB+-ATL uses a forward search of the state space,...

Full description

Published in: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)
Published: 2015
Online Access: http://ijcai.org/Proceedings/15/Papers/155.pdf
URI: https://cronfa.swan.ac.uk/Record/cronfa61992
first_indexed 2022-12-15T17:02:06Z
last_indexed 2023-01-13T19:23:08Z
id cronfa61992
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2022-12-15T17:02:08.2447791</datestamp><bib-version>v2</bib-version><id>61992</id><entry>2022-11-22</entry><title>Symbolic model-checking for single resource RB+-ATL</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>MACS</deptcode><abstract>RB+-ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The model-checking problem for RB+-ATL is known to be decidable. However the only available model-checking algorithm for RB+-ATL uses a forward search of the state space, and hence does not have an efficient symbolic implementation. In this paper, we consider a fragment of RB+-ATL, 1RB+-ATL, that allows only one resource type. We give a symbolic model-checking algorithm for this fragment of RB+-ATL, and evaluate the performance of an MCMAS-based implementation of the algorithm on an example problem that can be scaled to large state spaces.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>1</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2015</publishedYear><publishedDate>2015-01-01</publishedDate><doi/><url>http://ijcai.org/Proceedings/15/Papers/155.pdf</url><notes>http://ijcai.org/Proceedings/15/Papers/155.pdf</notes><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2022-12-15T17:02:08.2447791</lastEdited><Created>2022-11-22T12:17:07.8620958</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/><OutputDurs/></rfc1807>
spelling 2022-12-15T17:02:08.2447791 v2 61992 2022-11-22 Symbolic model-checking for single resource RB+-ATL cb24d5c5080534dc5b5e3390f24dd422 0000-0003-0260-1697 Hoang Nguyen Hoang Nguyen true false 2022-11-22 MACS RB+-ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The model-checking problem for RB+-ATL is known to be decidable. However the only available model-checking algorithm for RB+-ATL uses a forward search of the state space, and hence does not have an efficient symbolic implementation. In this paper, we consider a fragment of RB+-ATL, 1RB+-ATL, that allows only one resource type. We give a symbolic model-checking algorithm for this fragment of RB+-ATL, and evaluate the performance of an MCMAS-based implementation of the algorithm on an example problem that can be scaled to large state spaces. Conference Paper/Proceeding/Abstract Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015) 1 1 2015 2015-01-01 http://ijcai.org/Proceedings/15/Papers/155.pdf http://ijcai.org/Proceedings/15/Papers/155.pdf COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2022-12-15T17:02:08.2447791 2022-11-22T12:17:07.8620958 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
title Symbolic model-checking for single resource RB+-ATL
spellingShingle Symbolic model-checking for single resource RB+-ATL
Hoang Nguyen
title_short Symbolic model-checking for single resource RB+-ATL
title_full Symbolic model-checking for single resource RB+-ATL
title_fullStr Symbolic model-checking for single resource RB+-ATL
title_full_unstemmed Symbolic model-checking for single resource RB+-ATL
title_sort Symbolic model-checking for single resource RB+-ATL
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 Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)
publishDate 2015
institution Swansea University
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
url http://ijcai.org/Proceedings/15/Papers/155.pdf
document_store_str 0
active_str 0
description RB+-ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The model-checking problem for RB+-ATL is known to be decidable. However the only available model-checking algorithm for RB+-ATL uses a forward search of the state space, and hence does not have an efficient symbolic implementation. In this paper, we consider a fragment of RB+-ATL, 1RB+-ATL, that allows only one resource type. We give a symbolic model-checking algorithm for this fragment of RB+-ATL, and evaluate the performance of an MCMAS-based implementation of the algorithm on an example problem that can be scaled to large state spaces.
published_date 2015-01-01T20:30:24Z
_version_ 1822073001507553280
score 11.048302

Similar Items