{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,27]],"date-time":"2026-06-27T20:23:02Z","timestamp":1782591782801,"version":"3.54.5"},"publisher-location":"Singapore","reference-count":37,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819606160","type":"print"},{"value":"9789819606177","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-981-96-0617-7_1","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T14:47:27Z","timestamp":1732805247000},"page":"1-17","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["NL2CTL: Automatic Generation of\u00a0Formal Requirements Specifications via\u00a0Large Language Models"],"prefix":"10.1007","author":[{"given":"Mengyan","family":"Zhao","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ran","family":"Tao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yanhong","family":"Huang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jianqi","family":"Shi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yang","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"1_CR1","unstructured":"Achiam, J., et\u00a0al.: GPT-4 technical report. arXiv preprint arXiv:2303.08774 (2023)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Arora, C., John, G., Mohamed, A.: Advancing requirements engineering through generative AI: assessing the role of LLMs (2023). arXiv preprint arXiv:2310.13976","DOI":"10.1007\/978-3-031-55642-5_6"},{"key":"1_CR3","unstructured":"Brunello, A., Montanari, A., Reynolds, M.: Synthesis of LTL formulas from natural language texts: state of the art and research directions. In: 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Buzhinsky, I.: Formalization of natural language requirements into temporal logics: a survey. In: 2019 IEEE 17th International Conference on Industrial Informatics (INDIN), vol.\u00a01, pp. 400\u2013406. IEEE (2019)","DOI":"10.1109\/INDIN41052.2019.8972130"},{"key":"1_CR5","unstructured":"Chen, M., et\u00a0al.: Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 (2021)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Chen, Y., Gandhi, R., Zhang, Y., Fan, C.: NL2TL: transforming natural languages to temporal logics using large language models. arXiv preprint arXiv:2305.07766 (2023)","DOI":"10.18653\/v1\/2023.emnlp-main.985"},{"issue":"10\u201311","key":"1_CR7","doi-asserted-by":"publisher","first-page":"1255","DOI":"10.1177\/02783649211035177","volume":"40","author":"G Chou","year":"2021","unstructured":"Chou, G., Berenson, D., Ozay, N.: Learning constraints from demonstrations with grid and parametric representations. Int. J. Robot. Res. 40(10\u201311), 1255\u20131283 (2021)","journal-title":"Int. J. Robot. Res."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Chou, G., Ozay, N., Berenson, D.: Explaining multi-stage tasks by learning temporal logic formulas from suboptimal demonstrations. arXiv preprint arXiv:2006.02411 (2020)","DOI":"10.15607\/RSS.2020.XVI.097"},{"issue":"2","key":"1_CR9","doi-asserted-by":"publisher","first-page":"3682","DOI":"10.1109\/LRA.2020.2974427","volume":"5","author":"G Chou","year":"2020","unstructured":"Chou, G., Ozay, N., Berenson, D.: Learning constraints from locally-optimal demonstrations under cost function uncertainty. IEEE Robot. Autom. Lett. 5(2), 3682\u20133690 (2020)","journal-title":"IEEE Robot. Autom. Lett."},{"issue":"1","key":"1_CR10","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10514-021-10004-x","volume":"46","author":"G Chou","year":"2022","unstructured":"Chou, G., Ozay, N., Berenson, D.: Learning temporal logic formulas from suboptimal demonstrations: theory and experiments. Auton. Robot. 46(1), 149\u2013174 (2022)","journal-title":"Auton. Robot."},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-031-37703-7_18","volume-title":"Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17\u201322, 2023, Proceedings, Part II","author":"M Cosler","year":"2023","unstructured":"Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: nl2spec: interactively translating unstructured natural language to\u00a0temporal logics with\u00a0large language models. In: Enea, C., Lal, A. (eds.) Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17\u201322, 2023, Proceedings, Part II, pp. 383\u2013396. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice, pp. 7\u201315 (1998)","DOI":"10.1145\/298595.298598"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Finucane, C., Jing, G., Kress-Gazit, H.: LTLMoP: experimenting with language, temporal logic and robot control. In: 2010 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 1988\u20131993. IEEE (2010)","DOI":"10.1109\/IROS.2010.5650371"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Fuggitti, F., Chakraborti, T.: NL2LTL\u2013a Python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a037, pp. 16428\u201316430 (2023)","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Gavran, I., Darulova, E., Majumdar, R.: Interactive synthesis of temporal specifications from examples and natural language. In: Proceedings of the ACM on Programming Languages, vol. 4(OOPSLA), pp. 1\u201326 (2020)","DOI":"10.1145\/3428269"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Grunske, L.: Specification patterns for probabilistic quality properties. In: Proceedings of the 30th International Conference on Software Engineering, pp. 31\u201340 (2008)","DOI":"10.1145\/1368088.1368094"},{"key":"1_CR17","unstructured":"Hahn, C., Schmitt, F., Tillman, J.J., Metzger, N., Siber, J., Finkbeiner, B.: Formal specifications from natural language. arXiv preprint arXiv:2206.01962 (2022)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"He, J., Bartocci, E., Ni\u010dkovi\u0107, D., Isakovic, H., Grosu, R.: DeepSTL: from English requirements to signal temporal logic. In: Proceedings of the 44th International Conference on Software Engineering, pp. 610\u2013622 (2022)","DOI":"10.1145\/3510003.3510171"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Howard, T.M., Tellex, S., Roy, N.: A natural language planner interface for mobile manipulators. In: 2014 IEEE International Conference on Robotics and Automation (ICRA), pp. 6652\u20136659. IEEE (2014)","DOI":"10.1109\/ICRA.2014.6907841"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Hsiung, E., et al.: Generalizing to new domains by mapping natural language to lifted LTL. In: 2022 International Conference on Robotics and Automation (ICRA), pp. 3624\u20133630. IEEE (2022)","DOI":"10.1109\/ICRA46639.2022.9812169"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Kolahdouz-Rahimi, S., Lano, K., Lin, C.: Requirement formalisation using natural language processing and machine learning: a systematic review. arXiv preprint arXiv:2303.13365 (2023)","DOI":"10.5220\/0011789700003402"},{"key":"1_CR22","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11663430_6","volume-title":"Satellite Events at the MoDELS 2005 Conference","author":"S Konrad","year":"2006","unstructured":"Konrad, S., Cheng, B.H.C.: Automated analysis of natural language properties for UML models. In: Bruel, J.-M. (ed.) Satellite Events at the MoDELS 2005 Conference, pp. 48\u201357. Springer, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11663430_6"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.: Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering, pp. 372\u2013381 (2005)","DOI":"10.1109\/ICSE.2005.1553580"},{"key":"1_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":"1_CR25","first-page":"27730","volume":"35","author":"L Ouyang","year":"2022","unstructured":"Ouyang, L., et al.: Training language models to follow instructions with human feedback. Adv. Neural. Inf. Process. Syst. 35, 27730\u201327744 (2022)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"1_CR26","unstructured":"Patel, R., Pavlick, R., Tellex, S.: Learning to ground language to temporal logical form. In: Conference of the North American Chapter of the Association for Computational Linguistics (NAACL) (2019)"},{"issue":"140","key":"1_CR27","first-page":"1","volume":"21","author":"C Raffel","year":"2020","unstructured":"Raffel, C., et al.: Exploring the limits of transfer learning with a unified text-to-text transformer. J. Mach. Learn. Res. 21(140), 1\u201367 (2020)","journal-title":"J. Mach. Learn. Res."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Raman, V., Lignos, C., Finucane, C., Lee, K.C., Marcus, M.P., Kress-Gazit, H.: Sorry Dave, I\u2019m Afraid I Can\u2019t Do That: explaining unachievable robot tasks using natural language. In: Robotics: Science and Systems, vol.\u00a02, pp.\u00a02\u20131. Citeseer (2013)","DOI":"10.15607\/RSS.2013.IX.023"},{"key":"1_CR29","unstructured":"Ratnaparkhi, A.: Maximum entropy models for natural language ambiguity resolution. University of Pennsylvania (1998)"},{"issue":"3","key":"1_CR30","doi-asserted-by":"publisher","first-page":"1015","DOI":"10.1007\/s10270-021-00942-6","volume":"21","author":"R Saini","year":"2022","unstructured":"Saini, R., Mussbacher, G., Guo, J.L., Kienzle, J.: Automated, interactive, and traceable domain modelling empowered by artificial intelligence. Softw. Syst. Model. 21(3), 1015\u20131045 (2022)","journal-title":"Softw. Syst. Model."},{"key":"1_CR31","unstructured":"Scobee, D.R., Sastry, S.S.: Maximum likelihood constraint inference for inverse reinforcement learning. arXiv preprint arXiv:1909.05477 (2019)"},{"key":"1_CR32","unstructured":"Shah, A., Kamath, P., Shah, J.A., Li, S.: Bayesian inference of temporal task specifications from demonstrations. In: Advances in Neural Information Processing Systems, vol. 31 (2018)"},{"key":"1_CR33","unstructured":"Shah, A.J.: Interactive Robot Training for Complex Tasks. Ph.D. thesis, Massachusetts Institute of Technology (2021)"},{"issue":"4","key":"1_CR34","first-page":"64","volume":"32","author":"S Tellex","year":"2011","unstructured":"Tellex, S., et al.: Approaching the symbol grounding problem with probabilistic graphical models. AI Mag. 32(4), 64\u201376 (2011)","journal-title":"AI Mag."},{"key":"1_CR35","unstructured":"Vazquez-Chanlatte, M., Jha, S., Tiwari, A., Ho, M.K., Seshia, S.: Learning task specifications from demonstrations. In: Advances in Neural Information Processing Systems, vol. 31 (2018)"},{"key":"1_CR36","unstructured":"Wang, C., Ross, C., Kuo, Y.L., Katz, B., Barbu, A.: Learning a natural-language to LTL executable semantic parser for grounded robotics. In: Conference on Robot Learning, pp. 1706\u20131718. PMLR (2021)"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Wang, G., Trimbach, C., Lee, J.K., Ho, M.K., Littman, M.L.: Teaching a robot tasks of arbitrary complexity via human feedback. In: Proceedings of the 2020 ACM\/IEEE International Conference on Human-Robot Interaction, pp. 649\u2013657 (2020)","DOI":"10.1145\/3319502.3374824"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-0617-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T15:08:16Z","timestamp":1732806496000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-0617-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9789819606160","9789819606177"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-0617-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hiroshima","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.icfem2024.info\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}