I'm learning LTL (linear temporal logic) and we learned that a model $M$ and a starting position $q_0$ satisfies a LTL formula $\psi$ iff for every path $\pi$ starting at $q_0$ it is true that $\pi \models \psi$.

I also learned that the Next ($X$) operator is dual to its negation meaning $X \neg p = \neg Xp$. This confuses me, because in the simple example below, $Xp$ doesn't hold, hence $\neg Xp$ holds, and from the equality, $X \neg p$ holds, but that means that every path starting from $q_0$, $\neg p$ holds, which clearly isn't true.

Where does my logic doesn't hold?

enter image description here


1 Answer 1


Your error is in the sentence "Xp doesn't hold, hence ¬Xp holds". In your example, neither Xp nor ¬Xp hold for the model: of the two possible traces in the model, the upper branch only satisfies Xp, and the lower branch only satisfies ¬Xp. Neither Xp nor ¬Xp hold for all traces in the model, so neither of these LTL formulas holds for the model. TL;DR M ⊨/ φ does not imply M ⊨ ¬φ .


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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