CISPA
Browse
cispa_all_3678.pdf (510.5 kB)

Live Synthesis

Download (510.5 kB)
conference contribution
posted on 2023-11-29, 18:18 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 al- ready 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: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date

2022-05-09

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3678, title = "Live Synthesis", author = "Finkbeiner, Bernd and Klein, Felix and Metzger, Niklas", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC