Live Synthesis

TL;DR

This paper introduces live synthesis, a method for updating running systems while ensuring seamless transition and correctness, using an extended logic called LiveLTL, with solutions applicable within known complexity bounds.

Contribution

The paper proposes LiveLTL, an extension of LTL for specifying live synthesis requirements, and demonstrates that live synthesis can be solved with the same complexity as standard reactive synthesis.

Findings

Live synthesis is feasible within 2EXPTIME complexity.

LiveLTL effectively specifies transition requirements between old and new implementations.

Experimental results confirm the practicality of live synthesis for benchmarks and robot control.

Abstract

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.