HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Strategic Reasoning with a Bounded Number of Resources: the Quest for Tractability

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$^⁎$) and fragments have been identified to lower the complexity. In this work, we consider the variant RB±ATL+ that allows for 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 $\Delta_{2}^{P}$-complete, hence the same as for the standard branching-time temporal logic CTL+. In this case reasoning about resources comes at no extra computational cost. When a fixed finite set of linear-time temporal operators is considered, the model-checking problem drops to PTIME, which includes the special case of RB±ATL restricted to a single agent and a single resource. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the model-checking problem for RB±ATL+ can be solved in EXPTIME using a sophisticated Turing reduction to the parity game problem for alternating vector addition systems with states (AVASS).
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03298703
Contributor : Stéphane Demri Connect in order to contact the contributor
Submitted on : Friday, July 23, 2021 - 6:05:07 PM
Last modification on : Tuesday, January 18, 2022 - 2:26:08 PM
Long-term archiving on: : Sunday, October 24, 2021 - 6:57:32 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Francesco Belardinelli, Stéphane Demri. Strategic Reasoning with a Bounded Number of Resources: the Quest for Tractability. Artificial Intelligence, Elsevier, 2021, 300, pp.103557. ⟨10.1016/j.artint.2021.103557⟩. ⟨hal-03298703⟩

Share

Metrics

Record views

106

Files downloads

59