Syntax and semantics

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.

Build and Installation

Development

1. Pnueli, Amir. The temporal logic of programs.
   18th Annual Symposium on Foundations of Computer Science.
   IEEE, 1977.