Rhodes, Greece. September 2-8, 2023.
Copyright © 2023 International Joint Conferences on Artificial Intelligence Organization
We study the alternating-time temporal logic ATL+ enriched with one resource (written ATL+(1)) extending ATL+ with the possibility to manage a budget.
We propose a game-theoretic semantics via the introduction of two evaluation
games so that the compositional semantics is captured by strategies in the games.
We show that the model-checking problem for ATL+(1) is in PSpace and we identify
several non-trivial fragments that can be solved in PTime. By-products of our investigations include also a simplified Pspace decision procedure for
resource-free ATL+, an effective way to synthesize constraints in
a version of ATL+(1) with parameters and a PSpace bound to solve an energy game
with one counter whose objectives are LTL formulae of temporal depth one.