# Model Checking ATL* on vCGS

## TL;DR

This paper proves that model checking ATL* on vCGS is undecidable by reducing it to the problem on iCGS, highlighting fundamental limits in verifying strategic properties in complex systems.

## Contribution

It establishes the undecidability of ATL* model checking on vCGS, a significant theoretical result in formal verification.

## Key findings

- Model checking ATL* on vCGS is undecidable.
- Reduction from vCGS to iCGS for ATL* model checking.
- Highlights limits of automated verification in complex systems.

## 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.