{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T16:22:55Z","timestamp":1792254175549,"version":"4.4.0"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031505201","type":"print"},{"value":"9783031505218","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"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-3-031-50521-8_13","type":"book-chapter","created":{"date-parts":[[2023,12,29]],"date-time":"2023-12-29T08:03:15Z","timestamp":1703836995000},"page":"264-288","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Synthesizing Efficiently Monitorable Formulas in\u00a0Metric Temporal Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1467-1182","authenticated-orcid":false,"given":"Ritam","family":"Raha","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0202-1169","authenticated-orcid":false,"given":"Rajarshi","family":"Roy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6576-4680","authenticated-orcid":false,"given":"Nathana\u00ebl","family":"Fijalkow","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9276-6342","authenticated-orcid":false,"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1200-4952","authenticated-orcid":false,"given":"Guillermo A.","family":"P\u00e9rez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,12,30]]},"reference":[{"key":"13_CR1","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":"13_CR2","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":"13_CR3","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":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-35632-2_24","volume-title":"Runtime Verification","author":"K Baldor","year":"2013","unstructured":"Baldor, K., Niu, J.: Monitoring dense-time, continuous-semantics, metric temporal logic. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 245\u2013259. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_24"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 1267\u20131329. IOS Press (2021)","DOI":"10.3233\/FAIA201017"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-75632-5_5","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Deshmukh, J., Donz\u00e9, A., Fainekos, G., Maler, O., Ni\u010dkovi\u0107, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Mateis, C., Nesterini, E., Nickovic, D.: Survey on mining signal temporal logic specifications. Inform. Comput. 289, 104957 (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104957. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540122001122","DOI":"10.1016\/j.ic.2022.104957"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-29860-8_20","volume-title":"Runtime Verification","author":"D Basin","year":"2012","unstructured":"Basin, D., Klaedtke, F., Z\u0103linescu, E.: Algorithms for monitoring real-time properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 260\u2013275. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_20"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-67531-2_6","volume-title":"Runtime Verification","author":"D Basin","year":"2017","unstructured":"Basin, D., Krsti\u0107, S., Traytel, D.: Almost event-rate independent monitoring of metric dynamic logic. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 85\u2013102. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67531-2_6"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Basin, D.A., Krstic, S., Traytel, D.: AERIAL: almost event-rate independent algorithms for monitoring metric regular properties. In: RV-CuBES. Kalpa Publications in Computing, vol. 3, pp. 29\u201336. EasyChair (2017)","DOI":"10.29007\/bm4c"},{"key":"13_CR12","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":"13_CR13","doi-asserted-by":"publisher","unstructured":"Bombara, G., Belta, C.: Offline and online learning of signal temporal logic formulae using decision trees. ACM Trans. Cyber-Phys. Syst. 5(3) (2021). https:\/\/doi.org\/10.1145\/3433994","DOI":"10.1145\/3433994"},{"key":"13_CR14","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":"13_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":"13_CR16","doi-asserted-by":"publisher","unstructured":"Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear temporal logic. Proceedings of the International Conference on Automated Planning and Scheduling, vol. 29(1), 621\u2013630 (May 2021). https:\/\/doi.org\/10.1609\/icaps.v29i1.3529,https:\/\/ojs.aaai.org\/index.php\/ICAPS\/article\/view\/3529","DOI":"10.1609\/icaps.v29i1.3529,"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-030-60508-7_21","volume-title":"Runtime Verification","author":"A Chattopadhyay","year":"2020","unstructured":"Chattopadhyay, A., Mamouras, K.: A verified online monitor for metric temporal logic with quantitative semantics. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 383\u2013403. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_21"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"13_CR19","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Dang, T., Stolz, V. (eds.): Runtime Verification - 22nd International Conference, RV 2022, Tbilisi, Georgia, September 28\u201330, 2022, Proceedings. LNCS, vol. 13498. Springer (2022)","DOI":"10.1007\/978-3-031-17196-3"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Deshmukh, J.V., Donz\u00e9, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. In: RV. LNCS, vol. 9333, pp. 55\u201370. Springer (2015)","DOI":"10.1007\/978-3-319-23820-3_4"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-11164-3_19","volume-title":"Runtime Verification","author":"A Dokhanchi","year":"2014","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.: On-Line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231\u2013246. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_19"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-642-39799-8_19","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2013","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264\u2013279. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27\u201339. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_3"},{"key":"13_CR25","unstructured":"Fijalkow, N., Lagarde, G.: The complexity of learning linear temporal formulas from examples. In: ICGI. Proceedings of Machine Learning Research, vol. 153, pp. 237\u2013250. PMLR (2021)"},{"key":"13_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":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-030-72013-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Gorostiaga","year":"2021","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: HLola: a very functional tool for extensible stream runtime verification. In: TACAS 2021. LNCS, vol. 12652, pp. 349\u2013356. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_18"},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-030-03769-7_7","volume-title":"Runtime Verification","author":"K Havelund","year":"2018","unstructured":"Havelund, K., Peled, D.: Runtime verification: from propositional to first-order temporal logic. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 90\u2013112. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_7"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-11164-3_15","volume-title":"Runtime Verification","author":"H-M Ho","year":"2014","unstructured":"Ho, H.-M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 178\u2013192. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_15"},{"issue":"1","key":"13_CR30","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10009-017-0447-4","volume":"20","author":"B Hoxha","year":"2018","unstructured":"Hoxha, B., Dokhanchi, A., Fainekos, G.: Mining parametric temporal logic properties in model-based design for cyber-physical systems. Int. J. Softw. Tools Technol. Transf. 20(1), 79\u201393 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness for metric temporal logic. In: 2013 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 349\u2013357 (2013). https:\/\/doi.org\/10.1109\/LICS.2013.1","DOI":"10.1109\/LICS.2013.1"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-23820-3_7","volume-title":"Runtime Verification","author":"A Kane","year":"2015","unstructured":"Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 102\u2013117. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_7"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-030-57628-8_12","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B Kempa","year":"2020","unstructured":"Kempa, B., Zhang, P., Jones, P.H., Zambreno, J., Rozier, K.Y.: Embedding online runtime verification for fault disambiguation on Robonaut2. In: Bertrand, N., Jansen, N. (eds.) FORMATS 2020. LNCS, vol. 12288, pp. 196\u2013214. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-57628-8_12"},{"issue":"3","key":"13_CR34","doi-asserted-by":"publisher","first-page":"1210","DOI":"10.1109\/TAC.2016.2585083","volume":"62","author":"Z Kong","year":"2017","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","journal-title":"IEEE Trans. Autom. Control"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Kong, Z., Jones, A., Medina Ayala, A., Aydin Gol, 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"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Roman, G., Griswold, W.G., Nuseibeh, B. (eds.) 27th International Conference on Software Engineering (ICSE 2005), 15\u201321 May 2005, St. Louis, Missouri, USA, pp. 372\u2013381. ACM (2005). https:\/\/doi.org\/10.1145\/1062455.1062526","DOI":"10.1145\/1062455.1062526"},{"issue":"4","key":"13_CR37","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real Time Syst."},{"key":"13_CR38","doi-asserted-by":"crossref","unstructured":"Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining (T). In: ASE, pp. 81\u201392. IEEE Computer Society (2015)","DOI":"10.1109\/ASE.2015.71"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Lima, L., Herasimau, A., Raszyk, M., Traytel, D., Yuan, S.: Explainable online monitoring of metric temporal logic. In: TACAS (2). LNCS, vol. 13994, pp. 473\u2013491. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_28","DOI":"10.1007\/978-3-031-30820-8_28"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Linard, A., Tumova, J.: Active learning of signal temporal logic specifications. In: 2020 IEEE 16th International Conference on Automation Science and Engineering (CASE), pp. 779\u2013785 (2020). https:\/\/doi.org\/10.1109\/CASE48305.2020.9216778","DOI":"10.1109\/CASE48305.2020.9216778"},{"key":"13_CR41","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":"13_CR42","doi-asserted-by":"publisher","unstructured":"Lutz, S., Neider, D., Roy, R.: Specification sketching for linear temporal logic. In: ATVA. LNCS, vol. 14216, pp. 26\u201348. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_2","DOI":"10.1007\/978-3-031-45332-8_2"},{"key":"13_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"13_CR44","unstructured":"Meel, K.S., Strichman, O. (eds.): 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, 2\u20135 August 2022, Haifa, Israel, LIPIcs, vol. 236. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"13_CR45","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). DOI: https:\/\/doi.org\/10.1145\/3365365.3382218","DOI":"10.1145\/3365365.3382218"},{"key":"13_CR46","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"},{"issue":"9","key":"13_CR47","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"LM de Moura","year":"2011","unstructured":"de Moura, L.M., Bj\u00f8rner, N.S.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"13_CR48","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, 30 October - 2 November 2018. pp. 1\u201310. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603016","DOI":"10.23919\/FMCAD.2018.8603016"},{"key":"13_CR49","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":"13_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J Ouaknine","year":"2008","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1\u201313. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85778-5_1"},{"key":"13_CR51","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"13_CR52","unstructured":"Raha, R.: Learning and verifying temporal specifications for cyber-physical systems. Ph.D. thesis, University of Antwerp, Belgium (2023). https:\/\/hdl.handle.net\/10067\/1986580151162165141"},{"key":"13_CR53","series-title":"Lecture Notes in Computer Science","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: TACAS 2022. LNCS, vol. 13243, pp. 263\u2013280. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_14"},{"key":"13_CR54","doi-asserted-by":"crossref","unstructured":"Raha, R., Roy, R., Fijalkow, N., Neider, D., Perez, G.A.: Synthesizing efficiently monitorable formulas in metric temporal logic (2023). https:\/\/arxiv.org\/abs\/2310.17410","DOI":"10.1007\/978-3-031-50521-8_13"},{"key":"13_CR55","doi-asserted-by":"publisher","unstructured":"Raha, R., Roy, R., Fijalkow, N., Neider, D., Perez, G.A.: TEAL: Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic (Oct 2023). https:\/\/doi.org\/10.5281\/zenodo.10046302","DOI":"10.5281\/zenodo.10046302"},{"key":"13_CR56","doi-asserted-by":"crossref","unstructured":"Riener, H.: Exact synthesis of LTL properties from traces. In: FDL, pp. 1\u20136. IEEE (2019)","DOI":"10.1109\/FDL.2019.8876900"},{"key":"13_CR57","doi-asserted-by":"crossref","unstructured":"Roy, R., Fisman, D., Neider, D.: Learning interpretable models in the property specification language. In: IJCAI, pp. 2213\u20132219. https:\/\/www.ijcai.org\/Proceedings\/2020\/306 (2020)","DOI":"10.24963\/ijcai.2020\/306"},{"key":"13_CR58","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":"13_CR59","unstructured":"Silvetti, S., Nenzi, L., Bortolussi, L., Bartocci, E.: A robust genetic algorithm for learning temporal specifications from data. CoRR. arXiv: 1711.06202 (2017)"},{"key":"13_CR60","doi-asserted-by":"publisher","unstructured":"Thati, P., Rosu, G.: Monitoring algorithms for metric temporal logic specifications. In: Havelund, K., Rosu, G. (eds.) Proceedings of the Fourth Workshop on Runtime Verification, RV@ETAPS 2004, Barcelona, Spain, 3 April 2004. vol. 113, pp. 145\u2013162. Elsevier (2004). https:\/\/doi.org\/10.1016\/j.entcs.2004.01.029","DOI":"10.1016\/j.entcs.2004.01.029"},{"issue":"3\u20134","key":"13_CR61","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."},{"key":"13_CR62","doi-asserted-by":"publisher","unstructured":"Xu, Z., Topcu, U.: Transfer of temporal logic formulas in reinforcement learning. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, 10\u201316 August 2019, pp. 4010\u20134018. (2019). https:\/\/doi.org\/10.24963\/ijcai.2019\/557, https:\/\/www.ijcai.org","DOI":"10.24963\/ijcai.2019\/557"},{"key":"13_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-34691-0_11","volume-title":"Testing Software and Systems","author":"H Yang","year":"2012","unstructured":"Yang, H., Hoxha, B., Fainekos, G.: Querying parametric temporal logic properties on embedded systems. In: Nielsen, B., Weise, C. (eds.) ICTSS 2012. LNCS, vol. 7641, pp. 136\u2013151. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34691-0_11"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-50521-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,7]],"date-time":"2024-11-07T01:11:49Z","timestamp":1730941909000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-50521-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,30]]},"ISBN":["9783031505201","9783031505218"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-50521-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,30]]},"assertion":[{"value":"30 December 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","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":"15 January 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 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":"vmcai2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl24.sigplan.org\/home\/VMCAI-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"74","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}