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

2011/02/21 by Dima, Catalin, Tiplea, Ferucio Laurentiu · 3 citations
#03B42 #03B44 #68Q60 #D.2.4 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Multiagent Systems (cs.MA)

paper · doi:10.48550/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

• Formal Verification of Probabilistic Multi-Agent Systems for Ballistic Rocket Flight Using Probabilistic Alternating-Time Temporal Logic
• A Timed Obstruction Logic for Dynamic Game Models
• Strategy Logic, Imperfect Information, and Hyperproperties

Related

• Decidability results for ATL* with imperfect information and perfect recall
• Game-Theoretic Semantics for ATL+ with Applications to Model Checking
• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic
• Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics
• Approximating Strategic Abilities under Imperfect Information: a Naive\n Approach