  Synthesis automatically constructs an implementation that satisfies a given
logical specification. In this paper, 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.
