{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,3]],"date-time":"2025-08-03T01:11:52Z","timestamp":1754183512547,"version":"3.41.2"},"reference-count":9,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"8","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2025,8,1]]},"DOI":"10.1587\/transinf.2025edl8001","type":"journal-article","created":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T17:11:25Z","timestamp":1739293885000},"page":"1033-1036","source":"Crossref","is-referenced-by-count":0,"title":["A Study of Multi-Robot Tracking Problem in One-Dimensional System Using Probabilistic Model Checking"],"prefix":"10.1587","volume":"E108.D","author":[{"given":"Toshifusa","family":"SEKIZAWA","sequence":"first","affiliation":[{"name":"Department of Computer Science, College of Engineering, Nihon University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoaki","family":"YONEZAWA","sequence":"additional","affiliation":[{"name":"Department of Computer Science, College of Engineering, Nihon University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kozo","family":"OKANO","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Faculty of Engineering, Shinshu University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keitaro","family":"NARUSE","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Division of Information Systems, The University of Aizu"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"publisher","unstructured":"[1] G. Agha and K. Palmskog, \u201cA survey of statistical model checking,\u201d ACM Trans. Model. Comput. Simul., vol.28, no.1, pp.6:1-6:39, 2018. 10.1145\/3158668","DOI":"10.1145\/3158668"},{"key":"2","unstructured":"[2] E.M. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, 1999."},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] H. Hansson and B. Jonsson, \u201cA logic for reasoning about time and reliability,\u201d Formal Asp. Comput., vol.6, no.5, pp.512-535, 1994. 10.1007\/bf01211866","DOI":"10.1007\/BF01211866"},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] J.J.M.M. Rutten, M. Kwiatkowska, G. Norman, D. Parker, P. Panangaden, and F. van Breugel, Mathematical techniques for analyzing concurrent and probabilistic systems, CRM monograph series, vol.23, American Mathematical Society, 2004. 10.1090\/crmm\/023","DOI":"10.1090\/crmm\/023"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] M. Kwiatkowska, G. Norman, and D. Parker, \u201cPRISM 4.0: Verification of probabilistic real-time systems,\u201d Proc. 23rd International Conference on Computer Aided Verification (CAV\u2006\u201911), LNCS, vol.6806, pp.585-591, Springer, 2011. 10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] T. Sekizawa, F. Otsuki, K. Ito, and K. Okano, \u201cBehavior verification of autonomous robot vehicle in consideration of errors and disturbances,\u201d 2015 IEEE 39th Annual Computer Software and Applications Conference, pp.550-555, 2015. 10.1109\/compsac.2015.268","DOI":"10.1109\/COMPSAC.2015.268"},{"key":"7","doi-asserted-by":"crossref","unstructured":"[7] J.S. Sequeira, \u201cDependability in robotics as a consensus problem,\u201d 2017 IEEE International Conference on Robotics and Biomimetics (ROBIO), pp.1694-1701, 2017. 10.1109\/robio.2017.8324662","DOI":"10.1109\/ROBIO.2017.8324662"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] M. Foughali, F. Ingrand, and C. Seceleanu, \u201cStatistical model checking of complex robotic systems,\u201d Model Checking Software: 26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings 26, pp.114-134, Springer, 2019. 10.1007\/978-3-030-30923-7_7","DOI":"10.1007\/978-3-030-30923-7_7"},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] C. Chandler, B. Porr, A. Miller, and G. Lafratta, \u201cModel checking for closed-loop robot reactive planning,\u201d Proc. Fifth International Workshop on Formal Methods for Autonomous Systems, Electronic Proceedings in Theoretical Computer Science, vol.395, pp.77-94, Open Publishing Association, 2023. 10.4204\/eptcs.395.6","DOI":"10.4204\/EPTCS.395.6"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E108.D\/8\/E108.D_2025EDL8001\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T03:29:19Z","timestamp":1754105359000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E108.D\/8\/E108.D_2025EDL8001\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,1]]},"references-count":9,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2025]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2025edl8001","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"type":"print","value":"0916-8532"},{"type":"electronic","value":"1745-1361"}],"subject":[],"published":{"date-parts":[[2025,8,1]]},"article-number":"2025EDL8001"}}