LTL logo


Introduction

Linear temporal logic over finite and infinite traces, implemented in OCaml.

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:

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:

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.

Documentation

Module documentation is located here.

Build and Installation

Clone the repository from GitHub. LTL can be built with dune: run dune build to compile, and dune install to install.

Development

Source code is available on GitHub. LTL is free software under the GNU GPL v3.

References

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

Back © 2024 Matthew Kukla