{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,24]],"date-time":"2026-09-24T06:46:45Z","timestamp":1790232405733,"version":"4.1.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030763831","type":"print"},{"value":"9783030763848","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-76384-8_8","type":"book-chapter","created":{"date-parts":[[2021,5,18]],"date-time":"2021-05-18T23:50:53Z","timestamp":1621381853000},"page":"113-130","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Specification Decomposition for Reactive Synthesis"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gideon","family":"Geier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Noemi","family":"Passing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,5,19]]},"reference":[{"key":"8_CR1","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report 11\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-662-46681-0_50","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Chatterjee, K., Jacobs, S., K\u00f6nighofer, R.: Assume-guarantee synthesis for concurrent reactive programs with partial information. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 517\u2013532. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_50"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-540-71209-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 261\u2013275. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_21"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science. LICS 1989, pp. 353\u2013362. IEEE Computer Society (1989). https:\/\/doi.org\/10.1109\/LICS.1989.39190","DOI":"10.1109\/LICS.1989.39190"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-21437-0_4","volume-title":"FM 2011: Formal Methods","author":"W Damm","year":"2011","unstructured":"Damm, W., Finkbeiner, B.: Does it pay to extend the perimeter of a world model? In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 12\u201326. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_4"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-89960-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Dureja","year":"2018","unstructured":"Dureja, R., Rozier, K.Y.: More scalable LTL model checking via discovering design-space dependencies ($$D^{3}$$). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 309\u2013327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_17"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 a framework for LTL and $$\\omega $$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-19835-9_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272\u2013275. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_25"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-63390-9_17","volume-title":"Computer Aided Verification","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: an experimentation framework for bounded synthesis. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 325\u2013332. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-15643-4_10","volume-title":"Automated Technology for Verification and Analysis","author":"E Filiot","year":"2010","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 112\u2013127. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15643-4_10"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B.: Synthesis of reactive systems. In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Dependable Software Systems Engineering. NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 45, pp. 72\u201398. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-72","DOI":"10.3233\/978-1-61499-627-9-72"},{"key":"8_CR12","unstructured":"Finkbeiner, B., Geier, G., Passing, N.: Specification decomposition for reactive synthesis (full version). CoRR abs\/2103.08459 (2021). https:\/\/arxiv.org\/abs\/2103.08459"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-030-59152-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"B Finkbeiner","year":"2020","unstructured":"Finkbeiner, B., Passing, N.: Dependency-based compositional synthesis. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 447\u2013463. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_25"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Geier, G., Heim, P., Klein, F., Finkbeiner, B.: Syntroids: synthesizing a game for FPGAs using temporal logic specifications. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019, Proceedings, pp. 138\u2013146. IEEE (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894261","DOI":"10.23919\/FMCAD.2019.8894261"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Bloem, R.: The reactive synthesis competition: SYNTCOMP 2016 and beyond. In: Piskac, R., Dimitrova, R. (eds.) Fifth Workshop on Synthesis, SYNT@CAV 2016, Proceedings. EPTCS, vol. 229, pp. 133\u2013148 (2016). https:\/\/doi.org\/10.4204\/EPTCS.229.11","DOI":"10.4204\/EPTCS.229.11"},{"key":"8_CR16","unstructured":"Jacobs, S., et al.: The 5th reactive synthesis competition (SYNTCOMP 2018): benchmarks, participants & results. CoRR abs\/1904.07736 (2019). http:\/\/arxiv.org\/abs\/1904.07736"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Piskac, R., Dimitrova, R. (eds.) Fifth Workshop on Synthesis, SYNT@CAV 2016, Proceedings. EPTCS, vol. 229, pp. 112\u2013132 (2016). https:\/\/doi.org\/10.4204\/EPTCS.229.10","DOI":"10.4204\/EPTCS.229.10"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Jobstmann, B.: Applications and optimizations for LTL synthesis. Ph.D. thesis, Graz University of Technology (2007)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31\u201344. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_6"},{"key":"8_CR20","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS) 2005, Proceedings, pp. 531\u2013542. IEEE Computer Society (2005)"},{"issue":"11","key":"8_CR21","doi-asserted-by":"publisher","first-page":"3215","DOI":"10.1109\/TCAD.2020.3012641","volume":"39","author":"R Majumdar","year":"2020","unstructured":"Majumdar, R., Mallik, K., Schmuck, A., Zufferey, D.: Assume-guarantee distributed synthesis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(11), 3215\u20133226 (2020). https:\/\/doi.org\/10.1109\/TCAD.2020.3012641","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/978-3-319-96145-3_31","volume-title":"Computer Aided Verification","author":"PJ Meyer","year":"2018","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 578\u2013586. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31"},{"key":"8_CR23","unstructured":"P\u00e9rez, G.A.: The extended HOA format for synthesis. CoRR abs\/1912.05793 (2019). http:\/\/arxiv.org\/abs\/1912.05793"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science 1977, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages 1989, pp. 179\u2013190. ACM Press (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5","volume-title":"Compositionality: The Significant Difference","year":"1998","unstructured":"de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.): COMPOS 1997. LNCS, vol. 1536. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49213-5"},{"issue":"5\u20136","key":"8_CR27","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s10009-012-0224-3","volume":"15","author":"S Sohail","year":"2013","unstructured":"Sohail, S., Somenzi, F.: Safety first: a two-stage algorithm for the synthesis of reactive systems. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 433\u2013454 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0224-3","journal-title":"Int. J. Softw. Tools Technol. Transf."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-76384-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,18]],"date-time":"2021-05-18T23:54:42Z","timestamp":1621382082000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-76384-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030763831","9783030763848"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-76384-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 May 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 May 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"66","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}