{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:16Z","timestamp":1783545316566,"version":"3.55.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    In the development and verification of safety-critical aero-space software, Linear Temporal Logic (LTL) has been widely used to specify complex system properties derived from requirements. However, a significant gap remains in industrial practice: translating natural language (NL) requirements into formal LTL properties is a labor-intensive and error-prone process that requires rare expertise in both aerospace control engineering and formal methods. While recent NL-to-LTL tools (\n                    <jats:italic>e.g.<\/jats:italic>\n                    , NL2SPEC, NL2TL, NL2LTL) are capable of automating parts of this process, they often fail on real requirement documents in industrial settings, due to complex domain terminology or implicit temporal and logical structure. To address these challenges, we present\n                    <jats:sc>Aero<\/jats:sc>\n                    <jats:sc>Req2LTL<\/jats:sc>\n                    , a framework that automates LTL property generation for aerospace requirements using large language models (LLMs), with two key industrial innovations: (i) a data dictionary that normalizes technical jargon into precise atomic propositions; and (ii) a template-based requirement language that makes temporal cues and logical relations explicit before translation. On a real aerospace dataset,\n                    <jats:sc>Aero<\/jats:sc>\n                    <jats:sc>Req2LTL<\/jats:sc>\n                    achieves 85% precision and 88% recall in LTL generation, and its outputs can be directly consumed by existing verification tools.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_33","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:21:35Z","timestamp":1779024095000},"page":"670-690","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated LTL Specification Generation from\u00a0Industrial Aerospace Requirements"],"prefix":"10.1007","author":[{"given":"Zhi","family":"Ma","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiao","family":"Liang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cheng","family":"Wen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rui","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bin","family":"Gu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Rozier, K.Y.: Linear temporal logic symbolic model checking. Comput. Sci. Rev. 5(2), 163\u2013203 (2011)","DOI":"10.1016\/j.cosrev.2010.06.002"},{"key":"33_CR2","unstructured":"Merhav, S.: Aerospace sensor systems and applications. Springer Science & Business Media (1998)"},{"issue":"4","key":"33_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Software Eng. Methodol. (TOSEM) 20(4), 1\u201364 (2011)","journal-title":"ACM Trans. Software Eng. Methodol. (TOSEM)"},{"key":"33_CR4","unstructured":"Minaee, S., et al.: Large language models: a survey. arXiv preprint arXiv:2402.06196 (2024)"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Naveed, H., et al.: A comprehensive overview of large language models. ACM Trans. Intell. Syst. Technol. 16(5), 1\u201372 (2025)","DOI":"10.1145\/3744746"},{"issue":"7","key":"33_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3653718","volume":"18","author":"C Wen","year":"2024","unstructured":"Wen, C., et al.: Automatically inspecting thousands of static bug warnings with large language model: how far are we? ACM Trans. Knowl. Discov. Data 18(7), 1\u201334 (2024)","journal-title":"ACM Trans. Knowl. Discov. Data"},{"key":"33_CR7","doi-asserted-by":"publisher","unstructured":"Su, J., Deng, L., Wen, C., Qin, S., Tian, C.: CFStra: Enhancing configurable program analysis through LLM-driven strategy selection based on code features. In: Chin, WN., Xu, Z. (eds.) International Symposium on Theoretical Aspects of Software Engineering, pp. 374\u2013391. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-64626-3_22","DOI":"10.1007\/978-3-031-64626-3_22"},{"key":"33_CR8","doi-asserted-by":"publisher","unstructured":"Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In: Enea, C., Lal, A. (eds.) Proceedings of the 35th International Conference on Computer Aided Verification, volume 13965 of Lecture Notes in Computer Science, pp. 383\u2013396, Paris, France, Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Chen, Y., Gandhi, R., Zhang, Y., Fan, C.: NL2TL: transforming natural languages to temporal logics using large language models. In: Proceedings of the Conference on Empirical Methods in Natural Language Processing, pp. 15880\u201315903. Association for Computational Linguistics, Singapore (2023)","DOI":"10.18653\/v1\/2023.emnlp-main.985"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Fuggitti, F., Chakraborti, T.: NL2LTL - a python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence, the 35th Conference on Innovative Applications of Artificial Intelligence, the 13th Symposium on Educational Advances in Artificial Intelligence, pp. 16428\u201316430, Washington, DC, USA. AAAI Press (2023)","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"33_CR11","unstructured":"Bernstein, J.I.: Design methods in the aerospace industry: looking for evidence of set-based practices. PhD thesis, Massachusetts Institute of Technology (1998)"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Cao, J., et al.: From informal to formal\u2013incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs. In: Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 26984\u201327003 (2025)","DOI":"10.18653\/v1\/2025.acl-long.1310"},{"key":"33_CR13","doi-asserted-by":"publisher","unstructured":"Wen, C., et al.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: Gurfinkel, A., Ganesh, V. (eds.) International Conference on Computer Aided Verification, pp. 302\u2013328. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_16","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"33_CR14","doi-asserted-by":"publisher","DOI":"10.1016\/j.inffus.2025.103466","volume":"125","author":"Z Ma","year":"2026","unstructured":"Ma, Z., Wen, C., Bin, Yu., Jie, S.: Integrating ensemble learning and large language models for efficient formal verification of IP-based aerospace systems. Inf. Fus. 125, 103466 (2026)","journal-title":"Inf. Fus."},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Zhang, S., Liu, H.J., Ma, Z., Liang, X., Wen, C.: Formal verification of aerospace software IP components: a multi-tool case study. In: Proceedings of the 2026 6th International Conference on Computer Network Security and Software Engineering, pp. 1\u20139 (2026)","DOI":"10.1145\/3803633.3803667"},{"key":"33_CR16","unstructured":"Ma, Z., et al.: Towards practical requirement analysis and verification: a case study on software IP components in aerospace embedded systems. arXiv preprint arXiv:2404.00795 (2024)"},{"key":"33_CR17","unstructured":"OpenAI. GPT-4o technical report. https:\/\/openai.com\/index\/gpt-4o (2024). Accessed May 2025"},{"key":"33_CR18","unstructured":"Zhang, S., Zhao, H., et\u00a0al.: DeepSeek-VL: scaling vision-language models with vision token learner. arXiv preprint arXiv:2405.07927 (2024)"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Hendriks, M., Geilen, M., Behrouzian, A.R.B., Basten, T., Ara, H.A., Goswami, D.: Checking metric temporal logic with trace. In: 2016 16th International Conference on Application of Concurrency to System Design (ACSD), pp. 19\u201324 (2016)","DOI":"10.1109\/ACSD.2016.13"},{"key":"33_CR20","unstructured":"Cadar, C., Dunbar, D., Engler, D.R., et\u00a0al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, vol.\u00a08, pp. 209\u2013224 (2008)"},{"key":"33_CR21","doi-asserted-by":"publisher","first-page":"867","DOI":"10.1007\/s10009-020-00570-3","volume":"23","author":"C Cadar","year":"2021","unstructured":"Cadar, C., Nowack, M.: Klee symbolic execution engine in 2019. Int. J. Softw. Tools Technol. Transfer 23, 867\u2013870 (2021)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"33_CR22","doi-asserted-by":"publisher","unstructured":"van Hoey, J.: Program analysis with a debugger: GDB. In: Beginning x64 Assembly Programming: From Novice to AVX Professional, pp. 21\u201333. Springer, Berkeley, CA (2019). https:\/\/doi.org\/10.1007\/978-1-4842-5076-1_3","DOI":"10.1007\/978-1-4842-5076-1_3"},{"key":"33_CR23","unstructured":"English, W., Simon, D., Jha, S.K., Ewetz, R.: Grammar-forced translation of natural language to temporal logic using LLMs. In: International Conference on Machine Learning (2025)"},{"key":"33_CR24","unstructured":"Liu, J.X., et al.: Lang2LTL: translating natural language commands to temporal specification with large language models. In: Workshop on Language and Robotics at CoRL 2022 (2022)"},{"key":"33_CR25","doi-asserted-by":"crossref","unstructured":"Xu, Y., Feng, J., Miao, W.: Learning from failures: translation of natural language requirements into linear temporal logic with large language models. In: 2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS), pp. 204\u2013215. IEEE (2024)","DOI":"10.1109\/QRS62785.2024.00029"},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"Liu, J.X., Shah, A., Konidaris, G.D., Tellex, S., Paulius, D.: Lang2ltl-2: grounding spatiotemporal navigation commands using large language and vision-language models. In: 2024 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 2325\u20132332 (2024)","DOI":"10.1109\/IROS58592.2024.10802696"},{"key":"33_CR27","first-page":"10482","volume":"10","author":"X Shaojun","year":"2024","unstructured":"Shaojun, X., Luo, X., Huang, Y., Leng, L., Liu, R., Liu, C.: Nl2Hltl2Plan: scaling up natural language understanding for multi-robots through hierarchical temporal logic task specifications. IEEE Robot. Autom. Lett. 10, 10482\u201310489 (2024)","journal-title":"IEEE Robot. Autom. Lett."},{"key":"33_CR28","unstructured":"Olausson, T.X., Inala, J.P., Wang, C., Gao, J., Solar-Lezama, A.: Demystifying GPT self-repair for code generation. ArXiv, abs\/2306.09896 (2023)"},{"key":"33_CR29","doi-asserted-by":"crossref","unstructured":"Zhang, M., et al.: Automated extraction of protocol state machines from 3gpp specifications with domain-informed prompts and LLM ensembles. ArXiv, abs\/2510.14348 (2025)","DOI":"10.1109\/SECON68281.2026.11579014"},{"key":"33_CR30","doi-asserted-by":"publisher","unstructured":"Bj\u00f8ner, D.: Software Engineering 3: Domains, Requirements, and Software Design. Springer, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/3-540-33653-2","DOI":"10.1007\/3-540-33653-2"},{"key":"33_CR31","unstructured":"Bj\u00f8rner, D.: From Domain Descriptions to Requirements Prescriptions (2016)"},{"key":"33_CR32","unstructured":"Wu, Z., Chen, X., Jin, Z., Hu, M., Jin, D.: Unlocking the silent needs: business-logic-driven iterative requirements auto-completion. In: 2026 IEEE\/ACM 48th International Conference on Software Engineering (ICSE \u201926), p.\u00a012 (2026)"},{"key":"33_CR33","unstructured":"Shih, Y.-A., Lin, A., Gupta, A., Malik, S.: Flag: Formal and LLM-assisted SVA generation for formal specifications of on-chip communication protocols. ArXiv, abs\/2504.17226 (2025)"},{"key":"33_CR34","doi-asserted-by":"crossref","unstructured":"Meloche, R., Amyot, D., Mylopoulos, J.: Towards legal contract formalization with controlled natural language templates. In: 2023 IEEE 31st International Requirements Engineering Conference (RE), pp. 317\u2013322. IEEE (2023)","DOI":"10.1109\/RE57278.2023.00042"},{"key":"33_CR35","doi-asserted-by":"crossref","unstructured":"Ma, Z., et al.: Bridging natural language and formal specification\u2013automated translation of software requirements to LTL via hierarchical semantics decomposition using LLMs. arXiv preprint arXiv:2512.17334 (2025)","DOI":"10.1109\/ASE63991.2025.00104"},{"key":"33_CR36","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, D.: Domain engineering: a software engineering discipline in need of research. In: International Conference on Current Trends in Theory and Practice of Computer Science, pp. 1\u201317. Springer, Berlin, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44411-4_1","DOI":"10.1007\/3-540-44411-4_1"},{"key":"33_CR37","doi-asserted-by":"crossref","unstructured":"Wu, N., Li, Y., Yang, H., Chen, H., Dai, S., Hao, C.: Survey of machine learning for software-assisted hardware design verification: past, present, and prospect. ACM Trans. Design Autom. Electron. Syst. (2024)","DOI":"10.1145\/3661308"},{"key":"33_CR38","unstructured":"Abdollahi, M., Yeganli, S.F., Baharloo, M., Baniasadi, A.: A scoping review, challenges, and open issues. Electronics, Hardware design and verification with large language models (2024)"},{"key":"33_CR39","unstructured":"Huang, Y., Hu, M., Chen, X., Jin, Z., Xiao, S.: Modeling like peeling an onion: Layerwise analysis-driven automatic behavioral model generation. In: 2026 IEEE\/ACM 48th International Conference on Software Engineering (ICSE \u201926), p.\u00a012 (2026)"},{"key":"33_CR40","unstructured":"English, W., Walker, C., Simon, D., Jha, S.K., Ewetz, R.: Verifiable natural language to linear temporal logic translation: a benchmark dataset and evaluation suite. ArXiv, abs\/2507.00877 (2025)"},{"key":"33_CR41","unstructured":"Mendoza, D., Hahn, C., Trippel, C.: Translating natural language to temporal logics with large language models and model checkers. In: 2024 Formal Methods in Computer-Aided Design (FMCAD), pp. 1\u201311 (2024)"},{"key":"33_CR42","unstructured":"Wang, J., Sundarsingh, D.S., Deshmukh, J.V., Kantaros, Y.: ConformalNL2LTL: translating natural language instructions into temporal logic formulas with conformal correctness guarantees. ArXiv, abs\/2504.21022 (2025)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:30:57Z","timestamp":1783542657000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}