Abstract
Linear temporal logic over finite traces is used as a
formalism for temporal specification in automated
planning, process modelling and (runtime) verification. In this paper, we investigate first-order temporal logic over finite traces, lifting some known
results to a more expressive setting. Satisfiability in
the two-variable monodic fragment is shown to be
EXPSPACE-complete, as for the infinite trace case,
while it decreases to NEXPTIME when we consider
finite traces bounded in the number of instants. This
leads to new complexity results for temporal description logics over finite traces. We further investigate
satisfiability and equivalences of formulas under a
model-theoretic perspective, providing a set of semantic conditions that characterise when the distinction between reasoning over finite and infinite traces
can be blurred. Finally, we apply these conditions
to planning and verification