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