{"created":"2023-07-27T06:50:57.923135+00:00","id":44172,"links":{},"metadata":{"_buckets":{"deposit":"4e85a343-fed5-4098-ad38-a11d8f0587d1"},"_deposit":{"created_by":18,"id":"44172","owners":[18],"pid":{"revision_id":0,"type":"depid","value":"44172"},"status":"published"},"_oai":{"id":"oai:kanazawa-u.repo.nii.ac.jp:00044172","sets":["2268:2269:2270"]},"author_link":["12772","74228"],"item_4_biblio_info_8":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2017-05-15","bibliographicIssueDateType":"Issued"},"bibliographicPageEnd":"568","bibliographicPageStart":"567","bibliographicVolumeNumber":"2017-May","bibliographic_titles":[{"bibliographic_title":"Proceedings - 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017"}]}]},"item_4_creator_33":{"attribute_name":"著者別表示","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"栁瀨, 龍"}],"nameIdentifiers":[{}]}]},"item_4_description_21":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"Linear hybrid automaton is a specification language for hybrid systems. For verification of hybrid systems, it is important to check fairness assumptions. For example, an embedded system keeps running forever when it starts to move by turning on the switch. Such a system has to be checked not only system safety but also fairness and non-Zenoness. The state space explosion is a fundamental problem in model checking, since it is a method that performs an exhaustive search of states. To avoid state space explosion problem in model checking, CEGAR (Counter Example Guided Abstraction Re?nement) is an effective technique. In this paper, we propose transition predicate abstraction and CEGAR verification algorithm for linear hybrid automata. © 2017 IEEE.","subitem_description_type":"Abstract"}]},"item_4_description_5":{"attribute_name":"提供者所属","attribute_value_mlt":[{"subitem_description":"金沢大学新学術創成研究機構","subitem_description_type":"Other"}]},"item_4_identifier_registration":{"attribute_name":"ID登録","attribute_value_mlt":[{"subitem_identifier_reg_text":"10.24517/00050514","subitem_identifier_reg_type":"JaLC"}]},"item_4_publisher_17":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"Institute of Electrical and Electronics Engineers Inc."}]},"item_4_relation_12":{"attribute_name":"DOI","attribute_value_mlt":[{"subitem_relation_type":"isVersionOf","subitem_relation_type_id":{"subitem_relation_type_id_text":"10.1109/ICST.2017.78","subitem_relation_type_select":"DOI"}}]},"item_4_relation_28":{"attribute_name":"関連URI","attribute_value_mlt":[{"subitem_relation_name":[{"subitem_relation_name_text":"http://aster.or.jp/conference/icst2017/"}],"subitem_relation_type_id":{"subitem_relation_type_id_text":"http://aster.or.jp/conference/icst2017/","subitem_relation_type_select":"URI"}},{"subitem_relation_name":[{"subitem_relation_name_text":"https://www.ieee.org/"}],"subitem_relation_type_id":{"subitem_relation_type_id_text":"https://www.ieee.org/","subitem_relation_type_select":"URI"}}]},"item_4_rights_23":{"attribute_name":"権利","attribute_value_mlt":[{"subitem_rights":"Copyright © 2017 IEEE."}]},"item_4_version_type_25":{"attribute_name":"著者版フラグ","attribute_value_mlt":[{"subitem_version_resource":"http://purl.org/coar/version/c_ab4af688f83e57aa","subitem_version_type":"AM"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Yanase, Ryo"}],"nameIdentifiers":[{}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2018-04-16"}],"displaytype":"detail","filename":"TE-PR-YANASE-R-567.pdf","filesize":[{"value":"60.0 kB"}],"format":"application/pdf","licensetype":"license_11","mimetype":"application/pdf","url":{"label":"TE-PR-YANASE-R-567.pdf","url":"https://kanazawa-u.repo.nii.ac.jp/record/44172/files/TE-PR-YANASE-R-567.pdf"},"version_id":"18fb2cc5-a865-4281-89b8-bc59757d37d4"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"journal article","resourceuri":"http://purl.org/coar/resource_type/c_6501"}]},"item_title":"Abstraction refinement for non-zeno fairness verification of linear hybrid automata","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Abstraction refinement for non-zeno fairness verification of linear hybrid automata"}]},"item_type_id":"4","owner":"18","path":["2270"],"pubdate":{"attribute_name":"公開日","attribute_value":"2018-04-16"},"publish_date":"2018-04-16","publish_status":"0","recid":"44172","relation_version_is_last":true,"title":["Abstraction refinement for non-zeno fairness verification of linear hybrid automata"],"weko_creator_id":"18","weko_shared_id":-1},"updated":"2023-07-27T17:35:05.890736+00:00"}