M.: Reasoning on ltl on finite traces: Insensitivity to infiniteness

In this paper we study when an LTL formula on finite traces (LTLf formula) is insensitive to infiniteness, that is, it can be 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 specification patterns used in process and service mod-eling in CS, as well as trajectory constraints in Planning and transition-based LTLf specifications of action domains in KR, 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 Bü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.