{"links":{},"id":16734,"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00016734","sets":["934:935:963:966"]},"path":["966"],"owner":"1","recid":"16734","title":["プッシュダウンシステムの拡張およびそのモデル検査法"],"pubdate":{"attribute_name":"公開日","attribute_value":"2003-10-15"},"_buckets":{"deposit":"d7449fbc-77b4-4db8-9932-ea647137b55a"},"_deposit":{"id":"16734","pid":{"type":"depid","value":"16734","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"プッシュダウンシステムの拡張およびそのモデル検査法","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"プッシュダウンシステムの拡張およびそのモデル検査法"},{"subitem_title":"An Extension of Pushdown System and Its Model Checking Method","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"発表概要","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2003-10-15","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"奈良先端科学技術大学院大学情報科学研究科"},{"subitem_text_value":"奈良先端科学技術大学院大学情報科学研究科"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Graduate School of Information Science, Nara Institute of Science and Technology","subitem_text_language":"en"},{"subitem_text_value":"Graduate School of Information Science, Nara Institute of Science and Technology","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/16734/files/IPSJ-TPRO4413012.pdf"},"date":[{"dateType":"Available","dateValue":"2005-10-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO4413012.pdf","filesize":[{"value":"29.8 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"5"},{"tax":["include_tax"],"price":"0","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"a3e3da8b-6f75-4fa5-8639-f8833f82aff2","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2003 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"新田, 直也"},{"creatorName":"関, 浩之"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Naoya, Nitta","creatorNameLang":"en"},{"creatorName":"Hiroyuki, Seki","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"現在，無限の状態空間を持つ遷移システムに対するモデル検査法の研究がさかんに行われており，特にプッシュダウンシステムやペトリネットに対するモデル検査において良い結果が得られている．本発表では，プッシュダウンシステムを拡張した遷移システムを項書き換え系の部分クラスとして定義し，そのLTL （線形時相論理）によるモデル検査が決定可能となることを示す．プッシュダウンシステムの項書き換え系による定式化は，一般に文字列で表現されるスタック構造の木構造への拡張を意味し，この拡張によってより豊かなデータ構造を持った遷移システムの自動検証が可能になることが期待される．","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"Recently, in the field of model checking, many researches for infinite systems have been done. Particularly for pushdown systems and petri nets, there are good decidablity results on model checking. In this presentation, we define a class of transition systems which is an extension of pushdown systems as a subclass of TRS (term rewriting systems) and show that LTL (linear temporal logic) model checking problem for the class is decidable. Formulating pushdown systems as a subclass of TRS, we can extend the structure of stacks to tree structure. By this extension, it is expected that transition systems with richer data structure become verifiable.","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"111","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicPageStart":"111","bibliographicIssueDates":{"bibliographicIssueDate":"2003-10-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"SIG13(PRO18)","bibliographicVolumeNumber":"44"}]},"relation_version_is_last":true,"weko_creator_id":"1"},"created":"2025-01-18T22:49:55.460045+00:00","updated":"2025-01-22T23:42:51.303571+00:00"}