  Model checking of strategic ability under imperfect information is known to
be hard. The complexity results range from NP-completeness to undecidability,
depending on the precise setup of the problem. No less importantly, fixpoint
equivalences do not generally hold for imperfect information strategies, which
seriously hampers incremental synthesis of winning strategies. In this paper,
we propose translations of ATLir formulae that provide lower and upper bounds
for their truth values, and are cheaper to verify than the original
specifications. That is, if the expression is verified as true then the
corresponding formula of ATLir should also hold in the given model. We begin by
showing where the straightforward approach does not work. Then, we propose how
it can be modified to obtain guaranteed lower bounds. To this end, we alter the
next-step operator in such a way that traversing one's indistinguishability
relation is seen as atomic activity. Most interestingly, the lower
approximation is provided by a fixpoint expression that uses a nonstandard
variant of the next-step ability operator. We show the correctness of the
translations, establish their computational complexity, and validate the
approach by experiments with a scalable scenario of Bridge play.
