2B-4
GPUを用いたブール行列の積および関係の推移的閉包の計算
○大塚 寛（愛媛大）
オートマトンに基づくモデル検査システムでは、システムが仕様を
満たすことをBuchiオートマトンの受理言語の空言語判定問題に帰
着して示す。空言語判定問題は、状態空間に対する2重の深さ優先
探索で行われる。この問題は有向グラフにおける可達性と見ること
もでき、また一方で、グラフの操作はグラフを接続行列で表した時
の行列の演算で行うこともできる。
この研究では、接続行列に対する計算のうち特に基本的なブール行
列の積とグラフの連結成分を求める推移的閉包の計算をGPUを用い
て高速化した結果を報告する。