{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,4]],"date-time":"2025-10-04T03:40:59Z","timestamp":1759549259358,"version":"build-2065373602"},"reference-count":19,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"10","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2025,10,1]]},"DOI":"10.1587\/transinf.2024edp7192","type":"journal-article","created":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T18:16:03Z","timestamp":1743099363000},"page":"1170-1182","source":"Crossref","is-referenced-by-count":0,"title":["A Model Partitioning Method in Model Checking for Information and Control System"],"prefix":"10.1587","volume":"E108.D","author":[{"given":"Kei","family":"KOGAI","sequence":"first","affiliation":[{"name":"Graduate School of Science and Engineerin, Ibaraki University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoshikazu","family":"UEDA","sequence":"additional","affiliation":[{"name":"Graduate School of Science and Engineerin, Ibaraki University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","unstructured":"[1] S. Akasaka, and N. Ochi, \u201cWorld-leading advanced factory \u201cLighthouse\u201d and its information and control systems,\u201d Hitachi Review, vol.70, no.5, pp.33-36, 2021."},{"key":"2","unstructured":"[2] S. Nakajima, \u201cApplying model-checking techniques to verification of software design,\u201d Computer Software, vol.23, no.2, pp.72-86, 2006."},{"key":"3","unstructured":"[3] G.J. Holzmann, The SPIN model checker: primer and reference manual, Addison-Wesley, 2003."},{"key":"4","unstructured":"[4] M. Ishiguro, \u201cApproaches to employing formal methods in software development,\u201d WIAFM2010: Workshop on Industrial Applications of Formal Methods, pp.41-48, 2010."},{"key":"5","unstructured":"[5] K. Oyama, K. Kogai, Y. Ueda, T. Yamagata, and T. Takezawa, \u201cStep-by-step model checking method using SPIN for information control system, \u201d Proc. 30th JSSST Annual Conference, pp.274-281, 2013."},{"key":"6","unstructured":"[6] T. Miyajima, K. Kogai, Y. Ueda, T. Yamagata, and T. Takezawa, \u201cInvestigation of model checking by modular approach, and practicality of modular verification,\u201d IEICE Technical Report, vol.114, no.501, pp.25-30, 2015."},{"key":"7","doi-asserted-by":"crossref","unstructured":"[7] L. Antu\u00f1a, D. Araiza-Illan, S. Campos, and K. Eder, \u201cSymmetry reduction enables model checking of more complex emergent behaviours of swarm navigation algorithms,\u201d 16th Annual Conference on Towards Autonomous Robotic Systems, pp.26-37, Springer Verlag, 2015. 10.1007\/978-3-319-22416-9_4","DOI":"10.1007\/978-3-319-22416-9_4"},{"key":"8","doi-asserted-by":"publisher","unstructured":"[8] P. Dhaussy, F. Boniol, J.C. Roger, and L. Leroux, \u201cImproving model checking with context modelling,\u201d Advances in Software Engineering 2012, ID-547157, 2012. 10.1155\/2012\/547157","DOI":"10.1155\/2012\/547157"},{"key":"9","doi-asserted-by":"crossref","unstructured":"[9] \u00c1. Heged\u00fcs, \u00c1. Horv\u00e1th, I. R\u00e1th, and D. Varr\u00f3, \u201cA model-driven framework for guided design space exploration,\u201d Proceedings of the 2011 26th IEEE\/ACM International Conference on Automated Software Engineering, pp.173-182, 2011. 10.1109\/ase.2011.6100051","DOI":"10.1109\/ASE.2011.6100051"},{"key":"10","unstructured":"[10] C. Flanagan, and S. Qadeer, \u201cAssume-guarantee model checking,\u201d Technical report, Microsoft Research, 2003."},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] D. Giannakopoulou, K.S. Namjoshi, and C.S. P\u0103s\u0103reanu, \u201cCompositional Reasoning,\u201d Handbook of model checking, eds. E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem, pp.345-383, Springer, 2018. 10.1007\/978-3-319-10575-8_12","DOI":"10.1007\/978-3-319-10575-8_12"},{"key":"12","doi-asserted-by":"publisher","unstructured":"[12] X. Liu, \u201cCompositional Verification Using Geodesic Distance via Assume-Guarantee Reasoning,\u201d IEEE Access, vol.12, pp.92612-92621, 2024. 10.1109\/access.2024.3421239","DOI":"10.1109\/ACCESS.2024.3421239"},{"key":"13","doi-asserted-by":"publisher","unstructured":"[13] X. Zhang, S. Xiao, Y. Xia, J. Li, M. Chen, and G. Pu, \u201cAccelerate Safety Model Checking Based on Complementary Approximate Reachability,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.42, no.9, pp.3105-3117, 2023. 10.1109\/tcad.2023.3236272","DOI":"10.1109\/TCAD.2023.3236272"},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] K. Ye, S. Foster, and J. Woodcock, \u201cCompositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP,\u201d From Astrophysics to Unconventional Computation: Essays Presented to Susan Stepney on the Occasion of her 60th Birthday, eds. A. Adamatzky, and V. Kendon, pp.215-254, Springer, 2020. 10.1007\/978-3-030-15792-0_10","DOI":"10.1007\/978-3-030-15792-0_10"},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] U. von Luxburg, \u201cA tutorial on spectral clustering,\u201d Statistics and computing, vol.17, no.4, pp.395-416, 2007. 10.1007\/s11222-007-9033-z","DOI":"10.1007\/s11222-007-9033-z"},{"key":"16","doi-asserted-by":"crossref","unstructured":"[16] M.E.J. Newman and M. Girvan, \u201cFinding and evaluating community structure in networks,\u201d Physical review E, vol.69, no.2, 026113, 2004. 10.1103\/physreve.69.026113","DOI":"10.1103\/PhysRevE.69.026113"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] A. Banaszuk, V.A. Fonoberov, T.A. Frewen, M. Kobilarov, G. Mathew, I. Mezic, A. Pinto, T. Sahai, H. Sane, A. Speranzon, and A. Surana, \u201cScalable approach to uncertainty quantification and robust design of interconnected dynamical systems,\u201d Annual Reviews in Control, vol.35, no.1, pp.77-98, 2011. 10.1016\/j.arcontrol.2011.03.005","DOI":"10.1016\/j.arcontrol.2011.03.005"},{"key":"18","unstructured":"[18] M. Ben-Ari, \u201cPrinciples of the Spin Model Checker,\u201d Springer, 2008."},{"key":"19","doi-asserted-by":"crossref","unstructured":"[19] A. Clauset, M.E.J. Newman, and C. Moore, \u201cFinding community structure in very large networks,\u201d Physical review E, vol.70, no.6, 066111, 2004. 10.1103\/physreve.70.066111","DOI":"10.1103\/PhysRevE.70.066111"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E108.D\/10\/E108.D_2024EDP7192\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,4]],"date-time":"2025-10-04T03:28:28Z","timestamp":1759548508000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E108.D\/10\/E108.D_2024EDP7192\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,1]]},"references-count":19,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2025]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2024edp7192","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"type":"print","value":"0916-8532"},{"type":"electronic","value":"1745-1361"}],"subject":[],"published":{"date-parts":[[2025,10,1]]},"article-number":"2024EDP7192"}}