A Sahlqvist-style Correspondence Theorem for Linear-time Temporal Logic
This work addresses a foundational problem in formal logic for researchers in temporal logic and modal logic, but it is incremental as it builds on existing extensions of the Sahlqvist theorem.
The paper tackles the problem of extending the Sahlqvist correspondence theorem to Linear-time Temporal Logic (LTL), identifying a class of LTL formulas that correspond to first-order frame conditions, and proves this correspondence effectively.
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.