Bounded planning for strategic goals with incomplete information and perfect recall
Xiaowei Huang · Adaptive Agents and Multi-Agents Systems · 2013
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.