# What is the difference between LTL connectives X and O?

I have seen two different sets of connectives for LTL (see the picture): I have learned LTL by the connectives of the first column ($X, F, G,$ ...). The table (from Wikipedia) says that the connectives in the second column have the same meaning as the connectives of the first column and are just different symbols. But recently I read a paper and saw this equivalence: $\bigcirc\varphi\equiv\bot\mathcal{U}\varphi$.

I know that $X\varphi\equiv\bot U\varphi$ does not hold in LTL (because $\bot$ does not hold in any state, so $\bot U\varphi$ can be true only if $\varphi$ is true in the current state and no other state in the future. But this is different from $X\varphi$ which says $\varphi$ is true in the next state). But that table says $X$ and $\bigcirc$, and $U$ and $\mathcal{U}$ have the same meaning.

I am confused, any help would be appreciated.

• Perhaps the paper was wrong. Can you give a link to the paper? – Yuval Filmus Jan 26 '14 at 1:53
• If you employ the strict semantics for until, i.e. $w,i\models\psi\mathbin{\mathsf{U}}\varphi$ iff $\exists j>i$, $w,j\models\varphi$ and $\forall i<k<j$, $w,k\models\psi$, then indeed $\mathsf{X}\varphi\equiv\bot\mathbin{\mathsf{U}}\varphi$. – Sylvain Jan 26 '14 at 12:56
• @YuvalFilmus link page 4. – LoMaPh Jan 27 '14 at 4:19
• @LoMaPh Your belief is unfortunately wrong. There is no agreed-upon convention for which calligraphic style corresponds to strict and which to non-strict. It could have been done this way, but it isn't. – Yuval Filmus Jan 29 '14 at 14:08
• @LoMaPh: Some papers write $\mathsf{XU}$ for strict until, but it's not so fortunate in general, since $\mathsf{X}\equiv\bot$ on dense time frames. What you seem to take as a "clear definition" is actually a particular case of a more general framework. This particular convention is often taken for granted in the verification literature, but it's not the only field where LTL is studied. – Sylvain Feb 5 '14 at 22:22