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 :)
$\begingroup$
$\endgroup$
1
-
$\begingroup$ what is your guess? $\endgroup$– weceCommented May 18, 2013 at 12:54
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
9
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.
-
$\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$– user8241Commented May 18, 2013 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$– ShaullCommented May 18, 2013 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$– user8241Commented May 18, 2013 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$– ShaullCommented May 18, 2013 at 14:17
-
$\begingroup$ Oh yes right, I forgot this one, thanks :D $\endgroup$– user8241Commented May 18, 2013 at 14:19