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!
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
College: Faculty of Science and Engineering
Issue: 5
Start Page: 829
End Page: 859

Similar Items