I'm quoting a question from my homework which I don't understand its wording.
Also, I'm not looking for an answer for my problem, I just want to be pointed at some articles/tutorials/reading/tips to solve them.
Gp ⇒ (p U q) U p (p U q) ∧ (q U p) ⇔ p ∧ q Fp ⇔ F(Xp) X(Fp) ⇔ F(Xp) (p U (q ⇒ ¬Xq)) ∧ (FGq) ⇔ p U (Gq) They ask me to prove if these formulas are true for all paths but it seems like they want me to prove them to be equivalent instead.
Asked By : Thang Do
Answered By : Andreas T
The statements you wrote are tautologies, i.e. they are always true. I will give you an example proof for the arguably easiest statement $FXp \leftrightarrow XFp$ so you see how you could do it yourself for the others. Also, it would be good to know if you are working on finite or infinite paths. I am going to use infinite paths here because that is more common as far as I know.
The statement says "There is a point in the future so that at the next position $p$ holds if and only if there is a point in the future other than the current point at which $p$ holds.
We can describe the path with the single predicate $p$ by a set $A \subseteq \mathbb{N}$ at which $p$ is true, and $\mathbb{N} \setminus A$ at which $p$ is false. Let $n \in \mathbb{N}$ be any position.
If $n \models FXp$, this is (by definition) equal to: there is a position $m \geq n$ such that $m \models Xp$, which is equal to $m+1 \models p$, which is equal to $m+1 \in A$. In other words: $n \models FXp$ if and only if there is an $m \geq n$ such that $m+1 \in A$.
If $n \models XFp$, this is equal to $n+1 \models Fp$, which means there is an $m \geq n+1$ such that $k \models p$, so $k \in A$. Again, this means $n \models XFp$ if and only if there is an $k > n$ such that $k \in A$.
You can see that these two statements are clearly equivalent if you choose $k = m+1$. Therefore, $n \models FXp$ iff $n \models XFp$.
Question Source : http://cs.stackexchange.com/questions/56063
0 comments:
Post a Comment
Let us know your responses and feedback