Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources

Natasha Alechina, Brian Logan, Hoang Nga Nguyen, Franco Raimondi

    Research output: Contribution to journalArticle

    10 Citations (Scopus)
    20 Downloads (Pure)

    Abstract

    Several logics for expressing coalitional ability under resource bounds have been proposed andstudied in the literature. Previous work has shown that if only consumption of resources isconsidered or the total amount of resources produced or consumed on any path in the systemis 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 andconsumption, only some undecidability results are known. In this paper, we show that the modelcheckingproblem for RB-ATL with unbounded production and consumption of resources isdecidable but EXPSPACE-hard. We also investigate some tractable cases and provide a detailedcomparison to a variant of the resource logic RAL, together with new complexity results.

    Publisher Statement: This is an open access article under the CC BY license
    Original languageEnglish
    Pages (from-to)126-144
    Number of pages19
    JournalJournal of Computer and System Sciences
    Volume88
    Early online date4 Apr 2017
    DOIs
    Publication statusPublished - Sep 2017

    Bibliographical note

    This is an open access article under the CC BY license

    Keywords

    • model-checking
    • resources
    • coalitional ability
    • verification of multi-agent systems

    Fingerprint Dive into the research topics of 'Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources'. Together they form a unique fingerprint.

    Cite this