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

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

• I don't think that $\alpha \land AXAX\alpha$ is the same as $EG^2(\alpha)$, since it is only about positions $0,2$. However, $EG^2(\alpha)$ holds iff $\alpha$ holds now and $EG^2(\alpha)$ holds two positions from now. In other words, $EG^2(\alpha) \leftrightarrow \alpha \land AXAXEG^2(\alpha)$. Does that look like a fixpoint? – Yuval Filmus Jan 30 at 9:55
• @YuvalFilmus thank you for the comment. I think you are right. I have updated the question and provided an answer. Feel free to check it out. – Xugui Manuel Jan 30 at 14:54

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