BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Synthesis United: Live Synthesis - 
DTSTART:20220718T153000Z
DTEND:20220718T160000Z
UID:TALK176768@talks.cam.ac.uk
DESCRIPTION:Synthesis automatically constructs an implementation that sati
 sfies a given logical specification. In this talk\, we study the live synt
 hesis problem\, where the synthesized implementation replaces an already r
 unning system. In addition to satisfying its own specification\, the synth
 esized implementation must guarantee a sound transition from the previous 
 implementation. This version of the synthesis problem is highly relevant i
 n always-on applications\, where updates happen while the system is runnin
 g. To specify the correct handover between the old and new implementation\
 , we introduce an extension of linear-time temporal logic (LTL) called Liv
 eLTL. A LiveLTL specification defines separate requirements on the two imp
 lementations and ensures that the new implementation satisfies\, in additi
 on to its own requirements\, any obligations left unfinished by the old im
 plementation. For specifications in LiveLTL\, we show that the live synthe
 sis problem can be solved within the same complexity bound as standard rea
 ctive synthesis\, i.e.\, in 2EXPTIME. Our experiments show the necessity o
 f live synthesis for LiveLTL specifications created from benchmarks of SYN
 TCOMP and robot control.
LOCATION:Discussion Room\, Newton Institute
END:VEVENT
END:VCALENDAR