2
$\begingroup$

Can someone explain me how to find if these formulas are equivalent with Kripke structures?

AG(Fp or Fq) , A(GFp or GFq)

AGF(p and q) , A(GFp and GFq)

AFG(p and q) , A(FGp and FGq)

Thank you in advance for your help :)

$\endgroup$
  • $\begingroup$ what is your guess? $\endgroup$ – wece May 18 '13 at 12:54
2
$\begingroup$

First, these can all be looked at as LTL formulas. Therefore, their equivalence can be determined by their behaviour on traces (no need for Kripke structures with a complicated structure).

This answer is just a bunch of spoilers, so read only if you already tried your best.

For the first pair - they are equivalent. Intuitively, this is because there are infinitely many p's or infinitely many q's iff there are infinitely many (p's or q's). Foramlly,

$\pi\models G(Fp \vee Fq)$ iff at every index $i$, $\pi^i\models (Fp\vee Fq)$, meaning that in every index, there is eventually a $p$ or a $q$. Equivalently, this means that there are infinitely many $p$'s or $q$'s, which is equivalent to $\pi\models GFp\vee GFq$.

For the second pair - they are not equivalent. Try and think of a counter example. If you really can't - leave a comment.

The third pair are also equivalent. Informally - this is because they both state that after a finite prefix, both $p$ and $q$ always hold. The formal argument just follows from the semantics.

$\endgroup$
  • $\begingroup$ The second one, the first formula, there is always p,q at each index. The second formula, you can have multiple p in the future then a q arrive and it becomes p,q for all the next index right? But you can also have at each index p,q too on one execution, right ? $\endgroup$ – user8241 May 18 '13 at 13:44
  • $\begingroup$ I'm not sure I understand your comment. Are you suggesting a counterexample? If so - try to write the paths, it would be easier to see what you mean. $\endgroup$ – Shaull May 18 '13 at 13:50
  • $\begingroup$ paths could be in the future p->p->p->p,q->p,q->p,q... or q->q->q,p->q,p.... or p,q->p,q->p,q.... for the second formula. The first formula would always only get this path in the future p,q->p,q->p,q...... $\endgroup$ – user8241 May 18 '13 at 13:55
  • 1
    $\begingroup$ Yes, but all of these paths satisfy $GF(p\wedge q)$. However, note that there are also paths of the form $p\to q\to p\to q...$ without ever seeing $p\wedge q$. This satisfies the second, but not the first. $\endgroup$ – Shaull May 18 '13 at 14:17
  • $\begingroup$ Oh yes right, I forgot this one, thanks :D $\endgroup$ – user8241 May 18 '13 at 14:19

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.