0
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – David Richerby Apr 17 '16 at 14:16
  • $\begingroup$ oh. it's "Are the following LTL-formulas true for all paths?" $\endgroup$ – Thang Do Apr 17 '16 at 23:33
1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ thank you. but what about the first one? it uses "implies" sign though. $\endgroup$ – Thang Do Apr 17 '16 at 13:02
  • $\begingroup$ Implication means you have to show that if the left side is satisfied, so is the right side. Equivalency also required the other direction. $\endgroup$ – Andreas T Apr 17 '16 at 13:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.