=Paper=
{{Paper
|id=Vol-3876/invited1
|storemode=property
|title=From Infinite to Finite Traces and Back: Linear Temporal Logic in Sequential Decision Making
|pdfUrl=https://ceur-ws.org/Vol-3876/invited1.pdf
|volume=Vol-3876
|authors=Giuseppe De Giacomo
|dblpUrl=https://dblp.org/rec/conf/kodis/Giacomo24
}}
==From Infinite to Finite Traces and Back: Linear Temporal Logic in Sequential Decision Making==
<pdf width="1500px">https://ceur-ws.org/Vol-3876/invited1.pdf</pdf>
<pre>
                         Invited Talk: From Infinite to Finite Traces and Back:
                         Linear Temporal Logic in Sequential Decision Making
                         Giuseppe De Giacomo
                         University of Oxford, Oxford, UK
                         Sapienza University, Rome, Italy


                                      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.

                                      Keywords
                                      Linear Temporal Logic, Linear Temporal Logic on Finite Traces, Reactive Synthesis, Autonomous Decision Making




                         1. Author 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.




                          Workshop on Symbolic and Neuro-Symbolic Architectures for Intelligent Robotics Technology (SYNERGY) co-located with the
                          21st International Conference on Principles of Knowledge Representation and Reasoning (KR2024), November 2–8, 2024, Hanoi,
                          Vietnam.
                          $ giuseppe.degiacomo@cs.ox.ac.uk (G. De Giacomo)
                          € https://www.cs.ox.ac.uk/people/giuseppe.degiacomo/ (G. De Giacomo)
                           0000-0001-9680-7658 (G. De Giacomo)
                                   © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).


CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings

</pre>