  Model-checking the alternating-time temporal logics ATL and ATL* with
incomplete information is undecidable for perfect recall semantics. However,
when restricting to memoryless strategies the model-checking problem becomes
decidable. In this paper we consider two other types of semantics based on
finite-memory strategies. One where the memory size allowed is bounded and one
where the memory size is unbounded (but must be finite). This is motivated by
the high complexity of model-checking with perfect recall semantics and the
severe limitations of memoryless strategies. We show that both types of
semantics introduced are different from perfect recall and memoryless semantics
and next focus on the decidability and complexity of model-checking in both
complete and incomplete information games for ATL/ATL*. In particular, we show
that the complexity of model-checking with bounded-memory semantics is
Delta_2p-complete for ATL and PSPACE-complete for ATL* in incomplete
information games just as in the memoryless case. We also present a proof that
ATL and ATL* model-checking is undecidable for n >= 3 players with
finite-memory semantics in incomplete information games.
