English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

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