We study Linear Temporal Logic Modulo Theories over Finite Traces (LTL^MT_f), a recently introduced extension of LTL over finite traces (LTL_f) where propositions are replaced by first-order formulas and where first-order variables referring to different time points can be compared. In general, LTL^MT_f was shown to be semi-decidable for any decidable first-order theory (e.g., linear arithmetics), with a tableau-based semi-decision procedure.

In this paper we present a sound and complete pruning rule for the LTL^MT_f tableau. We show that for any LTL^MT_f formula that satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with the new rule is also guaranteed to terminate. Last but not least, this technique allows us to establish novel decidability results for the satisfiability of several fragments of LTL^MT_f, as well as to give new decidability proofs for classes that are already known.