{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T14:41:58Z","timestamp":1781620918228,"version":"3.54.5"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,5,18]],"date-time":"2016-05-18T00:00:00Z","timestamp":1463529600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mach Learn"],"published-print":{"date-parts":[[2016,11]]},"DOI":"10.1007\/s10994-016-5565-9","type":"journal-article","created":{"date-parts":[[2016,5,18]],"date-time":"2016-05-18T18:57:55Z","timestamp":1463597875000},"page":"255-299","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":57,"title":["Learning deterministic probabilistic automata from a model checking perspective"],"prefix":"10.1007","volume":"105","author":[{"given":"Hua","family":"Mao","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yingke","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Manfred","family":"Jaeger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas D.","family":"Nielsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brian","family":"Nielsen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,5,18]]},"reference":[{"key":"5565_CR1","doi-asserted-by":"crossref","unstructured":"Aarts, F., & Vaandrager, F. W. (2010). Learning I\/O automata. In Proceedings of the international conference on concurrency theory (CONCUR 2010), pp. 71\u201385.","DOI":"10.1007\/978-3-642-15375-4_6"},{"key":"5565_CR2","doi-asserted-by":"crossref","unstructured":"Ammons, G., Bod\u00edk, R., & Larus, J. R. (2002). Mining specifications. In Proceedings of the SIGPLAN-SIGACT symposium on principles of programming language (POPL 2002), pp. 4\u201316.","DOI":"10.1145\/503272.503275"},{"key":"5565_CR3","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D. (1987). Learning regular sets from queries and counterexamples. Journal of Information and Computation, 75, 87\u2013106.","journal-title":"Journal of Information and Computation"},{"key":"5565_CR4","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C., & Katoen, J. P. (2008). Principles of model checking. Cambridge, MA: The MIT Press."},{"issue":"6","key":"5565_CR5","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., & Katoen, J. P. (2003). Model-checking algorithms for continuous-time Markov chains. Journal of IEEE Transaction on Software Engineering, 29(6), 524\u2013541.","journal-title":"Journal of IEEE Transaction on Software Engineering"},{"issue":"2","key":"5565_CR6","first-page":"133","volume":"41","author":"G Behrmann","year":"2011","unstructured":"Behrmann, G., David, A., Larsen, K. G., Pettersson, P., & Yi, W. (2011). Developing uppaal over 15 years. Journal of Software: Practice and Experience, 41(2), 133\u2013142.","journal-title":"Journal of Software: Practice and Experience"},{"issue":"3","key":"5565_CR7","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1109\/TSE.2009.89","volume":"36","author":"B Bollig","year":"2010","unstructured":"Bollig, B., Katoen, J. P., Kern, C., & Leucker, M. (2010). Learning communicating automata from MSCs. IEEE Transactions on Software Engineering, 36(3), 390\u2013408.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5565_CR8","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Larsen, K. G., & Markey, N. (2008). Model checking one-clock priced timed automata. Journal of Logical Methods in Computer Science, 4(2), 1\u201328.","DOI":"10.2168\/LMCS-4(2:9)2008"},{"issue":"9","key":"5565_CR9","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1145\/1995376.1995396","volume":"54","author":"P Bouyer","year":"2011","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K. G., & Markey, N. (2011). Quantitative analysis of real-time systems using priced timed automata. Communications of the ACM, 54(9), 78\u201387.","journal-title":"Communications of the ACM"},{"key":"5565_CR10","doi-asserted-by":"crossref","unstructured":"Carrasco, R., & Oncina, J. (1994). Learning stochastic regular grammars by means of a state merging method. In Proceedings of the international colloquium on grammatical inference and applications (ICGIA 1994), pp. 139\u2013152.","DOI":"10.1007\/3-540-58473-0_144"},{"issue":"1","key":"5565_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1051\/ita:1999102","volume":"33","author":"RC Carrasco","year":"1999","unstructured":"Carrasco, R. C., & Oncina, J. (1999). Learning deterministic regular grammars from stochastic samples in polynomial time. Journal of Theoretial Informatics and Applications, 33(1), 1\u201320.","journal-title":"Journal of Theoretial Informatics and Applications"},{"key":"5565_CR12","doi-asserted-by":"crossref","unstructured":"Castro, J., & Gavald\u00e0, R. (2008). Towards feasible PAC-learning of probabilistic deterministic finite automata. In Grammatical inference: Algorithms and applications, pp. 163\u2013174.","DOI":"10.1007\/978-3-540-88009-7_13"},{"key":"5565_CR13","doi-asserted-by":"crossref","unstructured":"Chen, T., Han, T., Katoen, J. P., & Mereacre, A. (2009). Quantitative model checking of continuous-time Markov chains against timed automata specifications. In 24th annual IEEE symposium on logic in computer science pp. 309\u2013318.","DOI":"10.1109\/LICS.2009.21"},{"key":"5565_CR14","doi-asserted-by":"crossref","unstructured":"Chen, Y., & Nielsen, T. D. (2012). Active learning of Markov decision processes for system verification. In Proceedings of the international conference on machine learning and applications (ICMLA 2012), pp. 289\u2013294.","DOI":"10.1109\/ICMLA.2012.158"},{"key":"5565_CR15","doi-asserted-by":"crossref","unstructured":"Chen, Y., Mao, H., Jaeger, M., Nielsen, T. D., Larsen, K.G., & Nielsen, B. (2012). Learning Markov models for stationary system behaviors. In NASA formal methods symposium (NFM), pp. 216\u2013230.","DOI":"10.1007\/978-3-642-28891-3_22"},{"key":"5565_CR16","first-page":"473","volume":"5","author":"A Clark","year":"2004","unstructured":"Clark, A., & Thollard, F. (2004). PAC-learnability of probabilistic deterministic finite state automata. Journal of Machine Learning Research, 5, 473\u2013497.","journal-title":"Journal of Machine Learning Research"},{"key":"5565_CR17","doi-asserted-by":"crossref","unstructured":"Cobleigh, J. M., Giannakopoulou, D., & Pasareanu, C. S. (2003). Learning assumptions for compositional verification. In Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS), pp. 331\u2013346.","DOI":"10.1007\/3-540-36577-X_24"},{"issue":"4","key":"5565_CR18","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., & Yannakakis, M. (1995). The complexity of probabilistic verification. Journal of the ACM, 42(4), 857\u2013907.","journal-title":"Journal of the ACM"},{"issue":"3\/4","key":"5565_CR19","doi-asserted-by":"crossref","first-page":"354","DOI":"10.2307\/2333353","volume":"40","author":"DR Cox","year":"1953","unstructured":"Cox, D. R. (1953). Some simple approximate tests for Poisson variates. Biometrika, 40(3\/4), 354\u2013360.","journal-title":"Biometrika"},{"key":"5565_CR20","unstructured":"de\u00a0Higuera, C., & Oncina, J. (2004). Learning stochastic finite automata. In Proceedings of the international conference on grammatical inference, pp. 175\u2013186."},{"key":"5565_CR21","doi-asserted-by":"crossref","unstructured":"de\u00a0la Higuera, C., & Thollard, F. (2000). Identification in the limit with probability one of stochastic deterministic finite automata. In Proceedings of the international colloquium on grammatical inference: Algorithms and application (ICGI 2000), pp. 141\u2013156.","DOI":"10.1007\/978-3-540-45257-7_12"},{"key":"5565_CR22","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., & Panangaden, P. (1999). Metrics for labeled Markov systems. In Proceedings of international conference on concurrency theory (CONCUR), pp. 258\u2013273.","DOI":"10.1007\/3-540-48320-9_19"},{"key":"5565_CR23","doi-asserted-by":"crossref","unstructured":"Feng, L., Han, T., Kwiatkowska, M. Z., & Parker, D. (2011). Learning-based compositional verification for synchronous probabilistic systems. In 9th international symposium on automated technology for verification and analysis (ATVA), pp. 511\u2013521.","DOI":"10.1007\/978-3-642-24372-1_40"},{"issue":"1","key":"5565_CR24","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1093\/biomet\/56.1.127","volume":"56","author":"EA Gehan","year":"1969","unstructured":"Gehan, E. A., & Thomas, D. G. (1969). The performance of some two-sample tests in small samples with and without censoring. Biometrika, 56(1), 127\u2013132.","journal-title":"Biometrika"},{"key":"5565_CR25","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., & P\u0103s\u0103reanu, C. S. (2005). Learning-based assume-guarantee verification (Tool Paper). In P. Godefroid (Ed.), Model Checking Software: 12th International SPIN Workshop (pp. 282\u2013287). Berlin, Heidelberg: Springer.","DOI":"10.1007\/11537328_24"},{"issue":"3","key":"5565_CR26","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/j.entcs.2005.02.062","volume":"138","author":"O Grinchtein","year":"2005","unstructured":"Grinchtein, O., Jonsson, B., & Leucker, M. (2005). Inference of timed transition systems. Journal of Electronic Notes in Theoretical Compututer Science, 138(3), 87\u201399.","journal-title":"Journal of Electronic Notes in Theoretical Compututer Science"},{"key":"5565_CR27","doi-asserted-by":"crossref","unstructured":"Grinchtein, O., Jonsson, B., & Pettersson, P. (2006). Inference of event-recording automata using timed decision trees. In Proceedings of the international conference on concurrency theory (CONCUR), pp. 435\u2013449.","DOI":"10.1007\/11817949_29"},{"key":"5565_CR28","doi-asserted-by":"crossref","unstructured":"Haverkort, B. R., Hermanns, H., & Katoen, J. P. (2000). On the use of model checking techniques for dependability evaluation. In Proceedings of the IEEE symposium on reliable distributed systems (SRDS 2000), pp. 228\u2013237.","DOI":"10.1109\/RELDI.2000.885410"},{"key":"5565_CR29","doi-asserted-by":"crossref","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., & Peyronnet, S. (2004). Approximate probabilistic model checking. In Steffen, B., Levi, G. (Eds.), Verification, model checking, and abstract interpretation. Lecture Notes in Computer Science, Vol. 2937, Springer, Berlin, pp. 307\u2013329.","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"5565_CR30","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139194655","volume-title":"Grammatical inference: Learning automata and grammars","author":"Cd Higuera","year":"2010","unstructured":"Higuera, Cd. (2010). Grammatical inference: Learning automata and grammars. Cambridge: Cambridge University Press."},{"key":"5565_CR31","doi-asserted-by":"crossref","unstructured":"Jaeger, M., Mao, H., Larsen, K. G., & Mardare, R. (2014). Continuity properties of distances for Markov processes. In Proceedings of QEST 2014, LNCS, Vol. 8657, pp. 297\u2013312.","DOI":"10.1007\/978-3-319-10696-0_24"},{"key":"5565_CR32","unstructured":"Jansen, D. N. (2002). Probabilistic UML statecharts for specification and verification a case study. In Proceedings of the workshop on critical systems development with UML, pp. 121\u2013132."},{"key":"5565_CR33","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Pasareanu, C. S., & Clarke, E. M. (2012). Learning probabilistic systems from tree samples. In Proceedings of the 27th annual IEEE\/ACM symposium on logic in computer science, pp. 441\u2013450.","DOI":"10.1109\/LICS.2012.54"},{"key":"5565_CR34","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., & Parker, D. (2011). Prism 4.0: Verification of probabilistic real-time systems. In Proceedings of the international conference on computer aided verification (CAV\u201911), pp. 585\u2013591.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"5565_CR35","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Larsen, K. G., & Weise, C. (1995). From timed automata to logic- and back. In Proceedings of international symposim on mathematical foundations of computer science (MFCS 1995), pp. 529\u2013539.","DOI":"10.7146\/brics.v2i2.19504"},{"key":"5565_CR36","doi-asserted-by":"crossref","unstructured":"Legay, A., Delahaye, B., & Bensalem, S. (2010). Statistical model checking: An overview. In Proceedings of the first international conference on runtime verification, Springer, Berlin, RV\u201910, pp. 122\u2013135.","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"5565_CR37","doi-asserted-by":"crossref","unstructured":"Leucker, M. (2007). Learning meets verification. In Proceedings of the international conference on formal methods for components and objects (FMCO 2007), pp. 127\u2013151.","DOI":"10.1007\/978-3-540-74792-5_6"},{"key":"5565_CR38","unstructured":"Mao, H., & Jaeger, M. (2012). Learning and model checking networks of I\/O automata. In Proceedings of the fourth Asian conference on machine learning (ACML), pp. 285\u2013300."},{"key":"5565_CR39","doi-asserted-by":"crossref","unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T. D., Larsen, K. G., & Nielsen, B. (2011). Learning probabilistic automata for model checking. In Proceedings of the international conference on quantitative evaluation of system (QEST 2011), pp. 111\u2013120.","DOI":"10.1109\/QEST.2011.21"},{"key":"5565_CR40","doi-asserted-by":"crossref","unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T. D., Larsen, K. G., & Nielsen, B. (2012). Learning Markov decision processes for model checking. In Proceedings of the first workshop on quantities in formal methods (QFM), pp. 49\u201363.","DOI":"10.4204\/EPTCS.103.6"},{"key":"5565_CR41","unstructured":"Niese, O. (2003). An integrated approach to testing complex systems. PhD thesis, Universit\u00e4t Dortmund."},{"issue":"5","key":"5565_CR42","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1109\/34.211465","volume":"15","author":"J Oncina","year":"1993","unstructured":"Oncina, J., Garcia, P., & Vidal, E. (1993). Learning subsequential transducers for pattern recognition interpretation tasks. IEEE Transactions on Pattern Analysis Machine Intelligence, 15(5), 448\u2013458.","journal-title":"IEEE Transactions on Pattern Analysis Machine Intelligence"},{"key":"5565_CR43","doi-asserted-by":"crossref","unstructured":"Pnueli, A. (1977). The temporal logic of programs. In Proceedings of the annual symposium on foundations of computer science (FOCS) pp. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"5565_CR44","doi-asserted-by":"publisher","unstructured":"Rabin, M. O. (1963). Probabilistic automata. Information and Control, 6(3), 230\u2013245. doi: 10.1016\/S0019-9958(63)90290-0 . http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0019995863902900","DOI":"10.1016\/S0019-9958(63)90290-0"},{"key":"5565_CR45","doi-asserted-by":"crossref","unstructured":"Raffelt, H., & Steffen, B. (2006). Learnlib: A library for automata learning and experimentation. In Proceedings of the international conference on fundamental approaches to software engineering (FASE), pp. 377\u2013380.","DOI":"10.1007\/11693017_28"},{"issue":"2\u20133","key":"5565_CR46","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1023\/A:1026490906255","volume":"25","author":"D Ron","year":"1996","unstructured":"Ron, D., Singer, Y., & Tishby, N. (1996). The power of amnesia: Learning probabilistic automata with variable memory length. Machine Learning, 25(2\u20133), 117\u2013149.","journal-title":"Machine Learning"},{"issue":"2","key":"5565_CR47","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1006\/jcss.1997.1555","volume":"56","author":"D Ron","year":"1998","unstructured":"Ron, D., Singer, Y., & Tishby, N. (1998). On the learnability and usage of acyclic probabilistic finite automata. Journal of Computer and System Sciences, 56(2), 133\u2013152.","journal-title":"Journal of Computer and System Sciences"},{"key":"5565_CR48","unstructured":"Segala, R. (1996). Modeling and verification of randomized distributed real-time systems. Technical report. Cambridge, MA."},{"key":"5565_CR49","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., & Agha, G. (2004a). Learning continuous time Markov chains from sample executions. In Proceedings of international conference on quantitative evaluation of systems (QEST), pp. 146\u2013155.","DOI":"10.1109\/QEST.2004.1348029"},{"key":"5565_CR50","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., & Agha, G. (2004b). Statistical model checking of black-box probabilistic systems. In Alur, R., Peled, D. (Eds.), Computer aided verification. Lecture Notes in Computer Science, Vol. 3114, pp. 202\u2013215.","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"5565_CR51","unstructured":"Singh, R., Giannakopoulou, D., & Pasareanu, C. S. (2010). Learningcomponent interfaces with may and must abstractions. In Computer aided verification. Lecture Notes in Computer Science, Vol. 3576, pp. 527\u2013542."},{"key":"5565_CR52","unstructured":"Thollard, F., Dupont, P., & de\u00a0la Higuera, C. (2000). Probabilistic DFA inference using kullback-leibler divergence and minimality. In Proceedings of the international conference on machine learning (ICML), pp. 975\u2013982."},{"key":"5565_CR53","first-page":"151","volume":"8","author":"WG Tzeng","year":"1992","unstructured":"Tzeng, W. G. (1992). Learning probabilistic automata and markov chains via queries. Machine Learning, 8, 151\u2013166.","journal-title":"Machine Learning"},{"key":"5565_CR54","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.tcs.2004.09.035","volume":"331","author":"F Breugel van","year":"2005","unstructured":"van Breugel, F., & Worrell, J. (2005). A behavioural pseudometric for probabilistic transition system. Theoretical Computer Science, 331, 115\u2013142.","journal-title":"Theoretical Computer Science"},{"key":"5565_CR55","doi-asserted-by":"crossref","unstructured":"Vardi, M. Y. (1985). Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of the IEEE symposium on foundations of computer science (FOCS), pp. 327\u2013338.","DOI":"10.1109\/SFCS.1985.12"},{"key":"5565_CR56","doi-asserted-by":"crossref","unstructured":"Vardi, M. Y. (1999). Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In Proceedings of the international AMAST workshop on formal methods for real-time and probabilstic systems (ARTS 1999), pp. 265\u2013276.","DOI":"10.1007\/3-540-48778-6_16"},{"key":"5565_CR57","unstructured":"Verwer, S. (2010). Efficient identification of timed automata\u2014Theory and practice. PhD thesis, Technical University Delft."}],"container-title":["Machine Learning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10994-016-5565-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10994-016-5565-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10994-016-5565-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10994-016-5565-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T01:40:41Z","timestamp":1559353241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10994-016-5565-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5,18]]},"references-count":57,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,11]]}},"alternative-id":["5565"],"URL":"https:\/\/doi.org\/10.1007\/s10994-016-5565-9","relation":{},"ISSN":["0885-6125","1573-0565"],"issn-type":[{"value":"0885-6125","type":"print"},{"value":"1573-0565","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5,18]]}}}