From Infinite to Finite Traces and Back: Linear Temporal Logic in Sequential Decision Making

18^th March 2025, 13:00 ELEC204, 2th Floor Lecture Theatre EEE
Giuseppe De Giacomo
University of Oxford

Abstract

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 effectiveness 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.

Biography

Giuseppe De Giacomo is a Professor of Computer Science at the Department of Computer Science of the University of Oxford. He has been previously a Professor at the Department of Computer, Control, and Management Engineering of the University of Roma "La Sapienza". His research activity concerns theoretical, methodological, and practical aspects in different areas of AI and CS, most prominently Knowledge Representation, Reasoning about Actions, Generalized Planning, Autonomous Agents, Reactive Synthesis and Verification, Service Composition, Business Process Modeling, and Data Management and Integration. He is an AAAI Fellow, ACM Fellow, and EurAI Fellow. He received an ERC Advanced Grant for the project WhiteMech: White-box Self Programming Mechanisms. He was the Program Chair of ECAI 2020 and KR 2014. He is on the Board of EurAI. He chairs the steering committee of the new EurAI yearly summer school ESSAI.