{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:37:55Z","timestamp":1768005475396,"version":"3.49.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,3,23]],"date-time":"2024-03-23T00:00:00Z","timestamp":1711152000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,3,23]],"date-time":"2024-03-23T00:00:00Z","timestamp":1711152000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100018461","name":"Silicon Austria Labs","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100018461","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2024,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Black-box systems are inherently hard to verify. Many verification techniques, like model checking, require formal models as a basis. However, such models often do not exist, or they might be outdated. Active automata learning helps to address this issue by offering to automatically infer formal models from system interactions. Hence, automata learning has been receiving much attention in the verification community in recent years. This led to various efficiency improvements, paving the way toward industrial applications. Most research, however, has been focusing on deterministic systems. In this article, we present an approach to efficiently learn models of stochastic reactive systems. Our approach adapts <jats:inline-formula><jats:alternatives><jats:tex-math>$$L^*$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msup>\n                    <mml:mi>L<\/mml:mi>\n                    <mml:mo>\u2217<\/mml:mo>\n                  <\/mml:msup>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-based learning for Markov decision processes, which we improve and extend to stochastic Mealy machines. When compared with previous work, our evaluation demonstrates that the proposed optimizations and adaptations to stochastic Mealy machines can reduce learning costs by an order of magnitude while improving the accuracy of learned models.<\/jats:p>","DOI":"10.1007\/s10270-024-01158-0","type":"journal-article","created":{"date-parts":[[2024,3,23]],"date-time":"2024-03-23T08:02:11Z","timestamp":1711180931000},"page":"503-524","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Active model learning of stochastic reactive systems (extended version)"],"prefix":"10.1007","volume":"23","author":[{"given":"Edi","family":"Mu\u0161kardin","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4193-5609","authenticated-orcid":false,"given":"Martin","family":"Tappler","sequence":"additional","affiliation":[]},{"given":"Bernhard K.","family":"Aichernig","sequence":"additional","affiliation":[]},{"given":"Ingo","family":"Pill","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,3,23]]},"reference":[{"issue":"2","key":"1158_CR1","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."},{"issue":"2","key":"1158_CR2","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"RL Rivest","year":"1993","unstructured":"Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Inf. Comput. 103(2), 299\u2013347 (1993)","journal-title":"Inf. Comput."},{"key":"1158_CR3","doi-asserted-by":"crossref","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), Proceedings of the 5th International Conference on Runtime Verification, RV 2014. Lecture Notes in Computer Science, Toronto, ON, Canada, September 22-25, (2014), vol. 8734, pp. 307\u2013322 (2014)","DOI":"10.1007\/978-3-319-11164-3_26"},{"key":"1158_CR4","doi-asserted-by":"crossref","unstructured":"Hungar, H., Niese, O., Steffen, B.: Domain-specific optimization in automata learning. In: Proceedings of the 15th International Conference on Computer Aided Verification, CAV 2003. LNCS, Boulder, CO, USA, July 8-12, 2003, vol. 2725, pp. 315\u2013327 (2003)","DOI":"10.1007\/978-3-540-45069-6_31"},{"key":"1158_CR5","unstructured":"Margaria, T., Niese, O., Raffelt, H., Steffen, B.: Efficient test-based model generation for legacy reactive systems. In: 9th IEEE International High-Level Design Validation and Test Workshop 2004, Sonoma Valley, CA, USA, November 10-12, 2004, pp. 95\u2013100 (2004)"},{"key":"1158_CR6","doi-asserted-by":"crossref","unstructured":"Shahbaz, M., Groz, R.: Inferring Mealy machines. In: Proceedings of the 2nd World Congress on FM 2009: Formal Methods. LNCS, Eindhoven, The Netherlands, November 2-6, 2009, vol. 5850, pp. 207\u2013222 (2009)","DOI":"10.1007\/978-3-642-05089-3_14"},{"key":"1158_CR7","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Pferscher, A., Tappler, M.: From passive to active: Learning timed automata efficiently. In: Proceedings of the 12th International Symposium on NASA Formal Methods, NFM 2020. LNCS, Moffett Field, CA, USA, May 11-15, 2020, vol. 12229, pp. 1\u201319 (2020)","DOI":"10.1007\/978-3-030-55754-6_1"},{"key":"1158_CR8","doi-asserted-by":"crossref","unstructured":"Tappler, M., Aichernig, B.K., Lorber, F.: Timed automata learning via SMT solving. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds), Proceedings of the 14th International Symposium on NASA Formal Methods, NFM 2022. Lecture Notes in Computer Science, Pasadena, CA, USA, May 24-27, 2022, vol. 13260, pp. 489\u2013507 (2022)","DOI":"10.1007\/978-3-031-06773-0_26"},{"key":"1158_CR9","doi-asserted-by":"crossref","unstructured":"Aarts, F., Heidarian, F., Kuppens, H., Olsen, P., Vaandrager, F.W.: Automata learning through counterexample guided abstraction refinement. In: Giannakopoulou, D., M\u00e9ry, D. (eds), Proceedings of the 18th International Symposium on FM 2012: Formal Methods. Lecture Notes in Computer Science, Paris, France, August 27-31, 2012, vol. 7436, pp. 10\u201327 (2012)","DOI":"10.1007\/978-3-642-32759-9_4"},{"key":"1158_CR10","doi-asserted-by":"crossref","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, March 13-17, 2017, pp. 276\u2013287 (2017)","DOI":"10.1109\/ICST.2017.32"},{"key":"1158_CR11","doi-asserted-by":"crossref","unstructured":"Tappler, M., Aichernig, B.K., Bacci, G., Eichlseder, M., Larsen, K.G.: $${L}^*$$-based learning of Markov decision processes. In: Formal Methods\u2014The Next 30 Years\u2014Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, volume 11800 of LNCS, pp. 651\u2013669 (2019)","DOI":"10.1007\/978-3-030-30942-8_38"},{"issue":"4\u20135","key":"1158_CR12","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/s00165-021-00536-5","volume":"33","author":"M Tappler","year":"2021","unstructured":"Tappler, M., Aichernig, B.K., Bacci, G., Eichlseder, M., Larsen, K.G.: L*-based learning of Markov decision processes (extended version). Form. Asp. Comput. 33(4\u20135), 575\u2013615 (2021)","journal-title":"Form. Asp. Comput."},{"key":"1158_CR13","doi-asserted-by":"crossref","unstructured":"Mu\u0161kardin, E., Aichernig, B., Pill, I., Pferscher, A., Tappler, M.: AALpy: an active automata learning library. Innov. Syst. Softw. Eng., pp. 1\u201310, 03 (2022). The implementation of AALpy is available online at https:\/\/github.com\/DES-Lab\/AALpy","DOI":"10.1007\/s11334-022-00449-3"},{"key":"1158_CR14","doi-asserted-by":"crossref","unstructured":"Tappler, M., Muskardin, E., Aichernig, B.K., Pill, I.: Active model learning of stochastic reactive systems. In: Calinescu, R., Pasareanu, C.S. (eds), Proceedings of the 19th International Conference on Software Engineering and Formal Methods, SEFM 2021. Lecture Notes in Computer Science, Virtual Event, December 6-10, 2021, vol. 13085, pp. 481\u2013500 (2021)","DOI":"10.1007\/978-3-030-92124-8_27"},{"issue":"2","key":"1158_CR15","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s10994-016-5565-9","volume":"105","author":"H Mao","year":"2016","unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning deterministic probabilistic automata from a model checking perspective. Mach. Learn. 105(2), 255\u2013299 (2016)","journal-title":"Mach. Learn."},{"key":"1158_CR16","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Proceedings of the 23rd International Conference on Computer Aided Verification, CAV 2011. LNCS, Snowbird, UT, USA, July 14-20, 2011, vol. 6806, pp. 585\u2013591 (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"1158_CR17","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017): Part II.LNCS, Heidelberg, Germany, July 24-28, 2017, vol. 10427, pp. 592\u2013600 (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"1158_CR18","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139194655","volume-title":"Grammatical Inference: Learning Automata and Grammars","author":"C de la Higuera","year":"2010","unstructured":"de la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. Cambridge University Press, New York (2010)"},{"key":"1158_CR19","doi-asserted-by":"crossref","unstructured":"Carrasco, R.C., Oncina, J.: Learning stochastic regular grammars by means of a state merging method. In: Carrasco, R.C., Oncina, J. (eds), Proceedings of the 2nd International Colloquium on Grammatical Inference and Applications (ICGI-94). Lecture Notes in Computer Science, Alicante, Spain, September 21-23, 1994, vol. 862, pp. 139\u2013152 (1994)","DOI":"10.1007\/3-540-58473-0_144"},{"key":"1158_CR20","unstructured":"El-Fakih, K., Groz, R., Irfan, M., Shahbaz, M.: Learning finite state models of observable nondeterministic systems in a testing context. 01 (2010)"},{"issue":"47","key":"1158_CR21","doi-asserted-by":"publisher","first-page":"4029","DOI":"10.1016\/j.tcs.2010.07.008","volume":"411","author":"O Grinchtein","year":"2010","unstructured":"Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theor. Comput. Sci. 411(47), 4029\u20134054 (2010)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"1158_CR22","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1090\/S0002-9939-1958-0135681-9","volume":"9","author":"A Nerode","year":"1958","unstructured":"Nerode, A.: Linear automaton transformations. Proc. Am. Math. Soc. 9(4), 541\u2013544 (1958)","journal-title":"Proc. Am. Math. Soc."},{"issue":"301","key":"1158_CR23","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"issue":"302","key":"1158_CR24","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1080\/14786440009463897","volume":"50","author":"FRS Karl Pearson","year":"1900","unstructured":"Karl Pearson, F.R.S.: X on the criterion that a given system of deviations from the probable in the case of a correlated system of variables is such that it can be reasonably supposed to have arisen from random sampling. Lond. Edinb. Dublin Philos. Mag. J. Sci. 50(302), 157\u2013175 (1900)","journal-title":"Lond. Edinb. Dublin Philos. Mag. J. Sci."},{"issue":"2","key":"1158_CR25","doi-asserted-by":"publisher","first-page":"217","DOI":"10.2307\/2983604","volume":"1","author":"F Yates","year":"1934","unstructured":"Yates, F.: Contingency tables involving small numbers and the $$\\chi -$$2 test. Suppl. J. R. Stat. Soc. 1(2), 217\u2013235 (1934)","journal-title":"Suppl. J. R. Stat. Soc."},{"key":"1158_CR26","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Tappler, M., Wallner, F.: Benchmarking combinations of learning and testing algorithms for active automata learning. In: Proceedings of the 14th International Conference on Tests and Proofs, TAP@STAF 2020. LNCS, Bergen, Norway, June 22-23, 2020, vol. 12165, pp. 3\u201322 (2020)","DOI":"10.1007\/978-3-030-50995-8_1"},{"key":"1158_CR27","doi-asserted-by":"crossref","unstructured":"Howar, F., Steffen, B.: Active automata learning as black-box search and lazy partition refinement. In: Jansen, N., Stoelinga, M., van\u00a0den Bos, P. (eds), A Journey from Process Algebra via Timed Automata to Model Learning\u2014Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13560 , pp. 321\u2013338. Springer (2022)","DOI":"10.1007\/978-3-031-15629-8_17"},{"key":"1158_CR28","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Tappler, M.: Probabilistic black-box reachability checking (extended version). Formal Methods in System Design (2019)","DOI":"10.1007\/s10703-019-00333-0"},{"key":"1158_CR29","doi-asserted-by":"crossref","unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning Markov decision processes for model checking. In: Proceedings Quantities in Formal Methods, QFM 2012. EPTCS, Paris, France, 28 August 2012, vol. 103 , pp. 49\u201363 (2012)","DOI":"10.4204\/EPTCS.103.6"},{"key":"1158_CR30","doi-asserted-by":"crossref","unstructured":"Fiterau-Brostean, P., Janssen, R., Vaandrager, F.W.: Combining model learning and model checking to analyze TCP implementations. In: Proceedings of the 28th International Conference on Computer Aided Verification (CAV 2016): Part II. LNCS, Toronto, ON, Canada, July 17-23, 2016, vol 9780, pp. 454\u2013471 (2016)","DOI":"10.1007\/978-3-319-41540-6_25"},{"key":"1158_CR31","doi-asserted-by":"crossref","unstructured":"Pferscher, A., Aichernig, B.K.: Fingerprinting Bluetooth low energy devices via active automata learning. In: Huisman, M., Pasareanu, C.S., Zhan, N. (eds), Proceedings of the 24th International Symposium on Formal Methods, FM 2021, Virtual Event. Lecture Notes in Computer Science, November 20-26, 2021, vol. 13047, pp. 524\u2013542 (2021)","DOI":"10.1007\/978-3-030-90870-6_28"},{"key":"1158_CR32","unstructured":"Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: Margaria, T., Steffen, B. (eds), Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA 2016): Part I. Lecture Notes in Computer Science, Imperial, Corfu, Greece, October 10-14, 2016, vol. 9952, pp. 3\u201315 (2016)"},{"issue":"1","key":"1158_CR33","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BF02883985","volume":"10","author":"M Okamoto","year":"1959","unstructured":"Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10(1), 29\u201335 (1959)","journal-title":"Ann. Inst. Stat. Math."},{"key":"1158_CR34","doi-asserted-by":"crossref","unstructured":"STUDENT: The probable error of a mean. Biometrika 6(1), 1\u201325 (1908)","DOI":"10.1093\/biomet\/6.1.1"},{"issue":"1","key":"1158_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1051\/ita:1999102","volume":"33","author":"RC Carrasco","year":"1999","unstructured":"Carrasco, R.C., Oncina, J.: Learning deterministic regular grammars from stochastic samples in polynomial time. RAIRO Theor. Inform. Appl. (RAIRO: ITA) 33(1), 1\u201320 (1999)","journal-title":"RAIRO Theor. Inform. Appl. (RAIRO: ITA)"},{"key":"1158_CR36","doi-asserted-by":"crossref","unstructured":"Chen, Y., Nielsen, T.D.: Active learning of Markov decision processes for system verification. In: 11th International Conference on Machine Learning and Applications, ICMLA, Boca Raton, FL, USA, December 12-15, 2012. Vol. 2, pp. 289\u2013294 (2012)","DOI":"10.1109\/ICMLA.2012.158"},{"issue":"2","key":"1158_CR37","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1162\/089120104323093294","volume":"30","author":"F Casacuberta","year":"2004","unstructured":"Casacuberta, F., Vidal, E.: Machine translation with inferred stochastic finite-state transducers. Comput. Linguist. 30(2), 205\u2013225 (2004)","journal-title":"Comput. Linguist."},{"key":"1158_CR38","unstructured":"El-Fakih, K., Groz, R., Irfan, M.N., Shahbaz, M.: Learning finite state models of observable nondeterministic systems in a testing context. In: ICTSS 2010, pp. 97\u2013102 (2010)"},{"key":"1158_CR39","doi-asserted-by":"crossref","unstructured":"Pferscher, A., Aichernig, B.K.: Learning abstracted non-deterministic finite state machines. In: Casola, V., De Benedictis, A., Rak, M. (eds), Proceedings of the 32nd IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2020, Naples, Italy, December 9-11, 2020, volume 12543 of LNCS, pp. 52\u201369 (2020)","DOI":"10.1007\/978-3-030-64881-7_4"},{"key":"1158_CR40","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.72.1008","author":"M Volpato","year":"2015","unstructured":"Volpato, M., Tretmans, J.: Approximate active learning of nondeterministic input output transition systems. ECEASST (2015). https:\/\/doi.org\/10.14279\/tuj.eceasst.72.1008","journal-title":"ECEASST"},{"key":"1158_CR41","doi-asserted-by":"crossref","unstructured":"Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Reynouard, R.: Active learning of Markov Decision Processes using Baum\u2013Welch algorithm. In: Arif Wani, M., Sethi, I.K., Shi, W., Qu, G., Raicu, D.S., Jin, R., (eds), 20th IEEE International Conference on Machine Learning and Applications, ICMLA 2021, Pasadena, CA, USA, December 13-16, 2021, pp. 1203\u20131208 (2021)","DOI":"10.1109\/ICMLA52953.2021.00195"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01158-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-024-01158-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01158-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T12:06:32Z","timestamp":1715601992000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-024-01158-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,23]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["1158"],"URL":"https:\/\/doi.org\/10.1007\/s10270-024-01158-0","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3,23]]},"assertion":[{"value":"2 July 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 January 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2024","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}