Linear Temporal Logic Modulo Theories over Finite Traces

1 Introduction

Linear Temporal Logic (LTL) [Pnueli, 1977] and LTL over finite traces (LTLf) [De Giacomo and Vardi, 2013] are common languages to express temporal properties in the fields of formal verification and AI. In particular, LTLf has recently gained traction in AI and business process modeling [De Giacomo et al., 2014a]. In these fields, reasoning over finite traces is more natural.

However, in the modeling of data-aware processes [Calvanese et al., 2020; Li et al., 2017], the propositional nature of LTLf is a severe limitation. These are systems whose behavior depends on and/or manipulate a persistent data storage such as a relational database. In these contexts, one would like to express actions and constraints that depend on the contents of the database, which is an inherently first-order object. A similar use case is that of data-aware planning, i.e., planning problems [Ghallab et al., 2004] where conditions of actions depend on the contents of the persistent data storage.

In order to obtain the expressiveness needed to model and reason about these scenarios, this paper introduces and studies LTLf Modulo Theory (LTLf MT ), a logic that extends LTLf by replacing propositional symbols with first-order formulas over an arbitrary theory, in the spirit of Satisfiability Modulo Theory (SMT). While LTLf MT is easily seen to be undecidable in general, for decidable theories it is semi-decidable, i.e., a positive answer can always be obtained for satisfiable instances, while reasoning might not terminate over unsatisfiable instances. We argue that, for complex problems and scenarios like those mentioned above, where reasoning is inherently undecidable anyway, being able to solve satisfiable instances is a compromise worth studying.

In particular, we provide a semi-decision procedure for LTLf MT satisfiability based on the one-pass tree-shaped tableau for LTL by Reynolds [2016]. In contrast to classic graph-shaped tableaux for LTL, Reynolds' builds a tree structure where a single independent pass is sufficient to decide whether to accept or reject the current branch. Here, we adapt Reynolds' tableau to LTLf MT , showing that, for decidable underlying first-order theories, LTLf MT is semidecidable. While first-order extensions of LTL have already been studied before, our setting is more specific: on the one hand, we are more general than, e.g., [Cimatti et al., 2020] by supporting quantified formulas. On the other hand, we restrict general first-order LTL [Kontchakov et al., 2004; Artale et al., 2019] by not allowing temporal operators inside quantifiers.

Our main contribution is an SMT-based algorithmic technique for satisfiability checking of such an expressive logic, which we implement in the BLACK tool [Geatti et al., 2019; Geatti et al., 2021b]. BLACK is a recent state-of-the-art satisfiability checker for LTL and LTLf based on a SAT encoding of Reynolds' tableau. Inspired by that, we provide an SMT encoding of our tableau for LTLf MT : suitably encoded SMT formulas represent the branches of the tableau up to depth k, for increasing values of k.

An experimental evaluation assesses the applicability of our approach. With a number of novel benchmarks over different underlying theories, we show that BLACK is able to reason over satisfiable instances and, in some cases, over unsatisfiable instances as well, with promising performance.

The paper is organized as follows. We introduce LTLf MT in Section 2. Then, Section 3 discusses some relevant use cases that motivate our work. Sections 4 and 5 provide a semi-decision procedure for LTLf MT and its SMT encoding. Section 6 evaluates the implementation of this procedure in the BLACK satisfiability checker, and Section 7 concludes. Proofs can be found in [Geatti et al., 2022].

2 LTLModulo Theories over Finite Traces

LTLf MT extends Linear Temporal Logic over Finite Traces (LTLf) by replacing proposition letters with first-order formulas over arbitrary theories, similarly to how Satisfiability Modulo Theory (SMT) extends the classical Boolean satisfiability problem. Before going into the formal details of syntax and semantics, let us show some examples.

Consider the theory of linear integer arithmetic (LIA). This first-order theory predicates over the set of integer numbers Z, and interprets the + function symbol and the ≤ relation symbol as the usual sum and comparison between integer numbers. There is no multiplication symbol. With LTLf MT over LIA, we can express formulas such as the following:

This first formula on the left states that the interpretation of the variable x must always (i.e., in any time point) be the double of the variable y. The second formula states that the variable x must remain less than y until the first time y becomes equal to zero. The third one, which is unsatisfiable, demands x to be always greater than 5 but also to become less than 0 in the future. Quantifiers are allowed, but temporal operators cannot be nested inside them. For example, the following formula states that x has always to be even:

While these examples are interesting, there is often the need to go further, by relating the value of variables at a given time point to their value at the following instant. This is expressed by two term constructors, ©x and ©∼x, which both represent, in a different way, the value of the variable x at the next state. The difference lies in how these terms behave at the end of the finite trace. When a first-order formula contains some ©x, the next state is required to exist, while it is not required to exist if it contains only©∼x terms. This replicates the difference between the tomorrow and weak tomorrow temporal operators in LTLf [De Giacomo and Vardi, 2013; De Giacomo et al., 2014b]. With these two term constructors in place, we can express more interesting things such as:

The first formula states that variable x behaves as a counter that increments until reaching x = 42. The second one makes x represent any strictly increasing sequence of even numbers, while in the third formula x takes all the first n even numbers for any n ≥ 1. Note that, in the second and third formula, replacing ©∼x with ©x would result in an unsatisfiable formula, because each time point would require the existence of the next one, which is impossible in a finite-trace semantics.

Syntax. We are now ready to delve into the details of syntax and semantics of LTLf MT . Let us start from the syntax. We work with a multi-sorted first-order signature Σ = S ∪ P ∪ C ∪ F ∪ V ∪W, composed of a set of sort symbols S, a set of predicate symbols P, a set of constant symbols C, a set of function symbols F, a set of variable symbols V, and a set of quantified variables W. Each constant in C and each variable in V and W is associated with a sort symbol S ∈ S, and so are the domains of each relation symbol and the domains and ranges of each function symbol.

A Σ-term t is generated by the following grammar:

where x ∈ V and y ∈ W are variables, c ∈ C is a constant symbol, f ∈ F is a function symbol of arity k, each ti (for any i ∈ {1, . . . , k}) is a Σ-term, and © and ©∼ are the next and weak next constructors. Note that the distinction between variables in V and in W is needed since it does not make sense to apply ©x and ©∼ x to a quantified variable (recall that ©x represents the value of x at the next state). The grammar of LTLf MT formulas over Σ is the following:

where x ∈ W, p ∈ Σ is an k-ary predicate symbol, each ti is a Σ-term, and X, ˜X, U, and R are the tomorrow, weak tomorrow, until, and release temporal operators, respectively. In the definition of φ, we force λ to not have free variables fromW. Formulas of type λ as defined above are called firstorder formulas. We assume the usual shortcuts for temporal operators, such as Fφ ≡ ⊤Uφ and Gφ ≡ ⊥Rφ. Note that by the grammar above, LTLf MT formulas are always in negated normal form, for ease of exposition. The formulas of LTLf MT are assumed to be well-typed with regard to the sorts of all the involved symbols. One may also consider past operators, but we omit them here to ease exposition.

Semantics. We use the standard notion of first-order Σstructure M over the first-order (multi-sorted) signature Σ, which consists of a domain and of an interpretation sM of all sort, predicate, constant, and function symbols s ∈ Σ. In particular, sort symbols are interpreted as pairwise disjoint sets, whose union dom(M) is the domain of M. In line with [Barrett et al., 2009], we define a theory T as a (finite or infinite) class of Σ-structures.

Let Σ = S∪P∪C∪F∪V∪W be a signature and let T be a theory. A T -state s = (M, µ) is a pair made of a Σ-structure M ∈ T and a variable evaluation function µ : V → dom(M) assigning to each variable in V a value in the domain of M.

A word σ = 〈(M, µ0), . . . , (M, µn-1)〉 over the theory T is a finite sequence of T -states over the same first-order structure. We define |σ| = n. It is worth noticing that any two states can differ only in the variable evaluation functions, and not in their domain nor in the interpretations of the other symbols, which are rigidly interpreted. In the context of firstorder LTL, this is called constant domain semantics [Hodkinson et al., 2000].

Given a term t, a word σ = 〈(M, µ0), . . . , (M, µn-1)〉, an integer 0 ≤ i < n, and a variable evaluation function ξ : W → dom(M) for the variables in W, the evaluation of t at the instant i on the trace σ with environment ξ, denoted JtKiσ,ξ , is the following:

1. J©xKiσ,ξ = J©∼xKiσ,ξ = µi+1(x)
2. JcKiσ,ξ = cM
3. Jf(t1, . . . , tk)Kiσ,ξ = f M (Jt1Kiσ,ξ , . . . , JtkKiσ,ξ )

Intuitively, when evaluating a term, the free variables from V are evaluated according to the word σ, while the bound variables fromW are evaluated according to the environment ξ. Note that JtKiσ,ξ is well-defined for σ only if (1) i < |σ| - 1 or (2) i = |σ| - 1 and t does not contain terms of type ©x or ©∼x. That is, we cannot evaluate a variable beyond the end of the word. A first-order formula λ is well-defined for σ only if JtKσ,ξ is well-defined for all the terms t appearing in ψ. Given a variable evaluation function ξ : W → dom(M), we denote as ξ[x ← v] the function that agrees with ξ except that ξ(x) = v.

Given a theory T , the satisfaction modulo T of a first-order formula ψ over the word σ at time point i ∈ N with environment ξ, denoted with σ, ξ, i |= ψ, is inductively defined as:

1. σ, ξ, i |= p(t1, . . . , tk) is defined depending on whether terms of type ©x appear in t1, . . . , tk:
2. (a) if ©x appear in t1, . . . , tk for some variable x, then σ, ξ, i |= p(t1, . . . , tk) iff Jt1Kiσ,ξ , . . . , JtkKiσ,ξ are well-defined and (Jt1Kiσ,ξ , . . . , JtkKiσ,ξ ) ∈ pM ;
3. σ, ξ, i |= ¬p(t1, . . . , tk) iff σ, ξ, i ̸|= p(t1, . . . , tk);
4. (b) otherwise, σ, ξ, i |= p(t1, . . . , tk) if and only if at least one in Jt1Kiσ,ξ , . . . , JtkKiσ,ξ is not well-defined or (Jt1Kiσ,ξ , . . . , JtkKiσ,ξ ) ∈ pM ;
5. σ, ξ, i |= λ1 ∨ λ2 iff σ, ξ, i |= λ1 or σ, ξ, i |= λ2;
6. σ, ξ, i |= λ1 ∧ λ2 iff σ, ξ, i |= λ1 and σ, ξ, i |= λ2;
7. σ, ξ, i |= ∃x.ψ iff there exists a value v ∈ dom(M) such that σ, ξ[x ← v], i |= ψ;
8. σ, ξ, i |= ∀x.ψ iff for all values v ∈ dom(M) it holds that σ, ξ[x ← v], i |= ψ;

Note that Items 1a and 1b above are those where the semantics of ©x and ©∼x terms differ. In the first case, the next state must exist for the atom to hold. In the second case, the atom holds by definition if the next state does not exist. Given a theory T , the satisfaction modulo T of an LTLf MT formula φ over the word σ at time point i ∈ N, denoted as σ, i |= φ, is inductively defined as follows:

1. σ, i |= λ, where λ is a first-order formula, if σ, ξ, i |= λ for some ξ;
2. σ, i |= φ1 ∨ φ2 iff σ, i |= φ1 or σ, i |= φ2;
3. σ, i |= φ1 ∧ φ2 iff σ, i |= φ1 and σ, i |= φ2;
4. σ, i |= Xφ iff i < |σ| - 1 and σ, i + 1 |= φ;
5. σ, i |= ˜Xφ iff i = |σ| - 1 or σ, i + 1 |= φ;
6. σ, i |= φ1Uφ2 iff there exists a j ≥ i such that σ, j |= φ2 and σ, k |= φ1 for all i ≤ k < j;
7. σ, i |= φ1 R φ2 iff either σ, j |= φ2 for all i ≤ j < |σ|, or there exists k ≥ i such that σ, k |= φ1 and σ, j |= φ2 for all i ≤ j ≤ k.

We say that σ satisfies φ modulo T iff σ, 0 |= φ. The language modulo T of φ is the set of words σ over T that satisfy φ. A formula φ with no temporal operators and no ©x or ©∼x terms is a purely first-order formula. If a word σ satisfies such a φ, only the first state is involved in its satisfaction. In this case we can write s |= φ. An atom p(t1, . . . , tk) is strong if it contains at least a©x term. It is weak if it contains ©∼x terms but no©y terms.

The satisfiability checking problem for LTLf MT is easily seen to be undecidable, depending on the theory. For example, with the LIA theory one can easily encode the PLANEX(Cp+, C∅, E+1) numeric planning problem, proved to be undecidable by Helmert [Helmert, 2002]. However, for suitable theories (see Section 4), it is semi-decidable.

Expressiveness. It is interesting at this point to wonder how much expressiveness we gain by extending the classical (propositional) LTLf [De Giacomo and Vardi, 2013; De Giacomo et al., 2014b] in the way we previously shown. As LTLf is a propositional logic, it is trivially subsumed by LTLf MT with a theory B consisting only of the equality relation and a Boolean domain ({0, 1}). One may wonder, however, how expressive LTLf MT over other theories is with regards to B (i.e., to LTLf), when we abstract its models to propositional finite words. More formally, for a signature Σ = S ∪ P ∪ C ∪ F ∪ V ∪ W we consider unary predicates from P as propositional symbols, and given a word σ = 〈s0, . . . , sn-1〉 we define its Boolean abstraction B(σ) = 〈B(s0), . . . , B(sn-1)〉 as follows: P ∈ B(si) iff si |= ∃xP(x). For any theory T , the Boolean abstraction of a language modulo T is the set of the Boolean abstractions of all the words of the language. We can prove the following.

Theorem 1. There are languages definable in LTLf MT whose Boolean abstraction cannot be defined in LTLf.

Proof. Consider the theory of Linear Integer Arithmetic (LIA) together with uninterpreted unary predicates. It is wellknown [Wolper, 1983] that LTLf cannot express the language made of words where a proposition p appears in at least all even positions. Instead, such a language can be defined as the Boolean abstraction of the language modulo LIA recognized by the following LTLf MT formula:

Note the essential role of the ©∼x term here. Without such terms, the satisfaction of first-order formulas in different time steps of a LTLf MT model would be completely unrelated, which would allow us to abstract them into proposition symbols. As a matter of fact, we can prove the following.

Theorem 2. The Boolean abstraction of any language definable in LTLf MT without ©x nor ©∼x terms can also be defined in LTLf, and vice versa.

Regarding ©x and ©∼x terms, it should be noted that the LTLf MT syntax only allows these term constructors to be applied to single variables. However, the syntax may be extended to arbitrary nesting of © and ©∼ operators with a simple translation maintaining the equisatisfiability. For instance, the formula x = 1 ∧ ©x = 1 ∧ G(©∼©∼x = ©∼x + x), expressing the Fibonacci sequence, is equisatisfiable to x = 1 ∧ © x = 1 ∧ y = 1 ∧ G(y = ©∼ x ∧ ©∼ y = y + x).

3 Use Cases

Verification of data-aware processes. We take inspiration from verification of data-aware processes to present an interesting class of case studies. Specifically, we rely on the framework by Calvanese et al. [2020; 2021], who introduced a general model of transition systems interacting with relational databases, with the distinctive feature that the transitions can query the content of the persistent data storage. As shown there, the theory of equality and uninterpreted functions (EUF) provides an algebraic formalization of relational databases with primary and foreign key dependencies: in particular, unary functions map the primary key attribute of a relation schema to another attribute of the same relation, and implicitly represent key dependencies. If EUF is combined with an arithmetical theory such as LRA (e.g., following [Calvanese et al., 2019a; Calvanese et al., 2022]), complex datatype values can be injected into the database and used to model non-deterministic inputs from external users [Calvanese et al., 2019b]. A symbolic transition system Sys operating over databases can be formalized by means of: (i) a sequence of variable symbols x1, . . . , xn from V, describing the current configuration; (ii) a purely first-order formula I(x1, . . . , xn), describing the initial states; (iii) a weak firstorder formula Tr(x1, . . . , xn) describing the transitions from the current configuration to the next one. Given an LTLf MT formula ψ(x1, . . . , xn), called property, we are interested in establishing whether I ∧ G(Tr) ∧ ψ is satisfiable modulo the theory constraining the database, i.e., EUF ∪ LRA. As an example, imagine a job hiring business process modeling the evaluation of the applications received for a job position: the transition system is intuitively represented, via the BPMN standard language, 1 in Figure 1. The following property states that whenever a job position is opened, eventually it is closed.

Data-aware planning. LTLf MT satisfiability over LRA provides a straightforward approach to numeric planning problems, which are similarly undecidable [Helmert, 2002] but nevertheless very relevant in practice. Even more interestingly, we can model data-aware planning problems, i.e., planning problems [Ghallab et al., 2004] where precoditions of actions can query a relational database. As shown by Cialdea Mayer et al. [2007], LTL can encode classical STRIPS-like planning problems. Similarly, data-aware planning problems can be encoded with LTLf MT formulas. The encoding of the planning domain results into a data-aware transition system similar to the one above, with the property to verify corresponding to the reachability of the goal.

1 https://www.omg.org/spec/BPMN/

4 One-Pass Tree-Shaped Tableau for LTLf MT

Here we provide a semi-decision procedure for LTLf MT satisfiability based on an adaptation of the one-pass tree-shaped tableau for LTL by Reynolds [2016]. In contrast to classic graph-shaped tableaux, Reynolds' produces a purely treeshaped structure where a single pass is sufficient to either accept or reject a given branch. Reynolds' tableau proved to be amenable to efficient implementation [Bertello et al., 2016] and parallelization [McCabe-Dansted and Reynolds, 2017], and to direct extension to real-time logics [Geatti et al., 2021a]. A state-of-the-art SAT encoding of Reynolds' tableau has been implemented in the BLACK satisfiability solver [Geatti et al., 2019; Geatti et al., 2021b]. Here, we adapt the tableau system to LTLf MT , and provide an SMT encoding that we implement in the BLACK satisfiability tool.

The closure of a formula φ, denoted C(φ), is the set of all the subformulas of φ with the addition of X(ψ1 U ψ2) for any formula ψ1 U ψ2 ∈ C(φ), and ˜X(ψ1 R ψ2) for any formula ψ1 R ψ2 ∈ C(φ).

A tableau for an LTLf MT formula φ is a rooted tree where each node u is labelled by a set of formulas Γ(u) ⊆ C(φ). The root u0 is labelled by Γ(u0) = {φ}. The tree is built starting from the root, until all branches have been either accepted or rejected. If at least one branch is accepted, φ is satisfiable. The tree is built by applying a set of expansion rules to the formulas in each node's label. Such rules are listed in Table 1. When a rule is applied to a formula ψ ∈ Γ(u), two children u′ and u′′ are added to u, where Γ(u′ ) = Γ(u) \ {ψ} ∪Γ1(u) and Γ(u′′ ) = Γ(u) \ {ψ} ∪ Γ2(u), unless Γ2(u) is empty, in which case only a single child is added.

When no expansion rules are applicable to a node, it is called a poised node. A poised node contains only elementary formulas, i.e., only first-order, tomorrow (Xφ) or weak tomorrow (˜Xφ) formulas. A poised node represents a single state in a tentative model for the formula. So let u = 〈u0, . . . , un-1〉 be a branch of the tableau with un-1 a poised node. A temporal step can be made through the STEP rule.

STEP A new child un of un-1 is created such that:

By alternating the STEP rule with the expansion rules we build each branch of the tree. Then, we need a way to stop the construction when a branch is ready to be accepted or rejected. Two termination rules are provided for this purpose. The CONTRADICTION rule rejects a branch when it presents some contradiction. In order to define this rule, we need some definitions. Given a branch u = 〈u0, . . . , un-1〉, with un-1 a poised node, we define a first-order formula Ω(u) that summarizes the first-order formulas made true by the branch u over the different time points. This formula is defined over a new alphabet Σ′ = P ′ ∪ C ∪ F ∪ V ′ ∪ W where P ′ = P ∪ {ℓi |i ∈ N}, and V ′ = {xi |x ∈ V, i ∈ N}. Here, ℓi are fresh 0-ary EUF predicates, and V ′ is a set of stepped versions of the variables in V. Given a term t, the stepped version of t at time i is the term ti defined as follows:

1. ci = c 2. xi = x if x ∈W; 3. xi = xi if x ∈ V; 4. (©x)i = (©∼x)i = xi+1

By extension, given a first-order formula ψ, the formula ψi is obtained by replacing each term t in ψ with its stepped version ti . Given a first-order formula φ, the formula Li(φ) is obtained from φ by replacing all strong atoms α with ℓi ∧ α, and all weak atoms α with ℓi → α. Intuitively, if ℓi is true, i is not the last step of the model, hence Li(α) encodes this aspect of the semantics of ©x and ©∼x terms.

For the branch u, let π = 〈π0, . . . , πm-1〉 be the sequence of poised nodes of u. Let F(πi) be the set of first-order formulas of Γ(πi). Then we define the Ω(u) formula as follows:

Intuitively, the purpose of Ω(u), which is a purely firstorder formula over T ∪ EUF, is that of describing the whole tentative model represented by u in a single formula. Note that, in Ω(u), the value of ℓm-1 is left unconstrained. Hence, if Ω(u) is unsatisfiable, a contradiction exists independently from the choice of closing or extending the branch. Now we can define the rule.

CONTRADICTION The branch u is rejected if Ω(u) is unsatisfiable modulo T ∪ EUF.

Note that the CONTRADICTION rule can be easily checked by giving Ω(u) to an SMT solver over T ∪ EUF.

The EMPTY rule, instead, accepts suitable branches when there is no reason to further extend the model.

EMPTY If Γ(πm-1) does not contain tomorrow formulas and Ω(u) ∧¬ℓm-1 is satisfiable, the branch is accepted.

We can prove soundness and completeness of the system.

Theorem 3 (Soundness and completeness). Given a LTLf MT formula φ, the tableau for φ has an accepted branch if and only if φ is satisfiable.

If T ∪QF EUF is decidable, the breadth-first construction of the tableau tree provides a semi-decision procedure for LTLf MT satisfiability, as it always finds at least an accepted branch when given a satisfiable formula.

Despite the generality of our definitions, it is clear that our approach to LTLf MT satisfiability is applicable over decidable theories supported by the underlying SMT solvers. This is the case for most quantifier-free fragments of the supported theories and their combinations, and, in some cases (such as LRA and LIA), also in the quantified case.

Algorithm 1 BLACK's main procedure for LTLf MT

1: procedure BLACK(φ) 2: k ← 0 3: while True do 4: if 〈〈φ〉〉k is UNSAT then 5: return φ is UNSAT 6: end if 7: if |φ|k is SAT then 8: return φ is SAT 9: end if k ← k + 1 end while

10: 11: 12: end procedure

The procedure may also terminate on some unsatisfiable formulas, such as those where the unsatisfiability comes from theory contradictions, such as x = 3 ∧ G(∃y(x = y + y)). It cannot terminate instead on formulas where the unsatisfiability comes from unsatisfiable temporal requests. An example of such formulas is G(x > 3) ∧ F(x < 2), whose tableau contains an infinite branch which tries to fulfill the F(x < 2) eventuality at each step. In Reynolds' tableau for LTL [Reynolds, 2016], closing such branches is the purpose of the PRUNE rule, which however cannot be applied in LTLf MT (otherwise we would get a decision procedure for an undecidable problem). It is worth noticing that the PRUNE rule can be made to work if we do not allow ©x and ©∼x terms. That is, a decision procedure is possible for the fragment of LTLf MT without © x nor ©∼ x terms, which, however, as we have seen, is far less expressive.

5 The SMT Encoding

The SAT encoding of the original tableau for LTL by Reynolds has been implemented in the BLACK satisfiability checking tool as described by Geatti et al. [2019; 2021b]. Here, we extend it naturally, namely with an SMT encoding of the tableau system described above.

We encode the tableau for a formula φ as a pair of SMT formulas that represent the branches of the tree up to a depth k, for increasing values of k, as shown in Algorithm 1. The formula 〈〈φ〉〉k used at Line 4 is called the k-unraveling of φ, and represents the branches of the tree with at most k + 1 poised nodes. To define it, we encode the expansion rules of Table 1.

Definition 1 (Stepped Normal Form). Given an LTLf MT formula φ and an i ≥ 0, its i-th stepped normal form, denoted by snfi(φ), is defined as follows:

For a generic formula ψ and for i > 0, considering its stepped version ψi , we denote as ψiG the result of replacing each tomorrow or weak tomorrow formula τ with a fresh 0ary EUF predicate τ iG.

The k-unraveling of φ is recursively defined as follows:

where XR and ˜XR are the sets of all the tomorrow and weak tomorrow formulas, respectively, in C(φ).

If 〈〈φ〉〉k is unsatisfiable, it means all the branches of the tableau for φ are of at most k + 1 poised nodes and are all rejected by the CONTRADICTION rule.

The |φ|k formula encodes the EMPTY rule:

If |φ|k is satisfiable, the tableau for φ has at least a branch accepted by the EMPTY rule.

By relating the tableau branches with the models for 〈〈φ〉〉k and |φ|k, one can easily prove the following, taking inspiration from [Geatti et al., 2021b].

Theorem 4. Algorithm 1 answers SAT if and only if the tableau for φ has an accepted branch.

6 Experiments

We implemented the above encoding in the BLACK satisfiability checking tool. 2 The current implementation supports the full LTLf MT syntax limited to mono-sorted theories, but in addition to that, it supports past operators, which are handled in the tableau similarly to [Geatti et al., 2021a] and are encoded similarly to [Geatti et al., 2021b].

We tested BLACK on a number of crafted benchmarks intended to stress the underlying algorithm in different ways. We have a total of 990 formulas generated from 5 scalable patterns each parameterized on a value N. The scalable schemata are shown in Table 2. The table shows the theory over which the formulas are intended to be tested, the expected result of the satisfiability checking, and a qualitative plot of running times from N = 1 up to the maximum value of N which runs under the 5 minutes timeout. The tests were run on commodity hardware, setting BLACK to use the Z3 backend [de Moura and Bjørner, 2008].

2 The source code and all the tests and benchmarks are available in BLACK's GitHub repository, merged into version 0.7 of the tool.

The first LIA schema represents a set of simple counters going from 0 to N. The tableau for these formulas has an accepted branch of exponential size, but BLACK's encoding is not paying a price to that. In contrast, the explicit Boolean encoding of a counter found in BLACK's propositional LTL benchmark set [Geatti et al., 2019] takes orders of magnitude longer to solve in the harder cases. This unsurprising fact shows the advantage of the explicit arithmetic reasoning done by the SMT solver over bit blasting techniques. The second LIA schema is an example of unsatisfiable formulas where BLACK nevertheless halts, and stresses the behavior of the solver when nontrivial arithmetic is involved.

The LRA schemata represent behaviors that are only possible in a dense domain. Both build an arbitrary big integer value used to define an arbitrary small fraction to use as the target of the computation. The combined EUF+LIA schema recursively defines a function (inspired by the computational complexity proofs of common sorting algorithms) and forces the model to compute it for the given number of steps.

We can see that these formulas stress the solver but are solved in a manageable amount of time. Globally, this gives evidence of the applicability of our approach to data-aware reasoning.

7 Conclusions

This paper presented LTLf MT , an extension of LTLf where propositional symbols are replaced by first-order formulas over arbitrary theories, `a la SMT. We discussed how the logic can be useful to approach the model-checking problem for data-aware systems and a form of data-aware planning problems. Although LTLf MT is easily seen to be undecidable, we provided a semi-decision procedure in the form of a sound and complete tableau system `a la Reynolds, that we encode into an incremental SMT-based algorithm. We then implemented our approach in BLACK, a state-of-the-art LTL/LTLf satisfiability checker, proving the applicability of the approach with a number of crafted benchmark tests.

Investigating and developing the use cases discussed in Section 3 seems the most natural evolution of this work.

Acknowledgements

This work was supported by the projects VERBA, MENS, TOTA and STAGE by the Free University of Bozen-Bolzano.