Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable
Logic in Computer Science
2011-02-22 v1 Multiagent Systems
Abstract
We propose a formal proof of the undecidability of the model checking problem for alternating- time temporal logic under imperfect information and perfect recall semantics. This problem was announced to be undecidable according to a personal communication on multi-player games with imperfect information, but no formal proof was ever published. Our proof is based on a direct reduction from the non-halting problem for Turing machines.
Keywords
Cite
@article{arxiv.1102.4225,
title = {Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable},
author = {Catalin Dima and Ferucio Laurentiu Tiplea},
journal= {arXiv preprint arXiv:1102.4225},
year = {2011}
}