# 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:

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:

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

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

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

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

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

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

\(\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\).

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

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

\(\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:

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.