二分決定グラフを用いたプログラム検証の自動化に関する研究

1997 Fiscal Year Annual Research Report

• Project/Area Number: 09780231
• Research Institution: Ibaraki University
• Principal Investigator: 近藤 久 茨城大学, 工学部, 助手 (40261739)
• Keywords: 二分決定グラフ / プログラム検証 / 停止性 / 項書換え系

Research Abstract

今年度は,対象とするプログラムを項書換え系に絞り,その停止性検証の自動化に関する研究を行なった.その概要は以下のようにまとめられる.
1.停止性の検証に最もよく用いられる方法は,経路順序と呼ばれるクラスに属する半順序>を適当に定め,すべての書換え規則について(左辺)>(右辺)の成立を確認することである.経路順序は関数記号の集合上の半順序(優先順位)を項の集合上に拡張して得られる.この優先順位を決定する問題は,経路順序の定義と(左辺)>(右辺)という条件を制約とする制約充足問題となる.
2.1.で述べた問題に二分決定グラフを適用するために,辞書式経路順序を論理関数として定義した.さらに,優先順位の性質(推移性,非反射性)を推移性条件,非反射性条件として定義し,辞書式経路順序による停止性の証明可能性を論理関数として定義した.
3.2.で定義した停止性の証明可能性を表す論理関数を二分決定グラフで発表し停止性を検証するアルゴリズムを考案した.アルゴリズムに基づきLISP言語によりプログラムを作成し,数多くの実験を行なった.
4.実験結果に基づき,二分決定グラフの利用の際に重要となる制約順序と変数順序に関する考察を行なった.この考察に基づきプログラムを改良し,効率を改善した.この際,制約順序,変数順位の決定に利用できる幾つかのヒューリスティクスを得ることができた.
これまでの研究業績を学会発表,論文誌に投稿(採録決定)した.次年度は完備化手続きに対して,本年度得られた成果を適用する予定である.

Research Products

• [Publications] 近藤 久: "二分決定グラフを用いた項書換え系の停止性検証システム" 人工知能学会誌. 13・5(掲載予定). (1998)
• [Publications] 近藤 久: "二分決定グラフを用いた書換え型プログラムの停止性検証器" 情報処理学会研究報告. 97・112. 1-6 (1997)
• [Publications] 尾形 達哉: "二分決定グラフを用いた書換え型プログラムの停止性検証システム" 人工知能学会全国大会(第11回)論文集. 108-111 (1997)