{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:24:48Z","timestamp":1779074688684,"version":"3.51.4"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T00:00:00Z","timestamp":1558396800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T00:00:00Z","timestamp":1558396800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100008332","name":"Technische Universit\u00e4t Graz","doi-asserted-by":"publisher","award":["LEAD Project 1"],"award-info":[{"award-number":["LEAD Project 1"]}],"id":[{"id":"10.13039\/100008332","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2019,11]]},"DOI":"10.1007\/s10703-019-00333-0","type":"journal-article","created":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T05:04:54Z","timestamp":1558501494000},"page":"416-448","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Probabilistic black-box reachability checking (extended version)"],"prefix":"10.1007","volume":"54","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":[[2019,5,21]]},"reference":[{"key":"333_CR1","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-319-96562-8_3","volume-title":"Lecture Notes in Computer Science","author":"Bernhard K. Aichernig","year":"2018","unstructured":"Aichernig BK, Mostowski W, Mousavi MR, Tappler M, Taromirad M (2018) Model learning and model-based testing. In: Bennaceur A, H\u00e4hnle R, Meinke K (eds) Machine learning for dynamic software analysis: potentials and limits\u2013international Dagstuhl seminar 16172, Dagstuhl Castle, Germany, April 24\u201327, 2016. Revised papers, Lecture notes in computer science, vol 11026, pp 74\u2013100. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-319-96562-8_3"},{"key":"333_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-57288-8_2","volume-title":"Lecture Notes in Computer Science","author":"Bernhard K. Aichernig","year":"2017","unstructured":"Aichernig BK, Tappler M (2017) Learning from faults: mutation testing in active automata learning. In: Barrett C, Davies M, Kahsai T (eds) NASA formal methods\u20139th international symposium, NFM 2017, Moffett Field, CA, USA, May 16\u201318, 2017. Proceedings, Lecture notes in computer science, vol 10227, pp 19\u201334. \nhttps:\/\/doi.org\/10.1007\/978-3-319-57288-8_2"},{"key":"333_CR3","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-67531-2_4","volume-title":"Runtime Verification","author":"Bernhard K. Aichernig","year":"2017","unstructured":"Aichernig BK, Tappler M (2017) Probabilistic black-box reachability checking. In: Lahiri SK, Reger G (eds) Runtime verification\u201317th international conference, RV 2017, Seattle, WA, USA, September 13\u201316, 2017. Proceedings, Lecture notes in computer science, vol 10548, pp 50\u201367. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-319-67531-2_4"},{"issue":"2","key":"333_CR4","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 (1987) Learning regular sets from queries and counterexamples. Inf. Comput. 75(2):87\u2013106. \nhttps:\/\/doi.org\/10.1016\/0890-5401(87)90052-6","journal-title":"Inf. Comput."},{"key":"333_CR5","doi-asserted-by":"publisher","unstructured":"Argyros G, Stais I, Jana S, Keromytis AD, Kiayias A (2016) SFADiff: automated evasion attacks and fingerprinting using black-box differential automata learning. In: Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, pp 1690\u20131701. ACM. \nhttps:\/\/doi.org\/10.1145\/2976749.2978383","DOI":"10.1145\/2976749.2978383"},{"issue":"3","key":"333_CR6","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"11","author":"J Aspnes","year":"1990","unstructured":"Aspnes J, Herlihy M (1990) Fast randomized consensus using shared memory. J Algorithms 11(3):441\u2013461. \nhttps:\/\/doi.org\/10.1016\/0196-6774(90)90021-6","journal-title":"J Algorithms"},{"key":"333_CR7","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"333_CR8","unstructured":"Banks A. Gupta, R (ed.) (2014) MQTT version 3.1.1. OASIS standard. \nhttp:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v3.1.1\/os\/mqtt-v3.1.1-os.html\n\n. \nhttp:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v3.1.1\/os\/mqtt-v3.1.1-os.html"},{"issue":"3","key":"333_CR9","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1145\/337244.337257","volume":"47","author":"A Beimel","year":"2000","unstructured":"Beimel A, Bergadano F, Bshouty NH, Kushilevitz E, Varricchio S (2000) Learning functions represented as multiplicity automata. J ACM 47(3):506\u2013530. \nhttps:\/\/doi.org\/10.1145\/337244.337257","journal-title":"J ACM"},{"key":"333_CR10","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"Tom\u00e1\u0161 Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil T, Chatterjee K, Chmelik M, Forejt V, Kret\u00ednsk\u00fd J, Kwiatkowska MZ, Parker D, Ujma M Verification of Markov decision processes using learning algorithms. In: Cassez and Raskin [12], pp 98\u2013114. \nhttps:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"333_CR11","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/3-540-58473-0_144","volume-title":"Grammatical Inference and Applications","author":"Rafael C. Carrasco","year":"1994","unstructured":"Carrasco RC, Oncina J(1994) Learning stochastic regular grammars by means of a state merging method. In: Carrasco RC, Oncina J (eds) Grammatical inference and applications, second international colloquium, ICGI-94, Alicante, Spain, September 21\u201323, 1994. Proceedings, Lecture notes in computer science, vol 862, pp 139\u2013152. Springer. \nhttps:\/\/doi.org\/10.1007\/3-540-58473-0_144"},{"key":"333_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6","volume-title":"Automated Technology for Verification and Analysis","year":"2014","unstructured":"Cassez F, Raskin J (eds) (2014) Automated technology for verification and analysis\u201312th international symposium, ATVA 2014, Sydney, NSW, Australia, November 3\u20137, 2014. Proceedings, Lecture notes in computer science, vol 8837. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-319-11936-6"},{"key":"333_CR13","doi-asserted-by":"publisher","unstructured":"Chen Y, Nielsen TD (2012) 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. \nhttps:\/\/doi.org\/10.1109\/ICMLA.2012.158","DOI":"10.1109\/ICMLA.2012.158"},{"issue":"4","key":"333_CR14","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 (2015) Smart sampling for lightweight verification of Markov decision processes. STTT 17(4):469\u2013484. \nhttps:\/\/doi.org\/10.1007\/s10009-015-0383-0","journal-title":"STTT"},{"key":"333_CR15","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-11936-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"Alexandre David","year":"2014","unstructured":"David A, Jensen PG, Larsen KG, Legay A, Lime D, S\u00f8rensen MG, Taankvist JH. On time with minimal expected cost! In: Cassez and Raskin [12], pp 129\u2013145. \nhttps:\/\/doi.org\/10.1007\/978-3-319-11936-6_10"},{"key":"333_CR16","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":"Alexandre David","year":"2015","unstructured":"David A, Jensen PG, Larsen KG, Mikucionis M, Taankvist JH (2015) Uppaal stratego. In: Baier C, Tinelli C (eds) Tools and algorithms for the construction and analysis of systems\u201321st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, April 11\u201318, 2015. Proceedings, Lecture notes in computer science, vol 9035, pp 206\u2013211. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-662-46681-0_16"},{"key":"333_CR17","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/11888116_30","volume-title":"Lecture Notes in Computer Science","author":"Edith Elkind","year":"2006","unstructured":"Elkind E, Genest B, Peled DA, Qu H (2006) Grey-box checking. In: Najm E, Pradat-Peyre J, Donzeau-Gouge V (eds) Formal techniques for networked and distributed systems\u2013FORTE 2006, 26th IFIP WG 6.1 international conference, Paris, France, September 26\u201329, 2006. Lecture notes in computer science, vol 4229, pp 420\u2013435. Springer. \nhttps:\/\/doi.org\/10.1007\/11888116_30"},{"key":"333_CR18","unstructured":"EMQ. \nhttp:\/\/emqtt.io\/\n\n. Accessed 3 Dec 2018"},{"key":"333_CR19","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-24372-1_40","volume-title":"Automated Technology for Verification and Analysis","author":"Lu Feng","year":"2011","unstructured":"Feng L, Han T, Kwiatkowska MZ, Parker D (2011) Learning-based compositional verification for synchronous probabilistic systems. In: Bultan T, Hsiung P (eds) Automated technology for verification and analysis, 9th international symposium, ATVA 2011, Taipei, Taiwan, October 11\u201314, 2011. Proceedings, Lecture notes in computer science, vol 6996, pp 511\u2013521. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-642-24372-1_40"},{"key":"333_CR20","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-319-41540-6_25","volume-title":"Computer Aided Verification","author":"Paul Fiter\u0103u-Bro\u015ftean","year":"2016","unstructured":"Fiterau-Brostean P, Janssen R, Vaandrager FW (2016) Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri S, Farzan A (eds) Computer aided verification\u201328th international conference, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016. Proceedings, Part II, Lecture notes in computer science, vol 9780, pp 454\u2013471. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-319-41540-6_25"},{"key":"333_CR21","doi-asserted-by":"publisher","unstructured":"Fiterau-Brostean P, Lenaerts T, Poll E, de\u00a0Ruiter J, Vaandrager FW, Verleg P (2017) Model learning and model checking of SSH implementations. In: Erdogmus H, Havelund K (eds) Proceedings of the 24th ACM SIGSOFT international SPIN symposium on model checking of software, Santa Barbara, CA, July 10\u201314, 2017, pp 142\u2013151. ACM. \nhttps:\/\/doi.org\/10.1145\/3092282.3092289\n\n. \nhttp:\/\/doi.acm.org\/10.1145\/3092282.3092289","DOI":"10.1145\/3092282.3092289"},{"key":"333_CR22","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":"Vojt\u011bch Forejt","year":"2011","unstructured":"Forejt V, Kwiatkowska MZ, Norman G, Parker D (2011) Automated verification techniques for probabilistic systems. In: Bernardo M, Issarny V (eds) Formal methods for eternal networked software systems\u201311th international school on formal methods for the design of computer, communication and software systems, SFM 2011, Bertinoro, Italy, June 13\u201318, 2011. Advanced lectures, Lecture notes in computer science, vol 6659, pp 53\u2013113. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-642-21455-4_3"},{"key":"333_CR23","doi-asserted-by":"crossref","unstructured":"Fu J, Topcu U (2014) Probably approximately correct MDP learning and control with temporal logic constraints. In: Fox D, Kavraki LE, Kurniawati H (eds) Robotics: science and systems X, University of California, Berkeley, July 12\u201316, 2014. \nhttp:\/\/www.roboticsproceedings.org\/rss10\/p39.html","DOI":"10.15607\/RSS.2014.X.039"},{"key":"333_CR24","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-48989-6_18","volume-title":"FM 2016: Formal Methods","author":"Georgios Giantamidis","year":"2016","unstructured":"Giantamidis G, Tripakis S (2016) Learning Moore machines from input-output traces. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds) FM 2016: formal methods\u201321st international symposium, Limassol, Cyprus, November 9\u201311, 2016. Proceedings, Lecture notes in computer science, vol 9995, pp 291\u2013309. \nhttps:\/\/doi.org\/10.1007\/978-3-319-48989-6_18"},{"key":"333_CR25","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-540-30206-3_26","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"Olga Grinchtein","year":"2004","unstructured":"Grinchtein O, Jonsson B, Leucker M (2004) Learning of event-recording automata. In: Lakhnech Y, Yovine S (eds) Formal techniques, modelling and analysis of timed and fault-tolerant systems, joint international conferences on formal modelling and analysis of timed systems, FORMATS 2004 and formal techniques in real-time and fault-tolerant systems, FTRTFT 2004, Grenoble, France, September 22\u201324, 2004. Proceedings, Lecture notes in computer science, vol 3253, pp 379\u2013396. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-540-30206-3_26"},{"key":"333_CR26","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":"Alex Groce","year":"2002","unstructured":"Groce A, Peled DA, Yannakakis M (2002) Adaptive model checking. In: Katoen J, Stevens P (eds) Tools and algorithms for the construction and analysis of systems. In: 8th international conference, TACAS 2002, held as part of the joint European conference on theory and practice of software, ETAPS 2002, Grenoble, France, April 8\u201312, 2002. Proceedings, Lecture notes in computer science"},{"key":"333_CR27","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 (2010) Grammatical inference: learning automata and grammars. Cambridge University Press, New York, NY"},{"key":"333_CR28","unstructured":"Khalili A, Tacchella A (2014) Learning nondeterministic Mealy machines. In: Clark A, Kanazawa M, Yoshinaka R (eds) Proceedings of the 12th international conference on grammatical inference, ICGI 2014, Kyoto, Japan, September 17\u201319, 2014. JMLR workshop and conference proceedings, vol 34, pp 109\u2013123. \nhttp:\/\/jmlr.org\/proceedings\/papers\/v34\/khalili14a.html"},{"key":"333_CR29","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"Marta Kwiatkowska","year":"2011","unstructured":"Kwiatkowska MZ, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification\u201323rd international conference, CAV 2011, Snowbird, UT, July 14\u201320, 2011. Proceedings, Lecture notes in computer science, vol 6806, pp 585\u2013591. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"333_CR30","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":"Marta Kwiatkowska","year":"2013","unstructured":"Kwiatkowska MZ, Parker D (2013) Automated verification and strategy synthesis for probabilistic systems. In: Hung DV, Ogawa M (eds) Automated technology for verification and analysis\u201311th international symposium, ATVA 2013, Hanoi, Vietnam, October 15\u201318, 2013. Proceedings, Lecture notes in computer science, vol 8172, pp 5\u201322. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-319-02444-8_2"},{"key":"333_CR31","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":"Kim G. Larsen","year":"2016","unstructured":"Larsen KG, Legay A (2016) Statistical model checking: past, present, and future. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation: foundational techniques\u20137th international symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10\u201314, 2016. Proceedings, Part I, Lecture notes in computer science, vol 9952, pp 3\u201315. \nhttps:\/\/doi.org\/10.1007\/978-3-319-47166-2_1"},{"key":"333_CR32","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"Axel Legay","year":"2010","unstructured":"Legay A, Delahaye B, Bensalem S (2010) Statistical model checking: an overview. In: Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace GJ, Rosu G, Sokolsky O, Tillmann N (eds) Runtime verification\u2013first international conference, RV 2010, St. Julians, Malta, November 1\u20134, 2010. Proceedings, Lecture notes in computer science, vol 6418, pp 122\u2013135. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-642-16612-9_11"},{"key":"333_CR33","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-319-15201-1_23","volume-title":"Software Engineering and Formal Methods","author":"Axel Legay","year":"2015","unstructured":"Legay A, Sedwards S, Traonouez L (2014) Scalable verification of Markov decision processes. In: Canal C, Idani A (eds) Software engineering and formal methods\u2013SEFM 2014 collocated workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September 1\u20132, 2014. Revised selected papers, Lecture notes in computer science, vol 8938, pp 350\u2013362. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-319-15201-1_23"},{"key":"333_CR34","doi-asserted-by":"publisher","unstructured":"Mao H, Chen Y, Jaeger M, Nielsen TD, Larsen KG, Nielsen B (2011) Learning probabilistic automata for model checking. In: Eighth international conference on quantitative evaluation of systems, QEST 2011, Aachen, 5\u20138 September, 2011, pp 111\u2013120. IEEE Computer Society. \nhttps:\/\/doi.org\/10.1109\/QEST.2011.21","DOI":"10.1109\/QEST.2011.21"},{"key":"333_CR35","doi-asserted-by":"publisher","first-page":"49","DOI":"10.4204\/EPTCS.103.6","volume":"103","author":"Hua Mao","year":"2012","unstructured":"Mao H, Chen Y, Jaeger M, Nielsen TD, Larsen KG, Nielsen B (2012) Learning Markov decision processes for model checking. In: Fahrenberg U, Legay A, Thrane CR (eds) Proceedings quantities in formal methods, QFM 2012, Paris, France, 28 August 2012. EPTCS, vol 103, pp 49\u201363. \nhttps:\/\/doi.org\/10.4204\/EPTCS.103.6","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"2","key":"333_CR36","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 TD, Larsen KG, Nielsen B (2016) Learning deterministic probabilistic automata from a model checking perspective. Mach Learn 105(2):255\u2013299. \nhttps:\/\/doi.org\/10.1007\/s10994-016-5565-9","journal-title":"Mach Learn"},{"key":"333_CR37","doi-asserted-by":"publisher","unstructured":"Margaria T, Niese O, Raffelt H, Steffen B (2004) Efficient test-based model generation for legacy reactive systems. In: Ninth IEEE international high-level design validation and test workshop 2004, Sonoma Valley, CA, USA, November 10\u201312, 2004, pp. 95\u2013100. IEEE Computer Society. \nhttps:\/\/doi.org\/10.1109\/HLDVT.2004.1431246","DOI":"10.1109\/HLDVT.2004.1431246"},{"key":"333_CR38","doi-asserted-by":"publisher","unstructured":"Nachmanson L, Veanes M, Schulte W, Tillmann N, Grieskamp W (2004) Optimal strategies for testing nondeterministic systems. In: Avrunin GS, Rothermel G (eds) Proceedings of the ACM\/SIGSOFT international symposium on software testing and analysis, ISSTA 2004, Boston, MA, USA, July 11\u201314, 2004, pp 55\u201364. ACM. \nhttps:\/\/doi.org\/10.1145\/1007512.1007520","DOI":"10.1145\/1007512.1007520"},{"key":"333_CR39","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-319-11164-3_28","volume-title":"Runtime Verification","author":"Ayoub Nouri","year":"2014","unstructured":"Nouri A, Raman B, Bozga M, Legay A, Bensalem S (2014) Faster statistical model checking by means of abstraction and learning. In: Bonakdarpour B, Smolka SA (eds) Runtime verification\u20135th international conference, RV 2014, Toronto, ON, Canada, September 22\u201325, 2014. Proceedings, Lecture notes in computer science, vol 8734, pp 340\u2013355. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-319-11164-3_28"},{"issue":"1","key":"333_CR40","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BF02883985","volume":"10","author":"M Okamoto","year":"1959","unstructured":"Okamoto M (1959) Some inequalities relating to the partial sum of binomial probabilities. Ann Inst Stat Math 10(1):29\u201335. \nhttps:\/\/doi.org\/10.1007\/BF02883985","journal-title":"Ann Inst Stat Math"},{"key":"333_CR41","doi-asserted-by":"crossref","unstructured":"Oncina J, Garcia P (1992) Identifying regular languages in polynomial time. In: Advances in structural and syntactic pattern recognition. Volume 5 of series in Machine perception and artificial intelligence, pp 99\u2013108. World Scientific","DOI":"10.1142\/9789812797919_0007"},{"key":"333_CR42","doi-asserted-by":"crossref","unstructured":"Peled DA, Vardi MY, Yannakakis M (1999) Black box checking. In: Wu J, Chanson ST, Gao Q (eds) Formal methods for protocol engineering and distributed systems, FORTE XII\/PSTV XIX\u201999, IFIP TC6 WG6.1 joint international conference on formal description techniques for distributed systems and communication protocols (FORTE XII) and protocol specification, testing and verification (PSTV XIX), October 5\u20138, 1999, Beijing, China. IFIP conference proceedings, vol 156, pp 225\u2013240. Kluwer","DOI":"10.1007\/978-0-387-35578-8_13"},{"key":"333_CR43","unstructured":"prob-black-reach\u2014Java implementation of probabilistic black-box reachability checking. \nhttps:\/\/github.com\/mtappler\/prob-black-reach\n\n. Accessed 3 Dec 2018"},{"key":"333_CR44","unstructured":"de Ruiter J, Poll E (2015) Protocol state fuzzing of TLS implementations. In: Jung J, Holz T(eds) 24th USENIX security symposium, USENIX Security 15, Washington, D.C., USA, August 12\u201314, 2015, pp 193\u2013206. USENIX Association. \nhttps:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/de-ruiter"},{"key":"333_CR45","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"Koushik Sen","year":"2004","unstructured":"Sen K, Viswanathan M, Agha G (2004) Statistical model checking of black-box probabilistic systems. In: Alur R, Peled DA (eds) Computer aided verification, 16th international conference, CAV 2004, Boston, MA, USA, July 13\u201317, 2004. Proceedings, Lecture notes in computer science, vol 3114, pp 202\u2013215. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-540-27813-9_16"},{"key":"333_CR46","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-05089-3_14","volume-title":"FM 2009: Formal Methods","author":"Muzammil Shahbaz","year":"2009","unstructured":"Shahbaz M, Groz R (2009) Inferring Mealy machines. In: Cavalcanti A, Dams D (eds) FM 2009: formal methods, second world congress, Eindhoven, The Netherlands, November 2\u20136, 2009. Proceedings, Lecture notes in computer science, vol 5850, pp 207\u2013222. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-642-05089-3_14"},{"key":"333_CR47","doi-asserted-by":"publisher","unstructured":"Shu G, Lee D (2007) Testing security properties of protocol implementations\u2013a 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. \nhttps:\/\/doi.org\/10.1109\/ICDCS.2007.147","DOI":"10.1109\/ICDCS.2007.147"},{"key":"333_CR48","doi-asserted-by":"publisher","unstructured":"Sivakorn S, Argyros G, Pei K, Keromytis AD, Jana S (2017) HVLearn: automated black-box analysis of hostname verification in SSL\/TLS implementations. In: SP 2017, pp 521\u2013538. IEEE Computer Society. \nhttps:\/\/doi.org\/10.1109\/SP.2017.46","DOI":"10.1109\/SP.2017.46"},{"key":"333_CR49","doi-asserted-by":"publisher","unstructured":"Tappler M, Aichernig BK, Bloem R (2017) 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\u201317, 2017, pp 276\u2013287. IEEE Computer Society. \nhttps:\/\/doi.org\/10.1109\/ICST.2017.32","DOI":"10.1109\/ICST.2017.32"},{"key":"333_CR50","unstructured":"TCP models. \nhttps:\/\/gitlab.science.ru.nl\/pfiteraubrostean\/tcp-learner\/tree\/cav-aec\/models\n\n. Accessed 3 Dec 2018"},{"issue":"5","key":"333_CR51","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 (2012) A taxonomy of model-based testing approaches. Softw Test Verif Reliab 22(5):297\u2013312. \nhttps:\/\/doi.org\/10.1002\/stvr.456","journal-title":"Softw Test Verif Reliab"},{"key":"333_CR52","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":"Sicco Verwer","year":"2010","unstructured":"Verwer S, de Weerdt M, Witteveen C (2010) A likelihood-ratio test for identifying probabilistic deterministic real-time automata from positive data. In: Sempere JM, Garc\u00eda P (eds) Grammatical inference: theoretical results and applications, 10th international colloquium, ICGI 2010, Valencia, Spain, September 13\u201316, 2010. Proceedings, Lecture notes in computer science, vol 6339, pp 203\u2013216. Springer. \nhttps:\/\/doi.org\/10.1007\/978-3-642-15488-1_17"},{"key":"333_CR53","unstructured":"Volpato M, Tretmans J (2015) Approximate active learning of nondeterministic input output transition systems. In: ECEASST, vol 72. \nhttp:\/\/journal.ub.tu-berlin.de\/eceasst\/article\/view\/1008"},{"key":"333_CR54","unstructured":"Wang J, Sun J, Qin S Verifying complex systems probabilistically through learning, abstraction and refinement. In: CoRR. \narXiv:1610.06371\n\n (2016)"},{"key":"333_CR55","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/11513988_25","volume-title":"Computer Aided Verification","author":"H\u00e5kan L. S. Younes","year":"2005","unstructured":"Younes HLS (2005) Probabilistic verification for \u201cblack-box\u201d systems. In: Etessami K, Rajamani SK (eds) Computer aided verification, 17th international conference, CAV 2005, Edinburgh, Scotland, July 6\u201310, 2005. Proceedings, Lecture notes in computer science, vol 3576, pp 253\u2013265. Springer. \nhttps:\/\/doi.org\/10.1007\/11513988_25"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00333-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-019-00333-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00333-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,19]],"date-time":"2020-05-19T23:38:04Z","timestamp":1589931484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-019-00333-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,21]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,11]]}},"alternative-id":["333"],"URL":"https:\/\/doi.org\/10.1007\/s10703-019-00333-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,5,21]]},"assertion":[{"value":"21 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}