Live synthesis

Area of Science:

• Computer Science
• Formal Methods
• Software Engineering

Background:

• Automated synthesis generates implementations from logical specifications.
• Live synthesis addresses the challenge of updating running systems without downtime.
• Always-on applications require seamless transitions between system versions.

Purpose of the Study:

• To introduce and solve the live synthesis problem for systems requiring continuous operation.
• To develop a formal logic, LiveLTL, for specifying transitions between old and new implementations.
• To analyze the computational complexity of live synthesis.

Main Methods:

• Introduced LiveLTL, an extension of linear-time temporal logic (LTL), to specify handover requirements.
• Developed algorithms for live synthesis that consider both the new implementation's specification and the old one's unfinished obligations.
• Analyzed the complexity of the proposed live synthesis approach.

Main Results:

• The live synthesis problem for LiveLTL specifications can be solved with a 2EXPTIME complexity bound, matching standard reactive synthesis.
• Experimental results demonstrate the necessity of live synthesis for critical applications.
• Validated the approach using benchmarks from SYNTCOMP and robot control.

Conclusions:

• Live synthesis provides a formal framework for updating running systems safely.
• LiveLTL effectively captures the requirements for sound transitions in always-on systems.
• The 2EXPTIME complexity is feasible for practical applications of live synthesis.