Abstract
Alternating-time temporal logic (ATL) is a wellknown logic for reasoning about strategic abilities of agents. An important feature that distinguishes variants of ATL for imperfect information scenarios is that the standard ?xed point characterizations of temporal modalities do not hold anymore. In this paper, we show that adding explicit ?xed point operators to the “next-time” fragment of ATL already allows to capture abilities that could not be expressed in ATL. We also illustrate that the new language allows to specify important kinds of abilities, namely ones where the agents can always recompute their strategy while executing it. Thus, the agents are not assumed to remember their strategy by de?nition, like in the existing variants of ATL. Last but not least, we show that veri?cation of such abilities can be cheaper than for all the variants of “ATL with imperfect information” considered so far.