Reference request: An algebraic characterisation of LTL[XF]-definable word languages

Question

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). A similar characterisation is available for LTL[XF,XP], namely the variety $\mathbf{DA}$, see: Theorem 11 from 2.

1 Brzowoski, Fich: Languages of R-Trivial Monoids LINK

2 Tesson, P., Thérien, D.: Diamonds are forever: the variety DA LINK

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).

Answer 1

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, J. Comput. System Sci. 46 (1993), 271-294.

Answer 2

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