Logics for Qualitative Reasoning   Logics for time   Linear Temporal Logic

Linear Temporal Logic   (written by Przemysław Wałęga)

Formalism description:

Formulas $\varphi$ of linear temporal logic are generated by the following abstract syntax: $$ \varphi ::= p \mid \neg \varphi \mid \varphi \lor \varphi \mid \bigcirc \varphi \mid \lozenge\varphi, $$ where $p$ denotes a propositional letter.

Kripke-style semantics:

A linear temporal logic model is an infinite sequence of the form $\sigma = ( s_0, s_1, s_2, \ldots )$, where for any $i \in \mathbb{N}$, $s_i: Var \to \{ T,F \}$ assigns truth valu to each propositional variable in $Var$.

The satisfaction relation for a sequence $\sigma$ and $i \in \mathbb{N}$ is defined as follows:

\[ \begin{array}{lll} \sigma,i \models p & \text{iff} & s_i(p)=T \text{ for any } p\in Var; \\ \sigma,i \models \neg \varphi & \text{iff} & \sigma,i \not\models \varphi; \\ \sigma,i \models \varphi \lor \psi & \text{iff} & \sigma,i \models \varphi \text{ or } \sigma,i \models \psi; \\ \sigma,i \models \bigcirc \varphi & \text{iff} & \sigma, i+1 \models \varphi; \\ %\sigma,i \models \square \varphi & \text{iff} & \text{for all } j \geq i \text{ we have } \sigma, j \models \varphi ; \\ \sigma,i \models \lozenge \varphi & \text{iff} & \text{for some } j \geq i \text{ we have } \sigma, j \models \varphi . \\ \end{array} \] Application fields:

Temporal reasoning, program verification, task scheduling.

Comments and references:

Satisfiability problem in linear temporal logic is PSpace-complete (Sistla et al. 1982). When $\bigcirc$ is eliminated from the language, the logic becomes NP-complete (Sistla et al. 1982). A linear temporal logic formula may be treated as a set of infinite traces. It is known that for each formula a Büchi automaton may be constructed, which accepts exactly the traces represented by this formula. Hence, there is a reduction of satisfiability problem in a linear temporal logic formula to the nonemptiness problem of a Büchi automaton (Vardi et al. 1994).