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?

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

1 Answer 1


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

  • $\begingroup$ you are right, btw, what does it mean by $(f, \neg f)^{\omega}$ ? $\endgroup$
    – ramgorur
    Nov 20, 2014 at 7:36
  • 2
    $\begingroup$ It means that the path is of the form $f,\neg f,f,\neg f,...$ and continues like that infinitely. $\endgroup$
    – Shaull
    Nov 20, 2014 at 8:16
  • 3
    $\begingroup$ @ramgorur $\_^{\omega}$ is like the Kleene star but with "infinitely many repetitions", not "arbitrarily many repetitions". See $\omega$-regular languages. $\endgroup$
    – Raphael
    Nov 20, 2014 at 10:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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