<p>I've just found an answer to my question. It is inside Bojańczyk's notes titled &quot;Languages recognised by finite semigroups and their generalisations to objects such as trees and graphs with an emphasis on definability in monadic second-order logic&quot;, more precisely in Section 2.3 here: <a href="https://www.mimuw.edu.pl/%7Ebojan/upload/main-19.pdf" rel="nofollow noreferrer">https://www.mimuw.edu.pl/~bojan/upload/main-19.pdf</a></p>

CC BY-SA 4.0
2021-11-12T10:31:42.647Z
Bojańczyk uses F to denote the strict future, so his F is what I denote with XF.
Bartosz Bednarczyk
CC BY-SA 4.0
2021-11-12T10:31:13.770Z
2021-11-12T10:31:13.770Z
Bartosz Bednarczyk
<p>An algebraic characterisation of the restricted temporal logic (fragment using only next and eventually, but not until) is given in [1].
The expressive power of this fragment is the set of regular languages whose syntactic monoid are locally <span class="math-container">$\cal L$</span>-trivial.</p>
<p>I am not sure of the result you are looking for, but this article probably contains enough material to help you.</p>
<p>[1] J. Cohen, D. Perrin and J.-É. Pin, <a href="https://www.sciencedirect.com/science/article/pii/002200009390005H" rel="nofollow noreferrer">On the expressive power of temporal logic for finite words</a>, <em>J. Comput. System Sci.</em> <strong>46</strong> (1993), 271-294.</p>

CC BY-SA 4.0
2021-05-26T11:23:05.387Z
Thanks Jean. I was of course aware of your paper, however the answer is not there (as I mentioned, I'm looking for this very specific result).
But maybe if you do not know such a reference then it probably does not exists.
Bartosz Bednarczyk
CC BY-SA 4.0
2021-05-26T09:57:08.023Z
2021-05-26T09:57:08.023Z
J.-E. Pin
<p>I'm looking for a reference to the fact that LTL[XF]-definable languages (LTL where only the (strict) finally/future modality is allowed) correspond to the variety <span class="math-container">$\mathbf{R}$</span> (see: <a href="https://core.ac.uk/download/pdf/82409563.pdf" rel="nofollow noreferrer">1</a>).
A similar characterisation is available for LTL[XF,XP], namely the variety <span class="math-container">$\mathbf{DA}$</span>, see: Theorem 11 from <a href="https://www.cs.mcgill.ca/%7Edenis/papers/DA.ps" rel="nofollow noreferrer">2</a>.</p>
<p><a href="https://core.ac.uk/download/pdf/82409563.pdf" rel="nofollow noreferrer">1</a> Brzowoski, Fich: Languages of R-Trivial Monoids <a href="https://core.ac.uk/download/pdf/82409563.pdf" rel="nofollow noreferrer">LINK</a></p>
<p><a href="https://www.cs.mcgill.ca/%7Edenis/papers/DA.ps" rel="nofollow noreferrer">2</a> Tesson, P., Thérien, D.: Diamonds are forever: the variety DA <a href="https://www.cs.mcgill.ca/%7Edenis/papers/DA.ps" rel="nofollow noreferrer">LINK</a></p>
<p>PS: I have an idea how to prove it (by employing the correspondence that R = partially-ordered DFA), but before writing the result it would make sense to check whether this is already known in the literature (although I do not claim any breakthrough).</p>

<fl.formal-languages><regular-language><algebra><linear-temporal-logic>
Reference request: An algebraic characterisation of LTL[XF]-definable word languages
Bartosz Bednarczyk
# Reference request: An algebraic characterisation of LTL[XF]-definable word languages

(Asked by: username_0 on 2021-05-24)

I'm looking for a reference to the fact that LTL[XF]-definable languages (LTL where only the (strict) finally/future modality is allowed) correspond to the variety $\mathbf{R}$ (see: [1](https://core.ac.uk/download/pdf/82409563.pdf)).
A similar characterisation is available for LTL[XF,XP], namely the variety $\mathbf{DA}$, see: Theorem 11 from [2](https://www.cs.mcgill.ca/%7Edenis/papers/DA.ps).

[1](https://core.ac.uk/download/pdf/82409563.pdf) Brzowoski, Fich: Languages of R-Trivial Monoids [LINK](https://core.ac.uk/download/pdf/82409563.pdf)

[2](https://www.cs.mcgill.ca/%7Edenis/papers/DA.ps) Tesson, P., Thérien, D.: Diamonds are forever: the variety DA [LINK](https://www.cs.mcgill.ca/%7Edenis/papers/DA.ps)

PS: I have an idea how to prove it (by employing the correspondence that R = partially-ordered DFA), but before writing the result it would make sense to check whether this is already known in the literature (although I do not claim any breakthrough).

**Tags:** fl.formal-languages, regular-language, algebra, linear-temporal-logic

---

## 2 answers

### Answer by username_0 on 2021-11-12. Score: 2 | Accepted answer

I've just found an answer to my question. It is inside Bojańczyk's notes titled "Languages recognised by finite semigroups and their generalisations to objects such as trees and graphs with an emphasis on definability in monadic second-order logic", more precisely in Section 2.3 here: [https://www.mimuw.edu.pl/~bojan/upload/main-19.pdf](https://www.mimuw.edu.pl/%7Ebojan/upload/main-19.pdf)

> **Comments:**
> **username_0**: Bojańczyk uses F to denote the strict future, so his F is what I denote with XF.  

---

### Answer by username_1 on 2021-05-26. Score: 4

An algebraic characterisation of the restricted temporal logic (fragment using only next and eventually, but not until) is given in [1].
The expressive power of this fragment is the set of regular languages whose syntactic monoid are locally $\cal L$-trivial.

I am not sure of the result you are looking for, but this article probably contains enough material to help you.

[1] J. Cohen, D. Perrin and J.-É. Pin, [On the expressive power of temporal logic for finite words](https://www.sciencedirect.com/science/article/pii/002200009390005H), *J. Comput. System Sci.* **46** (1993), 271-294.

> **Comments:**
> **username_0**: Thanks Jean. I was of course aware of your paper, however the answer is not there (as I mentioned, I'm looking for this very specific result). But maybe if you do not know such a reference then it probably does not exists.  

---

