3
$\begingroup$

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

Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

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

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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... $\endgroup$
    – nrofis
    Jun 16, 2018 at 15:32
  • $\begingroup$ 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. $\endgroup$
    – Ariel
    Jun 16, 2018 at 15:57
  • $\begingroup$ 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? $\endgroup$
    – nrofis
    Jun 16, 2018 at 17:23
  • 1
    $\begingroup$ 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. $\endgroup$
    – Ariel
    Jun 16, 2018 at 17:27

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.