{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:15Z","timestamp":1779074595450,"version":"3.51.4"},"publisher-location":"Cham","reference-count":76,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031937057","type":"print"},{"value":"9783031937064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-93706-4_8","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:43Z","timestamp":1749316963000},"page":"116-137","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Mode-Based Reactive Synthesis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9427-9345","authenticated-orcid":false,"given":"Mat\u00edas","family":"Brizzio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3478-3408","authenticated-orcid":false,"given":"Felipe","family":"Gorostiaga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1611-3969","authenticated-orcid":false,"given":"Renzo","family":"Degiovanni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"ISO\/IEC\/IEEE international standard - systems and software engineering \u2013 life cycle processes \u2013requirements engineering. ISO\/IEC\/IEEE 29148:2011(E), pp. 1\u201394 (2011). https:\/\/doi.org\/10.1109\/IEEESTD.2011.6146379","DOI":"10.1109\/IEEESTD.2011.6146379"},{"issue":"7","key":"8_CR2","doi-asserted-by":"publisher","first-page":"817","DOI":"10.1016\/j.ijepes.2010.01.019","volume":"32","author":"H Arabian-Hoseynabadi","year":"2010","unstructured":"Arabian-Hoseynabadi, H., Oraee, H., Tavner, P.: Failure modes and effects analysis (FMEA) for wind turbines. Int. J. Electr. Power Energy Syst. 32(7), 817\u2013824 (2010)","journal-title":"Int. J. Electr. Power Energy Syst."},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Arora, C., Grundy, J., Abdelrazek, M.: Advancing requirements engineering through generative AI: assessing the role of LLMs. CoRR abs\/2310.13976 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2310.13976","DOI":"10.48550\/ARXIV.2310.13976"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Arora, C., Sabetzadeh, M., Briand, L., Zimmer, F.: Extracting domain models from natural-language requirements: approach and industrial evaluation. In: Proceedings of the ACM\/IEEE 19th International Conference on Model Driven Engineering Languages and Systems, MODELS 2016, pp. 250-260. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2976767.2976769","DOI":"10.1145\/2976767.2976769"},{"key":"8_CR5","unstructured":"Arvidsson, S., Axell, J.: Prompt engineering guidelines for LLMs in requirements engineering (2023)"},{"issue":"1","key":"8_CR6","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1109\/TAC.2017.2722960","volume":"63","author":"A Balkan","year":"2017","unstructured":"Balkan, A., Vardi, M., Tabuada, P.: Mode-target games: reactive synthesis for control applications. IEEE Trans. Autom. Control 63(1), 196\u2013202 (2017)","journal-title":"IEEE Trans. Autom. Control"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y.: Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In: AAAI 2020 (2020)","DOI":"10.1609\/aaai.v34i06.6528"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011). https:\/\/doi.org\/10.1145\/2000799.2000800","DOI":"10.1145\/2000799.2000800"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Beame, P., Impagliazzo, R., Pitassi, T., Segerlind, N.: Memoization and DPLL: formula caching proof systems. In: 2003 Proceedings of the 18th IEEE Annual Conference on Computational Complexity, pp. 248\u2013259 (2003). https:\/\/doi.org\/10.1109\/CCC.2003.1214425","DOI":"10.1109\/CCC.2003.1214425"},{"issue":"3","key":"8_CR10","first-page":"911","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. JCSS 78(3), 911\u2013938 (2012)","journal-title":"JCSS"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Brizzio, M.: Resolving goal-conflicts and scaling synthesis through mode-based decomposition. In: Proceedings of the 2024 IEEE\/ACM 46th International Conference on Software Engineering: Companion Proceedings, ICSE-Companion 2024, pp. 207\u2013211. Association for Computing Machinery, New York (2024). https:\/\/doi.org\/10.1145\/3639478.3639801","DOI":"10.1145\/3639478.3639801"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Brizzio, M., Cordy, M., Papadakis, M., S\u00e1nchez, C., Aguirre, N., Degiovanni, R.: Automated Repair of Unrealisable LTL Specifications Guided by Model Counting. In: Proceedings of GECCO 2023, pp. 1499\u20131507. ACM (2023). https:\/\/doi.acm.org\/10.1145\/3583131.3590454","DOI":"10.1145\/3583131.3590454"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Brizzio, M., S\u00e1nchez, C.: Efficient reactive synthesis using mode decomposition. In: \u00c1brah\u00e1m, E., Dubslaff, C., Tarifa, S.L.T. (eds.) ICTAC 2023. LNCS, vol. 14446, pp. 256\u2013275. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-47963-2_16","DOI":"10.1007\/978-3-031-47963-2_16"},{"key":"8_CR14","unstructured":"Brown, T.B., et al.: Language Models are Few-Shot Learners. In: NeurIPS (2020)"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Broy, M.: Multifunctional software systems: structured modeling and specification of functional requirements. Sci. Comput. Program. 75(12), 1193\u20131214 (2010). https:\/\/doi.org\/10.1016\/j.scico.2010.06.007, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S016764231000119X","DOI":"10.1016\/j.scico.2010.06.007"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Carvalho, L., Degiovanni, R., Brizzio, M., Cordy, M., Aguirre, N., Traon, Y.L., Papadakis, M.: ACoRe: automated goal-conflict resolution. In: Lambers, L., Uchitel, S. (eds.) FASE 2023. LNCS, vol. 13991, pp. 3\u201325. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30826-0_1","DOI":"10.1007\/978-3-031-30826-0_1"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Otop, J., Pavlogiannis, A.: Distributed synthesis for LTL fragments. In: 2013 Formal Methods in Computer-Aided Design, pp. 18\u201325. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679386"},{"key":"8_CR18","unstructured":"Chowdhery, A., et al: PALM: scaling language modeling with pathways. ArXiv abs\/2204.02311 (2022)"},{"key":"8_CR19","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. The Cyber-Physical Systems Series. MIT Press (1999). https:\/\/books.google.es\/books?id=Nmc4wEaLXFEC"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"De\u00a0Giacomo, G., Favorito, M.: Compositional approach to translate LTLf\/LDLf into deterministic finite automata. In: Proceedings of ICAPS 2021, pp. 122\u2013130 (2021)","DOI":"10.1609\/icaps.v31i1.15954"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Degiovanni, R., Molina, F., Regis, G., Aguirre, N.: A genetic algorithm for goal-conflict identification. In: Proceedings of ASE 2018, pp. 520\u2013531 (2018). https:\/\/doi.org\/10.1145\/3238147.3238220","DOI":"10.1145\/3238147.3238220"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Degiovanni, R., Ricci, N., Alrajeh, D., Castro, P.F., Aguirre, N.: Goal-conflict detection based on temporal satisfiability checking. In: Proceedings of ASE 2016, pp. 507\u2013518 (2016). http:\/\/doi.acm.org\/10.1145\/2970276.2970349","DOI":"10.1145\/2970276.2970349"},{"key":"8_CR23","unstructured":"Devlin, J., Chang, M.W., Lee, K., Toutanova, K.: BERT: pre-training of deep bidirectional transformers for language understanding (2019)"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Dietrich, D., Atlee, J.M.: A mode-based pattern for feature requirements, and a generic feature interface. In: 2013 21st IEEE International Requirements Engineering Conference (RE), pp. 82\u201391 (2013). https:\/\/doi.org\/10.1109\/RE.2013.6636708","DOI":"10.1109\/RE.2013.6636708"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Dietrich, D., Atlee, J.M.: A mode-based pattern for feature requirements, and a generic feature interface. In: 2013 21st IEEE International Requirements Engineering Conference (RE), pp. 82\u201391 (2013). https:\/\/api.semanticscholar.org\/CorpusID:29015370","DOI":"10.1109\/RE.2013.6636708"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Dureja, R., Rozier, K.Y.: More scalable LTL model checking via discovering design-space dependencies $$({D}^3)$$. In: Proceedings of TACAS 2018, pp. 309\u2013327. Springer (2018)","DOI":"10.1007\/978-3-319-89960-2_17"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-319-02444-8_31","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2013","unstructured":"Duret-Lutz, A.: Manipulating LTL formulas using spot 1.0. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 442\u2013445. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_31"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Esparza, J., K\u0159et\u00ednsk\u1ef3, J.: From LTL to deterministic automata: a safraless compositional approach. In: Proceedings of CAV 2014, pp. 192\u2013208. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_13"},{"issue":"9","key":"8_CR29","doi-asserted-by":"publisher","first-page":"1616","DOI":"10.1109\/JPROC.2018.2834926","volume":"106","author":"I Filippidis","year":"2018","unstructured":"Filippidis, I., Murray, R.M.: Layering assume-guarantee contracts for hierarchical system design. Proc. IEEE 106(9), 1616\u20131654 (2018)","journal-title":"Proc. IEEE"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Geier, G., Passing, N.: Specification decomposition for reactive synthesis. ISSE (2022)","DOI":"10.1007\/978-3-030-76384-8_8"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Fraser, G., Wotawa, F., Ammann, P.: Testing with model checkers: a survey. Softw. Test., Verif. Reliab. 19(3), 215\u2013261 (2009). https:\/\/doi.org\/10.1002\/stvr.402","DOI":"10.1002\/stvr.402"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-17524-9_13","volume-title":"NASA Formal Methods","author":"A Gacek","year":"2015","unstructured":"Gacek, A., Katis, A., Whalen, M.W., Backes, J., Cofer, D.: Towards realizability checking of contracts using theories. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 173\u2013187. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_13"},{"key":"8_CR33","unstructured":"Giannakopoulou, D., Mavridou, A., Rhein, J., Pressburger, T., Schumann, J., Shi, N.: Formal requirements elicitation with fret. In: International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020), No. ARC-E-DAA-TN77785 (2020)"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Golia, P., Roy, S., Meel, K.S.: Synthesis with explicit dependencies. In: 2023 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp.\u00a01\u20136. IEEE (2023)","DOI":"10.23919\/DATE56975.2023.10137282"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"Gro\u00dfer, K., Rukavitsyna, M., J\u00fcrjens, J.: A comparative evaluation of requirement template systems. In: Schneider, K., Dalpiaz, F., Horkoff, J. (eds.) 31st IEEE International Requirements Engineering Conference, RE 2023, Hannover, Germany, 4\u20138 September 2023, pp. 41\u201352. IEEE (2023). https:\/\/doi.org\/10.1109\/RE57278.2023.00014","DOI":"10.1109\/RE57278.2023.00014"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987). https:\/\/doi.org\/10.1016\/0167-6423(87)90035-9, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0167642387900359","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"8_CR37","unstructured":"Heitmeyer, C.: Requirements models for critical systems. In: Software and Systems Safety, pp. 158\u2013181. IOS Press (2011)"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C., Labaw, B., Kiskis, D.: Consistency checking of SCR-style requirements specifications. In: Proceedings of RE 1995, pp. 56\u201363. IEEE (1995)","DOI":"10.1109\/ISRE.1995.512546"},{"key":"8_CR39","unstructured":"Heitmeyer, C.L., Archer, M., Bharadwaj, R., Jeffords, R.D.: Tools for constructing requirements specifications: the SCR toolset at the age of nine. Comput. Syst. Sci. Eng. 20(1) (2005)"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Hermo, M., Lucio, P., S\u00e1nchez, C.: Tableaux for realizability of safety specifications. In: Chechik, M., Katoen, JP., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 495\u2013513. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_28","DOI":"10.1007\/978-3-031-27481-7_28"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Iannopollo, A., Tripakis, S., Vincentelli, A.: Specification decomposition for synthesis from libraries of LTL assume\/guarantee contracts. In: DATE. IEEE (2018)","DOI":"10.23919\/DATE.2018.8342266"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. EPTCS 229, 112\u2013132 (2016)","DOI":"10.4204\/EPTCS.229.10"},{"key":"8_CR43","doi-asserted-by":"publisher","unstructured":"Konrad, S., Cheng, B.: Facilitating the construction of specification pattern-based properties. In: 13th IEEE International Conference on Requirements Engineering (RE 2005), pp. 329\u2013338 (2005). https:\/\/doi.org\/10.1109\/RE.2005.29","DOI":"10.1109\/RE.2005.29"},{"key":"8_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-01090-4_34","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543\u2013550. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Proceedings of CAV 2006, pp. 31\u201344. Springer (2006)","DOI":"10.1007\/11817963_6"},{"key":"8_CR46","unstructured":"Leveson, N.G.: Safeware: System Safety and Computers. ACM (1995)"},{"key":"8_CR47","unstructured":"Liu, J.X., et al.: Lang2LTL: translating natural language commands to temporal robot task specification. In: Conference on Robbot Learning (2023)"},{"key":"8_CR48","unstructured":"Maderbacher, B., Bloem, R.: Reactive synthesis modulo theories using abstraction refinement. In: # PLACEHOLDER_PARENT_METADATA_VALUE#, pp. 315\u2013324. TU Wien Academic Press (2022)"},{"key":"8_CR49","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)"},{"key":"8_CR50","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995). https:\/\/doi.org\/10.1007\/978-1-4612-4222-2","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"8_CR51","doi-asserted-by":"publisher","unstructured":"Maoz, S., Ringert, J.O.: Spectra: a specification language for reactive systems. Softw. Syst. Model. 20(5), 1553\u20131586 (2021). https:\/\/doi.org\/10.1007\/s10270-021-00868-z","DOI":"10.1007\/s10270-021-00868-z"},{"key":"8_CR52","doi-asserted-by":"publisher","unstructured":"Maoz, S., Shalom, R.: Unrealizable cores for reactive systems specifications: artifact. In: Proceedings of the 43rd International Conference on Software Engineering: Companion Proceedings, ICSE 2021, pp. 217\u2013218. IEEE Press (2021). https:\/\/doi.org\/10.1109\/ICSE-Companion52605.2021.00097","DOI":"10.1109\/ICSE-Companion52605.2021.00097"},{"key":"8_CR53","doi-asserted-by":"publisher","unstructured":"Mavin, A., Wilkinson, P., Harwood, A., Novak, M.: Easy approach to requirements syntax (EARS). In: 2009 17th IEEE International Requirements Engineering Conference, pp. 317\u2013322 (2009). https:\/\/doi.org\/10.1109\/RE.2009.9","DOI":"10.1109\/RE.2009.9"},{"key":"8_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-030-90870-6_27","volume-title":"Formal Methods","author":"A Mavridou","year":"2021","unstructured":"Mavridou, A., Katis, A., Giannakopoulou, D., Kooi, D., Pressburger, T., Whalen, M.W.: From partial to global assume-guarantee contracts: compositional realizability analysis in FRET. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 503\u2013523. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_27"},{"key":"8_CR55","doi-asserted-by":"crossref","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Proceedings of CAV 2018 (Part I), pp. 578\u2013586. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"8_CR56","unstructured":"OpenAI: GPT-4 technical report (2023)"},{"key":"8_CR57","unstructured":"Ouyang, L., et al.: Training language models to follow instructions with human feedback. CoRR abs\/2203.02155 (2022)"},{"key":"8_CR58","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive (1) designs. In: Proceedings of VMCAI 2006, pp. 364\u2013380. Springer (2006)","DOI":"10.1007\/11609773_24"},{"key":"8_CR59","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: SFCS 1977, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"8_CR60","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1989), pp. 179\u2013190. ACM, New York (1989). https:\/\/doi.org\/10.1145\/75277.75293, http:\/\/doi.acm.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"8_CR61","doi-asserted-by":"publisher","unstructured":"Pressburger, T., Katis, A., Dutle, A., Mavridou, A.: Authoring, analyzing, and monitoring requirements for a lift-plus-cruise aircraft. In: Ferrari, A., Penzenstadler, B. (eds.) REFSQ 2023. LNCS, vol. 13975, pp. 295\u2013308. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-29786-1_21","DOI":"10.1007\/978-3-031-29786-1_21"},{"key":"8_CR62","doi-asserted-by":"publisher","unstructured":"Pudlitz, F., Brokhausen, F., Vogelsang, A.: Extraction of system states from natural language requirements. In: 2019 IEEE 27th International Requirements Engineering Conference (RE), pp. 211\u2013222 (2019). https:\/\/doi.org\/10.1109\/RE.2019.00031","DOI":"10.1109\/RE.2019.00031"},{"key":"8_CR63","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., S\u00e1nchez, C.: Boolean abstractions for realizability modulo theories. In: Enea, C., Lal, A. (eds.) CAV 2023, Part III. LNCS, vol. 13966, pp. 305\u2013328. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_15","DOI":"10.1007\/978-3-031-37709-9_15"},{"key":"8_CR64","doi-asserted-by":"publisher","unstructured":"Rodriguez, A., S\u00e1nchez, C.: Adaptive reactive synthesis for LTL and LTLf modulo theories. In: Proc. of the 38th AAAI Conf. on Artificial Intelligence (AAAI\u201924). vol. 38, pp. 10679\u201310686. AAAI Press (2024). https:\/\/doi.org\/10.1609\/aaai.v38i9.28939","DOI":"10.1609\/aaai.v38i9.28939"},{"key":"8_CR65","doi-asserted-by":"publisher","unstructured":"de\u00a0Roever, W.P., Langmaack, H., Pnueli, A. (eds.): Compositionality: The Significant Difference. Springer, Cham (1998). https:\/\/doi.org\/10.1007\/3-540-49213-5","DOI":"10.1007\/3-540-49213-5"},{"key":"8_CR66","doi-asserted-by":"crossref","unstructured":"Shaker, P., Atlee, J.M., Wang, S.: A feature-oriented requirements modelling language. In: 2012 20th IEEE International Requirements Engineering Conference (RE), pp. 151\u2013160. IEEE (2012)","DOI":"10.1109\/RE.2012.6345799"},{"key":"8_CR67","unstructured":"Thoppilan, R., et al.: LaMDA: language models for dialog applications (2022)"},{"key":"8_CR68","unstructured":"Touvron, H., et\u00a0al.: LLaMA 2: open foundation and fine-tuned chat models. arXiv preprint arXiv:2307.09288 (2023)"},{"key":"8_CR69","doi-asserted-by":"crossref","unstructured":"Vogelsang, A., Femmer, H., Winkler, C.: Systematic elicitation of mode models for multifunctional systems. In: 2015 IEEE 23rd International Requirements Engineering Conference (RE), pp. 305\u2013314. IEEE (2015)","DOI":"10.1109\/RE.2015.7320447"},{"key":"8_CR70","doi-asserted-by":"crossref","unstructured":"Vogelsang, A., Femmer, H., Winkler, C.: Take care of your modes! An investigation of defects in automotive requirements. In: Requirements Engineering: Foundation for Software Quality: 22nd International Working Conference, REFSQ 2016, Gothenburg, Sweden, 14\u201317 March 2016, pp. 161\u2013167. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-30282-9_11"},{"key":"8_CR71","unstructured":"Wei, J., et al.: Emergent abilities of large language models. CoRR abs\/2206.07682 (2022)"},{"key":"8_CR72","unstructured":"Yang, J., et al.: Harnessing the power of LLMs in practice: a survey on chatGPT and beyond (2023)"},{"key":"8_CR73","unstructured":"Ye, X., Ruess, H.: Efficient reactive synthesis. arXiv preprint arXiv:2404.17834 (2024)"},{"key":"8_CR74","unstructured":"Zeng, A., et al.: GLM-130B: an open bilingual pre-trained model. In: ICLR 2023 Poster (2023)"},{"key":"8_CR75","unstructured":"Zhang, S., et al.: OPT: open pre-trained transformer language models. ArXiv abs\/2205.01068 (2022)"},{"key":"8_CR76","doi-asserted-by":"crossref","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety LTL synthesis. In: Proceedings of HVC, pp. 147\u2013162. Springer (2017)","DOI":"10.1007\/978-3-319-70389-3_10"}],"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-031-93706-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:55Z","timestamp":1749316975000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93706-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":76,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"8 June 2025","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":"Hampton Roads, VA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}