World's most popular travel blog for travel bloggers.

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

, ,
Problem Detail:

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.

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