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

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

• I see that you asked earlier versions of this question, got feedback, and then deleted the question and asked a new version (1, 2). For future reference, we usually prefer that you edit the question rather than deleting it and asking a new one -- that way the feedback you've already received doesn't get lost. For instance, as Raphael previously pointed out, we ask that you avoid using images as the main content of your post. – D.W. Dec 5 '16 at 18:11

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

\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*}

• @Evil The marginal notes explain each step. – David Richerby May 14 '18 at 10:52
• @DavidRicherby I see comments. After your edit the answer is much clearer. My point is, the answer looks like ready to go eqution (source code) with commented list of steps, no description why or how. (Not really my topic, so I count on your judgement here). In that case my comments are obsolete, to be deleted. – Evil May 14 '18 at 12:15
• @Evil No, it's a sequence of logical deductions. The "why" and "how" are both "this is a valid deduction according to rule X." – David Richerby May 14 '18 at 12:16