Synthesis United: Live Synthesis

Add to your list(s) Download to your calendar using vCal

• 
• Monday 18 July 2022, 16:30-17:00
• Discussion Room, Newton Institute.

If you have a question about this talk, please contact nobody.

VSO2 - Verified software

Synthesis automatically constructs an implementation that satisfies a given logical specification. In this talk, we study the live synthesis problem, where the synthesized implementation replaces an already running system. In addition to satisfying its own specification, the synthesized implementation must guarantee a sound transition from the previous implementation. This version of the synthesis problem is highly relevant in always-on applications, where updates happen while the system is running. To specify the correct handover between the old and new implementation, we introduce an extension of linear-time temporal logic (LTL) called LiveLTL. A LiveLTL specification defines separate requirements on the two implementations and ensures that the new implementation satisfies, in addition to its own requirements, any obligations left unfinished by the old implementation. For specifications in LiveLTL, we show that the live synthesis problem can be solved within the same complexity bound as standard reactive synthesis, i.e., in 2EXPTIME. Our experiments show the necessity of live synthesis for LiveLTL specifications created from benchmarks of SYNTCOMP and robot control.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Discussion Room, Newton Institute
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• bld31

Note that ex-directory lists are not shown.