{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T22:11:16Z","timestamp":1780611076285,"version":"3.54.1"},"reference-count":29,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Shimonoseki City University"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2025]]},"DOI":"10.1109\/access.2025.3572089","type":"journal-article","created":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T17:40:49Z","timestamp":1747849249000},"page":"90017-90033","source":"Crossref","is-referenced-by-count":1,"title":["Specification and Verification Method of Parallel Hierarchical Timed Automata by Predicate Abstraction and Refinement"],"prefix":"10.1109","volume":"13","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7883-4054","authenticated-orcid":false,"given":"Satoshi","family":"Yamane","sequence":"first","affiliation":[{"name":"Department of Data Science, College of Data Science, Shimonoseki City University, Shimonoseki, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2024.04.040"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.3390\/drones7040248"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s12652-020-02769-3"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"issue":"5","key":"ref8","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1016\/S1571-0661(04)80478-X","article-title":"Predicate abstraction for dense real-time systems","volume":"68","author":"M\u00f6ller","year":"2002","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/11589976_5"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TLA.2020.9085271"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"ref12","volume-title":"OMG: Unified Modeling Language: Superstructure Ver 2.1.1","year":"2007"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/3579821"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/291252.288305"},{"issue":"3","key":"ref15","first-page":"155","article-title":"Automatic verification of statecharts by abstraction and refinement of hierarchical structure","volume":"26","author":"Ymazaki","year":"2009","journal-title":"Comput. Softw."},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45923-5_15"},{"key":"ref17","article-title":"Hierarchical modeling and analysis of timed systems","author":"David","year":"2003"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/9.272327"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/JAS.2024.124560"},{"key":"ref21","article-title":"Techniques for automatic verification of real-time systems","author":"Alur","year":"1991"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2023.3275440"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2025.121997"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63875-X_52"},{"key":"ref25","volume-title":"Introduction to Algorithms","author":"Cormen","year":"2022"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1024"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/6287639\/10820123\/11008569.pdf?arnumber=11008569","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:38:14Z","timestamp":1748493494000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11008569\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/access.2025.3572089","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]}}}