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. (C) 2020 Elsevier Inc. All rights reserved.