# Equivalence of logical Formula (Kripke structures)

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)

– wece
Commented May 18, 2013 at 12:54

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

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.

• 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 ? Commented May 18, 2013 at 13:44
• 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. Commented May 18, 2013 at 13:50
• 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...... Commented May 18, 2013 at 13:55
• 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. Commented May 18, 2013 at 14:17
• Oh yes right, I forgot this one, thanks :D Commented May 18, 2013 at 14:19