{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:45Z","timestamp":1740098925916,"version":"3.37.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319675305"},{"type":"electronic","value":"9783319675312"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67531-2_4","type":"book-chapter","created":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T05:33:37Z","timestamp":1504589617000},"page":"50-67","source":"Crossref","is-referenced-by-count":6,"title":["Probabilistic Black-Box Reachability Checking"],"prefix":"10.1007","author":[{"given":"Bernhard K.","family":"Aichernig","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Tappler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,6]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-57288-8_2","volume-title":"NASA Formal Methods","author":"BK Aichernig","year":"2017","unstructured":"Aichernig, B.K., Tappler, M.: Learning from faults: mutation testing in active automata learning. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 19\u201334. Springer, Cham (2017). doi:\n10.1007\/978-3-319-57288-8_2"},{"issue":"2","key":"4_CR2","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). doi:\n10.1016\/0890-5401(87)90052-6","journal-title":"Inf. Comput."},{"key":"4_CR3","unstructured":"Banks, A., Gupta, R. (eds.): MQTT Version 3.1.1. OASIS Standard, October 2014. \nhttp:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v3.1.1\/os\/mqtt-v3.1.1-os.html\n\n, latest version. \nhttp:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v3.1.1\/os\/mqtt-v3.1.1-os.html"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kret\u00ednsk\u00fd, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: Cassez and Raskin [6], pp. 98\u2013114. \nhttp:\/\/dx.doi.org\/10.1007\/978-3-319-11936-6_8","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/3-540-58473-0_144","volume-title":"Grammatical Inference and Applications","author":"RC Carrasco","year":"1994","unstructured":"Carrasco, R.C., Oncina, J.: Learning stochastic regular grammars by means of a state merging method. In: Carrasco, R.C., Oncina, J. (eds.) ICGI 1994. LNCS, vol. 862, pp. 139\u2013152. Springer, Heidelberg (1994). doi:\n10.1007\/3-540-58473-0_144"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Technology for Verification and Analysis","year":"2014","unstructured":"Cassez, F., Raskin, J.-F. (eds.): ATVA 2014. LNCS, vol. 8837. Springer, Cham (2014)"},{"key":"4_CR7","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\u201315, 2012, vol. 2, pp. 289\u2013294. IEEE (2012). \nhttp:\/\/dx.doi.org\/10.1109\/ICMLA.2012.158","DOI":"10.1109\/ICMLA.2012.158"},{"issue":"4","key":"4_CR8","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s10009-015-0383-0","volume":"17","author":"P D\u2019Argenio","year":"2015","unstructured":"D\u2019Argenio, P., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of Markov decision processes. STTT 17(4), 469\u2013484 (2015). doi:\n10.1007\/s10009-015-0383-0","journal-title":"STTT"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., S\u00f8rensen, M.G., Taankvist, J.H.: On time with minimal expected cost!. In: Cassez and Raskin [6], pp. 129\u2013145. \nhttp:\/\/dx.doi.org\/10.1007\/978-3-319-11936-6_10","DOI":"10.1007\/978-3-319-11936-6_10"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-662-46681-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2015","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.:  Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206\u2013211. Springer, Heidelberg (2015). doi:\n10.1007\/978-3-662-46681-0_16"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/11888116_30","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"E Elkind","year":"2006","unstructured":"Elkind, E., Genest, B., Peled, D., Qu, H.: Grey-box checking. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 420\u2013435. Springer, Heidelberg (2006). doi:\n10.1007\/11888116_30"},{"key":"4_CR12","unstructured":"EMQ. \nhttp:\/\/emqtt.io\/\n\n. Accessed 07 May 2017"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-319-41540-6_25","volume-title":"Computer Aided Verification","author":"P Fiter\u0103u-Bro\u015ftean","year":"2016","unstructured":"Fiter\u0103u-Bro\u015ftean, P., Janssen, R., Vaandrager, F.: Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 454\u2013471. Springer, Cham (2016). doi:\n10.1007\/978-3-319-41540-6_25"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53\u2013113. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-21455-4_3"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-46002-0_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Groce","year":"2002","unstructured":"Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 357\u2013370. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-46002-0_25"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22110-1_47"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-319-02444-8_2","volume-title":"Automated Technology for Verification and Analysis","author":"M Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5\u201322. Springer, Cham (2013). doi:\n10.1007\/978-3-319-02444-8_2"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-47166-2_1","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"KG Larsen","year":"2016","unstructured":"Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 3\u201315. Springer, Cham (2016). doi:\n10.1007\/978-3-319-47166-2_1"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-16612-9_11"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-319-15201-1_23","volume-title":"Software Engineering and Formal Methods","author":"A Legay","year":"2015","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Scalable verification of Markov decision processes. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 350\u2013362. Springer, Cham (2015). doi:\n10.1007\/978-3-319-15201-1_23"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning probabilistic automata for model checking. In: Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5\u20138, pp. 111\u2013120. IEEE Computer Society (2011). \nhttp:\/\/dx.doi.org\/10.1109\/QEST.2011.21","DOI":"10.1109\/QEST.2011.21"},{"key":"4_CR22","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: Fahrenberg, U., Legay, A., Thrane, C.R. (eds.) Proceedings Quantities in Formal Methods, QFM 2012, Paris, France, 28. EPTCS, vol. 103, pp. 49\u201363 (2012). \nhttp:\/\/dx.doi.org\/10.4204\/EPTCS.103.6","DOI":"10.4204\/EPTCS.103.6"},{"issue":"2","key":"4_CR23","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). doi:\n10.1007\/s10994-016-5565-9","journal-title":"Mach. Learn."},{"key":"4_CR24","unstructured":"Nachmanson, L., Veanes, M., Schulte, W., Tillmann, N., Grieskamp, W.: Optimal strategies for testing nondeterministic systems. In: Avrunin, G.S., Rothermel, G. (eds.) Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July 11\u201314, 2004, pp. 55\u201364. ACM (2004). \nhttp:\/\/doi.acm.org\/10.1145\/1007512.1007520"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-319-11164-3_28","volume-title":"Runtime Verification","author":"A Nouri","year":"2014","unstructured":"Nouri, A., Raman, B., Bozga, M., Legay, A., Bensalem, S.: Faster statistical model checking by means of abstraction and learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 340\u2013355. Springer, Cham (2014). doi:\n10.1007\/978-3-319-11164-3_28"},{"issue":"1","key":"4_CR26","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). doi:\n10.1007\/BF02883985","journal-title":"Ann. Inst. Stat. Math."},{"key":"4_CR27","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-0-387-35578-8_13","volume-title":"Formal Methods for Protocol Engineering and Distributed Systems","author":"D Peled","year":"1999","unstructured":"Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems. IAICT, vol. 28, pp. 225\u2013240. Springer, Boston, MA (1999). doi:\n10.1007\/978-0-387-35578-8_13"},{"key":"4_CR28","unstructured":"prob-black-reach - Java implementation of probabilistic black-box reachability checking. \nhttps:\/\/github.com\/mtappler\/prob-black-reach\n\n. Accessed 07 May 2017"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202\u2013215. Springer, Heidelberg (2004). doi:\n10.1007\/978-3-540-27813-9_16"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Shu, G., Lee, D.: Testing security properties of protocol implementations - a machine learning based approach. In: 27th IEEE International Conference on Distributed Computing Systems (ICDCS 2007), June 25\u201329, 2007, Toronto, Ontario, Canada, p. 25. IEEE Computer Society (2007). \nhttp:\/\/dx.doi.org\/10.1109\/ICDCS.2007.147","DOI":"10.1109\/ICDCS.2007.147"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Tappler, M., Aichernig, B.K., Bloem, R.: Model-based testing IoT communication via active automata learning. In: ICST 2017, pp. 276\u2013287. IEEE Computer Society (2017)","DOI":"10.1109\/ICST.2017.32"},{"key":"4_CR32","unstructured":"TCP models. \nhttps:\/\/gitlab.science.ru.nl\/pfiteraubrostean\/tcp-learner\/tree\/cav-aec\/models\n\n. Accessed 07 May 2017"},{"issue":"5","key":"4_CR33","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1002\/stvr.456","volume":"22","author":"M Utting","year":"2012","unstructured":"Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test., Verif. Reliab. 22(5), 297\u2013312 (2012). doi:\n10.1002\/stvr.456","journal-title":"Softw. Test., Verif. Reliab."},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-15488-1_17","volume-title":"Grammatical Inference: Theoretical Results and Applications","author":"S Verwer","year":"2010","unstructured":"Verwer, S., Weerdt, M., Witteveen, C.: A likelihood-ratio test for identifying probabilistic deterministic real-time automata from positive data. In: Sempere, J.M., Garc\u00eda, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 203\u2013216. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-15488-1_17"},{"key":"4_CR35","unstructured":"Wang, J., Sun, J., Qin, S.: Verifying complex systems probabilistically through learning, abstraction and refinement. CoRR abs\/1610.06371 (2016). \nhttp:\/\/arxiv.org\/abs\/1610.06371"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/11513988_25","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2005","unstructured":"Younes, H.L.S.: Probabilistic verification for \u201cBlack-Box\u201d systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 253\u2013265. Springer, Heidelberg (2005). doi:\n10.1007\/11513988_25"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67531-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T05:34:34Z","timestamp":1504589674000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67531-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319675305","9783319675312"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67531-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}