  Alternating-time temporal logic (ATL) allows to specify requirements on
abilities that different agents should (or should not) possess in a multi-agent
system. However, model checking ATL specifications in realistic systems is
computationally hard. In particular, if the agents have imperfect information
about the global state of the system, the complexity ranges from Delta2P to
undecidable, depending on the syntactic and semantic details. The problem is
also hard in practice, as evidenced by several recent attempts to tackle it. On
the other hand, model checking of alternating epistemic mu-calculus can have a
distinctly lower computational complexity.
  In this work, we look at the idea of approximating the former problem by the
verification of its "naive" translations to the latter. In other words, we look
at what happens when one uses the (incorrect) fixpoint algorithm to verify
formulae of ATL with imperfect information.
