0
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$ Jan 30, 2021 at 9:55
  • $\begingroup$ @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. $\endgroup$
    – guipa
    Jan 30, 2021 at 14:54

1 Answer 1

1
$\begingroup$

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.