Alternating Epistemic Mu-Calculus
Nils Bulling and Wojtek Jamroga
Alternating-time temporal logic (ATL) is a well known logic for reasoning about strategic abilities of agents. An important feature of ATL in imperfect information scenarios is that the standard fixed point characterizations of temporal modalities do not hold anymore. In this paper, we show that adding explicit fixed point operators to the “next time” fragment of ATL already allows to capture properties that could not be expressed in ATL. We also point out that the new language allows to specify an important kind of ability, namely one where the agents can always recompute their strategy while executing it. Thus, the agents are not assumed to remember their strategy by definition, like in the existing variants of ATL. Last but not least, we show that verification of such abilities is cheaper than for all the variants of “ATL with imperfect information” considered so far.