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.
翻译:模式逻辑语言能够表达 Kripke 框架的第一阶条件。 Henrik Sahlqvist 的经典结果确定了一流模式公式,其第一阶条件 -- -- 或Sahlqvist 记者 -- -- 能够以有效的算法方式找到。最近的工作成功地将这一经典结果扩展至更复杂的模式语言。在本文中,我们遵循类似的路线,并开发了Sahlqvist式的线性时空逻辑(LTL),这是用于时间规格的最广泛使用的正式语言之一。LTL将基本模式逻辑的合成扩展至专门的时空操作员下X和U。因此,拥有第一阶记者的公式的复杂程度也相应增加。在本文中,我们确定了使用模式操作员F、G、X和U建造的相当的LTL Sahlqvist公式。本文的主要结果是证明LTL Sahlqvists 公式的对应性,以第阶线语言确定。