I have seen two different sets of connectives for LTL (see the picture):

LTL Connectives

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.

  • $\begingroup$ Perhaps the paper was wrong. Can you give a link to the paper? $\endgroup$ – Yuval Filmus Jan 26 '14 at 1:53
  • 1
    $\begingroup$ 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$. $\endgroup$ – Sylvain Jan 26 '14 at 12:56
  • $\begingroup$ @YuvalFilmus link page 4. $\endgroup$ – LoMaPh Jan 27 '14 at 4:19
  • 1
    $\begingroup$ @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. $\endgroup$ – Yuval Filmus Jan 29 '14 at 14:08
  • 1
    $\begingroup$ @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. $\endgroup$ – Sylvain Feb 5 '14 at 22:22

Your Answer

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

Browse other questions tagged or ask your own question.