Relentful Strategic Reasoning in Alternating-Time Temporal Logic

Temporal logics are a well investigated formalism for the specification, verification, and synthesis of reactive systems. Within this family, alternating temporal logic,

Atl

*

, has been introduced as a useful generalization of classical linear- and branching-time temporal logics by allowing temporal operators to be indexed by coalitions of agents. Classically, temporal logics are memoryless: once a path in the computation tree is quantified at a given node, the computation that has led to that node is forgotten. Recently, m

Ctl

*

has been defined as a memoryful variant of

Ctl

*

, where path quantification is memoryful. In the context of multi-agent planning, memoryful quantification enables agents to “relent” and change their goals and strategies depending on their past history. In this paper, we define m

Atl

*

, a memoryful extension of

Atl

*

, in which a formula is satisfied at a certain node of a path by taking into account both the future and the past. We study the expressive power of m

Atl

*

, its succinctness, as well as related decision problems. We also investigate the relationship between memoryful quantification and past modalities and show their equivalence. We show that both the memoryful and the past extensions come without any computational price; indeed, we prove that both the satisfiability and the model-checking problems are 2

ExpTime-Complete

, as they are for

Atl

*

.