Equivalence rules for LTL - Getting stuck working with $ \square \lozenge $ & Until ($\textsf{ U}$ ) operators

Question

Need to prove equivalence for (or disprove equivalence for):

$ \hspace{1cm}\square ϕ → \lozenge ψ ≡ ϕ\textsf{ U }(ψ ∨ ¬ϕ) \\ $

My current attempt using the LTL equivalnce rules to determine equivalence:

$ \square ϕ → \lozenge ψ \\ ≡\ ¬\square ϕ \lor \lozenge ψ \hspace{1cm}(\textsf{"Mutual implication"} ϕ →ψ≡¬ϕ\lor ψ )\\ ≡ \lozenge ¬ϕ \lor \lozenge ψ \hspace{1cm}(\textsf{"Duality"} ¬\square≡\lozenge ¬ )\\ ≡ \lozenge (¬ϕ \lor ψ) \hspace{1cm}(\textsf{"Distributive law on"}\lozenge )\\ ≡true \textsf{ U} (¬ϕ \lor ψ) \hspace{1cm}(\textsf{"Def of"}\lozenge )\\ ≡true \textsf{ U} (ψ \lor ¬ϕ) \hspace{1cm}(\textsf{"Symmetry"}\lor)\\ $

After this I got stuck. I am not sure how to proceed from here to get the right side. Are other propositional logic rules allowed to be used in LTL, like for example identity disjunction?

Answer 1

In order to prove the equivalence of two formulas $\phi,\psi$, it is enough to show that for every computation $\pi$, it holds that $\pi\models \phi$ iff $\pi\models \psi$. This is semantic equivalence.

Let's look at (1). You got to the formula $true{\bf U} (\psi\vee \neg \phi)$. Now, this holds in a computation $\pi$ iff there exists $i\ge 0$ such that $\pi^i\models \psi\vee \neg \phi$. Assume now that $i$ is minimal with respect to this property, and consider the computations $\pi^j$ for $j<i$. If $\pi^j\models \neg \phi$, then $i$ is not minimal, so $\pi^j\models \phi$, which means that $\pi\models \phi {\bf U} (\psi\vee \neg \phi)$. Since the converse implication is trivial, we get that the two formulas are equivalent.

For (2) you should indeed show that the formulas are not equivalent. To do so, you need to show that there exists a computation $\pi$ that satisfies one but not the other.

Hint: It could be the case that $\phi$ holds only finitely many times, but $\psi$ does not hold after $\phi$.

Answer 2

\begin{alignat*}{2} \Box \varphi \to \Diamond q &\equiv \neg \Box \varphi \lor \Diamond \psi &&\text{($\to$ elim)}\\ &\equiv \Diamond \neg \varphi \lor \Diamond \psi &&\text{(neg near var)}\\ &\equiv \Diamond (\neg \varphi \lor \psi) &&\text{(grouping $\Diamond$)}\\ &\equiv \neg (\neg \varphi \lor \psi) U (\neg \varphi \lor \psi) &&\text{(def of $\Diamond$ using Until)}\\ &\equiv (\varphi \land \neg \psi) U (\neg \varphi \lor \psi) &\quad&\text{(neg inside)}\\ &\equiv \varphi U (\neg \varphi \lor \psi) &&\text{($\land$ elim)}\\ &\equiv \varphi U (\psi \lor\neg \varphi) &&\text{(just arrange) QED} \end{alignat*}