No Cover Image

Journal article 467 views 30 downloads

Model-checking for Resource-Bounded ATL with production and consumption of resources

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

Journal of Computer and System Sciences, Volume: 88, Pages: 126 - 144

Swansea University Author: Hoang Nguyen Orcid Logo

  • 61979.pdf

    PDF | Version of Record

    © 2017 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license

    Download (633.3KB)

Check full text

DOI (Published version): 10.1016/j.jcss.2017.03.008

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: Journal of Computer and System Sciences
ISSN: 0022-0000
Published: Elsevier BV 2017
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa61979
Tags: Add Tag
No Tags, Be the first to tag this record!
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 but EXPSPACE-hard. We also investigate some tractable cases and provide a detailed comparison to a variant of the resource logic RAL, together with new complexity results.
Keywords: Model-checking; Resources; Coalitional ability; Verification of multi-agent systems
College: Faculty of Science and Engineering
Start Page: 126
End Page: 144

Similar Items