# How to prove LTL-formulas true for all paths?

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.

• I don't understand your question. You say you want to understand the wording of a question you've been given but you don't tell us what that wording is. Apr 17, 2016 at 14:16
• oh. it's "Are the following LTL-formulas true for all paths?" Apr 17, 2016 at 23:33

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

• thank you. but what about the first one? it uses "implies" sign though. Apr 17, 2016 at 13:02
• Implication means you have to show that if the left side is satisfied, so is the right side. Equivalency also required the other direction. Apr 17, 2016 at 13:37