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 :)
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.Sign up to join this community
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.