WEKO3
アイテム
振舞等価性の証明のための等式付き書換えに基づく潜在帰納法
http://hdl.handle.net/2237/21098
http://hdl.handle.net/2237/21098d31f0e7f-9ccc-4f9c-90b9-ea6049cfe5d9
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
110006388628.pdf (863.6 kB)
|
|
| アイテムタイプ | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2015-01-19 | |||||
| タイトル | ||||||
| タイトル | 振舞等価性の証明のための等式付き書換えに基づく潜在帰納法 | |||||
| 言語 | ja | |||||
| その他のタイトル | ||||||
| その他のタイトル | Implicit Induction for Proving Behavioral Equivalence by Equational Rewriting | |||||
| 著者 |
笹田, 悠司
× 笹田, 悠司× 酒井, 正彦× 西田, 直樹× 坂部, 俊樹× 草刈, 圭一朗× SASADA, Yuji× SAKAI, Masahiko× NISHIDA, Naoki× SAKABE, Toshiki× KUSAKARI, Keiichiro |
|||||
| アクセス権 | ||||||
| アクセス権 | open access | |||||
| アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||
| 権利 | ||||||
| 権利情報 | (c)一般社団法人電子情報通信学会。本文データは学協会の許諾に基づきCiNiiから複製したものである | |||||
| 言語 | ja | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | 振舞仕様 | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | 文脈可簡約性 | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | 項書換え系 | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | Knuth-Bendix完備化 | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | システムがどのように外部観測的に振舞うかを規定する振舞仕様の下で、観測を通してシステムの2つの状態が等しいことを振舞等価という。振舞等価性の自動証明法の一つに、潜在帰納法に基づく証明法が提案されている.しかし,この手法では簡約化順序で順序付けができない2つの項が存在するとき振舞等価性の証明に失敗する。本論文では、このような場合にも証明できるようにするために、等式付き書換えを用いた潜在帰納法に基づく証明法を提案する。さらに,完全な仕様の場合には手続き中の条件を判定可能な十分条件に置き換えられることを示す. | |||||
| 言語 | ja | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | A behavioral specification is a description of what is supposed to happen. Two states are said to be behaviourally equivalent on a behavioral specification if they are observationally indistinguishable. A proof method based on implicit induction principle have been proposed as an automatic proof method for behavioral equivalence. However it is a problem that the method sometimes fails to prove when two terms that represent states cannnot be ordered by the given reduction order. This paper proposes an implicit induction proof-method based on equational rewriting in order to solve the above problem. We also show a decidable sufficient condition for the context reducibility that used in the procedure. | |||||
| 言語 | en | |||||
| 出版者 | ||||||
| 出版者 | 一般社団法人電子情報通信学会 | |||||
| 言語 | ja | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプresource | http://purl.org/coar/resource_type/c_6501 | |||||
| タイプ | journal article | |||||
| 出版タイプ | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
| 関連情報 | ||||||
| 関連タイプ | isVersionOf | |||||
| 識別子タイプ | URI | |||||
| 関連識別子 | http://ci.nii.ac.jp/naid/110006388628 | |||||
| ISSN | ||||||
| 収録物識別子タイプ | PISSN | |||||
| 収録物識別子 | 0913-5685 | |||||
| 書誌情報 |
ja : 電子情報通信学会技術研究報告SS, ソフトウェアサイエンス 巻 107, 号 176, p. 7-12, 発行日 2007-07 |
|||||
| 著者版フラグ | ||||||
| 値 | publisher | |||||
| URI | ||||||
| 識別子 | http://ci.nii.ac.jp/naid/110006388628 | |||||
| 識別子タイプ | URI | |||||
| URI | ||||||
| 識別子 | http://hdl.handle.net/2237/21098 | |||||
| 識別子タイプ | HDL | |||||
