# Linear temporal logic (LTL)

Based on [C. Baier, J.-P. Katoen: Principles of model checking, Ch. 5](https://mitpress.mit.edu/9780262026499/principles-of-model-checking/).

Linear temporal logic captures the logic of linear as in **non-branching** time. We will model discrete time as given by the natural numbers $\mathbb N$ with the standard partial order $\leq$:

We will be interested in paths over time such as:

The temporal aspect of logical propositions will be created by so-called **modalities**, i.e., operators on formulas that can be understood as changing the **mode** of truth.

In classical logic, we can say:
* "*The formula $p \land \lnot q$ is true.*"

In [modal](https://en.wikipedia.org/wiki/Modal_logic) [logic](https://plato.stanford.edu/entries/logic-modal/), we can express, for example:

* "*The formula $p \land \lnot q$ is **sometimes** true.*"
* "*The formula $p \land \lnot q$ is **necessarily** true.*"
* "*The formula $p \land \lnot q$ is **believed to be** true.*"
* ...

There are various modal logics for various modes of truth. **Temporal logics** relativize the notion of truth with respect to **time**.

## Syntax of LTL

Let $A$ be a set of atomic propositions. LTL formulas over $A$ is the language generated by the following grammar in [Backus--Naur form (BNF)](https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form):

$$\varphi := \top \;\; | \;\; p \;\; | \;\; \varphi_1 \land \varphi_2 \;\; |\;\; \lnot \varphi \;\; |\;\; \bigcirc \varphi \; \; |\; \;\varphi_1 \mathbf{U} \varphi_2$$
where $a \in A$ is an atomic proposition, or *atom* for short.

Here:

* $\top$ is the true atom
* $p$ is an arbitrary atom
* $\land$ is conjunction ("AND")
* $\lnot$ is negation ("NOT")
* $\bigcirc$ is the "next" modality
* $\mathbf{U}$ is the "until" modality

We should think about the modalities $\bigcirc$ and $\mathbf{U}$ as follows:

* $\bigcirc \varphi$ (read: "*next $\varphi$*"") is true now if $\varphi$ is true **next**
* $\varphi_1 \mathbf{U} \varphi_2$ (read: "*$\varphi_1$ until $\varphi_2$*") is true now if there is some future moment at which $\varphi_2$ holds and $\varphi_1$ holds at all moments **until** then.

We will make this precise shortly.

As usually in propositional logic, we can define the following connectives from just $\land$ and $\lnot$:
* disjunction $\lor$ ("OR")
* implication $\to$
* biimplication $\leftrightarrow$
* exclusive disjunction $\oplus$ ("XOR")

We can also derive the following modal connectives:
* $\lozenge \varphi := \top \mathbf{U} \varphi$
This models "$\varphi$ is true **eventually**", "$\varphi$ is true sometimes (in the future)."

* $\square \varphi := \lnot \lozenge \lnot \varphi$
This models "$\varphi$ is **always** true."

We can also combine these models to yield:

* $\square \lozenge \varphi$: "$\varphi$ holds **infinitely often**"
* $\lozenge \square \varphi$: "$\varphi$ holds **eventually forever**"

All this gives the following exemplary picture:

([Quiver](https://q.uiver.app/#q=WzAsNDksWzAsMCwiXFx0ZXh0e2F0b20gfSBwOiJdLFsxLDAsIntcXGNvbG9ye3JlZH1wfSJdLFsyLDAsIlxcdGV4dHthbnl9Il0sWzMsMCwiXFx0ZXh0e2FueX0iXSxbNCwwLCJcXHRleHR7YW55fSJdLFs1LDAsIlxcdGV4dHthbnl9Il0sWzYsMCwiXFxjZG90cyJdLFswLDEsIlxcdGV4dHtuZXh0IH0gXFxiaWdjaXJjIHA6Il0sWzEsMSwiXFx0ZXh0e2FueX0iXSxbMiwxLCJ7XFxjb2xvcntyZWR9cH0iXSxbMywxLCJcXHRleHR7YW55fSJdLFs0LDEsIlxcdGV4dHthbnl9Il0sWzUsMSwiXFx0ZXh0e2FueX0iXSxbNiwxLCJcXGNkb3RzIl0sWzAsMiwiXFx0ZXh0e3VudGlsIH0gcCBcXG1hdGhiZntVfSBxOiJdLFsxLDIsIntcXGNvbG9ye3JlZH1wIFxcbGFuZCBcXG5lZyBxfSJdLFsyLDIsIntcXGNvbG9ye3JlZH1wIFxcbGFuZCBcXG5lZyBxfSJdLFszLDIsIntcXGNvbG9ye3JlZH1wIFxcbGFuZCBcXG5lZyBxfSJdLFs0LDIsIntcXGNvbG9ye3JlZH1xfSJdLFs1LDIsIlxcdGV4dHthbnl9Il0sWzYsMiwiXFxjZG90cyJdLFswLDMsIlxcdGV4dHtldmVudHVhbGx5IH0gXFxEaWFtb25kIHA6Il0sWzEsMywiXFx0ZXh0e2FueX0iXSxbMiwzLCJcXHRleHR7YW55fSJdLFszLDMsIlxcdGV4dHthbnl9Il0sWzQsMywie1xcY29sb3J7cmVkfXB9Il0sWzUsMywiXFx0ZXh0e2FueX0iXSxbNiwzLCJcXGNkb3RzIl0sWzAsNCwiXFx0ZXh0e2Fsd2F5cyB9IFxcQm94IHA6Il0sWzEsNCwie1xcY29sb3J7cmVkfXB9Il0sWzIsNCwie1xcY29sb3J7cmVkfXB9Il0sWzMsNCwie1xcY29sb3J7cmVkfXB9Il0sWzQsNCwie1xcY29sb3J7cmVkfXB9Il0sWzUsNCwie1xcY29sb3J7cmVkfXB9Il0sWzYsNCwiXFxjZG90cyJdLFswLDUsIlxcdGV4dHthbHdheXMgZXZlbnR1YWxseSB9IFxcQm94XFxEaWFtb25kIHA6Il0sWzEsNSwiXFx0ZXh0e2FueX0iXSxbMiw1LCJ7XFxjb2xvcntyZWR9cH0iXSxbMyw1LCJcXHRleHR7YW55fSJdLFs0LDUsIntcXGNvbG9ye3JlZH1wfSJdLFs1LDUsIlxcdGV4dHthbnl9Il0sWzYsNSwiXFxjZG90cyJdLFswLDYsIlxcdGV4dHtldmVudHVhbGx5IGFsd2F5cyB9IFxcRGlhbW9uZFxcQm94IHA6Il0sWzEsNiwiXFx0ZXh0e2FueX0iXSxbMiw2LCJcXHRleHR7YW55fSJdLFszLDYsIntcXGNvbG9ye3JlZH1wfSJdLFs0LDYsIntcXGNvbG9ye3JlZH1wfSJdLFs1LDYsIntcXGNvbG9ye3JlZH1wfSJdLFs2LDYsIlxcY2RvdHMiXSxbMSwyXSxbMiwzXSxbMyw0XSxbNCw1XSxbNSw2XSxbOCw5XSxbOSwxMF0sWzEwLDExXSxbMTEsMTJdLFsxMiwxM10sWzE1LDE2XSxbMTYsMTddLFsxNywxOF0sWzE4LDE5XSxbMTksMjBdLFsyMiwyM10sWzIzLDI0XSxbMjQsMjVdLFsyNSwyNl0sWzI2LDI3XSxbMjksMzBdLFszMCwzMV0sWzMxLDMyXSxbMzIsMzNdLFszMywzNF0sWzM2LDM3XSxbMzcsMzhdLFszOCwzOV0sWzM5LDQwXSxbNDAsNDFdLFs0Myw0NF0sWzQ0LDQ1XSxbNDUsNDZdLFs0Niw0N10sWzQ3LDQ4XV0=))

# Word semantics for LTL

Let $\varphi$ be an LTL formula over a set of atoms $A$. We call the following set the \emph{LT property induced by $\varphi}:

$$ \mathrm{Words}(\varphi) = \{ \sigma \in (2^A)^\omega \; | \; \sigma \models \varphi \}$$

Recall that $2^A$ is the set of boolean valuations on $A$, i.e., functions $A \to \{0,1\}$ (which can be identified with the power set $\mathcal P(A)$). Consequently, $(2^A)^\omega$ is the set of sequences $\sigma = \sigma_1 \sigma_2 \sigma_3 \ldots$ of valuations $\sigma_i : A \to \{0,1\}$. Now, $\mathrm{Words}(\varphi)$ consists of those sequences $\sigma$ that *satisfy* $\varphi$ in the sense of the satisfaction relation $\models \subseteq (2^A)^\omega \times \mathrm{LTL}$, defined to be the smallest relation satisfying:

1. $\sigma \models \top$
2. $\sigma \models p$ iff $\sigma_0 \models p$ (meaning $p \in \sigma_0$ in the subset view)
3. $\sigma \models \varphi_1 \land \varphi_2$ iff $\sigma \models \varphi_1$ and $\sigma \models \varphi_2$
4. $\sigma \models \lnot \varphi$ iff $\sigma \not \models \varphi$
5. $\sigma \models \bigcirc \varphi$ iff $\sigma[1\ldots] = \sigma_1 \sigma_2 \sigma_3 \ldots \models \varphi$
6. $\sigma \models \varphi_1 \textbf{U} \varphi_2$ iff there exists $j\geq 0$ such that $\sigma[j \ldots] \models \varphi_2$ and for all $0 \leq i < j$ we have $\sigma[i \ldots] \models \varphi_1$.

Here, for $\sigma = \sigma_0 \sigma_1 \sigma_2 \ldots \in (2^A)^\omega$ we denote its **suffix** starting at the $(j+1)$-st symbol $\sigma_j$ by:
$$ \sigma[j\ldots] = \sigma_j \sigma_{j+1} \sigma_{j+2} \ldots$$

:::success
**Example (Eventuality).**
For example, for the eventuality operator we get:

* $\sigma \models \lozenge \varphi$
iff $\sigma \models \top \mathbf{U} \varphi$ (by def. of $\lozenge$)
iff there exists $j \geq 0$ with $\sigma[j \ldots] \models \varphi$ and for all $0 \leq i < j$: $\sigma[i \ldots] \models \top$ (by semantics of $\mathbf{U}$)
iff there exists $j \geq 0$: $\sigma[j \ldots] \models \varphi$ (as for every $\sigma$ we have $\sigma \models \top$)

Thus, as expected we find:
$\sigma \models \lozenge \varphi$
iff there exists $j \geq 0$ such that $\sigma[j \ldots] \models \varphi$
:::

:::warning
**Exercise 1 (Semantics of temporal modalities).**
Characterize other temporal modalities in a similar way by proving the following:
1. $\sigma \models \square \varphi$ iff for all $j \geq 0$ we have $\sigma[j \ldots] \models \varphi$.
2. $\sigma \models \square \lozenge \varphi$ iff for all $i \geq 0$ there exists $j \geq i$ such that $\sigma[j \ldots] \models \varphi$.
:::

# Rules for LTL

1. Duality law:
$\lnot \bigcirc \varphi \equiv \bigcirc \lnot \varphi$
$\lnot \lozenge \varphi \equiv \square \lnot \varphi$
$\lnot \square \varphi \equiv \lozenge \lnot \varphi$

2. Idempotency law:

$\lozenge \lozenge \varphi \equiv \lozenge \varphi$
$\square \square \varphi \equiv \square \varphi$
$\varphi \textbf{U} (\varphi \textbf{U} \psi) \equiv \varphi \textbf{U} \psi$
$(\varphi \textbf{U} \psi) \textbf{U} \psi \equiv \varphi \textbf{U} \psi$

3. Absorption law:

$\lozenge \square \lozenge \varphi \equiv \square \lozenge \varphi$
$\square \lozenge \square \varphi \equiv \lozenge \square \varphi$

4. Expansion law:
$\varphi \textbf{U} \psi \equiv \psi \lor (\varphi \land \bigcirc (\varphi \textbf{U} \psi))$
$\lozenge \psi \equiv \psi \lor \bigcirc \lozenge \psi$
$\square \psi \equiv \psi \land \bigcirc \square \psi$

## Paths and states semantics for LTL

Let $\mathcal T = (S, \Phi, \to, I, A, \lambda)$ be a [transition system](https://hackmd.io/ZHM1i5WiSTyq1QHuv8UkKQ?both) without terminal states, i.e., for all $s \in S$ there is some $s' \in S$ and $\alpha \in \Phi$ with $s \stackrel{\alpha}{\to} s'$.

Let $\varphi$ be an LTL-formula over $A$.

* For an infinite path fragment $\rho$ of $\mathcal T$, we define the satisfaction relation by:
$\rho \models \varphi$ iff $\mathrm{trace}(\rho) \models \varphi$

* For a state $s \in S$ the satisfaction relation $\models$ is defined by:
$s \models \varphi$ iff for all maximal path fragments $\rho$ starting at $s$ we have $\rho \models \varphi$.

* For $\mathcal T$, we define
$\mathcal T \models \varphi$ iff $\mathrm{Traces}(\mathcal T) \subseteq \mathrm{Words}(\varphi)$.

One can show from this definition that:
$\mathcal T \models \varphi$ iff $s_0 \models \varphi$ for all initial states $s_0 \in I$

If $\mathcal T \models \varphi$ we say "$\mathcal T$ satisfies the LTL property $\varphi$."

:::warning
**Exercise 2 (LTL properties of transition systems).**
Consider the following transition system $\mathcal T = (S, \Phi, \to, I, A, \lambda)$:
For each of the following properties, decide if $\mathcal T$ satisfies them or not. Give an argument or counterargument.
1. $\square p$
2. $\bigcirc (p \land q)$
3. $\square(\lnot q \to \square(p \land \lnot q))$
4. $q \mathbf{U} (p \land \lnot q)$
:::