Definition. Linear-time temporal logic [ltp-000V]

Properties are commonly written using linear-time temporal logic (LTL), a modal logic defined over behaviours. Given atomic propositions $\mathsf {a} : \Sigma \rightarrow \mathbb {B}$ , the syntax for formulae is given by:

\begin {array}{lcl} \varphi , \psi &::=& \top \mid \bot \mid \mathsf {a} \mid \varphi \land \psi \mid \varphi \lor \psi \mid \neg \varphi \\ &\mid & \mathop {\raisebox {-0.2em}{\text {\Large ○}}} \varphi \mid \mathop {\raisebox {-0.2em}{\text {\Large ◇}}} \varphi \mid \mathop {\raisebox {-0.1em}{\text {\Large □}}} \varphi \mid \varphi \mathbin {\mathcal {U}} \psi \mid \varphi \mathbin {\mathcal {R}} \psi \end {array}

To assign semantics, we compositionally map each formula to a property. Here the notation $f^k$ indicates the self-composition of $f$ $k$ times, i.e. $f^0(x)=x$ and $f^{k+1}(x)=f^k(f(x))$ . The function $\mathop {\triangleright }$ , the prepend operator, is defined as follows:

\mathop {\triangleright } X = \{ s\sigma \mid s \in \Sigma \land \sigma \in X \}

\begin {array}{lcl} \llbracket \top \rrbracket &=& \Sigma ^\omega \\ \llbracket \bot \rrbracket &=& \emptyset \\ \llbracket \mathsf {a}\rrbracket &=& \{ \sigma \mid \mathsf {a}(\sigma _0) \} \\ \llbracket \varphi \land \psi \rrbracket &=& \llbracket \varphi \rrbracket \cap \llbracket \psi \rrbracket \\ \llbracket \varphi \lor \psi \rrbracket &=& \llbracket \varphi \rrbracket \cup \llbracket \psi \rrbracket \\ \llbracket \neg \varphi \rrbracket &=& \llbracket \varphi \rrbracket ^\complement \\ \llbracket \mathop {\raisebox {-0.2em}{\text {\Large ○}}} \varphi \rrbracket &=& \mathop {\triangleright }\llbracket \varphi \rrbracket \\ \llbracket \mathop {\raisebox {-0.2em}{\text {\Large ◇}}} \varphi \rrbracket &=& \bigcup _{i \in \mathbb {N}}\mathop {\triangleright }^i\llbracket \varphi \rrbracket \\ \llbracket \mathop {\raisebox {-0.1em}{\text {\Large □}}} \varphi \rrbracket &=& \bigcap _{i \in \mathbb {N}}\mathop {\triangleright }^i\llbracket \varphi \rrbracket \\ \llbracket \varphi \mathbin {\mathcal {U}} \psi \rrbracket &=& \bigcup _{i \in \mathbb {N}}f^k(\llbracket \psi \rrbracket )\text {, where}\ f(X) = \mathop {\triangleright } X \cap \llbracket \varphi \rrbracket \\ \llbracket \varphi \mathbin {\mathcal {R}} \psi \rrbracket &=& \bigcap _{i \in \mathbb {N}}f^k(\llbracket \psi \rrbracket )\text {, where}\ f(X) = \mathop {\triangleright } X \cup \llbracket \varphi \rrbracket \\ \end {array}

These semantics are sometimes written in terms of a satisfaction relation like $\sigma \models \varphi$ . This notation is equivalent to our $\sigma \in \llbracket \varphi \rrbracket$ .