How to Manage a Budget with ATL+

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.