**Problem Detail:**

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

###### Asked By : user8241

#### Answered By : Shaull

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.

###### Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/12109

**3.2K people like this**

## 0 comments:

## Post a Comment

Let us know your responses and feedback