# What is the Kripke semantic for a linear temporal logic?

I've read that in general for a modal formula P, a world w and a Kripke frame ⟨W,R⟩

w⊨□P if and only if for every u∈W, if wRu then u⊢P

In case of LTL, being a modal logic, I assumed that the worlds are different moments in time and the relation R is the chain of "arrows" between those moments. However, in this case the semantic of □ in LTL would not correspond to the definition above.

What did I misunderstood?

In LTL, you don't have $$\diamond$$ and $$\Box$$, but you have $$X$$ and $$U$$, meaning next and until, respectively.

In LTL, every world has a unique successor.

Next is defined as $$w \models X \phi$$ if $$w' \models \phi$$, where $$w'$$ is the successor of $$w$$.

Until is defined as follows: $$w \models \phi U \psi$$ if there exists $$w''$$ such that $$w'' \models \psi$$ and for every $$w'$$ between $$w$$ and $$w''$$, we have that $$w' \models \phi$$.

Now, from these modalities, we can construct other modalities, such as globally, $$G \phi$$, and finally, $$F \phi$$. It is common to denote

• $$X \phi$$ as $$\bigcirc \phi$$
• $$F \phi$$ as $$\diamond \phi$$
• $$G \phi$$ as $$\Box \phi$$.
• you start with "In LTL, you don't have ⋄ and ◻" and finish with "It is common to denote 𝐹𝜙 as ⋄𝜙 and 𝐺𝜙 as ◻𝜙". Isn't it up to personal preference? Commented Mar 7, 2023 at 9:41
• I would rather call it convention than personal preference, and in temporal logics, the convention is using the alphabetic modalities, e.g. $F$, $X$, $G$, and $AF$, $EF$, $AG$, $EG$, $A (\phi U \psi)$ and $E (\phi U \psi)$. Meaning that CTL, CTL*, ATL and LTL are defined on the language using $A,E$ (when applicable), and $F,G,X$, and $U$. Then we throw in the boxes and diamonds as syntactic sugar, if you will. Commented Mar 7, 2023 at 12:05
• I'd remove the first sentence. It's an opinion at best and not supported by facts. Manna and Pnueli use $\bigcirc$, $\square$, $\diamond$ in their articles and reference books. Lamport's TLA doesn't have a next operator but he uses $\square$ and $\diamond$.
– Kai
Commented Mar 7, 2023 at 21:02

tl;dr The accessibility relation needs to be the reflexive transitive closure of what you had in mind.

Details: Let $$P$$ be a set of atomic proposition. Write $$\Sigma$$ for $$P$$'s powerset. Write $$T$$ for $$\Sigma^{\mathbb{N}}$$ (infinite traces).

A Kripke frame $$\langle W, R\rangle$$ where the meaning of formulas agrees with that of the fragment of LTL using just $$P$$, boolean connectives, $$\square$$ and $$\diamond$$ would consist of $$W = T\times\mathbb{N}$$ (ie infinite traces with an index) and $$R = \{~((\sigma,i),(\sigma,k))~|~\sigma\in T\wedge i\leq k\in\mathbb{N}~\}$$.