Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness

In this paper we study when an LTL formula on finite traces (LTLf formula)isinsensitivetoinfiniteness,thatis,itcanbe correctly handled as a formula on infinite traces under the assumption that at a certain point the infinite trace starts re- peating an end event forever, trivializing all other propositions to false. This intuition has been put forward and (wrongly) assumed to hold in general in the literature. We define a neces- sary and sufficient condition to characterize whether an LTLf formula is insensitive to infiniteness, which can be automati- cally checked by any LTL reasoner. Then, we show that typical LTLf specificationpatternsusedinprocessandservicemod- eling in CS, as well as trajectory constraints in Planning and transition-basedLTLf specificationsofactiondomainsinKR, are indeed very often insensitive to infiniteness. This may help to explain why the assumption of interpreting LTL on finite and on infinite traces has been (wrongly) blurred. Possibly be- cause of this blurring, virtually all literature detours to Bu ̈chi automata for constructing the NFA that accepts the traces satis- fying an LTLf formula. As a further contribution, we give a simple direct algorithm for computing such NFA.