Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable

TL;DR

This paper proves that model checking ATL with imperfect information and perfect recall semantics is undecidable by reducing it from the non-halting problem of Turing machines, filling a gap in formal verification literature.

Contribution

It provides the first formal proof of undecidability for ATL model checking under these semantics, using a reduction from Turing machine non-halting problem.

Findings

Model checking ATL under these semantics is undecidable.

The proof is based on a reduction from Turing machine non-halting problem.

Addresses a previously unproven claim of undecidability.

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.