Abstract
Linear temporal logic interpreted over finite traces (LTLf ) has been used as a formalism for temporal specification in automated planning, process modelling and (runtime) verification. In this paper, we lift some results from the propositional case to a decidable fragment of first-order temporal logic obtained by combining the description logic ALC with LTLf , denoted as TfU ALC. We show that the satisfiability problem in TfU ALC is ExpSpace-complete, as already known for the infinite trace case, while it decreases to NExpTime when we consider finite traces with a fixed number of instants, and even to ExpTime when additionally restricting to globally interpreted TBoxes. Moreover, we investigate two model-theoretical notions for TfU ALC: we show that, differently from the infinite trace case, it enjoys the bounded model property; we also discuss the notion of insensitivity to infiniteness, providing characterisations and sufficient conditions to preserve it.