{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:26:40Z","timestamp":1745994400683,"version":"3.37.3"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,3,15]],"date-time":"2023-03-15T00:00:00Z","timestamp":1678838400000},"content-version":"vor","delay-in-days":104,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Linear Temporal Logic (<jats:sc>LTL<\/jats:sc>) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in <jats:sc>LTL<\/jats:sc>. Unfortunately it has been proved to be too difficult computationally to perform full <jats:sc>LTL<\/jats:sc> synthesis. There have been two success stories with <jats:sc>LTL<\/jats:sc> synthesis, both having to do with the form of the specification. The first is the <jats:sc>GR(1)<\/jats:sc> approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or <jats:sc>GR(1)<\/jats:sc>. The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with <jats:sc>LTL<\/jats:sc><jats:inline-formula><jats:alternatives><jats:tex-math>$$_f$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mrow\/>\n                    <mml:mi>f<\/mml:mi>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> (<jats:sc>LTL<\/jats:sc> on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an <jats:sc>LTL<\/jats:sc><jats:inline-formula><jats:alternatives><jats:tex-math>$$_f$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mrow\/>\n                    <mml:mi>f<\/mml:mi>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> agent goal and a <jats:sc>GR(1)<\/jats:sc> environment specification. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of <jats:sc>LTL<\/jats:sc> synthesis.<\/jats:p>","DOI":"10.1007\/s10703-023-00413-2","type":"journal-article","created":{"date-parts":[[2023,3,15]],"date-time":"2023-03-15T15:03:04Z","timestamp":1678892584000},"page":"139-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Finite-trace and generalized-reactivity specifications in temporal synthesis"],"prefix":"10.1007","volume":"61","author":[{"given":"Giuseppe","family":"De Giacomo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5475-2978","authenticated-orcid":false,"given":"Antonio","family":"Di Stasio","sequence":"additional","affiliation":[]},{"given":"Lucas M.","family":"Tabajara","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]},{"given":"Shufang","family":"Zhu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,3,15]]},"reference":[{"key":"413_CR1","first-page":"72","volume":"45","author":"B Finkbeiner","year":"2016","unstructured":"Finkbeiner B (2016) Synthesis of reactive systems. Depend Softw Syst Eng 45:72\u201398","journal-title":"Depend Softw Syst Eng"},{"issue":"2","key":"413_CR2","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10626-015-0223-0","volume":"27","author":"R Ehlers","year":"2017","unstructured":"Ehlers R, Lafortune S, Tripakis S, Vardi MY (2017) Supervisory control and reactive synthesis: a comparative introduction. Discrete Event Dyn Syst 27(2):209\u2013260","journal-title":"Discrete Event Dyn Syst"},{"key":"413_CR3","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: POPL, pp 179\u2013190","DOI":"10.1145\/75277.75293"},{"key":"413_CR4","doi-asserted-by":"crossref","unstructured":"Kupferman O (2012) Recent challenges and ideas in temporal synthesis. In: SOFSEM 2012, pp 88\u201398","DOI":"10.1007\/978-3-642-27660-6_8"},{"key":"413_CR5","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem R, Jobstmann B, Piterman N, Pnueli A, Sa\u2019ar Y (2012) Synthesis of Reactive(1) designs. J Comput Syst Sci 78:911\u2013938","journal-title":"J Comput Syst Sci"},{"issue":"6","key":"413_CR6","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit H, Fainekos GE, Pappas GJ (2009) Temporal-logic-based reactive mission and motion planning. IEEE Trans Robot 25(6):1370\u20131381","journal-title":"IEEE Trans Robot"},{"key":"413_CR7","unstructured":"De\u00a0Giacomo G, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp 854\u2013860"},{"key":"413_CR8","unstructured":"De\u00a0Giacomo G, Vardi MY (2015) Synthesis for LTL and LDL on finite traces. In: IJCAI"},{"key":"413_CR9","doi-asserted-by":"crossref","unstructured":"Camacho A, Triantafillou E, Muise C, Baier JA, McIlraith S (2017) Non-deterministic planning with temporally extended goals: LTL over finite and infinite traces. In: AAAI, pp 3716\u20133724","DOI":"10.1609\/aaai.v31i1.11058"},{"key":"413_CR10","doi-asserted-by":"crossref","unstructured":"De Giacomo G, Rubin S (2018) Automata-theoretic foundations of fond planning for LTL$$_f$$\/LDL$$_f$$ goals. In: IJCAI, pp 4729\u20134735","DOI":"10.24963\/ijcai.2018\/657"},{"key":"413_CR11","unstructured":"Aminof B, Giacomo GD, Murano A, Rubin S (2018) Planning and synthesis under assumptions. CoRR"},{"key":"413_CR12","unstructured":"Camacho A, Bienvenu M, McIlraith SA (2018) Finite LTL synthesis with environment assumptions and quality measures. In: KR, pp 454\u2013463"},{"key":"413_CR13","doi-asserted-by":"crossref","unstructured":"He K, Wells AM, Kavraki LE, Vardi MY (2019) Efficient symbolic reactive synthesis for finite-horizon tasks. In: ICRA, pp 8993\u20138999","DOI":"10.1109\/ICRA.2019.8794170"},{"key":"413_CR14","doi-asserted-by":"crossref","unstructured":"Zhu S, Giacomo GD, Pu G, Vardi MY (2020) LTL$$_f$$ synthesis with fairness and stability assumptions. In: AAAI, pp 3088\u20133095","DOI":"10.1609\/aaai.v34i03.5704"},{"key":"413_CR15","doi-asserted-by":"crossref","unstructured":"Aminof B, De Giacomo G, Murano A, Rubin S (2019) Planning under LTL environment specifications. In: ICAPS, pp 31\u201339","DOI":"10.1609\/icaps.v29i1.3457"},{"key":"413_CR16","doi-asserted-by":"crossref","unstructured":"De Giacomo G, Di Stasio A, Vardi MY, Zhu S (2020) Two-stage technique for LTL$$_f$$ synthesis under LTL assumptions. In: KR, pp 304\u2013314","DOI":"10.24963\/kr.2020\/31"},{"key":"413_CR17","doi-asserted-by":"crossref","unstructured":"Ghallab M, Nau DS, Traverso P (2004) Automated planning - theory and practice","DOI":"10.1016\/B978-155860856-6\/50021-1"},{"key":"413_CR18","doi-asserted-by":"crossref","unstructured":"De Giacomo G, Di Stasio A, Tabajara LM, Vardi MY, Zhu S (2021) Finite-trace and generalized-reactivity specifications in temporal synthesis. In: IJCAI, pp 1852\u20131858","DOI":"10.24963\/ijcai.2021\/255"},{"key":"413_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: FOCS, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"413_CR20","doi-asserted-by":"crossref","unstructured":"Aminof B, De Giacomo G, Murano A, Rubin S (2019) Planning under LTL environment specifications. In: ICAPS, pp 31\u201339","DOI":"10.1609\/icaps.v29i1.3457"},{"key":"413_CR21","doi-asserted-by":"crossref","unstructured":"Zhu S, Tabajara LM, Li J, Pu G, Vardi MY (2017) Symbolic LTL$$_f$$ synthesis. In: IJCAI, pp 1362\u20131369","DOI":"10.24963\/ijcai.2017\/189"},{"key":"413_CR22","doi-asserted-by":"crossref","unstructured":"Lichtenstein O, Pnueli A, Zuck LD (1985) The glory of the past. In: Logic of programs, pp 196\u2013218","DOI":"10.1007\/3-540-15648-8_16"},{"key":"413_CR23","doi-asserted-by":"crossref","unstructured":"De Giacomo G, Di Stasio A, Fuggitti F, Rubin S (2020) Pure-past linear temporal and dynamic logic on finite traces. In: IJCAI 2020, pp 4959\u20134965","DOI":"10.24963\/ijcai.2020\/690"},{"key":"413_CR24","unstructured":"Somenzi F (2016) CUDD: CU decision diagram package 3.0.0. University of Colorado at Boulder"},{"key":"413_CR25","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-41540-6_18","volume":"9780","author":"R Ehlers","year":"2016","unstructured":"Ehlers R, Raman V (2016) Slugs: extensible GR(1) synthesis, CAV. Lect Notes Comput Sci 9780:333\u2013339","journal-title":"Lect Notes Comput Sci"},{"key":"413_CR26","unstructured":"DeCastro JA, Ehlers R, Rungger M, Balkan A, Tabuada P, Kress-Gazit H (2014) Dynamics-based reactive synthesis and automated revisions for high-level robot control. CoRR arXiv:1410.6375"},{"key":"413_CR27","doi-asserted-by":"crossref","unstructured":"Meyer PJ, Sickert S, Luttenberger M (2018) Strix: explicit reactive synthesis strikes back! In: CAV, pp 578\u2013586","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"413_CR28","unstructured":"Jacobs S, Perez GA (2020) 7th reactive synthesis competition: SYNTCOMP 2020. http:\/\/www.syntcomp.org\/syntcomp-2020-results\/"},{"key":"413_CR29","unstructured":"Sardi\u00f1a S, Giacomo GD (2008) Realizing multiple autonomous agents through scheduling of shared devices. In: ICAPS 2008, pp 304\u2013312"},{"key":"413_CR30","unstructured":"Aminof B, Giacomo GD, Murano A, Rubin S (2018) Synthesis under assumptions. In: KR, pp 615\u2013616"},{"key":"413_CR31","doi-asserted-by":"crossref","unstructured":"Zhu S, De\u00a0Giacomo G, Pu G, Vardi M (2020) LTL$$_f$$ synthesis with fairness and stability assumptions. In: AAAI, pp 3088\u20133095","DOI":"10.1609\/aaai.v34i03.5704"},{"key":"413_CR32","doi-asserted-by":"crossref","unstructured":"Camacho A, Bienvenu M, McIlraith SA (2019) Towards a unified view of AI planning and reactive synthesis. In: ICAPS, pp 58\u201367","DOI":"10.1609\/icaps.v29i1.3460"},{"key":"413_CR33","doi-asserted-by":"crossref","unstructured":"De\u00a0Giacomo G, Felli P, Patrizi F, Sardi\u00f1a S (2010) Two-player game structures for generalized planning and agent composition. In: AAAI, pp 297\u2013302","DOI":"10.1609\/aaai.v24i1.7597"},{"key":"413_CR34","doi-asserted-by":"crossref","unstructured":"Bansal S, Li Y, Tabajara LM, Vardi MY (2020) Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In: AAAI, pp 9766\u20139774","DOI":"10.1609\/aaai.v34i06.6528"},{"key":"413_CR35","doi-asserted-by":"crossref","unstructured":"De Giacomo G, Favorito M (2021) Compositional approach to translate LTL$$_f$$\/LDL$$_f$$ into deterministic finite automata. In: ICAPS 2021, pp 122\u2013130","DOI":"10.1609\/icaps.v31i1.15954"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00413-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00413-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00413-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,4]],"date-time":"2024-03-04T13:20:49Z","timestamp":1709558449000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00413-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":35,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["413"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00413-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2022,12]]},"assertion":[{"value":"2 April 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 January 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}