2
$\begingroup$

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?

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

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

$\endgroup$
  • $\begingroup$ you are right, btw, what does it mean by $(f, \neg f)^{\omega}$ ? $\endgroup$ – ramgorur Nov 20 '14 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 '14 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 '14 at 10:33

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.