CISPA
Browse
cispa_all_3681.pdf (454.58 kB)

Live synthesis

Download (454.58 kB)
journal contribution
posted on 2023-11-29, 18:06 authored by Bernd FinkbeinerBernd Finkbeiner, Felix Klein, Niklas MetzgerNiklas Metzger
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.

History

Preferred Citation

Bernd Finkbeiner, Felix Klein and Niklas Metzger. Live synthesis. In: Innovations in Systems and Software Engineering. 2022.

Primary Research Area

  • Threat Detection and Defenses

Legacy Posted Date

2022-05-09

Journal

Innovations in Systems and Software Engineering

Open Access Type

  • Gold

Sub Type

  • Article

BibTeX

@article{cispa_all_3681, title = "Live synthesis", author = "Finkbeiner, Bernd and Klein, Felix and Metzger, Niklas", journal="{Innovations in Systems and Software Engineering}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC