Satisfiability of ATL with strategy contexts

TL;DR

This paper investigates the satisfiability problem for ATL with strategy contexts, showing decidability in specific cases such as turn-based games and bounded moves, but undecidability with memoryless strategies.

Contribution

It identifies conditions under which the satisfiability problem for ATL with strategy contexts becomes decidable, extending understanding of the logic's computational boundaries.

Findings

Decidability of satisfiability in turn-based games.

Decidability when agents have bounded moves.

Undecidability with memoryless strategies.

Abstract

Various extensions of the temporal logic ATL have recently been introduced to express rich properties of multi-agent systems. Among these, ATLsc extends ATL with strategy contexts, while Strategy Logic has first-order quantification over strategies. There is a price to pay for the rich expressiveness of these logics: model-checking is non-elementary, and satisfiability is undecidable. We prove in this paper that satisfiability is decidable in several special cases. The most important one is when restricting to turn-based games. We prove that decidability also holds for concurrent games if the number of moves available to the agents is bounded. Finally, we prove that restricting strategy quantification to memoryless strategies brings back undecidability.