{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T16:31:02Z","timestamp":1759336262242,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030532901"},{"type":"electronic","value":"9783030532918"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53291-8_17","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:03:35Z","timestamp":1594843415000},"page":"304-326","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Global PAC Bounds for Learning Discrete Time Markov Chains"],"prefix":"10.1007","author":[{"given":"Hugo","family":"Bazille","sequence":"first","affiliation":[]},{"given":"Blaise","family":"Genest","sequence":"additional","affiliation":[]},{"given":"Cyrille","family":"Jegourel","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-030-25540-4_29","volume-title":"Computer Aided Verification","author":"P Ashok","year":"2019","unstructured":"Ashok, P., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: PAC statistical model checking for Markov decision processes and stochastic games. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 497\u2013519. Springer, Cham (2019). \n                    https:\/\/doi.org\/10.1007\/978-3-030-25540-4_29"},{"key":"17_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-40196-1_7","volume-title":"Quantitative Evaluation of Systems","author":"L Bortolussi","year":"2013","unstructured":"Bortolussi, L., Sanguinetti, G.: Learning and designing stochastic processes from logical constraints. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 89\u2013105. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-40196-1_7"},{"key":"17_CR4","unstructured":"Brambilla, M., Pinciroli, C., Birattari, M., Dorigo, M.: Property-driven design for swarm robotics. In: International Conference on Autonomous Agents and Multiagent Systems, AAMAS, Valencia, Spain, pp. 139\u2013146 (2012)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-540-88009-7_13","volume-title":"Grammatical Inference: Algorithms and Applications","author":"J Castro","year":"2008","unstructured":"Castro, J., Gavald\u00e0, R.: Towards feasible PAC-learning of probabilistic deterministic finite automata. In: Clark, A., Coste, F., Miclet, L. (eds.) ICGI 2008. LNCS (LNAI), vol. 5278, pp. 163\u2013174. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-88009-7_13"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Chen, J.: Properties of a new adaptive sampling method with applications to scalable learning. In: Web Intelligence, Atlanta, pp. 9\u201315 (2013)","DOI":"10.1109\/WI-IAT.2013.3"},{"issue":"4","key":"17_CR7","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1006\/csla.1999.0128","volume":"13","author":"SF Chen","year":"1999","unstructured":"Chen, S.F., Goodman, J.: An empirical study of smoothing techniques for language modeling. Comput. Speech Lang. 13(4), 359\u2013394 (1999)","journal-title":"Comput. Speech Lang."},{"key":"17_CR8","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). \n                    https:\/\/doi.org\/10.1007\/978-3-642-28891-3_22"},{"issue":"4","key":"17_CR9","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1214\/aoms\/1177729330","volume":"23","author":"H Chernoff","year":"1952","unstructured":"Chernoff, H.: A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations. Ann. Math. Statist. 23(4), 493\u2013507 (1952)","journal-title":"Ann. Math. Statist."},{"key":"17_CR10","first-page":"473","volume":"5","author":"A Clark","year":"2004","unstructured":"Clark, A., Thollard, F.: PAC-learnability of probabilistic deterministic finite state automata. J. Mach. Learn. Res. 5, 473\u2013497 (2004)","journal-title":"J. Mach. Learn. Res."},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). \n                    https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Cochran, W.G.: Contributions to survey sampling and applied statistics, chapter Laplace\u2019s ratio estimator, pp. 3\u201310. Academic Press, New York (1978)","DOI":"10.1016\/B978-0-12-204750-3.50008-3"},{"key":"17_CR13","unstructured":"Daca, P., Henzinger, T.A., Kret\u00ednsk\u00fd, J., Petrov, T.: Linear distances between Markov chains. In: 27th International Conference on Concurrency Theory, CONCUR 2016, 23\u201326 August 2016, Qu\u00e9bec City, Canada, pp. 20:1\u201320:15 (2016)"},{"issue":"2","key":"17_CR14","doi-asserted-by":"publisher","first-page":"12:1","DOI":"10.1145\/3060139","volume":"18","author":"P Daca","year":"2017","unstructured":"Daca, P., Henzinger, T.A., Kret\u00ednsk\u00fd, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Log. 18(2), 12:1\u201312:25 (2017)","journal-title":"ACM Trans. Comput. Log."},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1080\/09296179508590051","volume":"2","author":"WA Gale","year":"1995","unstructured":"Gale, W.A., Sampson, G.: Good-turing frequency estimation without tears. J. Quantit. Linguist. 2, 217\u2013237 (1995)","journal-title":"J. Quantit. Linguist."},{"key":"17_CR16","unstructured":"Ghosh, S., Lincoln, P., Tiwari, A., Zhu, X.: Trusted machine learning: model repair and data repair for probabilistic models. In: AAAI-17 Workshop on Symbolic Inference and Optimization (2017)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73\u201384. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-24622-0_8"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-66335-7_23","volume-title":"Quantitative Evaluation of Systems","author":"C Jegourel","year":"2017","unstructured":"Jegourel, C., Sun, J., Dong, J.S.: Sequential schemes for frequentist estimation of properties in statistical model checking. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 333\u2013350. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-66335-7_23"},{"issue":"1","key":"17_CR19","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1214\/aoms\/1177729694","volume":"22","author":"S Kullback","year":"1951","unstructured":"Kullback, S., Leibler, R.A.: On information and sufficiency. Ann. Math. Stat. 22(1), 79\u201386 (1951)","journal-title":"Ann. Math. Stat."},{"key":"17_CR20","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). \n                    https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-45994-3_2","volume-title":"Reachability Problems","author":"A Legay","year":"2016","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Rare events for statistical model checking an overview. In: Larsen, K.G., Potapov, I., Srba, J. (eds.) RP 2016. LNCS, vol. 9899, pp. 23\u201335. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-45994-3_2"},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"1269","DOI":"10.1214\/aop\/1176990746","volume":"18","author":"P Massart","year":"1990","unstructured":"Massart, P.: The tight constant in the Dvoretzky-Kiefer-Wolfowitz inequality. Ann. Probab. 18, 1269\u20131283 (1990)","journal-title":"Ann. Probab."},{"key":"17_CR23","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BF02883985","volume":"10","author":"M Okamoto","year":"1958","unstructured":"Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29\u201335 (1958)","journal-title":"Ann. Inst. Stat. Math."},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1","key":"17_CR25","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/s10479-005-5727-9","volume":"134","author":"A Ridder","year":"2005","unstructured":"Ridder, A.: Importance sampling simulations of Markovian reliability systems using cross-entropy. Ann. OR 134(1), 119\u2013136 (2005)","journal-title":"Ann. OR"},{"key":"17_CR26","unstructured":"Dorsa Sadigh, K. et al.: Data-driven probabilistic modeling and verification of human driver behavior. In: Formal Verification and Modeling in Human-Machine Systems - AAAI Spring Symposium (2014)"},{"issue":"3","key":"17_CR27","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1057\/jors.1995.55","volume":"46","author":"C Sherlaw-Johnson","year":"1995","unstructured":"Sherlaw-Johnson, C., Gallivan, S., Burridge, J.: Estimating a Markov transition matrix from observational data. J. Oper. Res. Soc. 46(3), 405\u2013410 (1995)","journal-title":"J. Oper. Res. Soc."},{"issue":"11","key":"17_CR28","doi-asserted-by":"publisher","first-page":"1134","DOI":"10.1145\/1968.1972","volume":"27","author":"LG Valiant","year":"1984","unstructured":"Valiant, L.G.: A theory of the learnable. Commun. ACM 27(11), 1134\u20131142 (1984)","journal-title":"Commun. ACM"},{"issue":"2","key":"17_CR29","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"key":"17_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-662-54494-5_1","volume-title":"Fundamental Approaches to Software Engineering","author":"J Wang","year":"2017","unstructured":"Wang, J., Sun, J., Yuan, Q., Pang, J.: Should we learn probabilistic models for model checking? A new approach and an empirical study. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 3\u201321. Springer, Heidelberg (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-662-54494-5_1"},{"key":"17_CR31","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). \n                    https:\/\/doi.org\/10.1007\/978-3-642-19829-8_10"},{"key":"17_CR32","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). \n                    https:\/\/doi.org\/10.1007\/3-540-45657-0_17"},{"issue":"2","key":"17_CR33","first-page":"338","volume":"43","author":"P Zuliani","year":"2013","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow\/simulink verification. FMSD 43(2), 338\u2013367 (2013)","journal-title":"FMSD"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53291-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,16]],"date-time":"2020-07-16T02:03:32Z","timestamp":1594865012000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53291-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532901","9783030532918"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53291-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}