A Sahlqvist-style Correspondence Theorem for Linear-time Temporal Logic

TL;DR

This paper extends Sahlqvist's correspondence theory to Linear-time Temporal Logic (LTL), identifying a class of formulas with effective first-order frame correspondents, enhancing understanding of temporal logic's expressiveness.

Contribution

It develops a Sahlqvist-style correspondence theorem specifically for LTL, linking a class of LTL formulas to first-order frame conditions.

Findings

Identifies a class of LTL Sahlqvist formulas with first-order correspondents

Proves the correspondence between LTL Sahlqvist formulas and first-order frame conditions

Enhances the theoretical understanding of LTL's expressiveness and frame semantics

Abstract

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.