How to Manage a Budget with ATL⁺

Abstract

<p>We study ATL<sup>+</sup> enriched with one resource (written ATL<sup>+</sup>(1)) extending ATL<sup>+</sup> 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<sup>+</sup>(1) is in PSPACE and we identify fragments in PTIME. By-products of our investigations include a simplified PSPACE decision procedure for resource-free ATL<sup>+</sup> based on small strategy skeletons, the synthesis of constraints in ATL<sup>+</sup>(1) with parameters and a PSPACE bound to solve a close energy game problem with one counter and objectives of temporal depth one.</p>