The virtues of idleness: A decidable fragment of resource agent logic

N. Alechina, N. Bulling, B. Logan, Hoang Nga Nguyen

    Research output: Contribution to journalArticlepeer-review

    13 Citations (Scopus)
    58 Downloads (Pure)


    Alternating Time Temporal Logic (ATL) is widely used for the verification of multi-agent systems. We consider Resource Agent Logic (RAL), which extends ATL to allow the verification of properties of systems where agents act under resource constraints. The model checking problem for RAL with unbounded production and consumption of resources is known to be undecidable. We review existing (un)decidability results for fragments of RAL, tighten some existing undecidability results, and identify several aspects which affect decidability of model checking. One of these aspects is the availability of a ‘do nothing’, or idle action, which does not produce or consume resources. Analysis of undecidability results allows us to identify a significant new fragment of RAL for which model checking is decidable.
    Original languageEnglish
    Pages (from-to)56-85
    JournalArtificial Intelligence
    Issue numberApril 2017
    Publication statusPublished - 4 Jan 2017

    Bibliographical note

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


    • Strategy logics
    • Resource constraints
    • Model checking


    Dive into the research topics of 'The virtues of idleness: A decidable fragment of resource agent logic'. Together they form a unique fingerprint.

    Cite this