氏名: 和歌隆志 (l0571672)

論文題目: BDDに基づく通信プロセスの等価性判定アルゴリズムの実装


論文概要

本論文では、BDD(二分決定グラフ)を用いた通信プロセスの 等価性判定アルゴリズムの実装について、実行時間とメモリ使用量に ついて実験した。通信プロセスの体系としてCCSを用いた。 以下の2つのアルゴリズムについて実験を行った。(1)CCS式からすべての 遷移関係を直接求めBDDに変換する。(2)CCS式から各エージェントごとの 遷移関係を求めBDDに変換し、それらをBDD上で合成する。 (2)の実行結果は、状態数31457281のschedulerで、メモリ使用量0.8MB、 計算時間6.6秒であった。これらの結果から、 BDDは、通信プロセスの等価性判定には有効であると言える。 さらにメモリの使用効率をあげるために通信プロセスの等価性判定に 特化したBDDライブラリの実装を提案する。
目次に戻る