No Cover Image

Journal article 125 views 24 downloads

Formal Modelling and Verification of Probabilistic Resource Bounded Agents

Hoang Nguyen Orcid Logo, Abdur Rakib Orcid Logo

Journal of Logic, Language and Information, Volume: 32, Issue: 5, Pages: 829 - 859

Swansea University Author: Hoang Nguyen Orcid Logo

  • 64995.VOR.pdf

    PDF | Version of Record

    © The Author(s) 2023. Distributed under the terms of a Creative Commons Attribution 4.0 International License (CC BY 4.0).

    Download (878.21KB)

Check full text

DOI (Published version): 10.1007/s10849-023-09405-1

Abstract

Many problems in Multi-Agent Systems (MASs) research are formulated in terms of the abilities of a coalition of agents. Existing approaches to reasoning about coalitional ability are usually focused on games or transition systems, which are described in terms of states and actions. Such approaches h...

Full description

Published in: Journal of Logic, Language and Information
ISSN: 0925-8531 1572-9583
Published: Springer Science and Business Media LLC 2023
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa64995
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2023-11-20T08:52:47Z
last_indexed 2023-11-20T08:52:47Z
id cronfa64995
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>64995</id><entry>2023-11-15</entry><title>Formal Modelling and Verification of Probabilistic Resource Bounded Agents</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>2023-11-15</date><deptcode>SCS</deptcode><abstract>Many problems in Multi-Agent Systems (MASs) research are formulated in terms of the abilities of a coalition of agents. Existing approaches to reasoning about coalitional ability are usually focused on games or transition systems, which are described in terms of states and actions. Such approaches however often neglect a key feature of multi-agent systems, namely that the actions of the agents require resources. In this paper, we describe a logic for reasoning about coalitional ability under resource constraints in the probabilistic setting. We extend Resource-bounded Alternating-time Temporal Logic (RB-ATL) with probabilistic reasoning and provide a standard algorithm for the model-checking problem of the resulting logic Probabilistic resource-bounded ATL (pRB-ATL). We implement model-checking algorithms and present experimental results using simple multi-agent model-checking problems of increasing complexity.</abstract><type>Journal Article</type><journal>Journal of Logic, Language and Information</journal><volume>32</volume><journalNumber>5</journalNumber><paginationStart>829</paginationStart><paginationEnd>859</paginationEnd><publisher>Springer Science and Business Media LLC</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>0925-8531</issnPrint><issnElectronic>1572-9583</issnElectronic><keywords>Logic of resources, Alternating-time temporal logic, Probabilistic logic, Markov decision process, Multi-agent systems</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-12-31</publishedDate><doi>10.1007/s10849-023-09405-1</doi><url>http://dx.doi.org/10.1007/s10849-023-09405-1</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>2023-12-12T17:01:42.4360765</lastEdited><Created>2023-11-15T23:25:42.2039805</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>Hoang</firstname><surname>Nguyen</surname><orcid>0000-0003-0260-1697</orcid><order>1</order></author><author><firstname>Abdur</firstname><surname>Rakib</surname><orcid>0000-0001-5430-450x</orcid><order>2</order></author></authors><documents><document><filename>64995__29251__d2f1af5c58624529966e818872975159.pdf</filename><originalFilename>64995.VOR.pdf</originalFilename><uploaded>2023-12-12T16:58:24.7165251</uploaded><type>Output</type><contentLength>899289</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>© The Author(s) 2023. Distributed under the terms of a Creative Commons Attribution 4.0 International License (CC BY 4.0).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling v2 64995 2023-11-15 Formal Modelling and Verification of Probabilistic Resource Bounded Agents cb24d5c5080534dc5b5e3390f24dd422 0000-0003-0260-1697 Hoang Nguyen Hoang Nguyen true false 2023-11-15 SCS Many problems in Multi-Agent Systems (MASs) research are formulated in terms of the abilities of a coalition of agents. Existing approaches to reasoning about coalitional ability are usually focused on games or transition systems, which are described in terms of states and actions. Such approaches however often neglect a key feature of multi-agent systems, namely that the actions of the agents require resources. In this paper, we describe a logic for reasoning about coalitional ability under resource constraints in the probabilistic setting. We extend Resource-bounded Alternating-time Temporal Logic (RB-ATL) with probabilistic reasoning and provide a standard algorithm for the model-checking problem of the resulting logic Probabilistic resource-bounded ATL (pRB-ATL). We implement model-checking algorithms and present experimental results using simple multi-agent model-checking problems of increasing complexity. Journal Article Journal of Logic, Language and Information 32 5 829 859 Springer Science and Business Media LLC 0925-8531 1572-9583 Logic of resources, Alternating-time temporal logic, Probabilistic logic, Markov decision process, Multi-agent systems 31 12 2023 2023-12-31 10.1007/s10849-023-09405-1 http://dx.doi.org/10.1007/s10849-023-09405-1 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2023-12-12T17:01:42.4360765 2023-11-15T23:25:42.2039805 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Hoang Nguyen 0000-0003-0260-1697 1 Abdur Rakib 0000-0001-5430-450x 2 64995__29251__d2f1af5c58624529966e818872975159.pdf 64995.VOR.pdf 2023-12-12T16:58:24.7165251 Output 899289 application/pdf Version of Record true © The Author(s) 2023. Distributed under the terms of a Creative Commons Attribution 4.0 International License (CC BY 4.0). true eng https://creativecommons.org/licenses/by/4.0/
title Formal Modelling and Verification of Probabilistic Resource Bounded Agents
spellingShingle Formal Modelling and Verification of Probabilistic Resource Bounded Agents
Hoang Nguyen
title_short Formal Modelling and Verification of Probabilistic Resource Bounded Agents
title_full Formal Modelling and Verification of Probabilistic Resource Bounded Agents
title_fullStr Formal Modelling and Verification of Probabilistic Resource Bounded Agents
title_full_unstemmed Formal Modelling and Verification of Probabilistic Resource Bounded Agents
title_sort Formal Modelling and Verification of Probabilistic Resource Bounded Agents
author_id_str_mv cb24d5c5080534dc5b5e3390f24dd422
author_id_fullname_str_mv cb24d5c5080534dc5b5e3390f24dd422_***_Hoang Nguyen
author Hoang Nguyen
author2 Hoang Nguyen
Abdur Rakib
format Journal article
container_title Journal of Logic, Language and Information
container_volume 32
container_issue 5
container_start_page 829
publishDate 2023
institution Swansea University
issn 0925-8531
1572-9583
doi_str_mv 10.1007/s10849-023-09405-1
publisher Springer Science and Business Media LLC
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://dx.doi.org/10.1007/s10849-023-09405-1
document_store_str 1
active_str 0
description Many problems in Multi-Agent Systems (MASs) research are formulated in terms of the abilities of a coalition of agents. Existing approaches to reasoning about coalitional ability are usually focused on games or transition systems, which are described in terms of states and actions. Such approaches however often neglect a key feature of multi-agent systems, namely that the actions of the agents require resources. In this paper, we describe a logic for reasoning about coalitional ability under resource constraints in the probabilistic setting. We extend Resource-bounded Alternating-time Temporal Logic (RB-ATL) with probabilistic reasoning and provide a standard algorithm for the model-checking problem of the resulting logic Probabilistic resource-bounded ATL (pRB-ATL). We implement model-checking algorithms and present experimental results using simple multi-agent model-checking problems of increasing complexity.
published_date 2023-12-31T17:01:43Z
_version_ 1785096310369550336
score 11.013148

Similar Items