Proving the equivalence of an LTL and a CTL formula

Question

For a lecture I am attending, we have to prove that

$$\forall \big(a \textsf{U} (b \land \forall \square a)\big) \equiv \big(a \textsf{U} (b \land \square a)\big).$$

That is, we need to prove that for the CTL formula $\forall \big(a \textsf{U} (b \land \forall \square a)\big)$, the LTL formula $\big(a \textsf{U} (b \land \square a)\big)$ is equivalent to it. I know how I would go about trying to disprove it, that is, by providing a transition system that fulfils one but not the other, but I am at a complete loss about how to prove something like this.

Note that we use $\square$ instead of $\textsf{G}$.

Edit:

I managed to prove $$\big(a\textsf{U}(b\land\square a) \big) \equiv \square a \land \lozenge b$$ if that's any help.

Answer 1

First, it is important to understand what the statement

$$\forall \big(a \textsf{U} (b \land \forall \square a)\big) \equiv \big(a \textsf{U} (b \land \square a)\big)$$

means. Hear LTL is interpreted over a transition system, and the semantics then is that all paths of the system satisfy the LTL formula. This is tightly connected to the CTL operator $\forall$.

Lets use the equivalence you have shown and prove $$\forall \big(a \textsf{U} (b \land \forall \square a)\big) \equiv \square a \land \lozenge b$$

To prove the statement, first take a transition system $\mathcal{T}$ that satisfies $\forall \big(a \textsf{U} (b \land \forall \square a)\big)$ and show that it satisfies $\square a \land \lozenge b$. Take arbitrary path $p$ of $\mathcal{T}$. By the CTL semantics you know that $p$ satisfies the path formula $\big(a \textsf{U} (b \land \forall \square a)\big)$. It will have a prefix labeled by $a$ and the state $s$ at the end of this prefix will satisfy the state formula $b \land \square a$. Thus all possible paths starting in $s$ are globally labeled by $a$. In particular, the suffix of the part $p$ we are considering will be labeled by $a$ globally. Also the state $s$ is labeled by $b$. Thus we can conclude that the path $p$ satisfies $\square a \land \lozenge b$.

The other direction is similar. Assume that all paths of $\mathcal{T}$ satisfy $\square a \land \lozenge b$ and show for arbitrary path $p$ of $\mathcal{T}$ that it satisfies $a \textsf{U}(b \land \forall \square a)$. It will be labeled by $b$ at some point, and as all paths of $\mathcal{T}$ are labeled by $a$ globally, in particular all suffixes of $p$ are. So the state on the path $p$ that is labeled by $b$ satisfies the state formula $b \land \forall \square a$.

There is an interesting result connected to your question: let $\varphi$ be a CTL formula. If the property $\varphi$ is definable by an LTL formula (i.e. there exists an LTL formula $\psi$ such that $\varphi \equiv \psi$), then the LTL formula you get by simply deleting all path quantifiers in $\varphi$ is equivalent to $\psi$. See the discussion in Equivalence preserving operator from CTL* to LTL.