Alternating-time temporal logic with resource bounds

Hoang Nga Nguyen; N. Alechina; B. Logan; A. Rakib

doi:10.1093/logcom/exv034

Alternating-time temporal logic with resource bounds

Hoang Nga Nguyen, N. Alechina, B. Logan, A. Rakib

Research output: Contribution to journal › Article › peer-review

12 Citations (Scopus)

63 Downloads (Pure)

Abstract

Many problems in AI and multi-agent systems research are most naturally formulated in terms of the abilities of a coalition of agents. There exist several excellent logical tools for reasoning about coalitional ability. However, coalitional ability can be affected by the availability of resources, and there is no straightforward way of reasoning about resource requirements in logics such as Coalition Logic (CL) and Alternating-time Temporal Logic (ATL). In this article, we describe a logic for reasoning about coalitional ability under resource constraints. We extend ATL with costs of actions and hence of strategies. We give a complete and sound axiomatization of the resulting logic, Resource-Bounded ATL (RB-ATL) and a model-checking algorithm for it.

Original language	English
Pages (from-to)	631-663
Number of pages	33
Journal	Journal of Logic and Computation
Volume	28
Issue number	4
Early online date	12 Jun 2015
DOIs	https://doi.org/10.1093/logcom/exv034
Publication status	Published - 7 Jun 2018
Externally published	Yes

Bibliographical note

This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http://
creativecommons.org/licenses/by/4.0/), which permits unrestricted reuse, distribution, and reproduction in any medium, provided
the original work is properly cited.

Keywords

Strategic ability
resources
axiomatisation of RB-ATL

Access to Document

10.1093/logcom/exv034Licence: CC BY

PublishedFinal published version, 762 KBLicence: CC BY

Cite this

@article{304fd778eb604e0d8655cac237c525a1,

title = "Alternating-time temporal logic with resource bounds",

abstract = "Many problems in AI and multi-agent systems research are most naturally formulated in terms of the abilities of a coalition of agents. There exist several excellent logical tools for reasoning about coalitional ability. However, coalitional ability can be affected by the availability of resources, and there is no straightforward way of reasoning about resource requirements in logics such as Coalition Logic (CL) and Alternating-time Temporal Logic (ATL). In this article, we describe a logic for reasoning about coalitional ability under resource constraints. We extend ATL with costs of actions and hence of strategies. We give a complete and sound axiomatization of the resulting logic, Resource-Bounded ATL (RB-ATL) and a model-checking algorithm for it. ",

keywords = "Strategic ability, resources, axiomatisation of RB-ATL",

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

note = "This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http:// creativecommons.org/licenses/by/4.0/), which permits unrestricted reuse, distribution, and reproduction in any medium, provided the original work is properly cited.",

year = "2018",

month = jun,

day = "7",

doi = "10.1093/logcom/exv034",

language = "English",

volume = "28",

pages = "631--663",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

publisher = "Oxford University Press",

number = "4",

}

TY - JOUR

T1 - Alternating-time temporal logic with resource bounds

AU - Nguyen, Hoang Nga

AU - Alechina, N.

AU - Logan, B.

AU - Rakib, A.

N1 - This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http:// creativecommons.org/licenses/by/4.0/), which permits unrestricted reuse, distribution, and reproduction in any medium, provided the original work is properly cited.

PY - 2018/6/7

Y1 - 2018/6/7

N2 - Many problems in AI and multi-agent systems research are most naturally formulated in terms of the abilities of a coalition of agents. There exist several excellent logical tools for reasoning about coalitional ability. However, coalitional ability can be affected by the availability of resources, and there is no straightforward way of reasoning about resource requirements in logics such as Coalition Logic (CL) and Alternating-time Temporal Logic (ATL). In this article, we describe a logic for reasoning about coalitional ability under resource constraints. We extend ATL with costs of actions and hence of strategies. We give a complete and sound axiomatization of the resulting logic, Resource-Bounded ATL (RB-ATL) and a model-checking algorithm for it.

AB - Many problems in AI and multi-agent systems research are most naturally formulated in terms of the abilities of a coalition of agents. There exist several excellent logical tools for reasoning about coalitional ability. However, coalitional ability can be affected by the availability of resources, and there is no straightforward way of reasoning about resource requirements in logics such as Coalition Logic (CL) and Alternating-time Temporal Logic (ATL). In this article, we describe a logic for reasoning about coalitional ability under resource constraints. We extend ATL with costs of actions and hence of strategies. We give a complete and sound axiomatization of the resulting logic, Resource-Bounded ATL (RB-ATL) and a model-checking algorithm for it.

KW - Strategic ability

KW - resources

KW - axiomatisation of RB-ATL

U2 - 10.1093/logcom/exv034

DO - 10.1093/logcom/exv034

M3 - Article

SN - 0955-792X

SN - 1465-363X

VL - 28

SP - 631

EP - 663

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 4

ER -

Alternating-time temporal logic with resource bounds

Abstract

Bibliographical note

Keywords

Access to Document

Fingerprint

Cite this