Formal Modelling and Verification of Probabilistic Resource Bounded Agents

Hoang Nga Nguyen; Rakib Abdur

doi:10.1007/s10849-023-09405-1

Formal Modelling and Verification of Probabilistic Resource Bounded Agents

Hoang Nga Nguyen, Rakib Abdur

Centre for Future Transport and Cities

Swansea University

Research output: Contribution to journal › Article › peer-review

70 Downloads (Pure)

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.

Original language	English
Pages (from-to)	829-859
Number of pages	31
Journal	The Journal of Logic, Language and Information
Volume	32
Issue number	5
Early online date	15 Nov 2023
DOIs	https://doi.org/10.1007/s10849-023-09405-1
Publication status	Published - Dec 2023

Bibliographical note

This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.

Keywords

Logic of Resources
Alternating-time Temporal Logic
Probabilistic Logic
Markov Decision Process
Multi-agent Systems

Access to Document

10.1007/s10849-023-09405-1Licence: CC BY

Post-PrintAccepted author manuscript, 816 KB
PublishedFinal published version, 1.19 MBLicence: CC BY

Cite this

@article{2f8d6504a6334e6f8ecbc28bc0c2cf82,

title = "Formal Modelling and Verification of Probabilistic Resource Bounded Agents",

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

keywords = "Logic of Resources, Alternating-time Temporal Logic, Probabilistic Logic, Markov Decision Process, Multi-agent Systems",

author = "Nguyen, {Hoang Nga} and Rakib Abdur",

note = "This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article{\textquoteright}s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article{\textquoteright}s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.",

year = "2023",

month = dec,

doi = "10.1007/s10849-023-09405-1",

language = "English",

volume = "32",

pages = "829--859",

journal = "The Journal of Logic, Language and Information",

issn = "1572-9583",

publisher = "Springer ",

number = "5",

}

TY - JOUR

T1 - Formal Modelling and Verification of Probabilistic Resource Bounded Agents

AU - Nguyen, Hoang Nga

AU - Abdur, Rakib

N1 - This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.

PY - 2023/12

Y1 - 2023/12

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

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

KW - Logic of Resources

KW - Alternating-time Temporal Logic

KW - Probabilistic Logic

KW - Markov Decision Process

KW - Multi-agent Systems

UR - http://www.scopus.com/inward/record.url?scp=85176794900&partnerID=8YFLogxK

U2 - 10.1007/s10849-023-09405-1

DO - 10.1007/s10849-023-09405-1

M3 - Article

SN - 1572-9583

VL - 32

SP - 829

EP - 859

JO - The Journal of Logic, Language and Information

JF - The Journal of Logic, Language and Information

IS - 5

ER -

Formal Modelling and Verification of Probabilistic Resource Bounded Agents

Abstract

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this