1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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