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 * , essentially extending a recently introduced GTS for ATL. We show that the new game-theoretic semantics is equivalent to the standard compositional semantics of ATL + (with perfectrecall 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 extend ATL.