{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T07:33:21Z","timestamp":1768289601359,"version":"3.49.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031067723","type":"print"},{"value":"9783031067730","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-06773-0_26","type":"book-chapter","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T11:24:44Z","timestamp":1652959484000},"page":"489-507","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Timed Automata Learning via\u00a0SMT Solving"],"prefix":"10.1007","author":[{"given":"Martin","family":"Tappler","sequence":"first","affiliation":[]},{"given":"Bernhard K.","family":"Aichernig","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Lorber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,20]]},"reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-319-96562-8_3","volume-title":"Machine Learning for Dynamic Software Analysis: Potentials and Limits","author":"BK Aichernig","year":"2018","unstructured":"Aichernig, B.K., Mostowski, W., Mousavi, M.R., Tappler, M., Taromirad, M.: Model learning and model-based testing. In: Bennaceur, A., H\u00e4hnle, R., Meinke, K. (eds.) Machine Learning for Dynamic Software Analysis: Potentials and Limits. LNCS, vol. 11026, pp. 74\u2013100. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96562-8_3"},{"issue":"2","key":"26_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/978-3-030-45190-5_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J An","year":"2020","unstructured":"An, J., Chen, M., Zhan, B., Zhan, N., Zhang, M.: Learning one-clock timed automata. In: TACAS 2020. LNCS, vol. 12078, pp. 444\u2013462. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_25"},{"issue":"9","key":"26_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11432-019-2767-4","volume":"64","author":"J An","year":"2021","unstructured":"An, J., Wang, L., Zhan, B., Zhan, N., Zhang, M.: Learning real-time automata. Sci. China Inf. Sci. 64(9), 1\u201317 (2021). https:\/\/doi.org\/10.1007\/s11432-019-2767-4","journal-title":"Sci. China Inf. Sci."},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-95582-7_6","volume-title":"Formal Methods","author":"F Avellaneda","year":"2018","unstructured":"Avellaneda, F., Petrenko, A.: FSM inference from long traces. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 93\u2013109. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_6"},{"key":"26_CR6","unstructured":"Avellaneda, F., Petrenko, A.: Inferring DFA without negative examples. In: International Conference on Grammatical Inference, pp. 17\u201329. PMLR (2019)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-030-81688-9_9","volume-title":"Computer Aided Verification","author":"D Baier","year":"2021","unstructured":"Baier, D., Beyer, D., Friedberger, K.: JavaSMT 3: interacting with SMT solvers in java. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 195\u2013208. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_9"},{"key":"26_CR8","unstructured":"Clemente, L., Lasota, S., Pi\u00f3rkowski, R.: Determinisability of register and timed automata. CoRR abs\/2104.03690 (2021). https:\/\/arxiv.org\/abs\/2104.03690"},{"key":"26_CR9","doi-asserted-by":"publisher","unstructured":"Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theor. Comput. Sci. 411(47), 4029\u20134054 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.07.008","DOI":"10.1016\/j.tcs.2010.07.008"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/11817949_29","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"O Grinchtein","year":"2006","unstructured":"Grinchtein, O., Jonsson, B., Pettersson, P.: Inference of event-recording automata using timed decision trees. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 435\u2013449. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817949_29"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-24617-6_9","volume-title":"Formal Approaches to Software Testing","author":"A Hessel","year":"2004","unstructured":"Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-optimal real-time test case generation using UPPAAL. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 114\u2013130. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24617-6_9"},{"key":"26_CR12","doi-asserted-by":"publisher","unstructured":"Heule, M., Verwer, S.: Software model synthesis using satisfiability solvers. Empir. Softw. Eng. 18(4), 825\u2013856 (2013). https:\/\/doi.org\/10.1007\/s10664-012-9222-z","DOI":"10.1007\/s10664-012-9222-z"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-96562-8_5","volume-title":"Machine Learning for Dynamic Software Analysis: Potentials and Limits","author":"F Howar","year":"2018","unstructured":"Howar, F., Steffen, B.: Active automata learning in practice. In: Bennaceur, A., H\u00e4hnle, R., Meinke, K. (eds.) Machine Learning for Dynamic Software Analysis: Potentials and Limits. LNCS, vol. 11026, pp. 123\u2013148. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96562-8_5"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1), 134\u2013152 (1997)","DOI":"10.1007\/s100090050010"},{"key":"26_CR15","doi-asserted-by":"publisher","unstructured":"Li, W., Forin, A., Seshia, S.A.: Scalable specification mining for verification and diagnosis. In: Sapatnekar, S.S. (ed.) Proceedings of the 47th Design Automation Conference, DAC 2010, Anaheim, California, USA, 13\u201318 July 2010, pp. 755\u2013760. ACM (2010). https:\/\/doi.org\/10.1145\/1837274.1837466","DOI":"10.1145\/1837274.1837466"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-24372-1_35","volume-title":"Automated Technology for Verification and Analysis","author":"S-W Lin","year":"2011","unstructured":"Lin, S.-W., Andr\u00e9, \u00c9., Dong, J.S., Sun, J., Liu, Y.: An efficient algorithm for learning event-recording automata. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 463\u2013472. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_35"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36675-8_2","volume-title":"Automated Reasoning and Mathematics","author":"L de Moura","year":"2013","unstructured":"de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 15\u201344. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36675-8_2"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-030-88885-5_5","volume-title":"Automated Technology for Verification and Analysis","author":"E Mu\u0161kardin","year":"2021","unstructured":"Mu\u0161kardin, E., Aichernig, B.K., Pill, I., Pferscher, A., Tappler, M.: AALpy: an active automata learning library. In: Hou, Z., Ganesh, V. (eds.) ATVA 2021. LNCS, vol. 12971, pp. 67\u201373. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_5"},{"key":"26_CR19","doi-asserted-by":"publisher","unstructured":"Pastore, F., Micucci, D., Mariani, L.: Timed k-tail: automatic inference of timed automata. In: 2017 IEEE International Conference on Software Testing, Verification and Validation, ICST 2017, Tokyo, Japan, 13\u201317 March 2017, pp. 401\u2013411. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ICST.2017.43","DOI":"10.1109\/ICST.2017.43"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-67549-7_8","volume-title":"Testing Software and Systems","author":"A Petrenko","year":"2017","unstructured":"Petrenko, A., Avellaneda, F., Groz, R., Oriat, C.: From passive to active FSM inference via checking sequence construction. In: Yevtushenko, N., Cavalli, A.R., Yenig\u00fcn, H. (eds.) ICTSS 2017. LNCS, vol. 10533, pp. 126\u2013141. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67549-7_8"},{"key":"26_CR21","unstructured":"De Ruiter, J., Poll, E.: Protocol state fuzzing of TLS implementations. In: Jung, J., Holz, T. (eds.) 24th USENIX Security Symposium, USENIX Security 15, Washington, D.C., USA, 12\u201314 August 2015. pp. 193\u2013206. USENIX Association (2015). https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/de-ruiter"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Learning continuous time Markov chains from sample executions. In: First International Conference on the Quantitative Evaluation of Systems, 2004. QEST 2004. Proceedings, pp. 146\u2013155. IEEE (2004)","DOI":"10.1109\/QEST.2004.1348029"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-319-77313-1_14","volume-title":"Language and Automata Theory and Applications","author":"R Smetsers","year":"2018","unstructured":"Smetsers, R., Fiter\u0103u-Bro\u015ftean, P., Vaandrager, F.: Model learning as a satisfiability modulo theories problem. In: Klein, S.T., Mart\u00edn-Vide, C., Shapira, D. (eds.) LATA 2018. LNCS, vol. 10792, pp. 182\u2013194. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77313-1_14"},{"key":"26_CR24","doi-asserted-by":"publisher","unstructured":"Springintveld, J., Vaandrager, F.W., D\u2019Argenio, P.R.: Testing timed automata. Theor. Comput. Sci. 254(1-2), 225\u2013257 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(99)00134-6","DOI":"10.1016\/S0304-3975(99)00134-6"},{"key":"26_CR25","doi-asserted-by":"publisher","unstructured":"Tappler, M., Aichernig, B.K., Bloem, R.: Model-based testing IoT communication via active automata learning. In: 2017 IEEE International Conference on Software Testing, Verification and Validation, ICST 2017, Tokyo, Japan, 13\u201317 March 2017, pp. 276\u2013287. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ICST.2017.32","DOI":"10.1109\/ICST.2017.32"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-29662-9_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Tappler","year":"2019","unstructured":"Tappler, M., Aichernig, B.K., Larsen, K.G., Lorber, F.: Time to learn\u2013learning timed automata from tests. In: Andr\u00e9, \u00c9., Stoelinga, M. (eds.) FORMATS 2019. LNCS, vol. 11750, pp. 216\u2013235. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29662-9_13"},{"key":"26_CR27","doi-asserted-by":"publisher","unstructured":"Turner, C.J., Tiwari, A., Olaiya, R., Xu, Y.: Process mining: from theory to practice. Bus. Process. Manag. J. 18(3), 493\u2013512 (2012). https:\/\/doi.org\/10.1108\/14637151211232669","DOI":"10.1108\/14637151211232669"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-030-68195-1_13","volume-title":"Language and Automata Theory and Applications","author":"F Vaandrager","year":"2021","unstructured":"Vaandrager, F., Bloem, R., Ebrahimi, M.: Learning Mealy machines with one timer. In: Leporati, A., Mart\u00edn-Vide, C., Shapira, D., Zandron, C. (eds.) LATA 2021. LNCS, vol. 12638, pp. 157\u2013170. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-68195-1_13"},{"key":"26_CR29","unstructured":"Verwer, S., De Weerdt, M., Witteveen, C.: An algorithm for learning real-time automata. In: Benelearn 2007: Proceedings of the Annual Machine Learning Conference of Belgium and the Netherlands, Amsterdam, The Netherlands, 14\u201315 May 2007"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-06773-0_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T11:12:57Z","timestamp":1659352377000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-06773-0_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031067723","9783031067730"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-06773-0_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"20 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2022\/","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":"118","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":"33","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":"6","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":"28% - 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.3","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}