氏名: 市川 純一 (m953403)
論文題目: 通信プロセスの等価性判定アルゴリズムのＢＤＤを用いたメモリ効率最適化
論文概要
本論文では通信プロセスの等価性判定を効率的に行なうために、
BDDの変数順序を動的に変更する手法を提案する。
通信プロセスではプロセスの非決定性が原因で、
等価性を判定するのに莫大な時間とメモリが必要となる。
そのため実用的なレベルのプロセスに対する等価性の判定は、
一般的には非常に困難である。
本研究ではこうした問題を克服するために、
データ構造にBDD(二分決定グラフ)を導入し、
等価性判定の効率的実現を行なった。
BDDは論理関数のグラフによる表現で、
変数の順序を固定し、冗長な節点の削除と
等価な部分グラフの共有を可能な限り行なうことで、
論理関数をコンパクトかつ一意に表すことができる。
通信プロセスの等価性判定は、
μ計算における論理式の真偽判定
に帰着できることから、
プロセスの振舞いをBDDで表現することにより、
BDDを用いた効率の良い等価性判定を行なうことが期待できる。
BDDでは変数の順序を変えると、
同じ論理関数でも異なる表現となり、
そのノード数が大きく変化する場合がある。
BDDのノード数は処理速度や必要記憶量に大きく影響するので、
ノード数を少なくする変数順序を定めることが重要である。
しかし変数順序の与え方については、
万能な方法が得られていないのが実情である。
そこで我々は変数順序を動的に変更することにより、
効率的にBDDを構成する手法を提案する。
等価性判定の計算を行なう過程で、
その計算に適した変数順序を与えることができれば、
より効率的に等価性判定を行なうことができる。
本論文では、通信プロセスからBDDを構成していくまでの
手順について述べると共に、通信プロセスにおけるBDDの
変数順序の定め方について議論する。
さらに例を通して通信プロセスの等価性判定に
適しているBDDの変数順序を定めることで、
本方法の有効性を確認する。
その結果、状態数が10万を越えるようなプロセスに対しても、
等価性の判定を行なえることが明らかになった。
目次に戻る