{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T23:56:34Z","timestamp":1772927794295,"version":"3.50.1"},"reference-count":15,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Fundamentals"],"published-print":{"date-parts":[[2026,3,1]]},"DOI":"10.1587\/transfun.2025eap1049","type":"journal-article","created":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T22:06:42Z","timestamp":1756678002000},"page":"638-650","source":"Crossref","is-referenced-by-count":0,"title":["Multitask Hybrid Observational Transition System and its Application"],"prefix":"10.1587","volume":"E109.A","author":[{"given":"Yifan","family":"WANG","sequence":"first","affiliation":[{"name":"Toyama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masaki","family":"NAKAMURA","sequence":"additional","affiliation":[{"name":"Toyama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryo","family":"TAKANO","sequence":"additional","affiliation":[{"name":"Toyama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takuya","family":"MATSUMOTO","sequence":"additional","affiliation":[{"name":"Toyama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazutoshi","family":"SAKAKIBARA","sequence":"additional","affiliation":[{"name":"Toyama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","unstructured":"[1] Y. Wang, M. Nakamura, and K. Sakakibara, \u201cFormal verification of autonomous vehicle group control systems by the OTS\/CafeOBJ method,\u201d 39th International Technical Conference on Circuits\/Systems, Computers, and Communications (ITC-CSCC 2024), 2024."},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] J.-B. Jeannin, K. Ghorbal, Y. Kouskoulas, A. Schmidt, R. Gardner, S. Mitsch, and A. Platzer, \u201cA formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system,\u201d Int. J. Softw. Tools Technol. Transfer., vol.19, pp.717-741, 2017. 10.1007\/s10009-016-0434-1","DOI":"10.1007\/s10009-016-0434-1"},{"key":"3","doi-asserted-by":"crossref","unstructured":"[3] A.E. Haxthausen and K. Hede, \u201cFormal verification of railway timetables-using the UPPAAL model checker,\u201d From Software Engineering to Formal Methods and Tools, and Back: Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, Lecture Notes in Computer Science, vol.11865, pp.433-448, 2019. 10.1007\/978-3-030-30985-5_25","DOI":"10.1007\/978-3-030-30985-5_25"},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] Y. Wang, M. Nakamura, and K. Sakakibara, \u201cFormal specification of an autonomous vehicle group control system with the hybrid OTS\/CafeOBJ method,\u201d 29th Int\u2019l Conf on Parallel and Distributed Processing Techniques and Applications: Workshop on Mathematical Modeling and Problem Solving (PDPTA\u201923, MPS144), pp.2169-2176, July, 2023.","DOI":"10.1109\/CSCE60160.2023.00355"},{"key":"5","doi-asserted-by":"publisher","unstructured":"[5] U. Berger, P. James, A. Lawrence, M. Roggenbach, and M. Seisenberger, \u201cVerification of the european rail traffic management system in real-time maude,\u201d Sci. Comput. Program., vol.154, pp.61-88, 2018. 10.1016\/j.scico.2017.10.011","DOI":"10.1016\/j.scico.2017.10.011"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] R. Diaconescu and K. Futatsugi, CafeOBJ Report, World Scientific, Singapore, 1998. 10.1142\/3831","DOI":"10.1142\/3831"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] K. Ogata and K. Futatsugi, \u201cProof scores in the OTS\/CafeOBJ method,\u201d Proc. 6th IFIP WG6.1 Int. Conf. Formal Methods for Open Object-Based Distributed Systems, Lecture Notes in Computer Science, vol.2884, pp.170-184, 2003. 10.1007\/978-3-540-39958-2_12","DOI":"10.1007\/978-3-540-39958-2_12"},{"key":"8","doi-asserted-by":"publisher","unstructured":"[8] K. Ogata and K. Futatsugi, \u201cSome tips on writing proof scores in the OTS\/CafeOBJ method,\u201d Algebra Meaning, and Computation, K. Futatsugi, J.-P. Jouannaud, and J. Meseguer, eds., Goguen Festschrift, Lecture Notes in Computer Science, vol.4060, pp.596-615, Springer, Heidelberg, 2006. 10.1007\/11780274_31","DOI":"10.1007\/11780274_31"},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] K. Ogata and K. Futatsugi, \u201cModeling and verification of real-time systems based on equations,\u201d Sci. Comput. Program., vol.66, no.2, pp.162-180, 2007. 10.1016\/j.scico.2006.10.011","DOI":"10.1016\/j.scico.2006.10.011"},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] M. Nakamura, S. Higashi, K. Sakakibara, and K. Ogata, \u201cSpecification and verification of multitask real-time systems using the OTS\/CafeOBJ method,\u201d IEICE Trans. Fundamentals, vol.E105-A, no.5, pp.823-832, May 2022. 10.1587\/transfun.2021map0007","DOI":"10.1587\/transfun.2021MAP0007"},{"key":"11","unstructured":"[11] K. Ogata, D. Yamagishi, T. Seino, and K. Futatsugi, \u201cModeling and verification of hybrid systems based on equations,\u201d Design Methods and Applications for Distributed Embedded Systems: IFIP 18th World Computer Congress TC10 Working Conference on Distributed and Parallel Embedded Systems (DIPES 2004) Aug. 2004, Toulouse, France, pp.43-52, Springer US, 2004. 10.1007\/1-4020-8149-9_5"},{"key":"12","unstructured":"[12] J.F. Raskin, \u201cAn introduction to hybrid automata,\u201d Handbook of Networked and Embedded Control Systems, D. Hristu-Varsakelis and W.S. Levine, eds., Control Engineering, Birkh\u00e4user Boston, 2005. 10.1007\/0-8176-4404-0_21"},{"key":"13","doi-asserted-by":"publisher","unstructured":"[13] P.C. \u00d6lveczky and J. Meseguer, \u201cSemantics and pragmatics of real-time Maude,\u201d Higher-Order Symb. Comput., vol.20, pp.161-196, Springer, 2007. 10.1007\/s10990-007-9001-5","DOI":"10.1007\/s10990-007-9001-5"},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] D. Lepri, E. \u00c1brah\u00e1m, and P.C. \u00d6lveczky, \u201cTimed CTL model checking in real-time Maude,\u201d Proc. 9th Int. Conf. Rewriting Logic and Its Applications, Lecture Notes in Computer Science, vol.7571, pp.182-200, 2012. 10.1007\/978-3-642-34005-5_10","DOI":"10.1007\/978-3-642-34005-5_10"},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] D. G\u0103in\u0103, D. Lucanu, K. Ogata, and K. Futatsugi, \u201cOn automation of OTS\/CafeOBJ method,\u201d Specific, Algebra and Software, Lecture Notes in Computer Science, vol.8373, Springer, pp.578-602, 2014. 10.1007\/978-3-642-54624-2_29","DOI":"10.1007\/978-3-642-54624-2_29"}],"container-title":["IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transfun\/E109.A\/3\/E109.A_2025EAP1049\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T04:11:18Z","timestamp":1772856678000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transfun\/E109.A\/3\/E109.A_2025EAP1049\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,1]]},"references-count":15,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026]]}},"URL":"https:\/\/doi.org\/10.1587\/transfun.2025eap1049","relation":{},"ISSN":["0916-8508","1745-1337"],"issn-type":[{"value":"0916-8508","type":"print"},{"value":"1745-1337","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,1]]},"article-number":"2025EAP1049"}}