Alternating-time temporal logic with finite-memory strategies

TL;DR

This paper investigates the decidability and complexity of model-checking ATL and ATL* with finite-memory strategies, revealing that bounded-memory semantics retain decidability while finite-memory semantics with three or more players lead to undecidability.

Contribution

It introduces and analyzes finite-memory semantics for ATL/ATL*, showing their differences from perfect recall and memoryless strategies, and establishes complexity results and undecidability boundaries.

Findings

Bounded-memory semantics have Delta_2p-complete complexity for ATL.

Bounded-memory semantics have PSPACE-complete complexity for ATL*.

Finite-memory semantics with three or more players are undecidable in incomplete information games.

Abstract

Model-checking the alternating-time temporal logics ATL and ATL* with incomplete information is undecidable for perfect recall semantics. However, when restricting to memoryless strategies the model-checking problem becomes decidable. In this paper we consider two other types of semantics based on finite-memory strategies. One where the memory size allowed is bounded and one where the memory size is unbounded (but must be finite). This is motivated by the high complexity of model-checking with perfect recall semantics and the severe limitations of memoryless strategies. We show that both types of semantics introduced are different from perfect recall and memoryless semantics and next focus on the decidability and complexity of model-checking in both complete and incomplete information games for ATL/ATL*. In particular, we show that the complexity of model-checking with bounded-memory semantics is Delta_2p-complete for ATL and PSPACE-complete for ATL* in incomplete information games just as in the memoryless case. We also present a proof that ATL and ATL* model-checking is undecidable for n >= 3 players with finite-memory semantics in incomplete information games.