Live synthesis

DOI10.1007/978-3-030-88885-5_11zbMATH Open1497.68299arXiv2107.01136OpenAlexW3179451681MaRDI QIDQ2147189FDOQ2147189

Niklas Metzger, Felix Klein, Bernd Finkbeiner

Publication date: 22 June 2022

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.

Full work available at URL: https://arxiv.org/abs/2107.01136

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Uses Software

This page was built for publication: Live synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147189)