Live Synthesis
Bernd Finkbeiner, Felix Klein, Niklas Metzger

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Model-Driven Software Engineering Techniques
