4
$\begingroup$

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

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$ May 26 at 11:23
2
$\begingroup$

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

$\endgroup$
1
  • 1
    $\begingroup$ Bojańczyk uses F to denote the strict future, so his F is what I denote with XF. $\endgroup$ Nov 12 at 10:31

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.