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