  The language of modal logic is capable of expressing first-order conditions
on Kripke frames. The classic result by Henrik Sahlqvist identifies a
significant class of modal formulas for which first-order conditions -- or
Sahlqvist correspondents -- can be find in an effective, algorithmic way.
Recent works have successfully extended this classic result to more complex
modal languages. In this paper, we pursue a similar line and develop a
Sahlqvist-style correspondence theorem for Linear-time Temporal Logic (LTL),
which is one of the most widely used formal languages for temporal
specification. LTL extends the syntax of basic modal logic with dedicated
temporal operators Next X and Until U . As a result, the complexity of the
class of formulas that have first-order correspondents also increases
accordingly. In this paper, we identify a significant class of LTL Sahlqvist
formulas built by using modal operators F , G, X, and U . The main result of
this paper is to prove the correspondence of LTL Sahlqvist formulas to frame
conditions that are definable in first-order language.
