大規模有向グラフの効率的記憶法 : アニーリング法を利用したラベル付け

概要

論文の詳細を見る
並行プログラムの解析や検証において、並行プログラムの挙動を、インターリーブ意味論に基づきグローバルな状態グラフで表現することが多い。例えば時相論理を用いた論理的検証では、検証項目を時相論理式fで記述し、プログラムから生成された状態グラフMがfのモデルになっているか否かを調べる。ところで、扱う並行プログラムが大規模になるに従い、生成される状態グラフのサイズは非常に大きくなり、例えば、我々が通常扱う並行プログラムでは、数万から数十万状態となってしまう。そこで必要となるのが、状態グラフ等の大規模有向グラフを、効率的に記憶する方法である。さて、有向グラフの効率的記憶法の一つとして、2分決定グラフ(BDD: Binary Decision Diagram)[1]を利用したグラフ表現方法がClarkeらにより提案されている[2]。この方法では、有向グラフの各ノードに識別のためのラベル付けカミ行なわれるが、ラベル付けの方法によっては、BDD表現による効果が十分に出ないことがある。そこで、我々はBDD表現に効果的なラベル付け法を提案する。
一般社団法人情報処理学会の論文
1991-02-25