Linear temporal logic

Definition

Let $AP$ be a set of atomic propositions. The formulas of linear temporal logic over $AP$ are given by the grammar $$\varphi ::= p \mid \neg \varphi \mid \varphi \land \varphi \mid X \varphi \mid \varphi \, U \, \varphi, \qquad p \in AP.$$ A formula is interpreted on an infinite word $w = w_0 w_1 w_2 \cdots$ with each $w_i \subseteq AP$. For $i \ge 0$, let $w^{i} = w_i w_{i+1} \cdots$ be the suffix of $w$ from position $i$. The relation $w \models \varphi$ is defined by induction on $\varphi$:

1. $w \models p$ if and only if $p \in w_0$;
2. $w \models \neg\varphi$ if and only if $w \not\models \varphi$, and $w \models \varphi \land \psi$ if and only if $w \models \varphi$ and $w \models \psi$;
3. $w \models X\varphi$ if and only if $w^{1} \models \varphi$;
4. $w \models \varphi \, U \, \psi$ if and only if there is $j \ge 0$ with $w^{j} \models \psi$ and $w^{i} \models \varphi$ for all $0 \le i < j$.

Let $s$ be a state of a Kripke structure with a total transition relation. Then $s$ satisfies $\varphi$ if the word of labels of every infinite path from $s$ satisfies $\varphi$.