Game-theoretic semantics for ATL⁺ with applications to model checking

We develop a game-theoretic semantics (GTS) for the fragment ATL⁺ of the alternating-time temporal logic ATL^⁎, thereby extending the recently introduced GTS for ATL. We show that the game-theoretic semantics is equivalent to the standard compositional semantics of ATL⁺ with perfect-recall strategies. Based on the new semantics, we provide an analysis of the memory and time resources needed for model checking ATL⁺ and show that strategies of the verifier that use only a very limited amount of memory suffice. Furthermore, using the GTS, we provide a new algorithm for model checking ATL⁺ and identify a natural hierarchy of tractable fragments of ATL⁺ that substantially extend ATL.