{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T04:33:22Z","timestamp":1782966802871,"version":"3.54.5"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660 TRR 248?CPEC"],"award-info":[{"award-number":["389792660 TRR 248?CPEC"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["610150"],"award-info":[{"award-number":["610150"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>Motivated by applications in robotics, we consider the task of synthesizing linear temporal logic (LTL) specifications based on examples and natural language descriptions. While LTL is a flexible, expressive, and unambiguous language to describe robotic tasks, it is often challenging for non-expert users. In this paper, we present an interactive method for synthesizing LTL specifications from a single example trace and a natural language description. The interaction is limited to showing a small number of behavioral examples to the user who decides whether or not they exhibit the original intent. Our approach generates candidate LTL specifications and distinguishing examples using an encoding into optimization modulo theories problems. Additionally, we use a grammar extension mechanism and a semantic parser to generalize synthesized specifications to parametric task descriptions for subsequent use. Our implementation in the tool LtlTalk starts with a domain-specific language that maps to a fragment of LTL and expands it through example-based user interactions, thus enabling natural language-like robot programming, while maintaining the expressive power and precision of a formal language. Our experiments show that the synthesis method is precise, quick, and asks only a few questions to the users, and we demonstrate in a case study how LtlTalk generalizes from the synthesized tasks to other, yet unseen, tasks.<\/jats:p>","DOI":"10.1145\/3428269","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Interactive synthesis of temporal specifications from examples and natural language"],"prefix":"10.1145","volume":"4","author":[{"given":"Ivan","family":"Gavran","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eva","family":"Darulova","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-495-4-1"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371124"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"e_1_2_2_4_1","unstructured":"Yoav Artzi. 2016. Cornell SPF : Cornell Semantic Parsing Framework. arXiv:arXiv:1311.3011  Yoav Artzi. 2016. Cornell SPF : Cornell Semantic Parsing Framework. arXiv:arXiv:1311.3011"},{"key":"e_1_2_2_5_1","volume-title":"International Conference on Learning Representations (ICLR).","author":"Balog Matej","year":"2017"},{"key":"e_1_2_2_6_1","unstructured":"Ezio Bartocci Luca Bortolussi and Guido Sanguinetti. 2013. Learning Temporal Logical Properties Discriminating ECG models of Cardiac Arrhytmias. CoRR abs\/1312.7523 ( 2013 ). arXiv: 1312. 7523  Ezio Bartocci Luca Bortolussi and Guido Sanguinetti. 2013. Learning Temporal Logical Properties Discriminating ECG models of Cardiac Arrhytmias. CoRR abs\/1312.7523 ( 2013 ). arXiv: 1312. 7523"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/P16-1069"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_14"},{"key":"e_1_2_2_10_1","volume-title":"Learning Interpretable Models Expressed in Linear Temporal Logic. In International Conference on Automated Planning and Scheduling (ICAPS).","author":"Camacho Alberto"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0355-5"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Qiaochu Chen Xinyu Wang Xi Ye Greg Durrett and Isil Dillig. 2020. Multi-modal Synthesis of Regular Expressions. In Programming Language Design and Implementation (PLDI).  Qiaochu Chen Xinyu Wang Xi Ye Greg Durrett and Isil Dillig. 2020. Multi-modal Synthesis of Regular Expressions. In Programming Language Design and Implementation (PLDI).","DOI":"10.1145\/3385412.3385988"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338951"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_24"},{"key":"e_1_2_2_15_1","volume-title":"Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In International Joint Conference on Artificial Intelligence (IJCAI).","author":"Giacomo Giuseppe De"},{"key":"e_1_2_2_16_1","volume-title":"Synthesis for LTL and LDL on Finite Traces. In International Joint Conference on Artificial Intelligence (IJCAI).","author":"Giacomo Giuseppe De"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884786"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_13"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(71)90010-5"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126513"},{"key":"e_1_2_2_23_1","volume-title":"PDDL: The Planning Domain Definition Language. Technical Report CVC TR98003\/DCS TR1165","author":"Ghallab M.","year":"1998"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)91165-5"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2588555.2612177"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/587051.587064"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2421907"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2019\/776"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2013.6631186"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562146"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2016.2585083"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1163\/156855308X344864"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(96)00121-5"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.14778\/2735461.2735468"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10514-014-9418-8"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.3115\/v1\/P14-5010"},{"key":"e_1_2_2_38_1","volume-title":"Conference on Artificial Intelligence (AAAI).","author":"Manshadi Mehdi Hafezi"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807442.2807459"},{"key":"e_1_2_2_40_1","volume-title":"Veloso","author":"Meri\u00e7li \u00c7etin","year":"2014"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/219717.219748"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382218"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603016"},{"key":"e_1_2_2_44_1","volume-title":"International Conference on Machine Learning (ICML).","author":"Nye Maxwell I.","year":"2019"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180189"},{"key":"e_1_2_2_46_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI).","author":"Perera Vittorio"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_2_48_1","volume-title":"International Conference on Learning Representations (ICLR).","author":"Polosukhin Illia","year":"2018"},{"key":"e_1_2_2_49_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI).","author":"Raza Mohammad","year":"2015"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2016.7479105"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_23"},{"key":"e_1_2_2_52_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI).","author":"Thomason Jesse","year":"2015"},{"key":"e_1_2_2_53_1","volume-title":"Seshia","author":"Vazquez-Chanlatte Marcell","year":"2018"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3058738"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062365"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/P17-1086"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133887"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428269","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428269","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428269"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":57,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428269"],"URL":"https:\/\/doi.org\/10.1145\/3428269","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}