# Game-Theoretic Semantics for ATL+ with Applications to Model Checking

## TL;DR

This paper introduces a game-theoretic semantics for ATL+ logic, demonstrating its equivalence to standard semantics, analyzing resource requirements for model checking, and proposing a new algorithm with tractable fragments.

## Contribution

It extends game-theoretic semantics to ATL+, analyzes memory and time resources for model checking, and proposes a new efficient algorithm with tractable fragments.

## Key findings

- Game-theoretic semantics for ATL+ is equivalent to standard semantics.
- Limited-memory strategies are sufficient for ATL+ model checking.
- A new algorithm and hierarchy of tractable ATL+ fragments are introduced.

## 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.

---
Source: https://tomesphere.com/paper/1702.08405