Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness


  • Giuseppe De Giacomo Sapienza Università di Roma
  • Riccardo De Masellis Sapienza Università di Roma
  • Marco Montali Free University of Bozen-Bolzano



Linear Temporal Logic on finite traces, LTL patterns, finite-state automata


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 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 LTLf formula is insensitive to infiniteness, which can be automatically checked by any LTL reasoner. Then, we show that typical LTLf specification patterns used in process and service modeling 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 because of this blurring, virtually all literature detours to Buechi automata for constructing the NFA that accepts the traces satisfying an LTLf formula. As a further contribution, we give a simple direct algorithm for computing such NFA.




How to Cite

De Giacomo, G., De Masellis, R., & Montali, M. (2014). Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness. Proceedings of the AAAI Conference on Artificial Intelligence, 28(1).



AAAI Technical Track: Knowledge Representation and Reasoning