研究課題
基盤研究(C)
本研究はSAT/SMTソルバによるパーフェクトサンプリング手法の実用化を行う.パーフェクトサンプリングとはマルコフ連鎖の定常解に従うサンプルを厳密にサンプリングする手法であり,数理的には無限時間のシミュレーションを有限時間で実行することに対応する.これはモデルの検証・評価において非常に強力な性質となる.SAT/SMTソルバを用いたパーフェクトサンプリング手法は超多状態システムに対しても適用できる手法であるが,実行速度や検証可能なモデルの制限なの問題点がある.本研究では,SAT/SMTソルバに与える式の簡略化と,準定常解と呼ばれる一般的な解を利用した拡張によりこれらの問題点の解決を目指す.