About next operator duality in LTL

Question

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?

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 ⊨ ¬φ .