Title: Game-Theoretic Semantics for ATL+ with Applications to Model Checking,
Abstract: We develop game-theoretic semantics (GTS) for the fragment ATL+ of the full
Alternating-time Temporal Logic ATL*, essentially extending a recently
introduced GTS for ATL. We first show that the new game-theoretic semantics is
equivalent to the standard semantics of ATL+ (based on perfect recall
strategies). We then provide an analysis, based on the new semantics, of the
memory and time resources needed for model checking ATL+. Based on that, we
establish that strategies that use only a very limited amount of memory suffice
for ATL+. Furthermore, using the GTS we provide a new algorithm for model
checking of ATL+ and identify a natural hierarchy of tractable fragments of
ATL+ that extend ATL.