Linear temporal logic extends propositional logic with several modal operators
for reasoning about truth over (linear) time paths.

Formulas are given by the following grammar:
$$\varphi ::= \top \mid v \mid \neg \psi \mid \psi_1 \wedge \psi_2 \mid
\bigcirc \psi \mid \psi_1 \mathrel{\mathcal{U}} \psi_2 $$
where $v$ is a propositional variable.
The operator $\bigcirc \varphi$ is interpreted as
"$\varphi$ holds in the next state" and $\psi_1
\mathrel{\mathcal{U}} \psi_2$ as "$\psi_1$ holds until $\psi_2$ is true."

Additional connectives and operators can be built from those above:

- $\bot := \neg \top$
- $\varphi \vee \psi := \neg(\neg \varphi \wedge \psi)$
- $\varphi \implies \psi := \neg \varphi \vee \psi$
- $\varphi \iff \psi := (\varphi \implies \psi) \wedge (\psi \implies \varphi)$
- $\lozenge \varphi := \top \mathrel{\mathcal{U}} \varphi$ ("eventual truth": there exists a state in which $\varphi$ is true)
- $\square \varphi \equiv \neg \lozenge \neg \varphi$ ("Global truth": $\varphi$ holds in all states)
- $\varphi \mathrel{\mathcal{W}} \psi := \psi \mathrel{\mathcal{U}}(\varphi \vee \lozenge \psi)$ ("Weak until")
- $\varphi \mathrel{\mathcal{R}} \psi := \neg(\neg \varphi \mathrel{\mathcal{U}} \neg \psi)$ ("Release")
- $\varphi \mathrel{\mathcal{M}} \psi := \varphi \mathrel{\mathcal{W}} (\varphi \wedge \psi)$ ("Strong release")

Formulas are evaluated over a *trace* — this is a possibly infinite
sequence of propositional valuations. Each valuation is a
*state*. The first state of a trace refers to the "start" or present
moment.

Given a trace $\Sigma = \{ \Sigma_i \}_{i \in I}$, denote by $\Sigma^j := \{
\Sigma_i\}_{i \in I, i \geq j}$ the subtrace containing all states from
$\Sigma_j$ onwards. The length of $\Sigma$ is denoted $\left | \Sigma \right
|$.

The truth of a formula over a trace is determined inductively. For a formula $\varphi$ and trace $\Sigma$, define a satisfaction relation $\models$ as follows:

- $\Sigma \models \top$
- $\Sigma \nvDash \bot$
- $\Sigma \models v$ iff $v = \top$ at start
- $\Sigma \models \varphi \wedge \psi$ iff $\Sigma_0 \models \varphi$ and $\Sigma_0 \models \psi$
- $\Sigma \models \varphi \vee \psi$ iff $\Sigma_0 \models \varphi$ or $\Sigma_0 \models \psi$
- $\Sigma \models \bigcirc \varphi$ iff $\Sigma_1 \models \varphi$ or if $\left |\Sigma \right |=1$ with $\Sigma_0 \models \varphi$
- $\Sigma \models \square \varphi$ iff $\Sigma_j \models \varphi$ for all $j \in I$
- $\Sigma \models \varphi \mathrel{\mathcal{U}} \psi$ iff there exists $0 \leq i \leq |\Sigma|$ with $\Sigma^i \models \psi$ and $\Sigma^j \models \varphi$ for all $0 \leq j \leq i$

Under this definition, a formula containing no modal operators is equivalent to an ordinary propositional formula taking values in the current state.

See [1] for the original definition of linear temporal logic, along with applications and examples.`dune build`

to
compile, and `dune install`

to install.
- Pnueli, Amir.
.*The temporal logic of programs*

18th Annual Symposium on Foundations of Computer Science.

IEEE, 1977.

Back © 2024 Matthew Kukla