{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T14:54:15Z","timestamp":1725807255707},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319117362"},{"type":"electronic","value":"9783319117379"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11737-9_21","type":"book-chapter","created":{"date-parts":[[2014,10,14]],"date-time":"2014-10-14T20:52:14Z","timestamp":1413319934000},"page":"316-331","source":"Crossref","is-referenced-by-count":5,"title":["On the Formal Analysis of HMM Using Theorem Proving"],"prefix":"10.1007","author":[{"given":"Liya","family":"Liu","sequence":"first","affiliation":[]},{"given":"Vincent","family":"Aravantinos","sequence":"additional","affiliation":[]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-32347-8_16","volume-title":"Interactive Theorem Proving","author":"R. Affeldt","year":"2012","unstructured":"Affeldt, R., Hagiwara, M.: Formalization of Shannon\u2019s Theorems in SSReflect-Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 233\u2013249. Springer, Heidelberg (2012)"},{"key":"21_CR2","unstructured":"C. Baier and J. Katoen. Principles of Model Checking. MIT Press (2008)"},{"key":"21_CR3","unstructured":"Bhattacharya, R.N., Waymire, E.C.: Stochastic Processes with Applications. John Wiley & Sons (1990)"},{"key":"21_CR4","unstructured":"ChIP-Seq Tool Set (2012), \n                  \n                    http:\/\/havoc.genomecenter.ucdavis.edu\/cgi-bin\/chipseq.cgi"},{"key":"21_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-49686-8","volume-title":"Markov chains with stationary transition probabilities","author":"K.L. Chung","year":"1960","unstructured":"Chung, K.L.: Markov chains with stationary transition probabilities. Springer, Heidelberg (1960)"},{"key":"21_CR6","unstructured":"Coq (2014), \n                  \n                    http:\/\/coq.inria.fr\/"},{"key":"21_CR7","unstructured":"Daniel, N.: Electrocardiogram Signal Processing using Hidden Markov Models. Ph.D. Thesis, Czech Technical University, Czech Republic (2003)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Eddy, S.R.: What is a Hidden Markov Model? Nature Biotechnology 22(10), 1315\u20131316 (2004)","DOI":"10.1038\/nbt1004-1315"},{"issue":"11","key":"21_CR9","doi-asserted-by":"publisher","first-page":"1399","DOI":"10.1093\/bioinformatics\/btn201","volume":"24","author":"S. Fr\u00e9d\u00e9ric","year":"2008","unstructured":"Fr\u00e9d\u00e9ric, S., Delorenzi, M.: MAMOT: Hidden Markov Modeling Tool. Bioinformatics\u00a024(11), 1399\u20131400 (2008)","journal-title":"Bioinformatics"},{"key":"21_CR10","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-1-4612-3658-0_10","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"M.J.C. Gordon","year":"1989","unstructured":"Gordon, M.J.C.: Mechanizing Programming Logics in Higher-0rder Logic. In: Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387\u2013439. Springer, Heidelberg (1989)"},{"key":"21_CR11","unstructured":"HMMER (2013), \n                  \n                    http:\/\/hmmer.janelia.org\/"},{"key":"21_CR12","unstructured":"HMMTool (2013), \n                  \n                    http:\/\/iri.columbia.edu\/climate\/forecast\/stochastictools\/"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-22863-6_12","volume-title":"Interactive Theorem Proving","author":"J. H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three Chapters of Measure Theory in Isabelle\/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 135\u2013151. Springer, Heidelberg (2011)"},{"key":"21_CR14","unstructured":"L. Liu (2013), \n                  \n                    http:\/\/hvg.ece.concordia.ca\/projects\/prob-it\/dtmc_hmm.html"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-24372-1_8","volume-title":"Automated Technology for Verification and Analysis","author":"L. Liu","year":"2011","unstructured":"Liu, L., Hasan, O., Tahar, S.: Formalization of finite-state discrete-time markov chains in HOL. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 90\u2013104. Springer, Heidelberg (2011)"},{"key":"21_CR16","unstructured":"MacDonald, I.L., Zucchini, W.: Hidden Markov and Other Models for Discrete-valued Time Series. Chapman & Hall, London (1997)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-14052-5_27","volume-title":"Interactive Theorem Proving","author":"T. Mhamdi","year":"2010","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: On the Formalization of the Lebesgue Integration Theory in HOL. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 387\u2013402. Springer, Heidelberg (2010)"},{"key":"21_CR18","unstructured":"MRMC (2013), \n                  \n                    http:\/\/www.mrmc-tool.org\/trac\/"},{"key":"21_CR19","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press (1999)"},{"key":"21_CR20","unstructured":"PRISM (2013), \n                  \n                    http:\/\/www.prismmodelchecker.org"},{"key":"21_CR21","doi-asserted-by":"publisher","first-page":"4407","DOI":"10.1175\/JCLI-3216.1","volume":"17","author":"A.W. Robertson","year":"2004","unstructured":"Robertson, A.W., Kirshner, S., Smyth, P.: Downscaling of Daily Rainfall Occurrence over Northeast Brazil using a Hidden Markov Model. Journal of Climate\u00a017, 4407\u20134424 (2004)","journal-title":"Journal of Climate"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Rutten, J., Kwaiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems. CRM Monograph Series, vol.\u00a023. American Mathematical Society (2004)","DOI":"10.1090\/crmm\/023"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: VESTA: A Statistical Model-Checker and Analyzer for Probabilistic Systems. In: IEEE International Conference on the Quantitative Evaluation of Systems, pp. 251\u2013252 (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"21_CR24","unstructured":"YMER (2013), \n                  \n                    http:\/\/www.tempastic.org\/ymer\/"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11562436_9","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"L. Zhang","year":"2005","unstructured":"Zhang, L., Hermanns, H., Jansen, D.N.: Logic and Model Checking for Hidden Markov Models. In: Wang, F. (ed.) FORTE 2005. LNCS, vol.\u00a03731, pp. 98\u2013112. Springer, Heidelberg (2005)"},{"key":"21_CR26","unstructured":"Zhang, L.J.: Logic and Model Checking for Hidden Markov Models. Master Thesis, Universit\u00e4t des Saarlandes, Germany (2004)"},{"issue":"1","key":"21_CR27","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1142\/S0218001401000836","volume":"15","author":"G. Zoubin","year":"2001","unstructured":"Zoubin, G.: An Introduction to Hidden Markov Models and Bayesian Networks. International Journal of Pattern Recognition and Artificial Intelligence\u00a015(1), 9\u201342 (2001)","journal-title":"International Journal of Pattern Recognition and Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11737-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T01:31:48Z","timestamp":1559007108000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11737-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319117362","9783319117379"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11737-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}