Model-Checking Alternating-time Temporal Logic with
Strategies Based on Common Knowledge Is Undecidable (joint work with Raluca Diaconu)
We present a semantics for the Alternating-time Temporal Logic (ATL) with imperfect information, in which the participants in a coalition choose their strategies such that each agent's choice is the same in all states that form the common knowledge for the coaltion. We show that ATL with this semantics has an undecidable model-checking problem if the semantics is also synchronous and the agents have perfect recall.
To appear in Applied Artificial Intelligence, 2011. A preliminary version was presented at EUMAS'2010