Sciweavers

ATAL
2010
Springer

Resource-bounded alternating-time temporal logic

13 years 4 months ago
Resource-bounded alternating-time temporal logic
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 paper, we propose 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 axiomatisation of the resulting logic Resource-Bounded ATL (RB-ATL) and an efficient model-checking algorithm for it. Categories and Subject Descriptors I.2.11 [Distributed Artificial Intelligence]: [multiagent systems] General Terms Theory, Verification Keywords Logics for agency, Verification of MAS
Natasha Alechina, Brian Logan, Nguyen Hoang Nga, A
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where ATAL
Authors Natasha Alechina, Brian Logan, Nguyen Hoang Nga, Abdur Rakib
Comments (0)