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

<p><img src="https://i.sstatic.net/qclb5.jpg" alt="LTL Connectives"></p>

<p>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$.<br/></p>

<p>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.<br/></p>

<p>I am confused, any help would be appreciated.</p>

CC BY-SA 3.0
2014-01-26T01:53:46.920Z
Perhaps the paper was wrong. Can you give a link to the paper?
Yuval Filmus
CC BY-SA 3.0
2014-01-26T12:56:35.767Z
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
CC BY-SA 3.0
2014-01-27T04:19:14.233Z
@YuvalFilmus [link](http://www.google.ca/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&ved=0CDAQFjAA&url=http%3A%2F%2Fwww.doc.ic.ac.uk%2F~imh%2Fpapers%2Fhwz.pdf&ei=F93lUouPKsbCoAScjIDIDA&usg=AFQjCNEWO3_kugCME3ZBBMJ91rOz-4yQaw&sig2=9uWRhIrY8yjjLKMk2RMuyQ&bvm=bv.59930103,d.cGU) page 4.
LoMaPh
CC BY-SA 3.0
2014-01-27T04:25:58.190Z
@Sylvain So you are saying $U$ and $\mathcal{U}$ have different semantics? In other words $U$ is *non-strict* and $\mathcal{U}$ is *strict*? If this is the case then my problem is solved.
LoMaPh
CC BY-SA 3.0
2014-01-27T06:17:21.647Z
@LoMaPh It's not a question of which symbol you use, it's a question of which convention you use. The symbols $U,\mathrm{U},\mathbf{U},\mathscr{U},\mathcal{U}$ all have the same meaning, which depends on the semantics you use.
Yuval Filmus
CC BY-SA 3.0
2014-01-27T14:03:31.493Z
Looking at the definition of the truth-relation of p.5 in the paper, the authors do use the strict semantics for $U$.
Klaus Draeger
CC BY-SA 3.0
2014-01-27T23:58:05.140Z
@LoMaPh: As explained by Yuval Filmus, it's a question of convention, and one should always check the definition employed by the authors.  A good rule of thumb is however that papers on verification tend to use the non-strict semantics, while papers considering more general tense or modal logics tend to use the strict semantics.  Also, the strict semantics makes proofs shorter since there is one less case, that of $\mathsf{X}$, to check!
Sylvain
CC BY-SA 3.0
2014-01-29T05:04:05.607Z
@YuvalFilmus: I don't agree with you about this "convention" thing. I believe it's a matter of "definition". $(X, F, G, U ...)$ are all defined clearly in LTL, and when I say $\varphi U \psi$ you know exactly what I mean. The same should apply to $(\bigcirc, \diamondsuit, \Box, \mathcal{U}, ...$). If we want to make a distinction between *strict* and *non-strict* semantics we should use different symbols to avoid ambiguity.
LoMaPh
CC BY-SA 3.0
2014-01-29T14:08:00.483Z
@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
CC BY-SA 3.0
2014-02-05T22:22:38.830Z
@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
<linear-temporal-logic>
What is the difference between LTL connectives X and O?
LoMaPh
# What is the difference between LTL connectives X and O?

(Asked by: username_0 on 2014-01-26)

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

![LTL Connectives](https://i.sstatic.net/qclb5.jpg)

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.

**Tags:** linear-temporal-logic
> **Comments:**
> **username_1**: Perhaps the paper was wrong. Can you give a link to the paper?  
> **username_2**: 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$.  
> **username_0**: @YuvalFilmus [link](http://www.google.ca/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&ved=0CDAQFjAA&url=http%3A%2F%2Fwww.doc.ic.ac.uk%2F~imh%2Fpapers%2Fhwz.pdf&ei=F93lUouPKsbCoAScjIDIDA&usg=AFQjCNEWO3_kugCME3ZBBMJ91rOz-4yQaw&sig2=9uWRhIrY8yjjLKMk2RMuyQ&bvm=bv.59930103,d.cGU) page 4.  
> **username_0**: @Sylvain So you are saying $U$ and $\mathcal{U}$ have different semantics? In other words $U$ is *non-strict* and $\mathcal{U}$ is *strict*? If this is the case then my problem is solved.  
> **username_1**: @LoMaPh It's not a question of which symbol you use, it's a question of which convention you use. The symbols $U,\mathrm{U},\mathbf{U},\mathscr{U},\mathcal{U}$ all have the same meaning, which depends on the semantics you use.  
> **username_3**: Looking at the definition of the truth-relation of p.5 in the paper, the authors do use the strict semantics for $U$.  
> **username_2**: @LoMaPh: As explained by Yuval Filmus, it's a question of convention, and one should always check the definition employed by the authors.  A good rule of thumb is however that papers on verification tend to use the non-strict semantics, while papers considering more general tense or modal logics tend to use the strict semantics.  Also, the strict semantics makes proofs shorter since there is one less case, that of $\mathsf{X}$, to check!  
> **username_0**: @YuvalFilmus: I don't agree with you about this "convention" thing. I believe it's a matter of "definition". $(X, F, G, U ...)$ are all defined clearly in LTL, and when I say $\varphi U \psi$ you know exactly what I mean. The same should apply to $(\bigcirc, \diamondsuit, \Box, \mathcal{U}, ...$). If we want to make a distinction between *strict* and *non-strict* semantics we should use different symbols to avoid ambiguity.  
> **username_1**: @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.  
> **username_2**: @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.  

---

## 0 answers

