# Least fix point of CTL formula

In the book Logic in Computer Science on page 244, there is a proof that $[[E(\phi U\psi)]]$ is the least fixed point of $G(X)=[[\psi]] \cup ([[\phi]]\cap\mathop{\textrm{pre}}_\exists(X))$. I don't get the idea of point 2. I tried to understand why this proof says that $[[E(\phi U\psi)]]$ is the least fixed point of $G$.

They prove that $G^{k+1}(\emptyset)\subseteq[[E(\phi U\psi)]]$ for each $k\geq0$.
This is fine, I understand each step on their the proof, I just don't understand why this proves that $[[E(\phi U\psi)]]$ is the least fixed point of $G$...

I can prove that $G^{k+1}(\emptyset)\subseteq S$ when $S$ is the group of all the states. $G$ is still the same function, and of course that for each such $i\geq0, G^i(\emptyset)\subseteq S$. This doesn't mean that $S$ is the least fixed point, or that each fixed point contains $S$.

So why this proof claims that $[[E(\phi U\psi)]]$ is the least fixed point of $G$?

They actually start by proving that $[[E(\varphi U\psi)]]=\bigcup\limits_{k\ge 1}G^k(\emptyset)$.

You can see (or prove by induction for the general case) that repeated applications of $G$ starting with the empty set yields:

$G(\emptyset)=[[\psi]]$,

$G^2(\emptyset)=[[\psi]]\cup ([[\varphi]]\cap pre_\exists([[\psi]]))=[[\psi]]\cup\left\{s\in S | s\in[[\varphi]] \land \exists s' \left(s\rightarrow s' \land s'\in[[\psi]]\right)\right\}$

$\vdots$

$G^{i+1}(\emptyset)=G^i(\emptyset)\cup \left\{s\in S| s\in[[\varphi]]\land\exists s' \left( s\rightarrow s'\land s'\in G^i(\emptyset)\right)\right\}$

The union of the above sets exactly coincides with the definition of $[[E(\varphi U \psi)]]$. To conclude the proof, they use the fact that $G$ is montone and that $G^{n+1}(\emptyset)$ is a fixed point of $G$, thus $\bigcup\limits_{k\ge 1}G^k(\emptyset)=G^{n+1}(\emptyset)$, which is the least fixed point of $G$.

• True, I understand that. But you can replace $[[E(\phi U \psi)]]$ with $S$ and then proof in the same way that $S=\bigcup\limits_{k\ge 1}G^k(\emptyset)$ and $S=G^{n+1}(\emptyset)$. Does it mean that $S$ is the least fixed point? No... – nrofis Jun 16 '18 at 15:32
• The problem is that you cannot replace $[[E(\varphi U \psi)]]$ with $S$, the argument is specific for this set and depends on it's exact definition (the existence of a path...). In your question you only required $\subseteq$, which obviously also holds for the entire set of states $S$, by they actually show equality and not only containment. – Ariel Jun 16 '18 at 15:57
• I don't understand how they showed the equality. Because they showed that for every $i\geq 0$ every $s_0 \in G^i$ are also $s_0 \in [[E(\phi U \psi)]]$. So actually they showed that $\bigcup\limits_{k\ge 1}G^k(\emptyset) \subseteq [[E(\phi U \psi)]]$ and the union is just $G^{n+1}(\emptyset)$ so they proved that $G^{n+1}(\emptyset) \subseteq [[E(\phi U \psi)]]$. Am I wrong? – nrofis Jun 16 '18 at 17:23
• Write down the definition of $[[E(\varphi U \psi)]]$, they show that $G^k(\emptyset)$ corresponds to taking a path of length $k$ in that definition. – Ariel Jun 16 '18 at 17:27