BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260408T090221Z
UID:Seminar-pizza-1343@lxserverA.csc.liv.ac.uk.csc.liv.ac.uk
ORGANIZER:CN=Qiyi Tang:MAILTO:Qiyi.Tang@liverpool.ac.uk
DTSTART:20251010T110000
DTEND:20251010T120000
SUMMARY:Friday Lunch and Talk Series
DESCRIPTION:Daniel Hausmann: Manna-Pnueli Games for Reactive Synthesis\n\nRecently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLf+ and PPLTL+, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. This talk will present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game. We then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved symbolically by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1343
LOCATION:ALT
END:VEVENT
END:VCALENDAR