# Proving Linear Time Temporal Logic formula □ ◊ f ⇔ ◊ □ f

I am new to this topic, Linear Time Temporal Logic and I am trying to prove this equivalence --

$\Box\Diamond f \Leftrightarrow \Diamond\Box f$

This is my take --

Basic definitions:

$(\sigma, j) \models \Box f: \forall k \, [(k \ge j) \Rightarrow ((\sigma, k) \models f)]$

$(\sigma, j) \models \Diamond f: \exists k \, [(k \ge j) \Rightarrow ((\sigma, k) \models f)]$

Here, $(\sigma, j) \models f$ means $\sigma$ satisfies $f$ at $\sigma(j)$, for more details about this syntax, please see here.

Now the LHS:

$\begin{eqnarray} (\sigma, j) \models \Box \Diamond f & : & \forall k \, [(k \ge j) \Rightarrow ((\sigma, k) \models \Diamond f)]\\ & \equiv & \forall k \, [(k \ge j) \Rightarrow [\exists p \, [(p \ge k) \Rightarrow ((\sigma, p) \models f)]]]\\ & \equiv & \forall k \, [(k<j) \vee [\exists p \, [(p<k) \vee ((\sigma,p) \models f)]]]\\ & \equiv & \forall k \, \exists p \, [(k<j) \vee (p<k) \vee ((\sigma,p) \models f)]\\ & \equiv & \forall k \, \exists p \, [(p<k<j) \vee ((\sigma,p) \models f)]\\ \end{eqnarray}$

Again, the RHS:

$\begin{eqnarray} (\sigma, j) \models \Diamond \Box f & : & \exists k \, [(k \ge j) \Rightarrow ((\sigma, k) \models \Box f)]\\ & \equiv & \exists k \, [(k \ge j) \Rightarrow [\forall p \, [(p \ge k) \Rightarrow ((\sigma, p) \models f)]]]\\ & \equiv & \exists k \, [(k<j) \vee [\forall p \, [(p<k) \vee ((\sigma,p) \models f)]]]\\ & \equiv & \exists k \, \forall p \, [(p<k<j) \vee ((\sigma,p) \models f)]\\ \end{eqnarray}$

Now if we look at the last line of the both sides, the statement

$\forall k \, \exists p \, [(p<k<j) \vee ((\sigma,p) \models f)] \equiv \exists k \, \forall p \, [(p<k<j) \vee ((\sigma,p) \models f)]$

needs to be true to complete the proof, however intuitively, this is not true.

What I am missing? How do I proceed? Any idea?

• Are you confident that the equivalence holds? – Raphael Nov 20 '14 at 10:31
• no, actually they don't. – ramgorur Nov 21 '14 at 20:07

You are not missing anything. These expressions are indeed not equivalent. Assume $f$ in your case is an atomic proposition. Then the computation: $f,\neg f,(f,\neg f)^\omega$ satisfies $□◊f$, but not $\Diamond \square f$.
Intuitively, $\Diamond \square f$ means "After a finite prefix, there is always $f$", while $\square \Diamond f$ means: "There are infinitely many $f$s".
By the way, you have some mistake in your semantics. It should be: $(\sigma,j)\models \Diamond f$: $\exists k[k\ge j\wedge (\sigma,k)\models f]$.
• you are right, btw, what does it mean by $(f, \neg f)^{\omega}$ ? – ramgorur Nov 20 '14 at 7:36
• It means that the path is of the form $f,\neg f,f,\neg f,...$ and continues like that infinitely. – Shaull Nov 20 '14 at 8:16
• @ramgorur $\_^{\omega}$ is like the Kleene star but with "infinitely many repetitions", not "arbitrarily many repetitions". See $\omega$-regular languages. – Raphael Nov 20 '14 at 10:33