振舞等価性の証明のための等式付き書換えに基づく潜在帰納法

• 笹田, 悠司

• 酒井, 正彦

• 西田, 直樹

• 坂部, 俊樹

• 草刈, 圭一朗

• SASADA, Yuji

• SAKAI, Masahiko

• NISHIDA, Naoki

• SAKABE, Toshiki

• KUSAKARI, Keiichiro

書誌事項

タイトル別名

• フルマイ トウカセイ ノ ショウメイ ノ タメノ トウシキツキ カキカエ ニ モトズク センザイ キノウホウ
• Implicit Induction for Proving Behavioral Equivalence by Equational Rewriting

抄録

システムがどのように外部観測的に振舞うかを規定する振舞仕様の下で、観測を通してシステムの2つの状態が等しいことを振舞等価という。振舞等価性の自動証明法の一つに、潜在帰納法に基づく証明法が提案されている.しかし,この手法では簡約化順序で順序付けができない2つの項が存在するとき振舞等価性の証明に失敗する。本論文では、このような場合にも証明できるようにするために、等式付き書換えを用いた潜在帰納法に基づく証明法を提案する。さらに,完全な仕様の場合には手続き中の条件を判定可能な十分条件に置き換えられることを示す.

収録刊行物

• 電子情報通信学会技術研究報告SS, ソフトウェアサイエンス

  電子情報通信学会技術研究報告SS, ソフトウェアサイエンス 107 (176), 7-12, 2007-07

  一般社団法人電子情報通信学会

キーワード

• 振舞仕様
• 文脈可簡約性
• 項書換え系
• Knuth-Bendix完備化

詳細情報

• CRID: 1050845763733622016
• NII論文ID: 120005526507
• NII論文ID: 110006388628
• NII書誌ID: AA1123312X
• HANDLE: 2237/21098
• NDL書誌ID: 8895951
• ISSN: 09135685
• Web Site: https://nagoya.repo.nii.ac.jp/records/18994
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I8895951
• 本文言語コード: ja
• 資料種別: journal article
• データソース種別:
  • IRDB
  • NDL
  • CiNii Articles
  • KAKEN