{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:45:58Z","timestamp":1762325158829,"version":"3.37.3"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T00:00:00Z","timestamp":1635984000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T00:00:00Z","timestamp":1635984000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.1007\/s10703-021-00383-3","type":"journal-article","created":{"date-parts":[[2021,11,4]],"date-time":"2021-11-04T09:02:31Z","timestamp":1636016551000},"page":"1-49","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Extended bounded response LTL: a new safety fragment for efficient reactive synthesis"],"prefix":"10.1007","volume":"64","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0000-0002-7125-787X","authenticated-orcid":false,"given":"Luca","family":"Geatti","sequence":"additional","affiliation":[]},{"given":"Nicola","family":"Gigante","sequence":"additional","affiliation":[]},{"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,4]]},"reference":[{"key":"383_CR1","doi-asserted-by":"crossref","unstructured":"Abel A, Reineke J (2015) Memin: SAT-based exact minimization of incompletely specified mealy machines. In: 2015 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). IEEE, pp 94\u2013101","DOI":"10.1109\/ICCAD.2015.7372555"},{"key":"383_CR2","unstructured":"Biere A, Heljanko K, Wieringa S (2011) Aiger 1.9 and beyond. https:\/\/2.zoppoz.workers.dev:443\/http\/fmv.jku.at\/hwmcc11\/beyond1.pdf"},{"issue":"3","key":"383_CR3","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, Saar Y (2012) Synthesis of reactive (1) designs. J Comput Syst Sci 78(3):911\u2013938","journal-title":"J Comput Syst Sci"},{"key":"383_CR4","doi-asserted-by":"crossref","unstructured":"Bloem R, K\u00f6nighofer R, Seidl M (2014) Sat-based synthesis methods for safety specs. In: International conference on verification, model checking, and abstract interpretation. Springer, pp 1\u201320","DOI":"10.1007\/978-3-642-54013-4_1"},{"key":"383_CR5","doi-asserted-by":"crossref","unstructured":"Brayton R, Mishchenko A (2010) ABC: an academic industrial-strength verification tool. In: International conference on computer aided verification. Springer, pp 24\u201340","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"383_CR6","doi-asserted-by":"crossref","unstructured":"B\u00fcchi JR (1990) On a decision method in restricted second order arithmetic. In: The collected works of J. Richard B\u00fcchi. Springer, pp 425\u2013435","DOI":"10.1007\/978-1-4613-8928-6_23"},{"key":"383_CR7","doi-asserted-by":"crossref","unstructured":"Buchi JR, Landweber LH (1990) Solving sequential conditions by finite-state strategies. In: The Collected Works of J. Richard B\u00fcchi. Springer, pp 525\u2013541","DOI":"10.1007\/978-1-4613-8928-6_29"},{"key":"383_CR8","doi-asserted-by":"crossref","unstructured":"Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuxmv symbolic model checker. In: International conference on computer aided verification. Springer, pp 334\u2013342","DOI":"10.1007\/978-3-319-08867-9_22"},{"issue":"3","key":"383_CR9","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1016\/0022-0000(86)90036-X","volume":"32","author":"BS Chlebus","year":"1986","unstructured":"Chlebus BS (1986) Domino-tiling games. J Comput Syst Sci 32(3):374\u2013392","journal-title":"J Comput Syst Sci"},{"key":"383_CR10","unstructured":"Church A (1962) Logic, arithmetic, and automata. In: Proceedings of the international congress of mathematicians, pp 23\u201335"},{"key":"383_CR11","unstructured":"Cimatti A, Geatti L, Gigante N, Montanari, A, Tonetta S (2020) Reactive synthesis from extended bounded response LTL specifications. In: 2020 formal methods in computer aided design (FMCAD). IEEE, pp 83\u201392"},{"issue":"3","key":"383_CR12","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/j.tcs.2007.07.008","volume":"386","author":"L De Alfaro","year":"2007","unstructured":"De Alfaro L, Henzinger TA, Kupferman O (2007) Concurrent reachability games. Theor Comput Sci 386(3):188\u2013217","journal-title":"Theor Comput Sci"},{"key":"383_CR13","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A, Lewkowicz A, Fauchille A, Michaud T, Renault E, Xu L (2016) Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: International symposium on automated technology for verification and analysis. Springer, pp 122\u2013129","DOI":"10.1007\/978-3-319-46520-3_8"},{"issue":"5\u20136","key":"383_CR14","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner B, Schewe S (2013) Bounded synthesis. Int J Softw Tools Technol Transf 15(5\u20136):519\u2013539","journal-title":"Int J Softw Tools Technol Transf"},{"key":"383_CR15","doi-asserted-by":"crossref","unstructured":"Henriksen JG, Jensen J, J\u00f8rgensen M, Klarlund N, Paige R, Rauhe T, Sandholm A (1995) Mona: Monadic second-order logic in practice. In International workshop on tools and algorithms for the construction and analysis of systems. Springer, pp 89\u2013110","DOI":"10.1007\/3-540-60630-0_5"},{"key":"383_CR16","unstructured":"Jacobs S, Bloem R (2018) The 5th reactive synthesis competition\u2014SYNTCOMP 2018. In: SYNT workshop at FLoC"},{"issue":"3","key":"383_CR17","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10009-016-0416-3","volume":"19","author":"S Jacobs","year":"2017","unstructured":"Jacobs S, Bloem R, Brenguier R, Ehlers R, Hell T, K\u00f6nighofer R, P\u00e9rez GA, Raskin JF, Ryzhyk L, Sankur O et al (2017) The 1st reactive synthesis competition\u2014SYNTCOMP 2014. Int J Softw Tools Technol Transf 19(3):367\u2013390","journal-title":"Int J Softw Tools Technol Transf"},{"key":"383_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi MY (2005) Safraless decision procedures. In: 46th annual IEEE symposium on foundations of computer science (FOCS\u201905). IEEE, pp 531\u2013540","DOI":"10.1109\/SFCS.2005.66"},{"issue":"5","key":"383_CR19","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker M, Schallhart C (2009) A brief account of runtime verification. J Logic Algebr Program 78(5):293\u2013303","journal-title":"J Logic Algebr Program"},{"issue":"1","key":"383_CR20","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"O Lichtenstein","year":"2000","unstructured":"Lichtenstein O, Pnueli A (2000) Propositional temporal logics: decidability and completeness. Log J IGPL 8(1):55\u201385. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1093\/jigpal\/8.1.55","journal-title":"Log J IGPL"},{"issue":"1","key":"383_CR21","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00236-019-00349-3","volume":"57","author":"M Luttenberger","year":"2020","unstructured":"Luttenberger M, Meyer PJ, Sickert S (2020) Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica 57(1):3\u201336","journal-title":"Acta Informatica"},{"key":"383_CR22","doi-asserted-by":"publisher","unstructured":"Maler O, Nickovic D, Pnueli A (2005) Real time temporal logic: past, present, future. In: Pettersson P, Yi W (eds) Formal modeling and analysis of timed systems, Third international conference, FORMATS 2005, Uppsala, Sweden, September 26\u201328, 2005, Proceedings. Lecture Notes in Computer Science, vol 3829. Springer, pp 2\u201316. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/11603009_2","DOI":"10.1007\/11603009_2"},{"key":"383_CR23","doi-asserted-by":"publisher","unstructured":"Maler O, Nickovic D, Pnueli A (2007) On synthesizing controllers from bounded-response properties. In: Damm W, Hermanns H (eds) Computer aided verification, 19th international conference, CAV 2007, Berlin, Germany, July 3\u20137, 2007, Proceedings. Lecture Notes in Computer Science, vol 4590. Springer, pp 95\u2013107. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-540-73368-3_12","DOI":"10.1007\/978-3-540-73368-3_12"},{"key":"383_CR24","doi-asserted-by":"publisher","unstructured":"Montanari A, Puppis G, Sala P, Sciavicco G (2010) Decidability of the interval temporal logic ABB over the natural numbers. In: Marion, J, Schwentick T (eds) 27th international symposium on theoretical aspects of computer science, STACS 2010, March 4\u20136, 2010, Nancy, France. LIPIcs, vol\u00a05, pp 597\u2013608. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.4230\/LIPIcs.STACS.2010.2488","DOI":"10.4230\/LIPIcs.STACS.2010.2488"},{"key":"383_CR25","doi-asserted-by":"crossref","unstructured":"Piterman N, Pnueli A, Sa\u2019ar Y (2006) Synthesis of reactive (1) designs. In: International workshop on verification, model checking, and abstract interpretation. Springer, pp 364\u2013380","DOI":"10.1007\/11609773_24"},{"key":"383_CR26","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, Rhode Island, USA, 31 October\u20131 November 1977. IEEE Computer Society, pp 46\u201357. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"383_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of an asynchronous reactive module. In: International colloquium on automata, languages, and programming. Springer, pp 652\u2013671","DOI":"10.1007\/BFb0035790"},{"key":"383_CR28","unstructured":"Rosner R (1992) Modular synthesis of reactive systems. PhD thesis, Weizmann Institute of Science"},{"key":"383_CR29","doi-asserted-by":"publisher","unstructured":"Sebastiani R, Tonetta S (2003) \u201cMore deterministic\u201d vs. \u201csmaller\u201d B\u00fcchi automata for efficient LTL model checking. In: Geist D, Tronci E (eds) CHARME, Lecture notes in computer science, vol 2860. Springer, pp 126\u2013140. https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-540-39724-3_12","DOI":"10.1007\/978-3-540-39724-3_12"},{"key":"383_CR30","series-title":"Lecture notes in pure and applied mathematics","first-page":"331","volume-title":"The convenience of tilings","author":"Boas P van Emde","year":"1997","unstructured":"van Emde Boas P et al (1997) The convenience of tilings. Lecture notes in pure and applied mathematics. CRC Press, Boca Raton, pp 331\u2013363"},{"issue":"1","key":"383_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi MY, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1\u201337","journal-title":"Inf Comput"},{"key":"383_CR32","doi-asserted-by":"crossref","unstructured":"Zhu S, Tabajara LM, Li J, Pu G, Vardi MY (2017) A symbolic approach to safety LTL synthesis. In: Haifa verification conference. Springer, pp 147\u2013162","DOI":"10.1007\/978-3-319-70389-3_10"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00383-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/article\/10.1007\/s10703-021-00383-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00383-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T18:02:46Z","timestamp":1735408966000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/10.1007\/s10703-021-00383-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,4]]},"references-count":32,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["383"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/s10703-021-00383-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,11,4]]},"assertion":[{"value":"5 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 September 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 November 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}