{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T00:00:14Z","timestamp":1780444814353,"version":"3.54.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032045577","type":"print"},{"value":"9783032045584","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-04558-4_3","type":"book-chapter","created":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T11:16:53Z","timestamp":1757589413000},"page":"26-41","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["DeepCTL: Neural Branching-Time CTL Satisfiability Checking via\u00a0Recursive Decision Trees"],"prefix":"10.1007","author":[{"given":"Bingchang","family":"Yuan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhaohui","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lingfeng","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jingran","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bojie","family":"Shao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,9,12]]},"reference":[{"issue":"9","key":"3_CR1","doi-asserted-by":"publisher","first-page":"302","DOI":"10.3390\/a15090302","volume":"15","author":"T Al-Yahya","year":"2022","unstructured":"Al-Yahya, T., Menai, M.E.B.A., Mathkour, H.: Boosting the performance of cdcl-based sat solvers by exploiting backbones and backdoors. Algorithms 15(9), 302 (2022)","journal-title":"Algorithms"},{"key":"3_CR2","unstructured":"Allamanis, M., Brockschmidt, M., Khademi, M.: Learning to represent programs with graphs. arXiv preprint arXiv:1711.00740 (2017)"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Bordais, B., Neider, D., Roy, R.: Learning branching-time properties in CTL and ATL via constraint solving. In: International Symposium on Formal Methods, pp. 304\u2013323. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_16","DOI":"10.1007\/978-3-031-71162-6_16"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-319-21690-4_36","volume-title":"Computer Aided Verification","author":"M Bozzano","year":"2015","unstructured":"Bozzano, M., et al.: Formal design and safety analysis of AIR6110 wheel brake system. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 518\u2013535. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_36"},{"key":"3_CR5","unstructured":"Chris\u00a0Cameron, Rex\u00a0Chen, J.S.H., Leyton-Brown, K.: Chris cameron, rex chen, jason s. hartford, and kevin leyton-brown (2020)"},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: a new symbolic model checker. Int. J. Softw. Tools Technol. Transfer 2, 410\u2013425 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Degiovanni, R., Molina, F., Regis, G., Aguirre, N.: A genetic algorithm for goal-conflict identification, pp. 520\u2013531 (2018)","DOI":"10.1145\/3238147.3238220"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Deng, J., Krause, J., Berg, A.C., Fei-Fei, L.: Hedging your bets: optimizing accuracy-specificity trade-offs in large scale visual recognition. In: 2012 IEEE Conference on Computer Vision and Pattern Recognition, pp. 3450\u20133457. IEEE (2012)","DOI":"10.1109\/CVPR.2012.6248086"},{"key":"3_CR9","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":"3_CR10","unstructured":"Jat, S., Khandelwal, S., Talukdar, P.: Improving distantly supervised relation extraction using word and entity based attention. arXiv preprint arXiv:1804.06987 (2018)"},{"key":"3_CR11","unstructured":"Lederman, G., Rabe, M.N., Seshia, S.A.: Learning heuristics for automated reasoning through deep reinforcement learning (2018)"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Lin, Y., Shen, S., Liu, Z., Luan, H., Sun, M.: Neural relation extraction with selective attention over instances. In: Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics, vol. 1: Long Papers, pp. 2124\u20132133 (2016)","DOI":"10.18653\/v1\/P16-1200"},{"key":"3_CR13","unstructured":"Loos, S., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search (2017)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Luo, W., Wan, H., Song, X., Yang, B., Zhong, H., Chen, Y.: How to identify boundary conditions with contrasty metric?, pp. 1473\u20131484 (2021)","DOI":"10.1109\/ICSE43902.2021.00132"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Luo, W., Wan, H., Zhang, D., Du, J., Su, H.: Checking ltl satisfiability via end-to-end learning. In: Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering, pp. 1\u201313 (2022)","DOI":"10.1145\/3551349.3561163"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Osama, M., Wijs, A., Biere, A.: Certified sat solving with gpu accelerated inprocessing. Formal Methods Syst. Des. 1\u201340 (2023)","DOI":"10.1007\/s10703-023-00432-z"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_11"},{"issue":"2","key":"3_CR18","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"KY Rozier","year":"2010","unstructured":"Rozier, K.Y., Vardi, M.Y.: Ltl satisfiability checking. Int. J. Softw. Tools Technol. Transfer 12(2), 123\u2013137 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"3_CR19","unstructured":"Selsam, D., Lamm, M., B\u00fcnz, B., Liang, P., de\u00a0Moura, L., Dill, D.L.: Learning a sat solver from single-bit supervision. arXiv preprint arXiv:1802.03685 (2018)"},{"key":"3_CR20","unstructured":"Selsam, D., Lamm, M., B\u00fcnz, B., Liang, P., De\u00a0Moura, L., Dill, D.L.: Learning a sat solver from single-bit supervision (2018)"},{"key":"3_CR21","unstructured":"Socher, R., Huval, B., Manning, C.D., Ng, A.Y.: Semantic compositionality through recursive matrix-vector spaces. In: Proceedings of the 2012 Joint Conference on Empirical Methods in Natural Language Processing and Computational Natural Language Learning, pp. 1201\u20131211 (2012)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Vashishth, S., Joshi, R., Prayaga, S.S., Bhattacharyya, C., Talukdar, P.: Reside: improving distantly-supervised neural relation extraction using side information. arXiv preprint arXiv:1812.04361 (2018)","DOI":"10.18653\/v1\/D18-1157"},{"key":"3_CR23","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2022.110080","volume":"259","author":"L Wang","year":"2023","unstructured":"Wang, L., et al.: SAT-GCN: self-attention graph convolutional network-based 3d object detection for autonomous driving. Knowl.-Based Syst. 259, 110080 (2023)","journal-title":"Knowl.-Based Syst."},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Zeng, D., Liu, K., Chen, Y., Zhao, J.: Distant supervision for relation extraction via piecewise convolutional neural networks. In: Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pp. 1753\u20131762 (2015)","DOI":"10.18653\/v1\/D15-1203"}],"container-title":["Lecture Notes in Computer Science","Artificial Neural Networks and Machine Learning \u2013 ICANN 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04558-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T11:16:58Z","timestamp":1757589418000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04558-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,12]]},"ISBN":["9783032045577","9783032045584"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04558-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,12]]},"assertion":[{"value":"12 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICANN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Artificial Neural Networks","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kaunas","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lithuania","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icann2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/e-nns.org\/icann2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}