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

情報処理学会

書誌事項

タイトル別名
  • The Practical Method to Represent a Large Directed Graph

この論文をさがす

抄録

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

収録刊行物

詳細情報 詳細情報について

問題の指摘

ページトップへ