{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T19:17:14Z","timestamp":1792264634633,"version":"4.4.0"},"publisher-location":"Cham","reference-count":73,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031757778","type":"print"},{"value":"9783031757785","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"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-75778-5_6","type":"book-chapter","created":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T07:09:19Z","timestamp":1731827359000},"page":"109-125","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["What Is Formal Verification Without Specifications? A Survey on\u00a0Mining LTL Specifications"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Neider","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rajarshi","family":"Roy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp.\u00a01\u20138. IEEE (2013). https:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Ammons, G., Bod\u00edk, R., Larus, J.R.: Mining specifications. In: Launchbury, J., Mitchell, J.C. (eds.) Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, 16\u201318 January 2002, pp. 4\u201316. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503275","DOI":"10.1145\/503272.503275"},{"key":"6_CR3","unstructured":"Arif, M.F., Larraz, D., Echeverria, M., Reynolds, A., Chowdhury, O., Tinelli, C.: SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. In: FMCAD, pp. 93\u2013103. IEEE (2020)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-29860-8_12","volume-title":"Runtime Verification","author":"E Asarin","year":"2012","unstructured":"Asarin, E., Donz\u00e9, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 147\u2013160. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_12"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/11813040_13","volume-title":"FM 2006: Formal Methods","author":"S Bacherini","year":"2006","unstructured":"Bacherini, S., Fantechi, A., Tempestini, M., Zingoni, N.: A story about formal methods adoption by a railway signaling manufacturer. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 179\u2013189. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_13"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11415787_20","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"F Badeau","year":"2005","unstructured":"Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334\u2013354. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11415787_20"},{"key":"6_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Mateis, C., Nesterini, E., Nickovic, D.: Survey on mining signal temporal logic specifications. Inf. Comput. 289(Part), 104957 (2022). https:\/\/doi.org\/10.1016\/J.IC.2022.104957","DOI":"10.1016\/J.IC.2022.104957"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Biere, A.: Picosat essentials. J. Satisf. Boolean Model. Comput. 4(2-4), 75\u201397 (2008). https:\/\/doi.org\/10.3233\/SAT190039","DOI":"10.3233\/SAT190039"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-06410-9_4","volume-title":"FM 2014: Formal Methods","author":"D Bj\u00f8rner","year":"2014","unstructured":"Bj\u00f8rner, D., Havelund, K.: 40 years of formal methods. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 42\u201361. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_4"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., Phan, A.: $$\\nu $$z - maximal satisfaction with Z3. In: Kutsia, T., Voronkov, A. (eds.) 6th International Symposium on Symbolic Computation in Software Science, SCSS 2014, Gammarth, La Marsa, Tunisia, 7\u20138 December 2014. EPiC Series in Computing, vol.\u00a030, pp.\u00a01\u20139. EasyChair (2014). https:\/\/doi.org\/10.29007\/JMXJ","DOI":"10.29007\/JMXJ"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Bombara, G., Vasile, C.I., Penedo, F., Yasuoka, H., Belta, C.: A decision tree approach to data classification using signal temporal logic. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 1\u201310. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2883817.2883843","DOI":"10.1145\/2883817.2883843"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Bordais, B., Neider, D., Roy, R.: Learning branching-time properties in CTL and ATL via constraint solving. CoRR abs\/2406.19890 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2406.19890","DOI":"10.48550\/ARXIV.2406.19890"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear temporal logic. In: ICAPS, pp. 621\u2013630. AAAI Press (2019)","DOI":"10.1609\/icaps.v29i1.3529"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/10722167_34","volume-title":"Computer Aided Verification","author":"W Chan","year":"2000","unstructured":"Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450\u2013463. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_34"},{"key":"6_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-98464-9_7","volume-title":"REFSQ 2022","author":"H Cherukuri","year":"2022","unstructured":"Cherukuri, H., Ferrari, A., Spoletini, P.: Towards explainable formal methods: from LTL to natural language with neural machine translation. In: Gervasi, V., Vogelsang, A. (eds.) REFSQ 2022. LNCS, vol. 13216, pp. 79\u201386. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-030-98464-9_7"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Chou, G., Ozay, N., Berenson, D.: Learning temporal logic formulas from suboptimal demonstrations: theory and experiments. Auton. Robots 46(1), 149\u2013174 (2022). https:\/\/doi.org\/10.1007\/S10514-021-10004-X","DOI":"10.1007\/S10514-021-10004-X"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001). https:\/\/doi.org\/10.1023\/A:1011276507260","DOI":"10.1023\/A:1011276507260"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-06200-6_1","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2014","unstructured":"Cofer, D., Miller, S.: DO-333 certification case studies. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 1\u201315. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_1"},{"key":"6_CR21","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-031-37703-7_18","volume-title":"CAV 2023, 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 temporal logics with large language models. In: Enea, C., Lal, A. (eds.) CAV 2023, Part II. LNCS, vol. 13965, pp. 383\u2013396. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Ardis, M.A., Atlee, J.M. (eds.) Proceedings of the Second Workshop on Formal Methods in Software Practice, Clearwater Beach, Florida, USA, 4\u20135 March 1998, pp. 7\u201315. ACM (1998). https:\/\/doi.org\/10.1145\/298595.298598","DOI":"10.1145\/298595.298598"},{"issue":"12","key":"6_CR23","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1016\/S0140-3664(99)00246-7","volume":"23","author":"MA Fecko","year":"2000","unstructured":"Fecko, M.A., et al.: A success story of formal description techniques: Estelle specification and test generation for MIL-STD 188\u2013220. Comput. Commun. 23(12), 1196\u20131213 (2000)","journal-title":"Comput. Commun."},{"key":"6_CR24","doi-asserted-by":"publisher","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, Taipei, Taiwan, 18\u201322 October 2010, pp. 1988\u20131993. IEEE (2010). https:\/\/doi.org\/10.1109\/IROS.2010.5650371","DOI":"10.1109\/IROS.2010.5650371"},{"key":"6_CR25","doi-asserted-by":"publisher","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 Thirty-Seventh AAAI Conference on Artificial Intelligence and Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence and Thirteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2023\/IAAI 2023\/EAAI 2023. AAAI Press (2023). https:\/\/doi.org\/10.1609\/aaai.v37i13.27068","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-88885-5_6","volume-title":"Automated Technology for Verification and Analysis","author":"J-R Gaglione","year":"2021","unstructured":"Gaglione, J.-R., Neider, D., Roy, R., Topcu, U., Xu, Z.: Learning linear temporal properties from noisy data: a MaxSAT-based approach. In: Hou, Z., Ganesh, V. (eds.) ATVA 2021. LNCS, vol. 12971, pp. 74\u201390. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_6"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41540-6_1","volume-title":"Computer Aided Verification","author":"M Gario","year":"2016","unstructured":"Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., Rozier, K.Y.: Model checking at scale: automated air traffic control design space exploration. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_1"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan & Claypool Publishers (2012). https:\/\/doi.org\/10.2200\/S00457ED1V01Y201211AIM019","DOI":"10.2200\/S00457ED1V01Y201211AIM019"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Gener. Comput. 9(3\/4), 365\u2013386 (1991). https:\/\/doi.org\/10.1007\/BF03037169","DOI":"10.1007\/BF03037169"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Ghiorzi, E., Colledanchise, M., Piquet, G., Bernagozzi, S., Tacchella, A., Natale, L.: Learning linear temporal properties for autonomous robotic systems. IEEE Robotics Autom. Lett. 8(5), 2930\u20132937 (2023). https:\/\/doi.org\/10.1109\/LRA.2023.3263368","DOI":"10.1109\/LRA.2023.3263368"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., Steiner, W.: ARSENAL: automatic requirements specification extraction from natural language. In: NASA Formal Methods, NFM (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_4","DOI":"10.1007\/978-3-319-40648-0_4"},{"key":"6_CR32","unstructured":"Giacomo, G.D., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, 3\u20139 August 2013, pp. 854\u2013860. IJCAI\/AAAI (2013). http:\/\/www.aaai.org\/ocs\/index.php\/IJCAI\/IJCAI13\/paper\/view\/6997"},{"key":"6_CR33","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Rhein, J., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. In: International Conference on Requirements Engineering: Foundation for Software Quality, REFSQ (2020). http:\/\/ceur-ws.org\/Vol-2584\/PT-paper4.pdf"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Greenman, B., Saarinen, S., Nelson, T., Krishnamurthi, S.: Little tricky logic: misconceptions in the understanding of LTL. Art Sci. Eng. Program. 7(2) (2023)","DOI":"10.22152\/programming-journal.org\/2023\/7\/7"},{"key":"6_CR35","unstructured":"Hahn, C., Schmitt, F., Kreber, J.U., Rabe, M.N., Finkbeiner, B.: Teaching temporal logics to neural networks. In: 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, 3\u20137 May 2021. OpenReview.net (2021). https:\/\/openreview.net\/forum?id=dOcQK-f4byz"},{"key":"6_CR36","unstructured":"Hamilton, W.L., Ying, R., Leskovec, J.: Representation learning on graphs: methods and applications. IEEE Data Eng. Bull. 40(3), 52\u201374 (2017). http:\/\/sites.computer.org\/debull\/A17sept\/p52.pdf"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The logic of bugs. In: SIGSOFT FSE, pp. 81\u201387. ACM (2002)","DOI":"10.1145\/587051.587064"},{"key":"6_CR38","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-031-49299-0_3","volume-title":"ILP 2023","author":"A Ielo","year":"2023","unstructured":"Ielo, A., Law, M., Fionda, V., Ricca, F., De Giacomo, G., Russo, A.: Towards ILP-based LTLF passive learning. In: Bellodi, E., Lisi, F.A., Zese, R. (eds.) ILP 2023. LNCS, vol. 14363, pp. 30\u201345. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-49299-0_3"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Kim, J., Muise, C., Shah, A., Agarwal, S., Shah, J.: Bayesian inference of linear temporal logic specifications for contrastive explanations. In: IJCAI, pp. 5591\u20135598. ijcai.org (2019)","DOI":"10.24963\/ijcai.2019\/776"},{"issue":"6","key":"6_CR40","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"6_CR41","doi-asserted-by":"publisher","unstructured":"Kong, Z., Jones, A., Belta, C.: Temporal logics for learning and detection of anomalous behavior. IEEE Trans. Autom. Control 62(3), 1210\u20131222 (2017). https:\/\/doi.org\/10.1109\/TAC.2016.2585083","DOI":"10.1109\/TAC.2016.2585083"},{"key":"6_CR42","doi-asserted-by":"publisher","unstructured":"Kong, Z., Jones, A., Medina\u00a0Ayala, A., Aydin\u00a0Gol, E., Belta, C.: Temporal logic inference for classification and prediction from data. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, pp. 273\u2013282. Association for Computing Machinery, New York (2014). https:\/\/doi.org\/10.1145\/2562059.2562146","DOI":"10.1145\/2562059.2562146"},{"issue":"12","key":"6_CR43","doi-asserted-by":"publisher","first-page":"1343","DOI":"10.1163\/156855308X344864","volume":"22","author":"H Kress-Gazit","year":"2008","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Translating structured English to robot controllers. Adv. Robot. 22(12), 1343\u20131359 (2008)","journal-title":"Adv. Robot."},{"key":"6_CR44","doi-asserted-by":"publisher","unstructured":"Lemieux, C., Beschastnikh, I.: Investigating program behavior using the texada LTL specifications miner. In: Cohen, M.B., Grunske, L., Whalen, M. (eds.) 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, 9\u201313 November 2015, pp. 870\u2013875. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/ASE.2015.94","DOI":"10.1109\/ASE.2015.94"},{"key":"6_CR45","doi-asserted-by":"crossref","unstructured":"Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In: MEMOCODE, pp. 43\u201350. IEEE (2011)","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"6_CR46","doi-asserted-by":"publisher","unstructured":"Liu, J.X., et al.: Lang2LTL: translating natural language commands to temporal robot task specification. CoRR abs\/2302.11649 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2302.11649","DOI":"10.48550\/ARXIV.2302.11649"},{"issue":"3","key":"6_CR47","first-page":"93","volume":"17","author":"G Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Softw. Concepts Tools 17(3), 93\u2013102 (1996)","journal-title":"Softw. Concepts Tools"},{"key":"6_CR48","doi-asserted-by":"crossref","unstructured":"Luo, W., Liang, P., Du, J., Wan, H., Peng, B., Zhang, D.: Bridging LTLf inference to GNN inference for learning LTLf formulae. In: AAAI, pp. 9849\u20139857. AAAI Press (2022)","DOI":"10.1609\/aaai.v36i9.21221"},{"key":"6_CR49","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-031-45332-8_2","volume-title":"ATVA 2023, Part II","author":"S Lutz","year":"2023","unstructured":"Lutz, S., Neider, D., Roy, R.: Specification sketching for linear temporal logic. In: Andr\u00e9, \u00c9., Sun, J. (eds.) ATVA 2023, Part II. LNCS, vol. 14216, pp. 26\u201348. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_2"},{"key":"6_CR50","doi-asserted-by":"publisher","unstructured":"Mohammadinejad, S., Deshmukh, J.V., Puranic, A.G., Vazquez-Chanlatte, M., Donz\u00e9, A.: Interpretable classification of time-series data using efficient enumerative techniques. In: HSCC 2020: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, 21\u201324 April 2020, pp. 9:1\u20139:10. ACM (2020). https:\/\/doi.org\/10.1145\/3365365.3382218","DOI":"10.1145\/3365365.3382218"},{"key":"6_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"6_CR52","doi-asserted-by":"publisher","unstructured":"Neider, D., Gavran, I.: Learning linear temporal properties. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pp. 1\u201310. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603016","DOI":"10.23919\/FMCAD.2018.8603016"},{"key":"6_CR53","doi-asserted-by":"publisher","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley Interscience Series in Discrete Mathematics and Optimization. Wiley (1988). https:\/\/doi.org\/10.1002\/9781118627372","DOI":"10.1002\/9781118627372"},{"key":"6_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-319-99154-2_20","volume-title":"Quantitative Evaluation of Systems","author":"L Nenzi","year":"2018","unstructured":"Nenzi, L., Silvetti, S., Bartocci, E., Bortolussi, L.: A robust genetic algorithm for learning temporal specifications from data. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 323\u2013338. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_20"},{"key":"6_CR55","doi-asserted-by":"publisher","unstructured":"Nikora, A.P., Balcom, G.: Automated identification of LTL patterns in natural language requirements. In: ISSRE 2009, 20th International Symposium on Software Reliability Engineering, Mysuru, Karnataka, India, 16\u201319 November 2009, pp. 185\u2013194. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/ISSRE.2009.15","DOI":"10.1109\/ISSRE.2009.15"},{"key":"6_CR56","doi-asserted-by":"publisher","unstructured":"Oh, Y., Patel, R., Nguyen, T., Huang, B., Pavlick, E., Tellex, S.: Planning with state abstractions for non-Markovian task specifications. In: Bicchi, A., Kress-Gazit, H., Hutchinson, S. (eds.) Robotics: Science and Systems XV, University of Freiburg, Freiburg im Breisgau, Germany, 22\u201326 June 2019 (2019). https:\/\/doi.org\/10.15607\/RSS.2019.XV.059","DOI":"10.15607\/RSS.2019.XV.059"},{"key":"6_CR57","doi-asserted-by":"publisher","unstructured":"Pan, J., Chou, G., Berenson, D.: Data-efficient learning of natural language to linear temporal logic translators for robot task specification. In: IEEE International Conference on Robotics and Automation, ICRA 2023, London, UK, May 29 - June 2, 2023, pp. 11554\u201311561. IEEE (2023). https:\/\/doi.org\/10.1109\/ICRA48891.2023.10161125","DOI":"10.1109\/ICRA48891.2023.10161125"},{"key":"6_CR58","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"6_CR59","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-031-63498-7_22","volume-title":"IJCAR 2024, Part I","author":"A Pommellet","year":"2024","unstructured":"Pommellet, A., Stan, D., Scatton, S.: SAT-based learning of computation tree logic. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) IJCAR 2024, Part I. LNCS, vol. 14739, pp. 366\u2013385. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_22"},{"key":"6_CR60","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-030-99524-9_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Raha","year":"2022","unstructured":"Raha, R., Roy, R., Fijalkow, N., Neider, D.: Scalable anytime algorithms for learning fragments of linear temporal logic. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 263\u2013280. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_14"},{"key":"6_CR61","doi-asserted-by":"publisher","unstructured":"Raha, R., Roy, R., Fijalkow, N., Neider, D.: Scarlet: scalable anytime algorithms for learning fragments of linear temporal logic. J. Open Source Softw. 9(93), 5052 (2024). https:\/\/doi.org\/10.21105\/JOSS.05052","DOI":"10.21105\/JOSS.05052"},{"key":"6_CR62","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-031-50521-8_13","volume-title":"VMCAI 2024","author":"R Raha","year":"2024","unstructured":"Raha, R., Roy, R., Fijalkow, N., Neider, D., P\u00e9rez, G.A.: Synthesizing efficiently monitorable formulas in metric temporal logic. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) VMCAI 2024. LNCS, vol. 14500, pp. 264\u2013288. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-50521-8_13"},{"key":"6_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-25543-5_5","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzli, A., Barrett, C., Tinelli, C.: cvc4sy: smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019, Part II. LNCS, vol. 11562, pp. 74\u201383. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5"},{"key":"6_CR64","doi-asserted-by":"crossref","unstructured":"Riener, H.: Exact synthesis of LTL properties from traces. In: FDL, pp.\u00a01\u20136. IEEE (2019)","DOI":"10.1109\/FDL.2019.8876900"},{"key":"6_CR65","doi-asserted-by":"crossref","unstructured":"Roy, R., Fisman, D., Neider, D.: Learning interpretable models in the property specification language. In: IJCAI, pp. 2213\u20132219. ijcai.org (2020)","DOI":"10.24963\/ijcai.2020\/306"},{"key":"6_CR66","unstructured":"Roy, R., Gaglione, J., Baharisangari, N., Neider, D., Xu, Z., Topcu, U.: Learning interpretable temporal properties from positive examples only. CoRR abs\/2209.02650 (2022)"},{"key":"6_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-319-48869-1_2","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"KY Rozier","year":"2016","unstructured":"Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 8\u201326. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2"},{"key":"6_CR68","unstructured":"Shah, A., Kamath, P., Shah, J.A., Li, S.: Bayesian inference of temporal task specifications from demonstrations. In: NeurIPS, pp. 3808\u20133817 (2018)"},{"key":"6_CR69","doi-asserted-by":"crossref","unstructured":"Valizadeh, M., Fijalkow, N., Berger, M.: LTL learning on GPUS. In: Gurfinkel, A., Ganesh, V. (eds.) CAV 2024. LNCS, vol. 14683, pp. 209\u2013231. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_10","DOI":"10.1007\/978-3-031-65633-0_10"},{"key":"6_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-74984-4_16","volume-title":"SDL 2007: Design for Dependable Systems","author":"E Verhulst","year":"2007","unstructured":"Verhulst, E., de Jong, G.: OpenComRTOS: an ultra-small network centric embedded RTOS designed using formal modeling. In: Gaudin, E., Najm, E., Reed, R. (eds.) SDL 2007. LNCS, vol. 4745, pp. 258\u2013271. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74984-4_16"},{"key":"6_CR71","doi-asserted-by":"publisher","unstructured":"W\u00e4chter, A., Biegler, L.T.: On the implementation of an interior-point filter line-search algorithm for large-scale nonlinear programming. Math. Program. 106(1), 25\u201357 (2006). https:\/\/doi.org\/10.1007\/S10107-004-0559-Y","DOI":"10.1007\/S10107-004-0559-Y"},{"key":"6_CR72","doi-asserted-by":"crossref","unstructured":"Wan, H., Liang, P., Du, J., Luo, W., Ye, R., Peng, B.: End-to-end learning of LTLF formulae by faithful LTLF encoding. In: AAAI, pp. 9071\u20139079. AAAI Press (2024)","DOI":"10.1609\/aaai.v38i8.28757"},{"issue":"3\u20134","key":"6_CR73","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10515-011-0084-1","volume":"18","author":"A Wasylkowski","year":"2011","unstructured":"Wasylkowski, A., Zeller, A.: Mining temporal specifications from object usage. Autom. Softw. Eng. 18(3\u20134), 263\u2013292 (2011)","journal-title":"Autom. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75778-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T08:02:46Z","timestamp":1731830566000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75778-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"ISBN":["9783031757778","9783031757785"],"references-count":73,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75778-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"18 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}