Alternating-time temporal logics with irrevocable strategies

Abstract

In Alternating-time Temporal Logic (ATL), one can express statements about the strategic ability of an agent (or a coalition of agents) to achieve a goal ϕ such as: "agent i can choose a strategy such that, if i follows this strategy then, no matter what other agents do, ϕ will always be true". However, strategies in ATL are revocable in the sense that in the evaluation of the goal ϕ the agent i is no longer restricted by the strategy she has chosen in order to reach the state where the goal is evaluated. In this paper we consider alternative variants of ATL where strategies, on the contrary, are irrevocable. The difference between revocable and irrevocable strategies shows up when we consider the ability to achieve a goal which, again, involves (nested) strategic ability. Furthermore, unlike in the standard semantics of ATL, memory plays an essential role in the semantics based on irrevocable strategies.