$Sat(EG^2\alpha)$ as a fixpoint of an operator

Question

Currently I am studying CTL model checking. I found this exercise:

Consider the CTL formula $EG^2(\alpha)$ which means that there exists a path that satisfies $\alpha$ at every even position. Define $Sat(EG^2(\alpha))$ as a fixpoint of an operator and describe how to extend the CTL model checking algorithm for formulas that contain the operator $EG^2(\alpha)$.

Answer 1

Let us prove that $EG^2\alpha$ is the greatest fixpoint of $\tau(Z):=\alpha\wedge EXEXZ$.

Suppose $s_0\in Sat(\tau(EG^2\alpha))$, then $s_0\in Sat(\alpha)$ and for some path starting at $s_0$, we have $s_2\in Sat(EG^2\alpha)$ where $s_2$ is a successor of $s_1$ and $s_1$ is a successor of $s_0$. That is, $s_0\in Sat(\alpha)$ and for some $\pi\in Paths(s_2)$, we have $\pi[2i]\in Sat(\alpha)$, $i\in \mathbb{N}$. Hence, $s_0\in Sat(EG^2\alpha)$.

Now, assume that $s_0\in Sat(EG^2\alpha)$, then for every $\pi\in Paths(s_0)$, $\pi[2i]\in Sat(\alpha)$, $i\in\mathbb{N}$. Therefore, $s_0\in Sat(\tau(EG^2\alpha))$.

We have seen that $EG^2\alpha$ is a fixpoint of $\tau(Z)$. Suppose, now, that $Y$ is a fixpoint of $\tau(Z)$, that is $Y=\tau(Y)$. Let us see that $Sat(Y)\subseteq Sat(EG^2\alpha)$. Let $s_0\in Sat(Y)$, then $s_0\in Sat(\alpha)$ and $s_2\in Sat(Y)$ for some $s_1\in suc(s_0)$ and $s_2\in suc(s_1)$. But then again $Sat(Y)=Sat(\tau(Y))$, so we have $s_0\in \alpha$, $s_2\in Sat(\alpha)$ and $s_4\in Sat(\alpha)$ for some $s_3\in suc(s_2)$ and $s_4\in suc(s_3)$. In the limit case, we get a path starting at $s_0$ that satisfies $EG^2\alpha$. Hence, $s_0\in Sat(EG^2\alpha)$.

To extend the CTL algorithm

$Sat(EG^2\alpha)$ is the largest $C\subseteq S$ ($S$ is the set of states) such that:

• $C\subseteq Sat(\alpha)$;
• $s\in C\Rightarrow\text{ for each }s'\in suc(s),\text{we have } suc(s')=C$.