Reasoning with a bounded number of resources in ATL+
File(s)
Published version
Author(s)
Belardinelli, Francesco
Demri, Stephane
Type
Conference Paper
Abstract
The resource-bounded alternating-time temporal logic RB±ATL combines strategic reasoning with reasoning about resources. Its model-checking problem is known to be 2EXPTIME-complete (the same as its proper extension RB±ATL*). Several fragments have been identified to lower the complexity.
In this work, we consider the variant RB±ATL+ which permits Boolean combinations of path formulae starting with single temporal operators, but restricted to a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. We show that the model-checking problem for RB±ATL+ restricted to a single agent and a single resource is Δp2-complete, hence the same as for CTL+. In this case reasoning about resources comes at no extra computational cost. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the problem can be solved in EXPTIME using a Turing reduction to the parity game problem for alternating vector addition systems with states.
In this work, we consider the variant RB±ATL+ which permits Boolean combinations of path formulae starting with single temporal operators, but restricted to a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. We show that the model-checking problem for RB±ATL+ restricted to a single agent and a single resource is Δp2-complete, hence the same as for CTL+. In this case reasoning about resources comes at no extra computational cost. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the problem can be solved in EXPTIME using a Turing reduction to the parity game problem for alternating vector addition systems with states.
Editor(s)
DeGiacomo, G
Catala, A
Dilkina, B
Milano, M
Barro, S
Bugarin, A
Lang, J
Date Issued
2020
Date Acceptance
2020-08-29
Citation
ECAI 2020: 24TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2020, 325, pp.624-631
ISBN
978-1-64368-100-9
ISSN
0922-6389
Publisher
IOS PRESS
Start Page
624
End Page
631
Journal / Book Title
ECAI 2020: 24TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE
Volume
325
Copyright Statement
© 2020 The authors and IOS Press.
This article is published online with Open Access by IOS Press and distributed under the terms
of the Creative Commons Attribution Non-Commercial License 4.0 (CC BY-NC 4.0).
This article is published online with Open Access by IOS Press and distributed under the terms
of the Creative Commons Attribution Non-Commercial License 4.0 (CC BY-NC 4.0).
License URL
Identifier
https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000650971300079&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=a2bf6146997ec60c407a63945d4e92bb
Source
24th European Conference on Artificial Intelligence (ECAI)
Subjects
COMPLEXITY
Computer Science
Computer Science, Artificial Intelligence
LOGIC
MODEL-CHECKING
Science & Technology
Technology
Publication Status
Published
Start Date
2020-08-29
Finish Date
2020-09-08
Coverage Spatial
Santiago de Compostela, Spain
Date Publish Online
2020