Model Checking ATL* on vCGS

Francesco Belardinelli; Catalin Dima; Ioana Boureanu; and Vadim; Malvone

arXiv:1903.04350·cs.LO·March 12, 2019

Model Checking ATL* on vCGS

Francesco Belardinelli, Catalin Dima, Ioana Boureanu, and Vadim, Malvone

PDF

Open Access

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

01

Model checking ATL* on vCGS is undecidable.

02

Reduction from vCGS to iCGS for ATL* model checking.

03

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.

Equations4

in v i s^{a} (W) = b \in A g ∖ {a} ⋀ v \in W ⋀ v i s (v, b) := ff

in v i s^{a} (W) = b \in A g ∖ {a} ⋀ v \in W ⋀ v i s (v, b) := ff

v i s (W, b) = v \in W ⋀ v i s (v, b) = tt

v i s (W, b) = v \in W ⋀ v i s (v, b) = tt

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

Full text

Model Checking $ATL^{*}$ on vCGS

F. Belardinelli, C. Dima, I. Boureanu, and V. Malvone

We prove that the model checking $ATL^{*}$ on vCGS is undecidable. To do so, we reduce this problem to model checking $ATL^{*}$ on iCGS.

Consider an $ATL^{*}$ formula $\varphi$ to be model-checked on a given iCGS $\texttt{M}=\langle Ag,\{Act_{a}\}_{a\in Ag},S,S_{0},P,\tau,\{\sim_{a}\}_{a\in Ag},\pi\rangle$ . Out of M and $\varphi$ , we define an vCGS $\Delta_{\texttt{M}}$ (which we sometimes refer to simply as $\Delta$ ) and an $ATL^{*}$ formula $\psi_{\varphi,\texttt{M}}$ , as follows.

Agents & atoms. The set of agents in $\Delta_{\texttt{M}}$ is $Ag^{\prime}=Ag\cup\{e\}$ , where $e$ denotes the Environment agent. For each agent $a\in Ag$ , the set of atoms controlled by $a$ includes an atom for each action in $Act_{a}$ , i.e., $V_{a}=\{p_{act}\mid act\in Act_{a}\}$ . The environment controls atoms corresponding to each state of the iCGS and each indistinguishability class for each agent, i.e., $V_{e}=\{p_{s}\mid s\in S\}\cup\{p_{[s]_{a}}\mid s\in S,a\in Ag\}$ , with $[s]_{a}=\{s^{\prime}\in S\mid s^{\prime}\sim_{a}s\}$ .

An agent specification is $spec_{a}=\langle V_{a},GC_{a}\rangle$ with the guarded commands to be defined hereafter. First, for each agent specification $spec_{a}$ and subset $W\subseteq V_{a}$ , by $invis^{a}(W)$ we denote the boolean formula specifying that all of $a$ ’s atoms in $W$ are left invisible to any agent other than $a$ , i.e., $a$ does not share any of her controlled atoms from $W$ with anyone:

[TABLE]

For the special case of the environment (i.e., where $a$ in the above is replaced with the Environment and $W\subseteq V_{e}$ , etc), we simply write $invis(W)$ instead of $invis^{a}(W)$ (i.e., $invis(W)=\bigwedge_{b\in Ag}\allowbreak\bigwedge_{v\in W}vis(v,b):=\mathrm{ff}$ .)

Second, for an agent $b\in Ag\setminus{\{a\}}$ , by $vis(W,b)$ we denote the boolean formula specifying that all atoms in $W$ are visible to $b$ , i.e., $a$ does share all her controlled atoms in $W$ with $b$ :

[TABLE]

For each agent $a\in Ag$ and for the Environment $e$ , we also use boolean variables $turn_{a}$ and $turn_{e}$ to simulate their turns and mechanise the (synchronisation over) actions.

Guarded commands of init-type.

For each $s_{0}\in S_{0}$ , a guarded command $\gamma_{[s_{0}]_{a}}$ of init-type to agents $a$ is defined in $\Delta_{\texttt{M}}$ as follows:

[TABLE] 2. 2.

For each $s_{0}\in S_{0}$ , a guarded command $\gamma_{[s_{0}]_{e}}$ of init-type for the Environment $e$ is defined in $\Delta_{\texttt{M}}$ as follows:

[TABLE]

Guarded commands of update-type. Let $Act_{a}$ in M be given as the set $\{\alpha_{1},\ldots,\alpha_{k_{a}}\}$ . Then, agent $a$ ’s guarded commands of update-type are added in $\Delta_{\texttt{M}}$ as follows:

For every $1\leq i\leq k_{a}$ and each equivalence class $[s]_{a}\in S$ , guarded command $\gamma_{i,[s]_{a}}$ is defined as

[TABLE] 2. 4.

To simulate $a$ ’s turn (or $a$ “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 $e$ , to make him “move forward” (i.e., take turns):

[TABLE] 2. 6.

For each $s\in S$ , $a\in Ag$ , and $i_{a}\leq k_{a}$ , let $t$ denoted $\tau(s,(\alpha_{i_{a}})_{a\in Ag})$ ; for this, another guarded command for $e$ 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 $ATL^{*}$ (resp. $ATL$ ) on iCGS is PTIME-reducible to the same on vCGS. *

Proof. 1

Given an $ATL^{*}$ formula $\varphi$ , we construct the formula $\varphi^{\prime}$ in which each next operator is duplicated. For example, for the formula $\varphi=Xp$ , we set $\varphi^{\prime}=XXp$ . For $ATL$ we duplicate each coalition-next operator instead: for $\varphi={\langle\!\langle A\rangle\!\rangle}Xp$ , we set $\varphi^{\prime}={\langle\!\langle A\rangle\!\rangle}X{\langle\!\langle A\rangle\!\rangle}Xp$ . Then we can show that, for any iCGS M, the vCGS $\Delta_{\texttt{M}}$ constructed as above is such that $\texttt{M}\models\varphi$ iff $\Delta_{\texttt{M}}\models\varphi^{\prime}$ . We do so by structural induction on the formula $\varphi$ .

Using Theorem 1 above and knowing from [1] that model checking $ATL^{*}$ and $ATL$ on iCGSs is undecidable, we can state the following result:

Corollary 1 (3.5)

*The model checking problem for $ATL^{*}$ (resp. $ATL$ ) on vCGS are undecidable. *

We conclude by recalling that if we assume positional strategies, the model checking problem for $ATL^{*}$ (resp. $ATL$ ) on iCGS are PSPACE- (resp. $\Delta^{P}_{2}$ -) complete [3, 2]. Hence, the same complexities apply to vCGS.

Bibliography3

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.

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

Taxonomy

Model Checking ATL∗ATL^{*}ATL∗ on vCGS

Theorem 1** (3.4)**

Proof. 1

Corollary 1** (3.5)**

Model Checking $ATL^{*}$ on vCGS

Theorem 1 (3.4)

Corollary 1 (3.5)