Relentful strategic reasoning in alternating-time temporal logic
Fabio Mogavero, Aniello Murano, Moshe Y. Vardi · Journal of Logic and Computation · 2014
Temporal logics are a well-investigated formalism for the specification, verification and synthesis of reactive systems. Within this family, Alternating-Time Temporal Logic (A tl *) 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, mC tl * has been defined as a memoryful variant of C tl *, 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 the histories of evolutions. In this article, we introduce Relentful A tl *(RA tl *), a kind of temporally memoryful extension of A tl *, in which a formula is satisfied at a certain node of a play by taking into account both its future and past. We study the expressive power of RA tl *, its succinctness, as well as related decision problems. We investigate the relationship between memoryful quantifications and past modalities and prove their equivalence. We also show that both the relentful and the past extensions come without any computational price; indeed, we prove that both the satisfiability and the model-checking problems are 2E xp T ime-complete , as for A tl *.