Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable
arXiv:1102.4225
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.
Cited by in corpus (11)
- Strategy Logic with Imperfect Information
- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
- Multi-Valued Verification of Strategic Ability
- Bisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting Protocol
- Fixpoint Approximation of Strategic Abilities under Imperfect Information
- Quantified CTL with imperfect information
- The Impact of Strategies and Information in Model Checking for Multi-Agent Systems
- A Hennessy-Milner Theorem for ATL with Imperfect Information
- Model Checking ATL* on vCGS
- Approximating Strategic Abilities under Imperfect Information: a Naive Approach
- A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability