{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:50:25Z","timestamp":1743155425903,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662544938"},{"type":"electronic","value":"9783662544945"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54494-5_1","type":"book-chapter","created":{"date-parts":[[2017,3,22]],"date-time":"2017-03-22T00:09:02Z","timestamp":1490141342000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Should We Learn Probabilistic Models for Model Checking? A New Approach and An Empirical Study"],"prefix":"10.1007","author":[{"given":"Jingyi","family":"Wang","sequence":"first","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Qixia","family":"Yuan","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,22]]},"reference":[{"issue":"2","key":"1_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."},{"unstructured":"Angluin, D.: Identifying languages from stochastic examples (1988)","key":"1_CR2"},{"key":"1_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P., et al.: Principles of Model Checking. MIT press, Cambridge (2008). vol. 26202649"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11944836_25","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"A Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260\u2013272. Springer, Heidelberg (2006). doi:10.1007\/11944836_25"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A Bianco","year":"1995","unstructured":"Bianco, A., Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499\u2013513. Springer, Heidelberg (1995). doi:10.1007\/3-540-60692-0_70"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","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":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u00edk, M., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). doi:10.1007\/978-3-319-11936-6_8"},{"key":"1_CR7","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:10.1007\/3-540-58473-0_144"},{"issue":"1","key":"1_CR8","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. Informatique th\u00e9orique et applications 33(1), 1\u201319 (1999)","journal-title":"Informatique th\u00e9orique et applications"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-642-28891-3_22","volume-title":"NASA Formal Methods","author":"Y Chen","year":"2012","unstructured":"Chen, Y., Mao, H., Jaeger, M., Nielsen, T.D., Guldstrand Larsen, K., Nielsen, B.: Learning Markov models for stationary system behaviors. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 216\u2013230. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-28891-3_22"},{"key":"1_CR10","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24372-1_1","volume-title":"Automated Technology for Verification and Analysis","author":"EM Clarke","year":"2011","unstructured":"Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1\u201312. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-24372-1_1"},{"unstructured":"Dyer, D.W.: Watchmaker framework for evolutionary computation. http:\/\/watchmaker.uncommons.org","key":"1_CR12"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). doi:10.1007\/3-540-46002-0_24"},{"issue":"1","key":"1_CR14","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TC.2009.105","volume":"59","author":"F He","year":"2010","unstructured":"He, F., Song, X., Hung, W.N., Gu, M., Sun, J.: Integrating evolutionary computation with abstraction refinement for model checking. IEEE Trans. Comput. 59(1), 116\u2013126 (2010)","journal-title":"IEEE Trans. Comput."},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Types for Proofs and Programs","author":"L Helmink","year":"1994","unstructured":"Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127\u2013165. Springer, Heidelberg (1994). doi:10.1007\/3-540-58085-9_75"},{"issue":"2","key":"1_CR16","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T Herman","year":"1990","unstructured":"Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63\u201367 (1990)","journal-title":"Inf. Process. Lett."},{"key":"1_CR17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139194655","volume-title":"Grammatical Inference","author":"C De la Higuera","year":"2010","unstructured":"De la Higuera, C.: Grammatical Inference, vol. 96. Cambridge University Press, Cambridge (2010)"},{"key":"1_CR18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1090.001.0001","volume-title":"Adaptation in Natural and Artificial Systems","author":"JH Holland","year":"1992","unstructured":"Holland, J.H.: Adaptation in Natural and Artificial Systems. MIT Press, Cambridge (1992)"},{"issue":"1","key":"1_CR19","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/0890-5401(90)90004-2","volume":"88","author":"A Itai","year":"1990","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60\u201387 (1990)","journal-title":"Inf. Comput."},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-45790-9_12","volume-title":"Grammatical Inference: Algorithms and Applications","author":"C Kermorvant","year":"2002","unstructured":"Kermorvant, C., Dupont, P.: Stochastic grammatical inference with multinomial tests. In: Adriaans, P., Fernau, H., Zaanen, M. (eds.) ICGI 2002. LNCS (LNAI), vol. 2484, pp. 149\u2013160. Springer, Heidelberg (2002). doi:10.1007\/3-540-45790-9_12"},{"doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of 9th International Conference on Quantitative Evaluation of SysTems (QEST 2012), pp. 203\u2013204. IEEE CS Press (2012)","key":"1_CR21","DOI":"10.1109\/QEST.2012.14"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation: Modelling Techniques and Tools","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200\u2013204. Springer, Heidelberg (2002). doi:10.1007\/3-540-46029-2_13"},{"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: 2011 Eighth International Conference on Quantitative Evaluation of Systems (QEST), pp. 111\u2013120. IEEE (2011)","key":"1_CR23","DOI":"10.1109\/QEST.2011.21"},{"unstructured":"Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning markov decision processes for model checking. arXiv preprint (2012). arXiv:1212.3873","key":"1_CR24"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-24953-7_16","volume-title":"Automated Technology for Verification and Analysis","author":"A Mizera","year":"2015","unstructured":"Mizera, A., Pang, J., Yuan, Q.: ASSA-PBN: an approximate steady-state analyser of probabilistic boolean networks. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 214\u2013220. Springer, Cham (2015). doi:10.1007\/978-3-319-24953-7_16"},{"issue":"10","key":"1_CR26","doi-asserted-by":"publisher","first-page":"1629","DOI":"10.1109\/TCAD.2005.852033","volume":"24","author":"G Norman","year":"2005","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S.: Evaluating the reliability of nand multiplexing with prism. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 24(10), 1629\u20131637 (2005)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circ. Syst."},{"issue":"6","key":"1_CR27","doi-asserted-by":"publisher","first-page":"561","DOI":"10.3233\/JCS-2006-14604","volume":"14","author":"G Norman","year":"2006","unstructured":"Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. J. Comput. Secur. 14(6), 561\u2013589 (2006)","journal-title":"J. Comput. Secur."},{"issue":"1","key":"1_CR28","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"MK Reiter","year":"1998","unstructured":"Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. ACM Trans. Inf. Syst. Secur. (TISSEC) 1(1), 66\u201392 (1998)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-40465-8_8","volume-title":"Transactions on Petri Nets and Other Models of Concurrency VIII","author":"C Rohr","year":"2013","unstructured":"Rohr, C.: Simulative model checking of steady state and time-unbounded temporal operators. In: Koutny, M., Aalst, W.M.P., Yakovlev, A. (eds.) Transactions on Petri Nets and Other Models of Concurrency VIII. LNCS, vol. 8100, pp. 142\u2013158. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-40465-8_8"},{"doi-asserted-by":"crossref","unstructured":"Ron, D., Singer, Y., Tishby, N.: On the learnability and usage of acyclic probabilistic finite automata. In: Proceedings of the Eighth Annual Conference on Computational Learning Theory, pp. 31\u201340. ACM (1995)","key":"1_CR30","DOI":"10.1145\/225298.225302"},{"issue":"2\u20133","key":"1_CR31","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1023\/A:1026490906255","volume":"25","author":"D Ron","year":"1996","unstructured":"Ron, D., Singer, Y., Tishby, N.: The power of amnesia: learning probabilistic automata with variable memory length. Mach. Learn. 25(2\u20133), 117\u2013149 (1996)","journal-title":"Mach. Learn."},{"doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Learning continuous time markov chains from sample executions. In: Proceedings of First International Conference on the Quantitative Evaluation of Systems, QEST 2004, pp. 146\u2013155. IEEE (2004)","key":"1_CR32","DOI":"10.1109\/QEST.2004.1348029"},{"key":"1_CR33","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:10.1007\/978-3-540-27813-9_16"},{"issue":"11","key":"1_CR34","doi-asserted-by":"publisher","first-page":"1778","DOI":"10.1109\/JPROC.2002.804686","volume":"90","author":"I Shmulevich","year":"2002","unstructured":"Shmulevich, I., Dougherty, E., Zhang, W.: From boolean to probabilistic boolean networks as models of genetic regulatory networks. Proc. IEEE 90(11), 1778\u20131792 (2002)","journal-title":"Proc. IEEE"},{"unstructured":"SUTD: Secure water treatment testbed. http:\/\/itrust.sutd.edu.sg\/research\/testbeds\/secure-water-treatment-swat\/","key":"1_CR35"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/11591191_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Tabakov","year":"2005","unstructured":"Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 396\u2013411. Springer, Heidelberg (2005). doi:10.1007\/11591191_28"},{"unstructured":"Wang, J.: ziqian. https:\/\/bitbucket.org\/jingyi_wang\/ziqian_develop","key":"1_CR37"},{"unstructured":"Wang, J.: ziqian evaluation. https:\/\/bitbucket.org\/jingyi_wang\/ziqian_evaluation","key":"1_CR38"},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-642-19829-8_10","volume-title":"Formal Methods: Foundations and Applications","author":"HLS Younes","year":"2011","unstructured":"Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 144\u2013160. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-19829-8_10"},{"issue":"3","key":"1_CR40","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"HL Younes","year":"2006","unstructured":"Younes, H.L., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transf. 8(3), 216\u2013228 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002). doi:10.1007\/3-540-45657-0_17"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54494-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:10:46Z","timestamp":1618971046000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54494-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544938","9783662544945"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54494-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"22 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}