{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T05:56:33Z","timestamp":1785304593470,"version":"3.55.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T00:00:00Z","timestamp":1648684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T00:00:00Z","timestamp":1648684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683300"],"award-info":[{"award-number":["683300"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001736","name":"German-Israeli Foundation for Scientific Research and Development","doi-asserted-by":"publisher","award":["I-1513-407.\/2019"],"award-info":[{"award-number":["I-1513-407.\/2019"]}],"id":[{"id":"10.13039\/501100001736","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["TRR 248, 389792660"],"award-info":[{"award-number":["TRR 248, 389792660"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2022,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Synthesis automatically constructs an implementation that satisfies a given logical specification. In this paper, we study the <jats:italic>live synthesis<\/jats:italic> 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 \u201calways-on\u201d 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 <jats:italic>LiveLTL<\/jats:italic>. 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.<\/jats:p>","DOI":"10.1007\/s11334-022-00447-5","type":"journal-article","created":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T09:03:56Z","timestamp":1648717436000},"page":"443-454","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Live synthesis"],"prefix":"10.1007","volume":"18","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Felix","family":"Klein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Niklas","family":"Metzger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,3,31]]},"reference":[{"key":"447_CR1","doi-asserted-by":"crossref","unstructured":"Baumann A, Heiser G, Appavoo J, Silva DD, Krieger O, Wisniewski RW, Kerr J (2005) Providing dynamic update in an operating system. In: USENIX","DOI":"10.1145\/1095810.1118622"},{"key":"447_CR2","unstructured":"Biere A (2007) The AIGER and-inverter graph (AIG) format version 20071012. Technical Report 07\/1, Institute for formal models and verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria"},{"key":"447_CR3","unstructured":"Chen Y, Zhang Y, Wang Z, Xia L, Bao C, Wei T (2017) Adaptive android kernel live patching. In: Kirda E, Ristenpart T (eds) USENIX Security"},{"key":"447_CR4","doi-asserted-by":"publisher","unstructured":"Duret-Lutz A, Lewkowicz A, Fauchille A, Michaud T, Renault E, Xu L (2016) Spot 2.0 - A framework for LTL and $$\\omega $$ -automata manipulation. In: ATVA, LNCS. https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"447_CR5","doi-asserted-by":"publisher","unstructured":"Esparza J, Kret\u00ednsk\u00fd J (2014) From LTL to deterministic automata: a safraless compositional approach. In: CAV. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_13","DOI":"10.1007\/978-3-319-08867-9_13"},{"key":"447_CR6","doi-asserted-by":"publisher","unstructured":"Esparza J, Kret\u00ednsk\u00fd J, Raskin J, Sickert S (2017) From LTL and limit-deterministic b\u00fcchi automata to deterministic parity automata. In: TACAS. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_25","DOI":"10.1007\/978-3-662-54577-5_25"},{"key":"447_CR7","unstructured":"Fabry RS (1976) How to design a system in which modules can be changed on the fly. In: ICSE. IEEE Computer Society, Proceedings of the 2nd international conference on Software engineering, pp. 470\u2013476"},{"key":"447_CR8","doi-asserted-by":"publisher","unstructured":"Faymonville P, Finkbeiner B, Tentrup L (2017) Bosy: An experimentation framework for bounded synthesis. In: CAV, pp. 470\u2013476. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"447_CR9","doi-asserted-by":"publisher","unstructured":"Finkbeiner B, Klein F, Metzger N (2021) Live synthesis. In: Hou Z, Ganesh V (eds) Automated technology for verification and analysis - 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings, Lecture Notes in Computer Science, vol. 12971, pp. 153\u2013169. Springer. https:\/\/doi.org\/10.1007\/978-3-030-88885-5_11","DOI":"10.1007\/978-3-030-88885-5_11"},{"key":"447_CR10","doi-asserted-by":"publisher","unstructured":"Frieder O, Segal ME (1991) On dynamically updating a computer program: from concept to prototype. JSS. https:\/\/doi.org\/10.1016\/0164-1212(91)90096-O","DOI":"10.1016\/0164-1212(91)90096-O"},{"key":"447_CR11","doi-asserted-by":"publisher","unstructured":"Ghezzi C, Greenyer J, Manna VPL (2012) Synthesizing dynamically updating controllers from changes in scenario-based specifications. In: SEAMS. IEEE Computer Society. https:\/\/doi.org\/10.1109\/SEAMS.2012.6224401","DOI":"10.1109\/SEAMS.2012.6224401"},{"key":"#cr-split#-447_CR12.1","unstructured":"Giacomo GD, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Rossi F"},{"key":"#cr-split#-447_CR12.2","unstructured":"(ed) IJCAI 2013, Proceedings of the 23rd international joint conference on artificial intelligence, Beijing, China, August 3-9, 2013, pp. 854-860. IJCAI\/AAAI. http:\/\/www.aaai.org\/ocs\/index.php\/IJCAI\/IJCAI13\/paper\/view\/6997"},{"key":"447_CR13","doi-asserted-by":"publisher","unstructured":"Giuffrida C, Kuijsten A, Tanenbaum AS Safe and automatic live update for operating systems. SIGPLAN Not. 48. https:\/\/doi.org\/10.1145\/2499368.2451147","DOI":"10.1145\/2499368.2451147"},{"key":"447_CR14","doi-asserted-by":"publisher","DOI":"10.1002\/smr.406","author":"AR Gregersen","year":"2009","unstructured":"Gregersen AR, J\u00f8rgensen BN (2009) Dynamic update of java applications - balancing change flexibility vs programming transparency. JSWM. https:\/\/doi.org\/10.1002\/smr.406","journal-title":"JSWM"},{"key":"447_CR15","doi-asserted-by":"publisher","unstructured":"Hayden CM, Magill S, Hicks M, Foster N, Foster JS (2012) Specifying and verifying the correctness of dynamic software updates. In: Joshi R, M\u00fcller P, Podelski A (eds) VSTTE, LNCS. https:\/\/doi.org\/10.1007\/978-3-642-27705-4_22","DOI":"10.1007\/978-3-642-27705-4_22"},{"key":"447_CR16","unstructured":"Hjalmtysson G, Gray R Dynamic C++ classes - A lightweight mechanism to update code in a running program. In: USENIX 1998. USENIX Association"},{"key":"447_CR17","doi-asserted-by":"publisher","unstructured":"Jacobs S, Basset N, Bloem R, Brenguier R, Colange M, Faymonville P, Finkbeiner B, Khalimov A, Klein F, Michaud T, P\u00e9rez GA, Raskin J, Sankur O, Tentrup L (2017) SYNTCOMP 2017. In: SYNT@CAV. https:\/\/doi.org\/10.4204\/EPTCS.260.10","DOI":"10.4204\/EPTCS.260.10"},{"key":"447_CR18","doi-asserted-by":"publisher","unstructured":"Li J, Zhang L, Pu G, Vardi MY, He J (2014) LTLf satisfiability checking. In: ECAI, FAIA. https:\/\/doi.org\/10.3233\/978-1-61499-419-0-513","DOI":"10.3233\/978-1-61499-419-0-513"},{"key":"447_CR19","doi-asserted-by":"publisher","unstructured":"Makris K, Ryu KD (2007) Dynamic and adaptive updates of non-quiescent subsystems in commodity operating system kernels. In: EuroSys. ACM. https:\/\/doi.org\/10.1145\/1272996.1273031","DOI":"10.1145\/1272996.1273031"},{"key":"447_CR20","doi-asserted-by":"publisher","unstructured":"Manna VPL, Greenyer J, Ghezzi C, Brenner C (2013) Formalizing correctness criteria of dynamic updates derived from specification changes. In: SEAMS. IEEE Computer Society. https:\/\/doi.org\/10.1109\/SEAMS.2013.6595493","DOI":"10.1109\/SEAMS.2013.6595493"},{"key":"447_CR21","doi-asserted-by":"publisher","unstructured":"Menghi C, Tsigkanos C, Berger T, Pelliccione P, Ghezzi C (2018) Property specification patterns for robotic missions. In: ICSE 2018. ACM. https:\/\/doi.org\/10.1145\/3183440.3195044","DOI":"10.1145\/3183440.3195044"},{"key":"447_CR22","doi-asserted-by":"publisher","unstructured":"Meyer PJ, Sickert S, Luttenberger M (2018) Strix: explicit reactive synthesis strikes back! In: Chockler H, Weissenbacher G (eds) CAV 2018, LNCS. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"447_CR23","doi-asserted-by":"publisher","unstructured":"Nahabedian L, Braberman VA, D\u2019Ippolito N, Honiden S, Kramer J, Tei K, Uchitel S (2016) Assured and correct dynamic update of controllers. In: SEAMS@ICSE 2016. ACM. https:\/\/doi.org\/10.1145\/2897053.2897056","DOI":"10.1145\/2897053.2897056"},{"key":"447_CR24","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: SFCS. https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"447_CR25","doi-asserted-by":"publisher","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Conference record of the sixteenth annual ACM symposium on principles of programming languages, Austin, Texas, USA, January 11-13, pp. 179\u2013190. ACM Press (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00447-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-022-00447-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00447-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,12]],"date-time":"2022-09-12T06:43:56Z","timestamp":1662965036000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-022-00447-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,31]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9]]}},"alternative-id":["447"],"URL":"https:\/\/doi.org\/10.1007\/s11334-022-00447-5","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,31]]},"assertion":[{"value":"23 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 March 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}