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

Rui Li  Sorbonne Université
Paris, France  Francesco Belardinelli  Department of Computing
Imperial College London
United Kingdom

###### Abstract

The language of modal logic is capable of expressing first-order conditions on
Kripke frames. For instance, the modal formula $(\Box q\to q)$ is valid in
exactly the reflexive frames, where reflexivity $\forall xR(x,x)$ is a first-
order condition. 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.

###### keywords:

Linear Temporal Logic; Sahlqvist formula; Correspondence Theory; Kripke frame.

111 Undergraduate Research Opportunities Program (UROP) fund, Department of
Computing, Imperial College London, summer 2021

##  1 Introduction

One of the most well-known results in the model theory of modal logic is that
modal languages are rich enough to express (first-order) conditions on Kripke
frames. Results along this direction have been known as Correspondence Theory
[15, 3]. For instance, the modal formula $(\Box q\to q)$ is valid in exactly
the reflexive frames, where reflexivity $\forall xR(x,x)$ is a first-order
condition. Since the 1970’s, much research in modal logic has been devoted to
identifying classes of formulas for which such first-order correspondents
exist, including algorithms for their automatic computation. The classic
result by H. Sahlqvist [13] identifies a significant class of modal formulas
for which first-order conditions – or Sahlqvist correspondents – can be found
in an effective, algorithmic way. Since then, correspondence theory has been
successfully extended to more complex and expressive modal languages [8, 14,
16].

#### Contribution.

In this paper we develop a Sahlqvist-style correspondence theorem for Linear-
time Temporal Logic (LTL), which is nowadays one of the most widely-used
formal languages for temporal specification [1]. LTL extends the syntax of
basic modal logic with dedicated temporal operators Next $X$ and Until $U$.
Formulas in LTL are interpreted on infinite words – or paths – representing
the execution of a reactive system. Interestingly, Kamp [12] proved that every
temporal operator on a class of continuous, strict linear orderings that is
definable in first-order logic is expressible in terms of Since $S$ and Until
$U$. As a result, the complexity of the class of modal formulas that have
first-order correspondents also increases accordingly. In this paper, we
identify a significant class of LTL formulas built by using temporal operators
Eventually $F$, Always $G$, Next $X$, and Until $U$. To accommodate the
enhanced expressiveness, we extend the class of Sahlqvist formulas with some
additional conditions. To facilitate the treatment, we introduce the
“intermediate” logic LTL’, which is more expressive than LTL, but whose syntax
is closer to that of normal modal logics. Our main result is to prove the
correspondence of such Sahlqvist formulas in LTL to frame conditions that are
definable in a first-order language.

#### Related Work.

As we mentioned above, Sahlqvist correspondence theorem has been extended in a
number of different directions, mainly considering more and more expressive
modal languages. For instance, in [8] a correspondence theorem is proved for
temporal modal logic, whereas in [16, 2] similar results are proved for the
$\mu$-calculus and modal fixed-point logic respectively. It has to be remarked
that these works extend the proof given in [14], rather than Sahlqvist’s
original result in [13]. More recently, correspondence results have been
proved for hybrid logics [7], distributive modal logics [9], and polyadic
modal logics [10]. Some efforts have also been applied to the problem of
finding more general and efficient algorithms to compute first-order
correspondents of modal formulas [5, 6, 17], including [14] mentioned earlier.
Still, to the best of our knowledge, no comparable result has been proved for
the kind of temporal logics used in the specification and verification of
reactive and distributed systems [1]. We deem such a result of interest to
theoreticians and practitioners in modal logics alike.

#### Structure of the Paper.

In Sec. 2 we introduce the syntax and semantics of LTL as well as the
auxiliary logic LTL’, and define correspondence between modal and first-order
formulas. In Sec. 3 we define the class of Sahlqvist formulas for LTL and
LTL’, and provide a few preliminary results. Finally, Sec. 4 is devoted to the
main result of this paper, namely the proof of the correspondence theorem.

##  2 Preliminaries: Linear-time Temporal Logic

In this section we provide background information about Linear-time Temporal
Logic (LTL) [1, 11]. Specifically, in Sec. 2.1 we introduce its syntax, as
well as the syntax of the auxiliary language LTL’. Then, in Sec. 2.2 we
interpret both languages on infinite system executions. Finally, in Sec. 2.3
we define their standard translations [3].

###  2.1 LTL: Syntax

We fix a set $Prop$ of atomic propositions (or atoms) and define the formulas
$\phi$ in Linear-time Temporal Logic in Backus-Naur form as follows:

$\displaystyle\phi$ $\displaystyle=$ $\displaystyle
Prop\mid\bot\mid\top\mid\neg\phi\mid\phi\wedge\phi\mid\phi\vee\phi\mid
G\phi\mid F\phi\mid X\phi\mid\phi U\phi$

where $G$ is read “always”, $F$ “eventually”, $X$ is the Next operator, and
$U$ is the Until operator [1]. The Boolean connectives $\to$ and
$\leftrightarrow$ can be introduced as standard. Operators $F$ and $G$ can be
defined in terms of $U$, but for convenience we assume them as primitive.

In this paper, we consider also a variant of LTL, that we call LTL’. Let $W$
be a set of possible worlds (which serves as the model of LTL and LTL’). Fix
$W$, then we define the syntax of LTL’ w.r.t. this particular $W$ as follows:

$\displaystyle\phi$ $\displaystyle=$ $\displaystyle
Prop\mid\bot\mid\top\mid\neg\phi\mid\phi\wedge\phi\mid\phi\vee\phi\mid
G\phi\mid F_{x}\phi\mid\widehat{G}_{w,w^{\prime}}\phi\mid X\phi$

where $w$ and $w^{\prime}$ ($w\neq w^{\prime}$) are states in $W$, and $x$ is
a variable over states. We will also use the following convention:
$w<w^{\prime}$. If it were the case that $w^{\prime}<w$, then it suffices to
switch the place of $w$ and $w^{\prime}$ and write
$\widehat{G}_{w,w^{\prime}}$ as $\widehat{G}_{w^{\prime},w}$. Remark that
$\widehat{G}_{w,w}$ is not in the language of LTL’.

######  Remark 2.1.

Although states are semantical notions, the symbols representing them can be
treated syntactically. The difference between the use of symbols in $F_{x}$
and $\widehat{G}_{w,w^{\prime}}$ is that $x$ in the former is a variable that
ranges over possible states, of which $w$ and $w^{\prime}$ in the latter are
members. In this paper, $x,y,z,\ldots$ would be used to denote variables,
whereas $w,w^{\prime},s,s^{\prime},\ldots$ would denote states that are fixed
in the context. Also, $u,u^{\prime}$ and $v,v^{\prime}$ can be used
interchangeably, whenever the context is clear.

###  2.2 LTL: Semantics

To provide a semantics to LTL, we consider transition systems $T=(S,\to)$,
where $S$ is a set of states, and the transition relation $\to\ \subseteq
S\times S$ is a binary relation on $S$. Normally, the relation $\to$ is
assumed to be serial: for all $s\in S$, there exists $s^{\prime}\in S$ such
that $s\to s^{\prime}$. Then, a path in a transition system is an infinite
sequence $s_{1},s_{2},s_{3},\ldots$, where for all $i\in\mathbb{N}$, $s_{i}\to
s_{i+1}$.

We now define models for LTL. Let $W$ be the set of all paths in $T$; whereas
$\leqslant$, $<$, and $\mathbf{S}$ are all binary relations on $W$, introduced
as follows. Let $w=s_{1},s_{2},s_{3},\ldots$ and
$v=s^{\prime}_{1},s^{\prime}_{2},s^{\prime}_{3},\ldots$ be paths in $T$, then
$w\leqslant v$ iff for some $i\geqslant 1$, $s_{i}=s_{1}^{\prime}$ and for all
$j>0$, $s_{i+j}=s^{\prime}_{1+j}$, that is, $v$ is a subpath of $w$ starting
from some index $i$. Then, $w<v$ iff $w\leqslant v$ and $w\neq v$. Further,
$\mathbf{S}$ means successor: $v=\mathbf{S}(w)$ iff for all $i>0$,
$s^{\prime}_{i}=s_{i+1}$. When the context is clear, we sometimes simply write
$R(w,v)$ for $w<v$, $w\leqslant v$ or $v=\mathbf{S}(w)$.

A model for LTL is a tuple $M=(T,h)$, where $T$ is a transition system, and
$h:Prop\to 2^{S}$ is an assignment function from atoms to set of states in
$S$. We lift the assignment $h$ from states to paths so that $w\in h(q)$ iff
$s_{1}\in h(q)$.

######  Definition 2.2 (Satisfaction).

Given a model $M$, path $w$, and formula $\phi$ in LTL’, the satisfaction
relation $\vDash$ is defined as follows:

$(M,w)\vDash q$ | iff | $w\in h(q)$
---|---|---
$(M,w)\vDash\neg\phi$ | iff | $(M,w)\not\vDash\phi$
$(M,w)\vDash\phi\wedge\varphi$ | iff |  $(M,w)\vDash\phi$ and $(M,w)\vDash\varphi$
$(M,w)\vDash\phi\vee\varphi$ | iff |  $(M,w)\vDash\phi$ or $(M,w)\vDash\varphi$
$(M,w)\vDash G\phi$ | iff |  for all $v\in W$, $w\leqslant v$ implies $(M,v)\vDash\phi$
$(M,w)\vDash F_{x}\phi$ | iff |  for some $x\in W$, $w\leqslant x$ and $(M,x)\vDash\phi$
$(M,w)\vDash\widehat{G}_{w,w^{\prime}}\phi$ | iff |  for all $u\in W,w\leqslant u<w^{\prime}$ implies $(M,u)\vDash\phi$
$(M,w)\vDash X\phi$ | iff |  $v=\mathbf{S}(w)$ and $(M,v)\vDash\phi$

Hereafter we use $w\vDash\phi$ as an abbreviation for $(M,w)\vDash\phi$. We
write $[\phi]^{h}_{w}=1$ iff $(M,w)\vDash\phi$ for $M=(T,h)$. For future
references, we precisely define below assignments for arbitrary formulas.

######  Definition 2.3 (Assignment).

Let $T=(S,\to)$ be a transition system, and $h:Prop\to 2^{W}$ an assignment
function as before. We extend the domain of $h$ from the set of atoms $Prop$
to the set $Form$ of all formulas:

$h:Form\to 2^{W}$

such that $h(\phi)$ is defined as $\\{w\in S\mid(T,h,w)\vDash\phi\\}$.

To provide an interpretation for LTL, we replace the clause for
$\widehat{G}_{w,w^{\prime}}$ with a clause for the Until operator $U$, as
follows:

$(M,w)\vDash\phi U\phi^{\prime}$ | iff | for some $u\geqslant w$, $(M,u)\vDash\phi^{\prime}$, and
---|---|---
|  | for all $v\in W$, $w\leqslant v<u$ implies $(M,v)\vDash\phi$

LTL also replaces $F_{x}$ with the operator $F$, where the variable path is no
longer shown in the syntax. But its semantics remains the same.

Now it is possible to translate LTL into LTL’.

######  Definition 2.4.

Let $Form_{LTL}$ be the class of all LTL formulas and $Form_{LTL^{\prime}}$ be
the class of all LTL’ formulas. Let

$\displaystyle\tau:Form_{LTL}$ $\displaystyle\to Form_{LTL^{\prime}}$

be the translation from LTL to LTL’ defined as follows:

$q$ |  $\mapsto$ | $q$
---|---|---
$\neg\phi$ |  $\mapsto$ | $\neg\tau(\phi)$
$\phi_{1}\wedge\phi_{2}$ |  $\mapsto$ | $\tau(\phi_{1})\wedge\tau(\phi_{2})$
$\phi_{1}\vee\phi_{2}$ |  $\mapsto$ | $\tau(\phi_{1})\vee\tau(\phi_{2})$
$G\phi$ |  $\mapsto$ | $G\tau(\phi)$
$F\phi$ |  $\mapsto$ | $F_{x}\tau(\phi)$
$X\phi$ |  $\mapsto$ | $X\tau(\phi)$
$\phi_{1}U\phi_{2}$ |  $\mapsto$ |  $F_{x}(\tau(\phi_{2})\land\widehat{G}_{w,x}\tau(\phi_{1}))$

where $x$ is a path variable, and $w$ is the path at which we aim to evaluate
the formula.

######  Remark 2.5 (Variable Convention).

In the conjunctive and disjunctive clause, if a path variable $x$ appears in
both $\tau(\phi_{1})$ and $\tau(\phi_{2})$, then in
$\tau(\phi_{1}\land\phi_{2})$ we replace $x$ in $\tau(\phi_{2})$ by another
path variable $x^{\prime}$ that do occur in either $\tau(\phi_{1})$ or
$\tau(\phi_{2})$.

If $x$ in $\tau(\phi_{1}U\phi_{2})$ appears in $\tau(\phi_{1})$ or
$\tau(\phi_{2})$, then we replace the occurrences of $x$ in $\tau(\phi_{1})$
and $\tau(\phi_{2})$ by $x_{1}$ and $x_{2}$.

######  Lemma 2.6.

Let $\tau$ be the translation from LTL to LTL’ in Def. 2.4. Then an LTL
formula and its translation w.r.t. $\tau$ are semantically equivalent.

######  Proof 2.7.

The proof makes use of structural induction on the formula. We only consider
the case for the LTL formula $\phi=\phi_{1}U\phi_{2}$. Let $w$ be any path,
and $\phi$ is evaluated at $w$. The translation $\tau(\phi)$ of $\phi$ at $w$
is

$\exists x(w<x\land\tau(\phi_{2})\land\forall u(w\leqslant
u<x\to\tau(\phi_{1})))$

By induction hypothesis, $x\vDash\tau(\phi_{2})\Leftrightarrow
x\vDash\phi_{2}$ and $u\vDash\tau(\phi_{1})\Leftrightarrow u\vDash\phi_{1}$.
So $w\vDash\tau(\phi)\Leftrightarrow w\vDash\phi$. Since $w$ is arbitrary,
$\phi$ and $\tau(\phi)$ are semantically equivalent.

###  2.3 Standard Translation and Correspondence

The standard translation of formulas in LTL’ mirrors their semantics. For
every atom $q\in Prop$, we introduce a predicate symbol $Q$. For an arbitrary
formula $\phi$ in LTL’, we denote the first-order standard translation of
$\phi$ at $w$ as $ST_{w}(\phi)$, and it is inductively defined as follows:

######  Definition 2.8 (Standard Translation).

The standard translation $ST_{w}(\phi)$ of formula $\phi$ at path $w$ is
inductively defined as case of $\phi$:

$q$ | : | $Q(w)$
---|---|---
$\neg\phi$ | : | $\neg ST_{w}(\phi)$
$\phi\wedge\varphi$ | : | $ST_{w}(\phi)\wedge ST_{w}(\varphi)$
$\phi\vee\varphi$ | : | $ST_{w}(\phi)\vee ST_{w}(\varphi)$
$G\phi$ | : | $\forall v(w\leqslant v\to ST_{v}(\phi))$
$F_{x}\phi$ | : | $\exists x(w\leqslant x\wedge ST_{x}(\phi))$
$\widehat{G}_{s,s^{\prime}}\phi$ | : | $\forall v(s\leqslant v<s^{\prime}\to ST_{v}(\phi))$
$X\phi$ | : |  $ST_{\mathbf{S}(w)}(\phi)$

To simplify the notation, instead of saying that $ST_{w}(\phi)$ is the
standard translation of $\phi$ at $w$, we say that it is the standard
translation of $\phi[w]$. Then, the second-order standard translation of
$\phi[w]$ is obtained by prefixing universal quantification for every
predicate $Q_{1},Q_{2},\ldots,Q_{k}$ in $ST_{w}(\phi)$. There is no
abbreviated notation for this second-order standard translation. Whenever the
context is clear, we will also call it the standard translation. For the most
part, we work with the second-order standard translation.

Since the models for LTL’ and for first-order logic are the same (they are
both relational structure), we say that $(M,w)\vDash\phi$, where $\phi$ is a
first order formula. However, when it comes to the second-order formulas, the
models have to be modified. In second-order logic, quantification over
predicates (sets) is allowed, and the domain of a predicate is determined by
the assignment $h$, i.e., $dom(Q)=h(q)$. Therefore, assignments in transition
systems are equivalent to (universal) quantification over predicates in
second-order logic.

######  Definition 2.9 (Correspondence).

Let $T=(S,\to)$ be a transition system, and $w\in W$. An LTL’ formula
$\phi(q_{1},q_{2},\ldots,q_{k})$ is said to (locally) correspond to a formula
$\varphi$ in second order logic at $w$ whenever $\phi$ are $\varphi$ are both
evaluated to be true at $w$ in $T$.

The following lemma shows why local correspondence is defined the way it is. A
proof can be obtain by a straightforward induction on the structure of formula
$\phi$.

######  Lemma 2.10.

An LTL’ formula $\phi(q_{1},q_{2},\ldots,q_{k})$ (locally) corresponds to
$\forall Q_{1}\forall Q_{2}\ldots\forall Q_{k}ST_{w}(\phi)$ at $w$, where
$ST_{w}(\phi)$ is the (first-order) standard translation of $\phi[w]$.

######  Remark 2.11.

In light of this lemma, we will be using semantics and standard translation
interchangeably in this paper.

The main result we prove in this paper can be stated informally as follows:
there is a collection of LTL formulas $\phi$, such that for all paths $w$, the
local correspondent $\phi[w]$ of $\phi$ at $w$ can be expressed as a first-
order formula. This is the basic content of Sahlqvist correspondence theorem,
which will be stated later on in more precise terms. Note that, although the
standard translation is only defined for LTL’, the translation for LTL and its
semantics can be defined in a similar manner, where the main difference is the
following clause:

$ST_{w}(\phi U\phi^{\prime}$) | = |  $\exists u,w\leqslant u\wedge ST_{u}(\psi)\wedge(\forall v,w\leqslant v<u\to ST_{v}(\phi^{\prime}))$
---|---|---

##  3 Sahlqvist Formulas for LTL

In this section, we introduce two particular types of formulas that play key
roles in the construction of Sahlqvist formulas: boxed formulas and negative
formulas. We prove the monotonicity theorem in Sec. 3.2 and introduce
Sahlqvist formulas for LTL in Sec. 3.3.

###  3.1 Boxed Formulas

In standard modal logic, boxed formulas are defined as a sequence of boxes
$\Box$ followed by an atomic formula, i.e., they have the form $\Box\ldots\Box
q$ for a possible empty sequence of boxes. The sequence of boxes can be
denoted as $\Box^{n}$, for $n\in\mathbb{N}$, whose semantics is similar to the
one for a single box: $w\vDash\Box^{n}q$ iff for all $v$, $R^{n}(w,v)$ implies
$v\vDash q$, where $R^{n}$ is not difficult to construct (see Lemma 3.2).

Similarly for LTL’, the syntactic operators having universally quantified
implication as semantics can be integrated into the LTL’ boxed formulas for
the same reason. We denote an arbitrary boxed formula as
$\boxplus^{n}q=\boxplus\ldots\boxplus q$, where each $\boxplus$ is a distinct
element from $\\{G,\widehat{G}_{w,w^{\prime}},X\\}$ (i.e., the set of boxed
operators). Now we define the corresponding accessibility relation.

######  Definition 3.1 (Accessibility Relation $R_{\boxplus^{n}}$).

We define the accessibility relation $R_{\boxplus^{n}}$ by induction on
$n\in\mathbb{N}$.

Base case: if $n=0$, i.e. $\boxplus^{n}q=q$, then $R^{0}(w,v)$ iff $w=v$.

Inductive cases: let $R_{\boxplus^{n}}$ be defined, then

  * •

If $\boxplus^{n+1}q=G\boxplus^{n}q$, then $R_{\boxplus^{n+1}}(w,v)$ iff for
some $u\in W$, $w\leqslant u$ and $R_{\boxplus^{n}}(u,v)$.

  * •

If $\boxplus^{n+1}q=X\boxplus^{n}q$, then $R_{\boxplus^{n+1}}(w,v)$ iff
$R_{\boxplus^{n}}(\mathbf{S}(w),v)$.

  * •

If $\boxplus^{n+1}q=\widehat{G}_{s,s^{\prime}}\boxplus^{n}q$, then
$R_{\boxplus^{n+1}}(w,v)$ iff for some $u\in W$, $s\leqslant u<s^{\prime}$ and
$R_{\boxplus^{n}}(u,v)$.

Whenever the context is clear, we use $R^{n}$ to denote $R_{\boxplus^{n}}$.

By Def. 3.1 we can prove the following auxiliary result concerning boxed
formulas.

######  Lemma 3.2 (Boxed Formulas Lemma).

Let $\boxplus^{n}q$ be an LTL’ boxed formula with $n$ boxed operators
appearing in front of atom $q$ (with $n$ possibly equal to 0). Then
$w\vDash\boxplus^{n}q$ iff for all $v\in W$, $R^{n}(w,v)$ implies $v\vDash q$.

######  Proof 3.3.

We prove this lemma by induction on $n$. The base case for $n=0$ is immediate:
$w\vDash q$ iff for all $v$, $w=v$ implies $v\vDash q$, that is $R^{0}(w,v)$.
Now suppose that the lemma holds for an arbitrary $n$, i.e.,
$w\vDash\boxplus^{n}q$ iff for all $v\in W$, $R^{n}(w,v)$ implies $v\vDash q$.
We have to show that $w\vDash\boxplus^{n+1}q$ iff for all $v\in W$,
$R^{n+1}(w,v)$ implies $v\vDash q$. We discuss by case the options for the
first boxed operator $\boxplus_{0}$ in $\boxplus^{n+1}q$.

For $\boxplus_{0}=\widehat{G}_{s,s^{\prime}}$,
$w\vDash\boxplus_{0}\boxplus^{n}q$ iff for every $v$, $s\leqslant
v<s^{\prime}$ implies $v\vDash\boxplus^{n}q$. By induction hypothesis,
$w\vDash\boxplus_{0}\boxplus^{n}q$ iff for every $v$, $s\leqslant
v<s^{\prime}$ implies that for every $u$ such that $R^{n}(v,u)$, $u\vDash q$.
We want to show that this is equivalent to: for all $u$, $R^{n+1}(w,u)$
implies $u\vDash q$. Suppose $w\vDash\boxplus_{0}\boxplus^{n}q$ is the case;
fix $u_{0}$. Let $v_{0}$ be a path such that $s\leqslant v_{0}<s^{\prime}$, if
$R^{n}(v_{0},u_{0})$, then $u_{0}\vDash q$ by assumption. Since $u_{0}$ is
arbitrary, we get $R^{n+1}(w,u_{0})$ for every $u_{0}$. Conversely, assume
that for every $u$, if for any $v$ such that $s\leqslant v<s^{\prime}$ and
$R^{n}(v,u)$, then $u\vDash q$. Fix $v_{0}$ such that $s\leqslant
v_{0}<s^{\prime}$. Then take an arbitrary $u_{0}$. If $R^{n}(v_{0},u_{0})$,
then by assumption, $u_{0}\vDash q$. Since $v_{0}$ is arbitrary, for every
$v_{0}$, $s\leqslant v_{0}<s^{\prime}$ and $R^{n}(v_{0},u_{0})$ imply
$u_{0}\vDash q$ for arbitrary $u_{0}$, as desired. This concludes the case for
$\boxplus_{0}=\widehat{G}_{s,s^{\prime}}$. The proofs for the cases
$\boxplus_{0}=G$ and $\boxplus_{0}=X$ are similar.

######  Remark 3.4.

This lemma shows that the standard translation of every boxed formula
$\boxplus^{n}q$ can be written in the form of $\forall v,R(w,v)\to Q(v)$ using
a unique relation $R$. This construction will be invaluable in defining the
minimal assignment for Sahlqvist formulas.

###  3.2 Negative Formulas

Similarly to standard modal logic, LTL’ positive formulas $\phi$ can be
defined as the ones constructed from atoms using $\wedge$, $\vee$, $G$,
$F_{x}$, $\widehat{G}_{w,w^{\prime}}$, $X$ only:

$\displaystyle\phi=Prop\mid\bot\mid\top\mid\phi\wedge\phi\mid\phi\vee\phi\mid
G\phi\mid F_{x}\phi\mid\widehat{G}_{w,w^{\prime}}\phi\mid X\phi$

An LTL’ negative formula has one of the two following forms:

  1. (1)

$\neg\phi$, where $\phi$ is an LTL’ positive formula;

  2. (2)

$\widehat{G}_{w,w^{\prime}}N$, where $N$ is an LTL’ negative formula.

For example, $GF_{x}q$ is a positive formula,
$\widehat{G}_{w,w^{\prime}}\neg(q_{1}\wedge q_{2})$ is a negative formula;
whereas $F_{x}(\widehat{G}_{w,x}q_{1}\wedge\neg q_{2})$ and $\neg X\neg Xq$
are neither positive nor negative.

######  Remark 3.5.

Although negative formulas are defined to be a syntactic notion, the proof of
the correspondence theorem is semantical. Therefore, whenever possible, if a
formula is semantically equivalent to a negative formula, then we shall also
call this formula negative. For example, if $N$ is a negative formula, then
$GN$ is also a negative formula.

######  Lemma 3.6 (Monotonocity).

Let $\phi$ be an LTL’ positive formula, $q_{1},\ldots,q_{k}$ be the atoms
appearing in $\phi$, and $h_{1}$ and $h_{2}$ be assignments.

If for all $q_{j}$, $h_{1}(q_{j})\subseteq h_{2}(q_{j})$, then
$h_{1}(\phi)\subseteq h_{2}(\phi)$.

######  Proof 3.7.

The proof is by induction on the structure of $\phi$. The base case for
$\phi=q$ is immediate. Now suppose that $\phi_{1}(q_{1},\ldots,q_{k})$ and
$\phi_{2}(q_{1},\ldots,q_{k})$ are two LTL’ positive formulas that satisfy the
statement of the lemma. We show that $\phi_{3}(q_{1},\ldots,q_{k})$, which is
built from $\phi_{1}$ and $\phi_{2}$ using one of the operators from
$\\{\wedge,\vee,G,F_{x},\widehat{G}_{w,w^{\prime}},X\\}$ also satisfies the
statement. If either $\phi_{3}=G\phi_{1}$, or
$\phi_{3}=\widehat{G}_{w,w^{\prime}}\phi_{1}$, or $\phi_{3}=F_{x}\phi_{1}$ or
$\phi_{3}=X\phi_{1}$, since $h_{1}(\phi_{1})\subseteq h_{2}(\phi_{1})$, it is
easy to see that $h_{1}(\phi_{3})\subseteq h_{2}(\phi_{3})$. It is also
immediate to check that if $h_{1}(\phi_{1})\subseteq h_{2}(\phi_{1})$ and
$h_{1}(\phi_{2})\subseteq h_{2}(\phi_{2})$, then
$h_{1}(\phi_{1}\wedge\phi_{2})\subseteq h_{2}(\phi_{1}\wedge\phi_{2})$ and
$h_{1}(\phi_{1}\vee\phi_{2})\subseteq h_{2}(\phi_{1}\vee\phi_{2})$. This
concludes the induction.

######  Corollary 3.8.

Let $N$ be an arbitrary LTL’ negative formula, $q_{1},q_{2},\ldots,q_{k}$ are
the atomic variables appearing in $N$. Let $h_{1}$ and $h_{2}$ be two random
assignments. If for all $q_{j}$, $h_{1}(q_{j})\subseteq h_{2}(q_{j})$, then
$h_{2}(N)\subseteq h_{1}(N)$.

######  Proof 3.9.

If $N$ is of the first form of LTL’ negative formula, then the statement
follows directly from the Lemma 3.6. Now suppose $N$ is of the second form,
that is, $N=\widehat{G}_{s,s^{\prime}}N^{\prime}$, where $N^{\prime}$ is
negative. Let $w$ be any path, then $ST_{w}(N)$ is

$\neg\exists y(s\leqslant y<s^{\prime}\wedge ST_{y}(\neg N^{\prime}))$

Remark that the part in the scope of the negation is in fact a positive
fragment in the interpretation of LTL’ formulas. By monotonocity lemma, if for
all $q_{j}$ occurring in $N^{\prime}$, $h_{1}(q_{j})\subseteq h_{2}(q_{j})$,
then $h_{1}(\neg N^{\prime})\subseteq h_{2}(\neg N^{\prime})$. In other words,
if $(T,h_{1},y)\vDash ST_{y}(\neg N^{\prime})$, then $(T,h_{2},y)\vDash
ST_{y}(\neg N^{\prime})$. Therefore, if there is a path $y$ between $s$ and
$s^{\prime}$ such that $y\vDash ST_{y}(\neg N^{\prime})$ and $y\in h_{1}(\neg
N^{\prime})$, then there is also such a path for $h_{2}$. So if
$(T,h_{1},x)\vDash\exists y(s\leqslant y<s^{\prime}\wedge ST_{y}(\neg
N^{\prime}))$, then $(T,h_{2},x)\vDash\exists y(s\leqslant y<s^{\prime}\wedge
ST_{y}(\neg N^{\prime}))$. It follows that $h_{2}(N)\subseteq h_{1}(N)$, as
desired.

###  3.3 Sahlqvist Formulas

The main goal of this paper is to find a significant class of Sahlqvist
formulas for LTL, we therefore define them here. Then, we will show that this
construction can be simplified by using the auxiliary language LTL’.

A formula $A_{LTL}$ is an LTL boxed formula if it is a sequence of boxes
followed by an atom, where each element of the sequence belongs to
$\\{X,G\\}$. A formula is an LTL positive formula if it can be constructed
from all logical symbols and modal operators of LTL except negation; a formula
$N_{LTL}$ is an LTL negative formula if it is the negation of an LTL positive
formula.

We now define LTL Sahlqvist formulas.

######  Definition 3.10 (LTL Sahlqvist Formulas).

Suppose $\beta$ is an LTL boxed formula or negative formula. Then we define
LTL untied formula as follows:

$\displaystyle\phi$ $\displaystyle=$ $\displaystyle A_{LTL}\mid
N_{LTL}\mid\beta U\phi\mid\phi\land\phi$

The LTL Sahlqvist formulas are the conjunction of negations of LTL untied
formulas.

######  Remark 3.11.

In the definition of LTL untied formula, $F\phi$ can be retrieved using $\top
U\phi$.

As for LTL’, its Sahlqvist formulas are defined as follows:

######  Definition 3.12 (LTL’ Sahlqvist Formulas).

An LTL’ untied formula is constructed from LTL’ boxed formulas and LTL’
negative formulas using only $F_{x}$ and conjunction:

$\displaystyle\phi$ $\displaystyle=$ $\displaystyle A_{LTL^{\prime}}\mid
N_{LTL^{\prime}}\mid\phi\wedge\phi\mid F_{x}\phi$

As before, LTL’ Sahlqvist formulas are the conjunctions of negations of LTL’
untied formulas.

##  4 Correspondence Theorem

In this section we present the proof of the correspondence theorem for LTL. By
embedding LTL Sahlqvist formulas into LTL’ Sahlqvist formulas, we only need to
show that the theorem holds for the latter. We start by showing that the
translation $t$ from LTL to LTL’ in Sec. 2.2 preserves Sahlqvist formulas.
Then we introduce the main lemma crucial to the theorem. Finally, a detailed
proof of the theorem is provided.

###  4.1 Translation

We show that LTL Sahlqvist formulas can be translated into LTL’ Sahlqvist
formulas.

######  Lemma 4.1.

Let $\tau$ be the translation from LTL to LTL’ in Def. 2.4. Then the following
claims are true:

  1. $(1)$

The translation of an LTL untied formula w.r.t. $\tau$ is an LTL’ untied
formula.

  2. $(2)$

An LTL untied formula and its translation w.r.t. $\tau$ are semantically
equivalent.

######  Proof 4.2.

  1. $(1)$

The claim can be proved using structural induction on the formula. We only
consider the case for the LTL untied formula $\phi=\beta U\psi$, where $\psi$
is also LTL untied. Let $w$ be any path, and $\phi$ is evaluated at $w$. By
definition 2.4,
$\tau(\phi)=F_{x}(\tau(\psi)\land\widehat{G}_{w,x}\tau(\beta))$. If $\beta$ is
an LTL boxed formula, then $\tau(\beta)$ is also an LTL’ boxed formula; so
$\widehat{G}_{w,x}\tau(\beta)$ is also an LTL’ boxed formula. If $\beta$ is an
LTL negative formula, then $\tau(\beta)$ is an LTL’ negative formula; so
$\widehat{G}_{w,x}\tau(\beta)$ is also an LTL’ negative formula. Therefore,
$\widehat{G}_{w,x}\tau(\beta)$ is untied. By induction hypothesis,
$\tau(\psi)$ is an LTL’ untied formula, hence
$F_{x}(\tau(\psi)\land\widehat{G}_{w,x}\tau(\beta))$ is LTL’ untied.

  2. $(2)$

It follows immediately from Lemma 2.6.

Whenever two formulas are semantically equivalent, they have the same frame
conditions. Therefore, having shown that for each LTL Sahlqvist formula, a
semantically equivalent LTL’ formula exists and is also Sahlqvist, we can
conclude the following lemma:

######  Lemma 4.3.

If every LTL’ Sahlqvist formula locally corresponds to a first order formula,
then every LTL Sahlqvist formula locally corresponds to a first order formula.

###  4.2 Main Lemma

In this section, we prove the main lemma, essential to the proof of the
correspondence theorem for LTL’. The LTL’ untied formulas are solely built
from boxed formula and negative formula, hence intuitively in order to find
first-order correpondents for LTL’ Sahlqvist formula $\phi$, it suffices to
find an assignment $h_{0}$ that satisfies the following for every boxed
formula $A$ and every negative formula $N$ in $\phi$:

$\displaystyle\exists Q,ST_{w}(A)$ $\displaystyle\iff$ $\displaystyle
ST_{w}(A)[Q_{0}]\text{ and }$ $\displaystyle\exists Q,ST_{w}(N)$
$\displaystyle\iff$ $\displaystyle ST_{w}(N)[Q_{0}]$

where $Q_{0}(x)$ is true iff $x\in h_{0}(q)$. $Q_{0}$ is called minimal
predicate.

######  Definition 4.4 (Substitution).

We first fix the notation on substitution in the minimal assignment. Let
$\phi(q)$ be a formula and $h_{0}(q)$ be its minimal assignment for atom $q$
(to be defined subsequently). Let $Q_{0}$ be its corresponding minimal
predicate. Suppose $t$ to be a symbol occurring in the expression of $Q_{0}$.
Then we use $[t^{\prime}/t]Q_{0}$ to denote the substitution of $t^{\prime}$
for all occurrences of $t$ in $Q_{0}$.

We can now introduce the notion of minimal assignment.

######  Definition 4.5 (Minimal assignment).

Let $\phi(q_{1},\ldots,q_{k})$ be an LTL’ untied formula; let $w$ be a path.
For every variable $q_{j}$ occurring in $\phi$, we define the minimal
assignment $h_{0}(q_{j})$ of $\phi$ at $w$ by induction on the structure of
formula.

Base cases: Suppose that $\phi(q_{j})$ is a boxed formula and its standard
translation at $w$ is $\forall v(R_{j}(w,v)\to Q_{j}(v))$, then the minimal
assignment for $q_{j}$ is $h_{0}(q_{j})=\\{u\in W\mid R_{j}(w,u)\\}$.

Suppose $\phi$ is a negative formula, then $h_{0}(q_{j})=\emptyset$ (and
$Q_{j0}(w)\equiv\bot$ for every $w$).

Inductive cases:

If the minimal assignment for $\phi_{1}(q_{1},\ldots,q_{k})$ and
$\phi_{2}(q_{1},\ldots,q_{k})$ are respectively $h_{0}^{1}$ and $h_{0}^{2}$,
then the minimal assignment for $\phi_{1}\wedge\phi_{2}$ is $h_{0}^{1}\cup
h_{0}^{2}$.

If the minimal assignment for $\phi$ at $v$ is $h_{0}$, then the minimal
assignment for $F_{x}\phi$ at $w$ is $[x/v]h_{0}$.

If the minimal assignment for $\phi$ at $v$ is $h_{0}$, then the minimal
assignment for $X\phi$ at $w$ is $[\textbf{S}(w)/v]h_{0}$.

Suppose the minimal assignment for $\phi$ at $v$ is $h_{0}$. The minimal
predicates for $q_{j}$ occurring in $\phi$ is defined as
$Q_{j0}(z)\Leftrightarrow z\in h_{0}(q_{j})$. Then the minimal assignment
$h_{0}^{\prime}$ for $\widehat{G}_{s,s^{\prime}}\phi$ at $w$ is defined as
$h_{0}^{\prime}(q_{j})=\\{y\in W\mid\exists x(s\leqslant
x<s^{\prime}\wedge[x/v]Q_{j0}(y))\\}$ for every $q_{j}$.

######  Remark 4.6.

The minimal assignment for an LTL untied formula can be obtained by
translating it into an LTL’ untied formula.

Let $A$ be of the form $\boxplus^{n}q$ and $w\vDash A$ iff $\forall
x(R^{n}(w,x)\to Q(x))$. Let $Q_{0}(x)$ be $R^{n}(w,x)$, we claim that $\exists
Q\forall x(R^{n}(w,x)\to Q(x))$ iff $\forall x(R^{n}(w,x)\to Q_{0}(x))$. The
proof of this claim is immediate: the right hand side is always true; the
right-to-left implication is also always true. It turns out that for every
Sahlqvist formula, the recursive construction of the minimal assignment will
always produce a first-order correspondent to its second-order translation. In
particular, we need to show how the occurrences of negative formulas in a
Sahlqvist formula can be given such first-order correspondents via minimal
assignment.

######  Lemma 4.7 (Main Lemma).

Let $E$ be an LTL’ untied formula, $w$ is a state, and $h_{0}$ is the minimal
assignment of $E$ at $w$ (possibly empty). Let $h$ be an assignment. If there
exists an assignment $g$ and a state $w$ such that $[E]^{g}_{w}=1$, then the
following are equivalent:

  1. $(a)$

For all $q_{j}\in\\{q_{1},\ldots,q_{k}\\}$, $h_{0}(q_{j})\subseteq h(q_{j})$.

  2. $(b)$

$[B]^{h}_{w}=1$.

where $B$ is defined is obtained from $E$ by replacing all occurrences of
negative formulas $N_{1},N_{2},\ldots,N_{m}$ in $E$ by $\top$.

######  Proof 4.8.

We proceed by induction on the structure of the formula.

For the base cases, we suppose that $E$ is either an LTL’ boxed formula $A$ or
an LTL’ negative formula $N$. If $E$ is a negative formula $N$, then $h_{0}$
is empty, therefore ($a$) must be true. As $B$ becomes $\top$, ($b$) is true,
hence ($a$) and ($b$) are equivalent. If $E$ is a boxed formula $A$, then
$B=A$. As only one atom appears in $A$, let it be $q$. Since $A(q)$ is true at
$w$, $Q_{0}(x)$ is $R(w,x)$ where $R$ is obtained from the standard
translation of $A(q)$. As $h(q)=\\{x\in W\mid Q(x)\\}$ and $h_{0}(q)=\\{x\in
W\mid Q_{0}(x)\\}=\\{x\in W\mid R(w,x)\\}$, $h_{0}(q)\subseteq h(q)$ is
therefore just saying that for all $x$, $(R(w,x)\to Q(x))$. But this is
exactly what ($b$) says. Namely, $[E]^{h}_{w}=1$ iff $w\vDash A$ iff $\forall
x(R(w,x)\to Q(x))$. Therefore ($a$) and ($b$) are equivalent.

There are two cases for inductive steps: $E_{1}\wedge E_{2}$, $F_{x}E$.

Case $(i)$: Suppose that there is an assignment $g$ making $E=E_{1}\wedge
E_{2}$ true at $w$. Then $g$ also makes both $E_{1}$ and $E_{2}$ true at $w$.
By induction hypothesis, $(a)\Leftrightarrow(b)$ holds for both $B_{1}$ and
$B_{2}$. Let $h$ be an arbitrary assignment. Let $h_{0}^{1},h_{0}^{2},h_{0}$
denote the minimal assignments for $E_{1},E_{2},E$. We know
$h_{0}^{1},h_{0}^{2}\subseteq h_{0}$. Also, for every atomic formula $q_{j}$
in $E$, it must be in either $E_{1}$ or $E_{2}$. Thus if for every $q_{j}$,
$h_{0}(q_{j})\subseteq h(q_{j})$, then $[B_{1}]^{h}_{w}=[B_{2}]^{h}_{w}=1$. So
$(a)\Rightarrow(b)$ holds for $B$. Now assume $[B]^{h}_{w}=1$. As before,
$[B_{1}]^{h}_{w}=1$ and $[B_{2}]^{h}_{w}=1$. So for every atom $q_{j}$, if
$q_{j}$ occurs in $B_{i}$, then $h_{0}^{i}(q_{j})\subseteq h(q_{j})$
($i\in\\{1,2\\}$). By definition of $h_{0}$, it is also the case that
$h_{0}^{1}(q_{j})\cup h_{0}^{2}(q_{j})=h_{0}(q_{j})\subseteq h(q_{j})$ for
every $q_{j}$. Hence $(b)\Rightarrow(a)$ holds for $B$.

Case $(ii)$: Suppose that there is an assignment $g$ making $F_{x}E$ true at
$w$. Then there is a state $x\geqslant w$ at which $g$ makes $E$ true. By
induction hypothesis, $(1)$ and $(2)$ are equivalent:

  1. $(1)$

For every atomic variable $q_{j}$ in $E$, $h_{0}(q_{j})\subseteq h(q_{j})$.

  2. $(2)$

$[B]^{h}_{x}=1$.

If $[B]^{h}_{x}=1$, then $[F_{x}B]^{h}_{w}=1$; so
$(1)\Rightarrow[F_{x}B]^{h}_{w}=1$. Also, if
$(a)\Rightarrow[F_{x}B]^{h}_{w}=1$, then there is a state $y$ at which
$[B]^{h}_{y}=1$. Since $x$ in $(1)\Leftrightarrow(2)$ is arbitrary, we get
$(1)$ back. Therefore, $(a)\Leftrightarrow(b)$ holds for $F_{x}B$.

###  4.3 Correspondence Theorem

It finally only remains to show that all LTL’ Sahlqvist formulas $S$ have
first-order correspondents.

######  Theorem 4.9 (LTL Correspondence Theorem).

Let $S$ be an LTL’ Sahlqvist formula, then the local correspondent of $S[w]$
can be expressed in first-order terms, i.e., $\forall Q_{1},\ldots,\forall
Q_{k},ST_{w}(S(q_{1},\ldots,q_{k}))$ has a first-order correspondent.

######  Proof 4.10.

Let $S=\bigwedge_{i=1}^{m}\neg E_{i}$ where $E_{i}$ are LTL’ untied formulas.
The second order standard translation of $S[x]$ is $\bigwedge_{i=1}^{m}\forall
Q_{1},\forall Q_{2},\ldots,\forall Q_{k},\neg ST_{x}(E_{i})$. However, to
simplify the task, we can work with each conjunctive clause $E_{i}$
individually. In addition, we are going to work with the first correspondence
of its negation:

$\exists Q_{1},\exists Q_{2},\ldots,\exists Q_{k},ST_{x}(E_{i})$

We proceed by induction on the complexity of the formula.

Base case: Let’s write the formula for the base case as follows:

$\bigwedge\limits_{j=1}^{m}\oplus_{a_{j}}C_{j}$

where $C_{j}$ is either an LTL’ boxed formula or an LTL’ negative formula, and
$a_{j}$ is the number of $F_{x}$ appearing in front of each $C_{j}$.

For each $j$, if $C_{j}$ is a boxed formula, then the standard translation of
$\oplus_{a_{j}}C_{j}[x]$ can be written as

$\exists x_{1},\ldots,\exists x_{a_{j}}(R_{j1}(x,x_{j1})\wedge\ldots\wedge
R_{ja_{j}}(x_{a_{j}-1},x_{a_{j}})\wedge(\forall y(R_{j}(x_{a_{j}},y)\to
Q_{j}(y))))$

However, if $C_{j}$ is a negative formula, we do not need to write down the
standard translation of $\oplus_{a_{j}}C_{j}[x]$. We can omit $\oplus_{a_{j}}$
because it can be part of the LTL’ negative formula. Therefore, the standard
translation of $E_{i}[x]$ can be written as

$\bigwedge\limits_{f=1}^{t}(\exists x_{1},\ldots,\exists
x_{a_{f}}\bigwedge\limits_{s=1}^{a_{f}}R_{fs}(x_{s-1},x_{s})\wedge(\forall
y(R_{f}(x_{a_{f}},y)\to
Q_{f}(y))))\wedge\bigwedge\limits_{l=1}^{r}ST_{x}(N_{l})$ (1)

where $t+r=m$. Here, $C_{1},\ldots,C_{m}$ are
$A_{1},\ldots,A_{t},N_{1},\ldots,N_{r}$.

For the first conjunct of this formula, the following two formulas are
equivalent by definition of minimal assignments, where $Q_{f0}$ is the minimal
predicate of the atomic variable $Q_{f}$:

$\displaystyle\exists Q_{1},\ldots,Q_{k}\bigwedge\limits_{f=1}^{t}(\exists
x_{1},\ldots,x_{a_{f}}\bigwedge\limits_{s=1}^{a_{f}}R_{fs}(x_{s-1},x_{s})\wedge(\forall
y(R_{f}(x_{a_{f}},y)\to Q_{f}(y))))\ \ \ \ \ $ (2)
$\displaystyle\bigwedge\limits_{f=1}^{t}(\exists x_{1},\ldots,\exists
x_{a_{f}}\bigwedge\limits_{s=1}^{a_{f}}R_{fs}(x_{s-1},x_{s})\wedge(\forall
y(R_{f}(x_{a_{f}},y)\to Q_{f0}(y))))$ (3)

For the second conjunct of (1) $\bigwedge_{l=1}^{r}ST_{x}(N_{l})$, notice that
$E_{i}$ satisfies the condition of the main lemma: namely, there exists an
assignment under which it is satisfied at $x$. Also, let $h$ be an arbitrary
assignment, if $[E_{i}]^{h}_{x}=1$, then $[B_{i}]^{h}_{x}=1$, where $B_{i}$ is
obtained from $E_{i}$ by substituting $\top$ for every occurrence of negative
formulas in $E_{i}$. It follows that for all
$q_{j}\in\\{q_{1},\ldots,q_{k}\\}$, $h_{0}(q_{j})\subseteq h(q_{j})$. As
$N_{l}$ are negative formulas, by the monotonocity lemma for negative formulas
(Corollary 3.8), $h(N_{l})\subseteq h_{0}(N_{l})$. Therefore, for all $h$, if
$[N_{l}]^{h}_{x}=1$, then $[N_{l}]^{h_{0}}_{x}=1$. From this, we can easily
prove that (4) and (5) below are equivalent.

$\displaystyle\exists Q_{1},\exists Q_{2},\ldots,\exists
Q_{k},\bigwedge\limits_{l=1}^{r}ST_{x}(N_{l})$ (4)
$\displaystyle\bigwedge\limits_{l=1}^{r}ST_{x}(N_{l})[Q_{10},Q_{20},\ldots,Q_{k0}]$
(5)

From the equivalence (2) $\wedge$ (4)$\iff$(3) $\wedge$ (5), $(1)$ obtains its
first order correspondent by substituting minimal predicate
$Q_{10},\ldots,Q_{k0}$ for $Q_{1},\ldots,Q_{k}$, hence the quantifiers over
them can also be dropped. Therefore, $\forall Q_{1},\ldots,\forall
Q_{k},ST_{x}(S)\equiv\bigwedge_{i=1}^{m}\neg(\exists Q_{1},\ldots,\exists
Q_{k},ST_{x}(E_{i}))$ also has first-order correspondent
$\bigwedge_{i=1}^{m}\neg ST_{x}(E_{i})[Q_{10}/Q_{1},\ldots,Q_{k0}/Q_{k}]$.

Now we proceed to the inductive steps. There are two cases:

Case 1: Suppose the untied formula $E$ is of the form $F_{y}C$, where $C$ is
an untied formula. If $E$ is true at the state $x$, then there is a state $y$
such that $x\leqslant y$ and $C$ is true at $y$. By induction hypothesis, we
can find the minimal predicates for $C$ which is
$\vec{Q_{0}^{C}}=Q_{10},\ldots,Q_{k0}$ such that

$\exists\vec{Q}ST_{y}(C)\Leftrightarrow[\vec{Q_{0}^{C}}/\vec{Q}]ST_{y}(C)$

Since the minimal predicate for $E$ is $Q_{0}^{E}=[x/y]\vec{Q_{0}^{C}}$, we
get

$\exists\vec{Q}ST_{x}(E)\Leftrightarrow[\vec{Q_{0}^{E}}/\vec{Q}]ST_{x}(E)$

Case 2: Suppose $E=E_{1}\wedge E_{2}$ where $E_{1}$ and $E_{2}$ are both
untied. Let $q_{1},\ldots,q_{k}$ be the atoms appearing in both $E_{1}$ and
$E_{2}$. Then by induction hypothesis, we have two sets of minimal predicates
$\\{Q_{10}^{1},\ldots,Q_{k0}^{1}\\}$ and $\\{Q_{10}^{2},\ldots,Q_{k0}^{2}\\}$.
The minimal predicates for $E$ are defined as

$Q_{j0}=Q_{j0}^{1}\vee Q_{j0}^{2}$

By induction hypothesis, we know that

$\exists\vec{Q}ST_{x}(E_{1})\Leftrightarrow[\vec{Q_{0}^{1}}/\vec{Q}]ST_{x}(E_{1})$
$\exists\vec{Q}ST_{x}(E_{2})\Leftrightarrow[\vec{Q_{0}^{2}}/\vec{Q}]ST_{x}(E_{2})$

We want to show that

$\exists\vec{Q}ST_{x}(E)\Leftrightarrow[\vec{Q_{0}}/\vec{Q}]ST_{x}(E)$

$(\Rightarrow):$ Assume $\exists\vec{Q}ST_{x}(E)$. Then,
$\exists\vec{Q}ST_{x}(E_{1})$ and $\exists\vec{Q}ST_{x}(E_{2})$ hold. So both
$[\vec{Q_{0}^{1}}/\vec{Q}]ST_{x}(E_{1})$ and
$[\vec{Q_{0}^{2}}/\vec{Q}]ST_{x}(E_{2})$ are the case. Since
$h_{0}^{1}\subseteq h_{0}$, $[\vec{Q_{0}}/\vec{Q}]ST_{x}(E_{1})$ is also true.
Similarly, so is $[\vec{Q_{0}}/\vec{Q}]ST_{x}(E_{2})$. Therefore,
$[\vec{Q_{0}}/\vec{Q}]ST_{x}(E)$.

$(\Leftarrow):$ $\vec{Q_{0}}$ is an instance of $\vec{Q}$.

This concludes the proof of the Sahlqvist correspondence theorem for LTL’.
First-order correspondents for LTL can be found by first translating the LTL
Sahlqvist formulas into LTL’.

###  4.4 Example

The above proof of the correspondence theorem also yields an algorithm for
translating the frame condition of an LTL Sahlqvist formula into a first order
formula. We do not elaborate the algorithm here. But the algorithm for the
Sahlqvist formula for standard modal logic applies with appropriate
modification. Let’s see an example for LTL involving the Until operator. Let
$\varphi=\neg(\neg qUq)$, readers can easily verify that it is an LTL
Sahlqvist formula. The standard translation of $\varphi[w]$ is

$\neg\exists Q(\exists v,w\leqslant v\wedge(\forall u,v\leqslant u\to
Q(u))\wedge(\forall z,w\leqslant z<v\to\neg Q(z)))$

Taking the minimal assignment $Q(x)\equiv v\leqslant x$, we reduce the
$ST_{w}(\varphi)$ to

$\neg(\exists v,w\leqslant v)$ (6)

Formula (6) identifies the empty class of structures, as there exists no class
of frames over which formula (6) can be true at any state.

##  5 Conclusions

In this paper we introduced a notion of Sahlqvist formula for the Linear-time
Temporal Logic LTL and proved a Sahlqvist correspondence theorem for this
language. In some respects, they can be viewed as a generalization of the same
result for standard modal logic, in the sense that we allow states to index
temporal operators $F_{x}$ and $G_{x,x^{\prime}}$. One should also remark that
LTL’ Sahlqvist formulas are in fact very similar to the Sahlqvist formulas of
standard modal logic to the extent that the proof for the completeness
property [3, 8] for Sahlqvist formulas almost identically applies to the LTL’
Sahlqvist formulas.

Further research direction may consists in finding an even larger class of LTL
Sahlqvist formulas. For standard modal logic, Chagrova [4] has proved that it
is undecidable if an arbitrary formula has a first-order correspondent.
Therefore, the same problem is equally undecidable for LTL as the latter is
strictly more expressive than the former.

## References

  * [1] Baier, C. and J.-P. Katoen, “Principles of Model Checking (Representation and Mind Series),” The MIT Press, 2008.
  * [2] Bezhanishvili, N. and I. Hodkinson, _Sahlqvist theorem for modal fixed point logic_ , Theoretical Computer Science 424 (2012), p. 1–19.
  * [3] Blackburn, P., M. de Rijke and Y. Venema, “Modal Logic,” Cambridge Tracts in Theoretical Computer Science 53, Cambridge University Press, 2002.
  * [4] Chagrova, L. A., _An undecidable problem in correspondence theory_ , J. Symb. Logic 56 (1991), p. 1261–1272.
URL https://doi.org/10.2307/2275473

  * [5] Conradie, W., V. Goranko and D. Vakarelov, _Algorithmic correspondence and completeness in modal logic. i. the core algorithm sqema_ , Logical Methods in Computer Science 2 (2006).
URL http://dx.doi.org/10.2168/LMCS-2(1:5)2006

  * [6] Conradie, W., A. Palmigiano and S. Sourabh, _Algebraic modal correspondence: Sahlqvist and beyond_ , Journal of Logical and Algebraic Methods in Programming 91 (2017), pp. 60–84.
URL https://www.sciencedirect.com/science/article/pii/S2352220816301341

  * [7] Conradie, W. and C. Robinson, _On sahlqvist theory for hybrid logics_ , Journal of Logic and Computation 27 (2017), pp. 867–900.
  * [8] Gabbay, D. M., I. M. Hodkinson and M. A. Reynolds, “Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 1: Mathematical Foundations,” Oxford University Press, 1994.
  * [9] Gehrke, M., H. Nagahashi and Y. Venema, _A sahlqvist theorem for distributive modal logic_ , Annals of Pure and Applied Logic 131 (2005), pp. 65–102.
URL https://www.sciencedirect.com/science/article/pii/S0168007204000880

  * [10] Goranko, V. and D. Vakarelov, _Sahlqvist formulas unleashed in polyadic modal languages_ , in: _Advances In Modal Logic: Volume 3_ , World Scientific, 2002 pp. 221–240.
  * [11] Huth, M. R. A. and M. D. Ryan, “Logic in Computer Science: Modelling and Reasoning about Systems,” Cambridge University Press, Cambridge, England, 2000\.
  * [12] Kamp, H., “Tense Logic and the Theory of Linear Order,” Ph.D. thesis, Ucla (1968).
  * [13] Sahlqvist, H., _Completeness and correspondence in the first and second order semantics for modal logic**this paper is a revised version of parts of the author’s cand. real.-thesis submitted to the university of oslo, dept. of mathematics, spring 1973._ , in: S. Kanger, editor, _Proceedings of the Third Scandinavian Logic Symposium_ , Studies in Logic and the Foundations of Mathematics 82, Elsevier, 1975 pp. 110–143.
URL https://www.sciencedirect.com/science/article/pii/S0049237X08707286

  * [14] Sambin, G. and V. Vaccaro, _A new proof of sahlqvist’s theorem on modal definability and completeness_ , J. Symb. Log. 54 (1989), pp. 992–999.
  * [15] Van Benthem, J., “Correspondence Theory,” Springer Netherlands, Dordrecht, 1984 pp. 167–247.
URL https://doi.org/10.1007/978-94-009-6259-0_4

  * [16] van Benthem, J., N. Bezhanishvili and I. M. Hodkinson, _Sahlqvist correspondence for modal mu-calculus_ , Stud Logica 100 (2012), pp. 31–60.
  * [17] Zhao, Z., A. Palmigiano and W. Conradie, _Sahlqvist via translation_ , Logical Methods in Computer Science 15 (2019).