Linear Temporal Logic (LTL) has a long history in CS and AI due to its ability to express sophisticated temporal properties over infinite traces. Recently, finite-trace variants of LTL, such as LTL on Finite Traces (LTLf) and Pure Past LTL (PPLTL), have gained popularity in AI, particularly in sequential decision-making tasks where an autonomous agent nominally loops through three finite phases: acquiring a goal, reasoning strategically to achieve it, and executing the resulting strategy (or plan). A key advantage of these finite-trace variants is their reducibility to equivalent regular automata, which can be determinized and transformed into two-player games on graphs. This gives them unprecedented computational efectiveness and scalability. Can these advantages be extended to infinite traces? In this talk, we provide a positive answer. By leveraging Manna and Pnueli's safety-progress hierarchy for LTL, we introduce infinite-trace extensions of LTLf and PPLTL that retain the full expressive power of LTL, while preserving the crucial feature that the game arena for strategy extraction can still be derived from deterministic finite automata.
1. Author Biography