{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T00:01:53Z","timestamp":1769644913446,"version":"3.49.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We address the problem of learning temporal properties from the branching-time behavior of systems. Existing research in this field has mostly focused on learning linear temporal properties specified using popular logics, such as Linear Temporal Logic (LTL) and Signal Temporal Logic (STL). Branching-time logics such as Computation Tree Logic (CTL) and Alternating-time Temporal Logic (ATL), despite being extensively used in specifying and verifying distributed and multi-agent systems, have not received adequate attention. Thus, in this paper, we investigate the problem of learning CTL and ATL formulas from examples of system behavior. As input to the learning problems, we rely on the typical representations of branching behavior as Kripke structures and concurrent game structures, respectively. Given a sample of structures, we learn concise formulas by encoding the learning problem into a satisfiability problem, most notably by symbolically encoding both the search for prospective formulas and their fixed-point based model checking algorithms. We also study the decision problem of checking the existence of prospective ATL formulas for a given sample. We implement our algorithms in a Python prototype and have evaluated them to extract several common CTL and ATL formulas used in practical applications.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_16","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"304-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Learning Branching-Time Properties in\u00a0CTL and\u00a0ATL via\u00a0Constraint Solving"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Bordais","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[]},{"given":"Rajarshi","family":"Roy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002). https:\/\/doi.org\/10.1145\/585265.585270","DOI":"10.1145\/585265.585270"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: CAV. Lecture Notes in Computer Science, vol.\u00a01427, pp. 521\u2013525. Springer (1998)","DOI":"10.1007\/BFb0028774"},{"key":"16_CR3","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, January 16-18, 2002, pp. 4\u201316. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503275","DOI":"10.1145\/503272.503275"},{"issue":"2","key":"16_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"16_CR5","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":"16_CR6","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":"16_CR7","doi-asserted-by":"crossref","unstructured":"Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27(1), 1840001:1\u20131840001:25 (2018)","DOI":"10.1142\/S0218213018400018"},{"key":"16_CR8","unstructured":"Avellaneda, F., Petrenko, A.: Inferring DFA without negative examples. In: Unold, O., Dyrka, W., Wieczorek, W. (eds.) Proceedings of the 14th International Conference on Grammatical Inference, ICGI 2018, Wroc\u0142aw, Poland, September 5-7, 2018. Proceedings of Machine Learning Research, vol.\u00a093, pp. 17\u201329. PMLR (2018). http:\/\/proceedings.mlr.press\/v93\/avellaneda19a.html"},{"key":"16_CR9","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"16_CR10","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., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: 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":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2014 a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020949"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Bertrand, N., Fearnley, J., Schewe, S.: Bounded satisfiability for PCTL. In: C\u00e9gielski, P., Durand, A. (eds.) Computer Science Logic (CSL\u201912) - 26th International Workshop\/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France. LIPIcs, vol.\u00a016, pp. 92\u2013106. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2012.92","DOI":"10.4230\/LIPIcs.CSL.2012.92"},{"issue":"6","key":"16_CR13","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1109\/TC.1972.5009015","volume":"21","author":"AW Biermann","year":"1972","unstructured":"Biermann, A.W., Feldman, J.A.: On the synthesis of finite-state machines from samples of their behavior. IEEE Trans. Comput. 21(6), 592\u2013597 (1972)","journal-title":"IEEE Trans. Comput."},{"key":"16_CR14","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":"16_CR15","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":"16_CR16","unstructured":"Bordais, B., Neider, D., Roy, R.: Learning branching-time properties in ctl and atl via constraint solving. CoRR abs\/2406.19890 (2024). https:\/\/arxiv.org\/abs\/2406.19890"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115\u2013131 (1988). https:\/\/doi.org\/10.1016\/0304-3975(88)90098-9","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16"},{"key":"16_CR19","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":"16_CR20","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":"16_CR21","doi-asserted-by":"crossref","unstructured":"Chen, T., Lu, J.: Probabilistic alternating-time temporal logic and model checking algorithm. In: FSKD (2), pp. 35\u201339. IEEE Computer Society (2007)","DOI":"10.1109\/FSKD.2007.458"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495\u2013499. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_44"},{"key":"16_CR23","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":"16_CR24","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs. Lecture Notes in Computer Science, vol.\u00a0131, pp. 52\u201371. Springer (1981)","DOI":"10.1007\/BFb0025774"},{"key":"16_CR25","unstructured":"Fijalkow, N., Lagarde, G.: The complexity of learning linear temporal formulas from examples. In: ICGI. Proceedings of Machine Learning Research, vol.\u00a0153, pp. 237\u2013250. PMLR (2021)"},{"key":"16_CR26","unstructured":"Gario, M., Micheli, A.: Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms. In: SMT Workshop 2015 (2015)"},{"issue":"3","key":"16_CR27","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1016\/S0019-9958(78)90562-4","volume":"37","author":"EM Gold","year":"1978","unstructured":"Gold, E.M.: Complexity of automaton identification from given data. Inf. Control 37(3), 302\u2013320 (1978)","journal-title":"Inf. Control"},{"issue":"5","key":"16_CR28","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"16_CR29","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1023\/A:1026185103185","volume":"75","author":"W van der Hoek","year":"2003","unstructured":"van der Hoek, W., Wooldridge, M.J.: Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications. Stud. Logica. 75(1), 125\u2013157 (2003)","journal-title":"Stud. Logica."},{"issue":"5","key":"16_CR30","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"16_CR31","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":"3","key":"16_CR32","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":"16_CR33","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"},{"key":"16_CR34","doi-asserted-by":"publisher","unstructured":"Krogmeier, P., Madhusudan, P.: Languages with decidable learning: a meta-theorem. Proc. ACM Program. Lang. 7(OOPSLA1), 143\u2013171 (2023). https:\/\/doi.org\/10.1145\/3586032","DOI":"10.1145\/3586032"},{"key":"16_CR35","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":"16_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/11691372_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Lomuscio","year":"2006","unstructured":"Lomuscio, A., Raimondi, F.: mcmas: a model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450\u2013454. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_31"},{"key":"16_CR37","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":"16_CR38","doi-asserted-by":"publisher","unstructured":"Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: on the model-checking problem. ACM Trans. Comput. Log. 15(4), 34:1\u201334:47 (2014). https:\/\/doi.org\/10.1145\/2631917","DOI":"10.1145\/2631917"},{"key":"16_CR39","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 \u201920: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21-24, 2020, pp. 9:1\u20139:10. ACM (2020). https:\/\/doi.org\/10.1145\/3365365.3382218","DOI":"10.1145\/3365365.3382218"},{"key":"16_CR40","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":"16_CR41","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":"16_CR42","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":"16_CR43","doi-asserted-by":"publisher","unstructured":"Pommellet, A., Stan, D., Scatton, S.: Sat-based learning of computation tree logic. CoRR abs\/2402.06366 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2402.06366","DOI":"10.48550\/ARXIV.2402.06366"},{"key":"16_CR44","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":"16_CR45","doi-asserted-by":"crossref","unstructured":"Raha, R., Roy, R., Fijalkow, N., Neider, D., P\u00e9rez, G.A.: Synthesizing efficiently monitorable formulas in metric temporal logic. In: VMCAI (2). Lecture Notes in Computer Science, vol. 14500, pp. 264\u2013288. Springer (2024)","DOI":"10.1007\/978-3-031-50521-8_13"},{"key":"16_CR46","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":"16_CR47","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":"16_CR48","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":"16_CR49","unstructured":"Roy, R., Neider, D.: Inferring properties in computation tree logic. CoRR abs\/2310.13778 (2023)"},{"key":"16_CR50","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":"16_CR51","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":"16_CR52","doi-asserted-by":"publisher","unstructured":"Valizadeh, M., Fijalkow, N., Berger, M.: LTL learning on gpus. CoRR abs\/2402.12373 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2402.12373","DOI":"10.48550\/ARXIV.2402.12373"},{"key":"16_CR53","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":"16_CR54","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","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:05:09Z","timestamp":1725933909000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","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":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}