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

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

doi:10.1016/j.artint.2016.12.005

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

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

Research output: Contribution to journal › Article

9 Citations (Scopus)

36 Downloads (Pure)

Abstract

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 language	English
Pages (from-to)	56-85
Journal	Artificial Intelligence
Volume	245
Issue number	April 2017
DOIs	https://doi.org/10.1016/j.artint.2016.12.005
Publication status	Published - 4 Jan 2017

Bibliographical note

© 2017 The Authors. Published by Elsevier B.V. This is an open access article under the
CC BY license (http://creativecommons.org/licenses/by/4.0/).

Keywords

Strategy logics
Resource constraints
Model checking

Access to Document

10.1016/j.artint.2016.12.005

NguyencombFinal published version, 1.23 MB

Fingerprint 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

@article{9d816474485440859d927cf6d7f1091a,

title = "The virtues of idleness: A decidable fragment of resource agent logic",

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

keywords = "Strategy logics, Resource constraints, Model checking",

author = "N. Alechina and N. Bulling and B. Logan and Nguyen, {Hoang Nga}",

note = "{\circledC} 2017 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).",

year = "2017",

month = "1",

day = "4",

doi = "10.1016/j.artint.2016.12.005",

language = "English",

volume = "245",

pages = "56--85",

journal = "Artificial Intelligence",

issn = "0004-3702",

publisher = "Elsevier",

number = "April 2017",

}

TY - JOUR

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

AU - Alechina, N.

AU - Bulling, N.

AU - Logan, B.

AU - Nguyen, Hoang Nga

PY - 2017/1/4

Y1 - 2017/1/4

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

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

KW - Strategy logics

KW - Resource constraints

KW - Model checking

U2 - 10.1016/j.artint.2016.12.005

DO - 10.1016/j.artint.2016.12.005

M3 - Article

VL - 245

SP - 56

EP - 85

JO - Artificial Intelligence

JF - Artificial Intelligence

SN - 0004-3702

IS - April 2017

ER -