2024-03-29T01:11:44Z
https://nagoya.repo.nii.ac.jp/oai
oai:nagoya.repo.nii.ac.jp:00018994
2023-01-16T04:32:23Z
312:313:314
振舞等価性の証明のための等式付き書換えに基づく潜在帰納法
Implicit Induction for Proving Behavioral Equivalence by Equational Rewriting
笹田, 悠司
酒井, 正彦
西田, 直樹
坂部, 俊樹
草刈, 圭一朗
SASADA, Yuji
SAKAI, Masahiko
NISHIDA, Naoki
SAKABE, Toshiki
KUSAKARI, Keiichiro
open access
(c)一般社団法人電子情報通信学会。本文データは学協会の許諾に基づきCiNiiから複製したものである
振舞仕様
文脈可簡約性
項書換え系
Knuth-Bendix完備化
システムがどのように外部観測的に振舞うかを規定する振舞仕様の下で、観測を通してシステムの2つの状態が等しいことを振舞等価という。振舞等価性の自動証明法の一つに、潜在帰納法に基づく証明法が提案されている.しかし,この手法では簡約化順序で順序付けができない2つの項が存在するとき振舞等価性の証明に失敗する。本論文では、このような場合にも証明できるようにするために、等式付き書換えを用いた潜在帰納法に基づく証明法を提案する。さらに,完全な仕様の場合には手続き中の条件を判定可能な十分条件に置き換えられることを示す.
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.
一般社団法人電子情報通信学会
2007-07
jpn
journal article
VoR
http://hdl.handle.net/2237/21098
https://nagoya.repo.nii.ac.jp/records/18994
http://ci.nii.ac.jp/naid/110006388628
0913-5685
電子情報通信学会技術研究報告SS, ソフトウェアサイエンス
107
176
7
12
https://nagoya.repo.nii.ac.jp/record/18994/files/110006388628.pdf
application/pdf
863.6 kB
2018-02-21