No Cover Image

Journal article 549 views 53 downloads

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

Natasha Alechina Orcid Logo, Nils Bulling, Brian Logan Orcid Logo, Hoang Nguyen Orcid Logo

Artificial Intelligence, Volume: 245, Pages: 56 - 85

Swansea University Author: Hoang Nguyen Orcid Logo

  • 61980.pdf

    PDF | Version of Record

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

    Download (1.13MB)

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

Full description

Published in: Artificial Intelligence
ISSN: 0004-3702
Published: Elsevier BV 2017
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa61980
Tags: Add Tag
No Tags, Be the first to tag this record!
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
College: Faculty of Science and Engineering
Start Page: 56
End Page: 85