Model Checking ATL* on vCGS
Francesco Belardinelli, Cătălin Dima, Ioana Boureanu, Vadim Malvone · arXiv (Cornell University) · 2019
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.