Bounded Planning for Strategic Goals with Incomplete Information and Perfect Recall

The paper proposes an OBDD-based bounded model checking algorithm for alternating-time temporal logic in systems of incomplete information and multiple players. Players are assumed to have perfect recall memory over their observations and local actions. The algorithm is implemented in a model checker and experimental results are reported to show its applications in bounded planning for strategic goals. The computational complexity of model checking is also addressed.