{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:43:14Z","timestamp":1725831794454},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319249520"},{"type":"electronic","value":"9783319249537"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24953-7_14","type":"book-chapter","created":{"date-parts":[[2015,10,7]],"date-time":"2015-10-07T11:00:11Z","timestamp":1444215611000},"page":"201-206","source":"Crossref","is-referenced-by-count":1,"title":["Marimba: A Tool for Verifying Properties of Hidden Markov Models"],"prefix":"10.1007","author":[{"given":"No\u00e9","family":"Hern\u00e1ndez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kerstin","family":"Eder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Evgeni","family":"Magid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jes\u00fas","family":"Savage","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David A.","family":"Rosenblueth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1109\/5.18626","volume":"77","author":"LR Rabiner","year":"1989","unstructured":"Rabiner, L.R.: A tutorial on hidden Markov models and selected applications in speech recognition. Proc. IEEE 77, 257\u2013286 (1989)","journal-title":"Proc. IEEE"},{"key":"14_CR2","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. 3731, pp. 98\u2013112. Springer, Heidelberg (2005)"},{"key":"14_CR3","unstructured":"Hern\u00e1ndez, N.: Model checking based on the hidden Markov model and its application to human-robot interaction. Master\u2019s thesis, Universidad Nacional Aut\u00f3noma de M\u00e9xico, M\u00e9xico (2014). \n                    http:\/\/132.248.9.195\/ptd2014\/noviembre\/303087692\/Index.html"},{"key":"14_CR4","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)"},{"issue":"4","key":"14_CR5","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"14_CR6","first-page":"101","volume":"23","author":"JJMM Rutten","year":"2004","unstructured":"Rutten, J.J.M.M., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical techniques for analyzing concurrent and probabilistic systems. CRM monograph series. Am. Math. Soc. 23, 101\u2013116 (2004)","journal-title":"Am. Math. Soc."},{"key":"14_CR7","unstructured":"Erkok, L.: linearEqSolver: a library to solve systems of linear equations, using SMT solvers. \n                    https:\/\/github.com\/LeventErkok\/linearEqSolver"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-44833-4_2","volume-title":"Advanced Functional Programming","author":"MMT Chakravarty","year":"2003","unstructured":"Chakravarty, M.M.T., Keller, G.: An approach to fast arrays in Haskell. In: Jeuring, J., Jones, S.L.P. (eds.) AFP 2002. LNCS, vol. 2638, pp. 27\u201358. Springer, Heidelberg (2003)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Grigore, E.C., Eder, K., Pipe, A.G., Melhuish, C., Leonards, U.: Joint action understanding improves robot-to-human object handover. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 4622\u20134629. IEEE (2013)","DOI":"10.1109\/IROS.2013.6697021"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Lenz, A., Skachek, S., Hamann, K., Steinwender, J., Pipe, A.G., Melhuish, C.: The BERT2 infrastructure: an integrated system for the study of human-robot interaction. In: 10th IEEE-RAS International Conference on Humanoid Robots, pp. 346\u2013351. IEEE (2010)","DOI":"10.1109\/ICHR.2010.5686319"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/TCOM.1980.1094577","volume":"28","author":"Y Linde","year":"1980","unstructured":"Linde, Y., Buzo, A., Gray, R.M.: An algorithm for vector quantizer design. IEEE Trans. Commun. 28, 84\u201395 (1980)","journal-title":"IEEE Trans. Commun."}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24953-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:02:25Z","timestamp":1559260945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24953-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319249520","9783319249537"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24953-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}