Model Checking ATL* on vCGS
Francesco Belardinelli, Catalin Dima, Ioana Boureanu, and Vadim, Malvone

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.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Formal Methods in Verification · Logic, programming, and type systems
Model Checking on vCGS
F. Belardinelli, C. Dima, I. Boureanu, and V. Malvone
We prove that the model checking on vCGS is undecidable. To do so, we reduce this problem to model checking on iCGS.
Consider an formula to be model-checked on a given iCGS . Out of M and , we define an vCGS (which we sometimes refer to simply as ) and an formula , as follows.
Agents & atoms. The set of agents in is , where denotes the Environment agent. For each agent , the set of atoms controlled by includes an atom for each action in , i.e., . The environment controls atoms corresponding to each state of the iCGS and each indistinguishability class for each agent, i.e., , with .
An agent specification is with the guarded commands to be defined hereafter. First, for each agent specification and subset , by we denote the boolean formula specifying that all of ’s atoms in are left invisible to any agent other than , i.e., does not share any of her controlled atoms from with anyone:
[TABLE]
For the special case of the environment (i.e., where in the above is replaced with the Environment and , etc), we simply write instead of (i.e., .)
Second, for an agent , by we denote the boolean formula specifying that all atoms in are visible to , i.e., does share all her controlled atoms in with :
[TABLE]
For each agent and for the Environment , we also use boolean variables and to simulate their turns and mechanise the (synchronisation over) actions.
Guarded commands of init-type.
For each , a guarded command of init-type to agents is defined in as follows:
[TABLE] 2. 2.
For each , a guarded command of init-type for the Environment is defined in as follows:
[TABLE]
Guarded commands of update-type. Let in M be given as the set . Then, agent ’s guarded commands of update-type are added in as follows:
For every and each equivalence class , guarded command is defined as
[TABLE] 2. 4.
To simulate ’s turn (or “moving forward” in the system –hence the name below), we add the following guarded command:
[TABLE]
Then, the environment agent has the following guarded commands of update-type:
One guarded command of update-type for , to make him “move forward” (i.e., take turns):
[TABLE] 2. 6.
For each , , and , let denoted ; for this, another guarded command for is as follows:
[TABLE]
Now, using the reduction above (which is in PTIME), we can formally state the following result:
Theorem 1** (3.4)**
*The model checking problem for (resp. ) on iCGS is PTIME-reducible to the same on vCGS. *
Proof. 1
Given an formula , we construct the formula in which each next operator is duplicated. For example, for the formula , we set . For we duplicate each coalition-next operator instead: for , we set . Then we can show that, for any iCGS M, the vCGS constructed as above is such that iff . We do so by structural induction on the formula .
Using Theorem 1 above and knowing from [1] that model checking and on iCGSs is undecidable, we can state the following result:
Corollary 1** (3.5)**
*The model checking problem for (resp. ) on vCGS are undecidable. *
We conclude by recalling that if we assume positional strategies, the model checking problem for (resp. ) on iCGS are PSPACE- (resp. -) complete [3, 2]. Hence, the same complexities apply to vCGS.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] C. Dima and F. Tiplea. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. Co RR , abs/1102.4225, 2011.
- 2[2] W. Jamroga and J. Dix. Model checking abilities under incomplete information is indeed Δ p 2 superscript subscript Δ 𝑝 2 {\Delta}_{p}^{2} -complete. In EUMAS’06 , pages 14–15, 2006.
- 3[3] P.-Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science , 85(2):82–93, 2004.
