Model Checking Abilities under Incomplete Information Is Indeed Delta2-complete.
Wojciech Jamroga, Jürgen Dix · 2006
We study the model checking complexity of Alternating-time temporal logic with imperfect information and imperfect recall (ATLir). Contrary to what we have stated in [10], the problem turns out to be ∆P2-complete, thus confirming the ini-tial intuition of Schobbens. We prove the∆P2-hardness through a reduction of the SNSAT problem, while the membership in ∆P2 stems from the algorithm pre-sented in [16].