{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T05:12:06Z","timestamp":1790831526953,"version":"4.1.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319773124","type":"print"},{"value":"9783319773131","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-77313-1_14","type":"book-chapter","created":{"date-parts":[[2018,3,6]],"date-time":"2018-03-06T21:20:49Z","timestamp":1520371249000},"page":"182-194","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Model Learning as a Satisfiability Modulo Theories Problem"],"prefix":"10.1007","author":[{"given":"Rick","family":"Smetsers","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Fiter\u0103u-Bro\u015ftean","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,3,8]]},"reference":[{"issue":"1","key":"14_CR1","first-page":"1","volume":"46","author":"F Aarts","year":"2015","unstructured":"Aarts, F., et al.: Generating models of infinite-state communication protocols using regular inference with abstraction. FMSD 46(1), 1\u201341 (2015)","journal-title":"FMSD"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-319-25150-9_11","volume-title":"Theoretical Aspects of Computing - ICTAC 2015","author":"F Aarts","year":"2015","unstructured":"Aarts, F., Fiterau-Brostean, P., Kuppens, H., Vaandrager, F.: Learning register automata with fresh value generation. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 165\u2013183. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-25150-9_11\n\n. \nhttp:\/\/www.sws.cs.ru.nl\/publications\/papers\/fvaan\/TomteFresh\/"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Aarts, F., de Ruiter, J., Poll, E.: Formal models of bank cards for free. In: ICST Workshops, pp. 461\u2013468. IEEE (2013)","DOI":"10.1109\/ICSTW.2013.60"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1007\/978-3-642-16558-0_54","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"F Aarts","year":"2010","unstructured":"Aarts, F., Schmaltz, J., Vaandrager, F.: Inference and abstraction of the biometric passport. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6415, pp. 673\u2013686. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-16558-0_54"},{"issue":"2","key":"14_CR5","first-page":"87","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. I&C 75(2), 87\u2013106 (1987)","journal-title":"I&C"},{"key":"14_CR6","first-page":"121","volume":"5","author":"D Angluin","year":"1990","unstructured":"Angluin, D.: Negative results for equivalence queries. Mach. Learn. 5, 121\u2013150 (1990)","journal-title":"Mach. Learn."},{"issue":"6","key":"14_CR7","first-page":"783","volume":"15","author":"M Bruynooghe","year":"2015","unstructured":"Bruynooghe, M., et al.: Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems with IDP3. TPLP 15(6), 783\u2013817 (2015)","journal-title":"TPLP"},{"issue":"2","key":"14_CR8","first-page":"233","volume":"28","author":"S Cassel","year":"2016","unstructured":"Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Active learning for extended finite state machines. FAOC 28(2), 233\u2013263 (2016)","journal-title":"FAOC"},{"issue":"9","key":"14_CR9","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L Moura De","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. CACM 54(9), 69\u201377 (2011)","journal-title":"CACM"},{"key":"14_CR10","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1016\/j.tcs.2014.09.023","volume":"558","author":"CC Flor\u00eancio","year":"2014","unstructured":"Flor\u00eancio, C.C., Verwer, S.: Regular inference as vertex coloring. TCS 558, 18\u201334 (2014)","journal-title":"TCS"},{"issue":"5","key":"14_CR11","first-page":"447","volume":"10","author":"E Gold","year":"1967","unstructured":"Gold, E.: Language identification in the limit. I&C 10(5), 447\u2013474 (1967)","journal-title":"I&C"},{"issue":"4","key":"14_CR12","doi-asserted-by":"crossref","first-page":"825","DOI":"10.1007\/s10664-012-9222-z","volume":"18","author":"M Heule","year":"2013","unstructured":"Heule, M., Verwer, S.: Software model synthesis using satisfiability solvers. Empir. Softw. Eng. 18(4), 825\u2013856 (2013)","journal-title":"Empir. Softw. Eng."},{"key":"14_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139194655","volume-title":"Grammatical Inference: Learning Automata and Grammars","author":"C Higuera De la","year":"2010","unstructured":"De la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. Cambridge University Press, Cambridge (2010)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-642-27940-9_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Howar","year":"2012","unstructured":"Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 251\u2013266. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-27940-9_17"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-11164-3_26","volume-title":"Runtime Verification","author":"M Isberner","year":"2014","unstructured":"Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: a redundancy-free approach to active automata learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 307\u2013322. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-11164-3_26"},{"issue":"3","key":"14_CR16","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1109\/12.272431","volume":"43","author":"D Lee","year":"1994","unstructured":"Lee, D., Yannakakis, M.: Testing finite-state machines: state identification and verification. IEEE Trans. Comput. 43(3), 306\u2013320 (1994)","journal-title":"IEEE Trans. Comput."},{"issue":"8","key":"14_CR17","doi-asserted-by":"crossref","first-page":"1090","DOI":"10.1109\/5.533956","volume":"84","author":"D Lee","year":"1996","unstructured":"Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines\u2014a survey. Proc. IEEE 84(8), 1090\u20131123 (1996)","journal-title":"Proc. IEEE"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-33386-6_28","volume-title":"Automated Technology for Verification and Analysis","author":"D Neider","year":"2012","unstructured":"Neider, D.: Computing minimal separating DFAs and regular invariants using SAT and SMT solvers. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 354\u2013369. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-33386-6_28"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Peled, D., Vardi, M., Yannakakis, M.: Black box checking. In: FORTE, pp. 225\u2013240. Kluwer (1999)","DOI":"10.1007\/978-0-387-35578-8_13"},{"key":"14_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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-67549-7_8"},{"issue":"5","key":"14_CR21","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1007\/s10009-009-0111-8","volume":"11","author":"H Raffelt","year":"2009","unstructured":"Raffelt, H., Steffen, B., Berg, T., Margaria, T.: LearnLib: a framework for extrapolating behavioral models. STTT 11(5), 393\u2013407 (2009)","journal-title":"STTT"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-319-33693-0_20","volume-title":"Integrated Formal Methods","author":"M Schuts","year":"2016","unstructured":"Schuts, M., Hooman, J., Vaandrager, F.: Refactoring of legacy software using model learning and equivalence checking: an industrial experience report. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 311\u2013325. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33693-0_20"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-319-25423-4_5","volume-title":"Formal Methods and Software Engineering","author":"W Smeenk","year":"2015","unstructured":"Smeenk, W., Moerman, J., Vaandrager, F., Jansen, D.N.: Applying automata learning to embedded control software. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 67\u201383. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-25423-4_5"},{"key":"14_CR24","unstructured":"Smetsers, R.: Grammatical Inference as a Satisfiability Modulo Theories Problem. arXiv preprint \narXiv:1705.10639\n\n (2017)"},{"issue":"2","key":"14_CR25","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1145\/2967606","volume":"60","author":"F Vaandrager","year":"2017","unstructured":"Vaandrager, F.: Model learning. CACM 60(2), 86\u201395 (2017)","journal-title":"CACM"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-642-05089-3_20","volume-title":"FM 2009: Formal Methods","author":"N Walkinshaw","year":"2009","unstructured":"Walkinshaw, N., Derrick, J., Guo, Q.: Iterative refinement of reverse-engineered models by model-based testing. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 305\u2013320. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-05089-3_20"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77313-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,3,6]],"date-time":"2018-03-06T21:27:13Z","timestamp":1520371633000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77313-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319773124","9783319773131"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77313-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}