{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:05Z","timestamp":1776333425259,"version":"3.51.2"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Linear temporal logic (LTL) is widely used in industrial verification. LTL formulae can be learned from traces. Scaling LTL formula learning is an open problem. We implement the first GPU-based LTL learner using a novel form of enumerative program synthesis. The learner is sound and complete. Our benchmarks indicate that it handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners. This is achieved with, among others, a branch-free implementation of LTL that has <jats:inline-formula><jats:alternatives><jats:tex-math>$$O(\\log n)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>O<\/mml:mi>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mo>log<\/mml:mo>\n                    <mml:mi>n<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> time complexity, where <jats:italic>n<\/jats:italic> is trace length, while previous implementations are <jats:inline-formula><jats:alternatives><jats:tex-math>$$O(n^2)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>O<\/mml:mi>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:msup>\n                      <mml:mi>n<\/mml:mi>\n                      <mml:mn>2<\/mml:mn>\n                    <\/mml:msup>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> or worse (assuming bitwise boolean operations and shifts by powers of 2 have unit costs\u2014a realistic assumption on modern processors).<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_10","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"209-231","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["LTL Learning on\u00a0GPUs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1582-3213","authenticated-orcid":false,"given":"Mojtaba","family":"Valizadeh","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6576-4680","authenticated-orcid":false,"given":"Nathana\u00ebl","family":"Fijalkow","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3239-5812","authenticated-orcid":false,"given":"Martin","family":"Berger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"10_CR1","unstructured":"Github repository. https:\/\/github.com\/MojtabaValizadeh\/ltl-learning-on-gpus (2024)"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Ammons, G., Bod\u00edk, R., Larus, J.R.: Mining specifications. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 4\u201316. POPL \u201902, Association for Computing Machinery, New York, NY, USA (2002). https:\/\/doi.org\/10.1145\/503272.503275","DOI":"10.1145\/503272.503275"},{"key":"10_CR3","unstructured":"Anderson, S.E.: Bit twiddling hacks: round up to the next highest power of 2 (2005). https:\/\/graphics.stanford.edu\/~seander\/bithacks.html"},{"key":"10_CR4","doi-asserted-by":"publisher","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: Proceedings of the International Conference on Formal Methods in Computer Aided Design, FMCAD, pp. 93\u2013103 (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_16","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_16"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear temporal logic. In: Proceedings of the Twenty-Ninth International Conference on Automated Planning and Scheduling, ICAPS 2019, Berkeley, CA, USA, July 11-15, 2019, pp. 621\u2013630. AAAI Press (2019). https:\/\/ojs.aaai.org\/index.php\/ICAPS\/article\/view\/3529","DOI":"10.1609\/icaps.v29i1.3529"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear temporal logic. In: International Conference on Automated Planning and Scheduling, ICAPS. vol. 29, pp. 621\u2013630 (2019). https:\/\/ojs.aaai.org\/index.php\/ICAPS\/article\/view\/3529","DOI":"10.1609\/icaps.v29i1.3529"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-00768-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"YF Chen","year":"2009","unstructured":"Chen, Y.F., Farzan, A., Clarke, E.M., Tsay, Y.K., Wang, B.Y.: Learning minimal separating DFA\u2019s for compositional verification. In: Kowalewski, S., Philippou, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 31\u201345. Springer, Berlin Heidelberg, Berlin, Heidelberg (2009)"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Dally, W.J., Turakhia, Y., Han, S.: Domain-specific hardware accelerators. Commun. ACM 63(7), 48\u201357 (2020). https:\/\/doi.org\/10.1145\/3361682","DOI":"10.1145\/3361682"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"David, C., Kroening, D.: Program Synthesis: Challenges and Opportunities. Philos. Trans. A 375(2104), 20150403 (2017)","DOI":"10.1098\/rsta.2015.0403"},{"key":"10_CR10","unstructured":"De\u00a0Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, pp. 854\u2013860. IJCAI \u201913, AAAI Press (2013)"},{"key":"10_CR11","unstructured":"Fijalkow, N., Lagarde, G.: The complexity of learning linear temporal formulas from examples. In: Proceedings of the Fifteenth International Conference on Grammatical Inference. Proceedings of Machine Learning Research, vol. 153, pp. 237\u2013250. PMLR (2021). https:\/\/proceedings.mlr.press\/v153\/fijalkow21a.html"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Gabel, M., Su, Z.: Javert: fully automatic mining of general temporal properties from dynamic traces. In: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 339\u2013349. SIGSOFT \u201908\/FSE-16, Association for Computing Machinery, New York, NY, USA (2008). https:\/\/doi.org\/10.1145\/1453101.1453150","DOI":"10.1145\/1453101.1453150"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Gabel, M., Su, Z.: Symbolic Mining of Temporal Specifications. In: Proceedings of the 30th International Conference on Software Engineering, pp. 51\u201360. ICSE \u201908, Association for Computing Machinery, New York, NY, USA (2008). https:\/\/doi.org\/10.1145\/1368088.1368096","DOI":"10.1145\/1368088.1368096"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Gabel, M., Su, Z.: Online Inference and Enforcement of Temporal Properties. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering - Volume 1, pp. 15\u201324. ICSE \u201910, Association for Computing Machinery, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1806799.1806806","DOI":"10.1145\/1806799.1806806"},{"issue":"3","key":"10_CR15","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/S11334-022-00444-8","volume":"18","author":"J Gaglione","year":"2022","unstructured":"Gaglione, J., Neider, D., Roy, R., Topcu, U., Xu, Z.: Maxsat-based temporal logic inference from noisy data. Innovations Syst. Softw. Eng. 18(3), 427\u2013442 (2022). https:\/\/doi.org\/10.1007\/S11334-022-00444-8","journal-title":"Innovations Syst. Softw. Eng."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Polozov, O., Singh, R.: Program Synthesis. Now Foundations and Trends (2017). http:\/\/ieeexplore.ieee.org\/document\/8187066","DOI":"10.1561\/9781680832938"},{"key":"10_CR17","unstructured":"Hennessy, J., Patterson, D.: Computer Architecture: a quantitative approach. The Morgan Kaufmann Series in Computer Architecture and Design, Morgan Kaufmann (2017)"},{"key":"10_CR18","unstructured":"Hwu, W.M.W., Kirk, D.B., Hajj, I.E.: Programming Massively Parallel Processors, Morgan Kaufmann (2022)"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Ielo, A., Law, M., Fionda, V., Ricca, F., De\u00a0Giacomo, G., Russo, A.: Towards ILP-Based $$\\text{LTL}_{f}$$ Passive Learning. In: Inductive Logic Programming, pp. 30\u201345. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-49299-0_3","DOI":"10.1007\/978-3-031-49299-0_3"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Jeppu, N., Melham, T., Kroening, D., O\u2019Leary, J.: Learning Concise Models from Long Execution Traces. In: Proceedings of the 57th ACM\/IEEE Design Automation Conference, DAC. pp.\u00a01\u20136 (2020).https:\/\/doi.org\/10.1109\/DAC18072.2020.9218613","DOI":"10.1109\/DAC18072.2020.9218613"},{"key":"10_CR21","unstructured":"J\u00fcnger, D.: WARPCORE: hashing at the speed of light on modern CUDA-accelerators (2022). https:\/\/github.com\/sleeepyjack\/warpcore"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"J\u00fcnger, D., et al.: WarpCore: a library for fast hash tables on GPUs. In: Proceedings of the 27th International Conference on High Performance Computing, Data, and Analytics, HiPC, pp. 11\u201320 (2020). https:\/\/doi.org\/10.1109\/HiPC50609.2020.00015","DOI":"10.1109\/HiPC50609.2020.00015"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Kim, J., Muise, C., Shah, A., Agarwal, S., Shah, J.: Bayesian inference of linear temporal logic specifications for contrastive explanations. In: International Joint Conference on Artificial Intelligence, IJCAI (2019). https:\/\/doi.org\/10.24963\/ijcai.2019\/776","DOI":"10.24963\/ijcai.2019\/776"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Lemieux, C., Beschastnikh, I.: Investigating program behavior using the texada LTL specifications miner. In: Proceedings of the 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 870\u2013875. IEEE Computer Society, Los Alamitos, CA, USA (2015). https:\/\/doi.org\/10.1109\/ASE.2015.94","DOI":"10.1109\/ASE.2015.94"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining. In: Proceedings of the 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 81\u201392. IEEE Computer Society, Los Alamitos, CA, USA (2015). https:\/\/doi.org\/10.1109\/ASE.2015.71","DOI":"10.1109\/ASE.2015.71"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Luo, W., Liang, P., Du, J., Wan, H., Peng, B., Zhang, D.: Bridging LTLf inference to GNN inference for learning LTLf formulae. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 36(9), 9849\u20139857 (2022). https:\/\/doi.org\/10.1609\/aaai.v36i9.21221","DOI":"10.1609\/aaai.v36i9.21221"},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Mascle, C., Fijalkow, N., Lagarde, G.: Learning temporal formulas from examples is hard (2023). https:\/\/doi.org\/10.48550\/arXiv.2312.16336","DOI":"10.48550\/arXiv.2312.16336"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Neider, D., Gavran, I.: Learning linear temporal properties. In: Formal Methods in Computer Aided Design, FMCADm, pp. 1\u201310 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603016","DOI":"10.23919\/FMCAD.2018.8603016"},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"Peng, B., et al.: PURLTL: mining LTL specification from imperfect traces in testing. In: Proceedings of the 38th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 1766\u20131770. IEEE Computer Society, Los Alamitos, CA, USA (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00202","DOI":"10.1109\/ASE56229.2023.00202"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, FOCS, pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Raha, R., Rajarshi, R., Fijalkow, N., Neider, D.: Scarlet: scalable anytime algorithms for learning fragments of linear temporal logic (2024)","DOI":"10.21105\/joss.05052"},{"key":"10_CR32","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":"10_CR33","doi-asserted-by":"publisher","unstructured":"Valizadeh, M., Berger, M.: Search-based regular expression inference on a GPU. Proc. ACM Program. Lang. 7(PLDI), 1317\u20131339 (2023). https:\/\/doi.org\/10.1145\/3591274, technical report available at https:\/\/arxiv.org\/abs\/2305.18575, implementation: https:\/\/github.com\/MojtabaValizadeh\/paresy","DOI":"10.1145\/3591274"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-540-31980-1_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Weimer","year":"2005","unstructured":"Weimer, W., Necula, G.C.: Mining temporal specifications for error detection. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 461\u2013476. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_30"},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Yang, J., Evans, D., Bhardwaj, D., Bhat, T., Das, M.: Perracotta: mining temporal API rules from imperfect traces. In: Proceedings of the 28th International Conference on Software Engineering, pp. 282\u2013291. ICSE \u201906, Association for Computing Machinery, New York, NY, USA (2006). https:\/\/doi.org\/10.1145\/1134285.1134325","DOI":"10.1145\/1134285.1134325"},{"key":"10_CR36","unstructured":"Yogananda\u00a0Jeppu, N.: Learning symbolic abstractions from system execution traces. Ph.D. thesis, University of Oxford (2022)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:04:24Z","timestamp":1721891064000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}