Reasoning on LTL on finite traces: Insensitivity to infiniteness

Abstract

In this paper we study when an LTL formula on finite traces (LTL/ 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 repeating 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 necessary and sufficient condition to characterize whether an LTL/ formula is insensitive to infiniteness, which can be automatically checked by any LTL reasoner. Then, we show that typical LTL/ specification patterns used in process and service modeling in CS, as well as trajectory constraints in Planning and transition-based LTL/ 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 because of this blurring, virtually all literature detours to Buchi automata for constructing the NFA that accepts the traces satisfying an LTL/ formula. As a further contribution, we give a simple direct algorithm for computing such NFA.