振舞等価性の証明のための等式付き書換えに基づく潜在帰納法
スポンサーリンク
概要
- 論文の詳細を見る
システムがどのように外部観測的に振舞うかを規定する振舞仕様の下で、観測を通してシステムの2つの状態が等しいことを振舞等価という。振舞等価性の自動証明法の一つに、潜在帰納法に基づく証明法が提案されている.しかし,この手法では簡約化順序で順序付けができない2つの項が存在するとき振舞等価性の証明に失敗する。本論文では、このような場合にも証明できるようにするために、等式付き書換えを用いた潜在帰納法に基づく証明法を提案する。さらに,完全な仕様の場合には手続き中の条件を判定可能な十分条件に置き換えられることを示す.
- 社団法人電子情報通信学会の論文
- 2007-07-26
著者
-
酒井 正彦
名古屋大学大学院情報科学研究科
-
西田 直樹
名古屋大学大学院情報科学研究科
-
坂部 俊樹
名古屋大学大学院情報科学研究科
-
草刈 圭一朗
名古屋大学大学院情報科学研究科
-
笹田 悠司
名古屋大学大学院情報科学研究科
-
草刈 圭一朗
名古屋大学 大学院情報科学研究科
-
酒井 正彦
名古屋大学
関連論文
- 基本対称関数に基づく節をもつCNF論理式の充足可能性判定(計算論,計算モデル)
- ビットエラー通信路におけるスケーラブルCANの動作解析
- 条件付き等式の変換に基づくプログラム生成 (ソフトウェアサイエンス)
- 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について (ソフトウェアサイエンス)
- シャローな依存対から構成される項書換え系の停止性の決定可能性
- 基本対称関数を付加したCNF論理式の充足可能性判定
- 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序
- プレスブルガー文付き項書換え系における書換え帰納法について
- フォーマルアプローチ論文特集の発行にあたって
- 例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム(ディペンダブルコンピューティング)