Supported logics#

Here you find a brief recap of the logics supported by BLACK and their properties. This presentation is not meant as an introduction to these logics, but rather as a quick reference to make sure the user and BLACK are on the same page. For more details we refer to the Publications page.

Linear Temporal Logic#

LTL is a propositional modal logic interpreted over infinite sequences of states, also said infinite words. Each state of the sequence is labelled by a set of propositions taken from a global alphabet \(\Sigma\). The syntax of LTL extends classical propositional logic with a few temporal operators. BLACK supports both future temporal operators, such as tomorrow and until, and past temporal operators, such as yesterday and since. LTL, when augmented with past operators, is often called LTL+P.

Recently, the finite-trace semantics of LTL gained much popularity in the field of artificial intelligence. With this semantics, the logic is often called LTL\({}_f\). In LTL\({}_f\), formulas are interpreted over finite words. Particular attention must be paid for the semantics of the operators to make sense. BLACK supports both LTL and LTL\({}_f\), with or without past operators (LTL\({}_f\)+P).

The abstract syntax of LTL+P and LTL\({}_f\)+P, independently from the adopted semantics, is outlined below. For the concrete input syntax accepted by BLACK, refer to the Input Syntax page. An LTL+P (or LTL\({}_f\)+P) formula \(\phi\) respects the following grammar:

\[\begin{split}\phi \equiv p & \mid \neg\phi \mid \phi \lor \phi \mid \phi \land \phi \\ & \mid \mathsf{X}\phi \mid \mathsf{\widetilde{X}}\phi \mid \phi\mathrel{\mathsf{U}}\phi \mid \mathsf{Y}\phi \mid \mathsf{Z}\phi \mid \phi\mathrel{\mathsf{S}}\phi\end{split}\]

where \(p\in\Sigma\). Usual shortcuts are available, such as \(\top\equiv p \lor \neg p\), \(\bot\equiv\neg\top\), \(\phi_1\mathrel{\mathsf{R}}\phi_2\equiv\neg(\neg\phi_1\mathrel{\mathsf{U}}\neg\phi_2)\), \(\mathsf{F}\phi\equiv \top\mathrel{\mathsf{U}}\phi\), \(\mathsf{G}\phi\equiv \neg\mathsf{F}\neg \phi\) (or also \(\mathsf{G}\phi\equiv \bot\mathrel{\mathsf{R}}\phi\)), \(\phi_1\mathrel{\mathsf{T}}\phi_2\equiv\neg(\neg\phi_1\mathrel{\mathsf{S}}\neg\phi_2)\), \(\mathsf{O}\phi\equiv \top\mathrel{\mathsf{S}}\phi\), and \(\mathsf{H}\phi\equiv \neg\mathsf{O}\neg \phi\) (or also \(\mathsf{H}\phi\equiv \bot\mathrel{\mathsf{T}}\phi\)),

A (finite or infinite) sequence \(\overline{\sigma}=\langle \sigma_0,\sigma_1,\ldots\rangle\) where \(\sigma_i\in 2^\Sigma\), satisfies a formula \(\phi\) at position \(i\ge0\), written \(\overline{\sigma},i\models\phi\), if the following holds:

  1. \(\overline{\sigma},i\models p\) iff \(p\in\sigma_i\)

  2. \(\overline{\sigma},i\models \neg\psi\) iff \(\overline{\sigma},i\not\models\psi\)

  3. \(\overline{\sigma},i\models \psi_1\lor\psi_2\) iff \(\overline{\sigma},i\models \psi_1\) or \(\overline{\sigma},i\models \psi_2\)

  4. \(\overline{\sigma},i\models \psi_1\land\psi_2\) iff \(\overline{\sigma},i\models \psi_1\) and \(\overline{\sigma},i\models \psi_2\)

  5. \(\overline{\sigma},i\models \mathsf{X}\psi\) iff \(i+1 < |\overline{\sigma}|\) and \(\overline{\sigma},i+1\models \psi\)

  6. \(\overline{\sigma},i\models \mathsf{\widetilde{X}}\psi\) iff \(i+1= |\overline{\sigma}|\) or \(\overline{\sigma},i+1\models \psi\)

  7. \(\overline{\sigma},i\models \psi_1\mathrel{\mathsf{U}}\psi_2\) iff there exists \(i \le j < |\overline{\sigma}|\) such that \(\overline{\sigma},j\models \psi_2\) and \(\overline{\sigma},k\models \psi_1\) for all \(k\) with \(j<k <i\).

  8. \(\overline{\sigma},i\models \mathsf{Y}\psi\) iff \(i > 0\) and \(\overline{\sigma},i-1\models \psi\)

  9. \(\overline{\sigma},i\models \mathsf{Z}\psi\) iff \(i = 0\) or \(\overline{\sigma},i+1\models \psi\)

  10. \(\overline{\sigma},i\models \psi_1\mathrel{\mathsf{S}}\psi_2\) iff there exists \(j \le i\) such that \(\overline{\sigma},j\models \psi_2\) and \(\overline{\sigma},k\models \psi_1\) for all \(k\) with \(j<k\le i\).

Note that, on infinite words, the tomorrow and weak tomorrow operators are equivalent, so the weak tomorrow operator is redundant. BLACK accepts both anyway, for uniformity, independently from the semantics chosen.

Linear Temporal Logic modulo Theories#

Starting from LTL\({}_f\), and replacing propositional letters with first-order formulas over arbitrary theories, we obtain LTL\({}_f\) Modulo Theories (LTL\({}_f\)MT). This is similar to how Satisfiability Modulo Theories extends the classical Boolean satisfiability problem. This logic features a greatly increased expressive power w.r.t. LTL\({}_f\), so much indeed that the logic is in fact undecidable. Nevertheless, BLACK implements a semi-decision procedure for LTL\({}_f\)MT, i.e. a procedure that always replies SAT for satisfiable formulas, and for unsatisfiable formulas may reply UNSAT or not terminate.

The syntax of LTL\({}_f\)MT is, as said, that of LTL\({}_f\) with first-order formulas in place of propositions, but a few temporal operators are supported inside first-order formulas as well. An LTL\({}_f\)MT formula \(\phi\) respects the following grammar:

\[\begin{split}\phi := {} & \psi \mid \neg\phi \mid \phi \lor \phi \mid \phi \land \phi \\ & \phantom{\psi} \mid \mathsf{X}\phi \mid \mathsf{\widetilde{X}}\phi \mid \phi\mathrel{\mathsf{U}}\phi \mid \mathsf{Y}\phi \mid \mathsf{Z}\phi \mid \phi\mathrel{\mathsf{S}}\phi \\[2ex] \psi := {} & p(t_1,\ldots, t_n) \mid \neg\psi \mid \psi\lor\psi \mid \psi\land\psi \mid \exists x \psi \mid \forall x \psi \mid \\ & \phantom{p(t_1,\ldots,t_n)} \mid \mathsf{X}\psi \mid \mathsf{\widetilde{X}}\psi \mid \mathsf{Y}\psi \mid \mathsf{Z}\psi\\[2ex] t := {} & f(t_1,\ldots,t_m) \mid c \mid x \mid \bigcirc x \mid \bigcirc\kern-1.2em\sim x\end{split}\]

where \(c\) is a constant, \(x\) is a variable, \(p\) is an \(n\)-ary predicate, and \(f\) is an \(m\)-ary function.

Intuitively, the semantics of first-order formulas is standard, and the semantics of temporal operators follows that of LTL\({}_f\). The term constructors \(\bigcirc x\) and \(\bigcirc\kern-1.2em\sim x\) allow the formula to refer to the value of \(x\) at the next state. However, \(\bigcirc x\) (the strong next term constructor), similarly to the tomorrow operator, mandates the existence of such state. Instead, \(\bigcirc\kern-1.2em\sim x\) (the weak next term constructor), similarly to the weak tomorrow operator, refers to such value only if the next state exists. More precisely, any atom \(p(t_1,\ldots,t_n)\) that contains a strong next term is always false at the last state of the word, while any atom that contains a weak next term (but not strong ones) is always true at the last state.

BLACK currently supports LTL\({}_f\)MT formulas over the LIA, LRA and EUF theories, and combinations thereof.

We refer the user to [GGG22] for a formal account of the semantics of the logic.

Note

[GGG22] describes the LTL\({}_f\)MT logic as was supported by BLACK in version 0.7. From v0.8, BLACK supports tomorrow and yesterday (and weak versions) temporal operators inside first-order formulas, and uninterpreted functions and relations are non-rigid, i.e. they change over time. Moreover, BLACK supports past operators, which are not covered in the paper.