Model Checking ATL* on vCGS

Abstract

We prove that the model checking ATL* on concurrent game structures with propositional control for atom-visibility (vCGS) is undecidable. To do so, we reduce this problem to model checking ATL* on iCGS.

References in corpus (1)

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