BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260922T121723Z
UID:Seminar-dept-1263@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Lutz Oettershagen:MAILTO:Lutz.Oettershagen@liverpool.ac.uk
DTSTART:20250318T130000
DTEND:20250318T140000
SUMMARY:School Seminar Series
DESCRIPTION:Giuseppe De Giacomo: From Infinite to Finite Traces and Back: Linear Temporal Logic in Sequential Decision Making\n\nLinear 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.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1263
LOCATION:ELEC204, 2th Floor Lecture Theatre EEE
END:VEVENT
END:VCALENDAR