2020 Fiscal Year Research-status Report

A Development of Perfect Sampling with SAT/SMT Solvers

Research Project

Project/Area Number	20K11694
Research Institution	Hiroshima University
Principal Investigator	岡村寛之広島大学, 先進理工系科学研究科(工), 教授 (10311812)
Project Period (FY)	2020-04-01 – 2023-03-31
Keywords	シミュレーション / パーフェクトサンプリング / マルコフ過程 / SAT/SMTソルバ
Outline of Annual Research Achievements	令和2年度は主にGSPNへの適用するための改良を行った．GSPNへの適用に関しては遅延時間なしのトランジション（瞬時トランジション）の取り扱いが重要となる．瞬時トランジションを扱う場合，瞬時トランジションが指数トランジションよりも優先して発火するため，元の確率過程と時間軸が異なる確率過程を考慮する必要があった．その点に関して，本研究では (i) GSPN における瞬時トランジションを指数トランジションに置き換えた SPN を構成，(ii) その SPN の定常分布がもとの GSPN 定常分布と同じになるような棄却サンプリングを導出することで，GSPN に対するパーフェクトサンプリングアルゴリズムの開発を行った． GSPN に対してはSAT/SMTの式を直接的に修正して対応することも可能であるが，この手法では SAT/SMT の式における変数が瞬時トランジションの数に対して指数的に増加することになり実用性に欠ける．一方で，今回提案した手法では瞬時トランジションが増えたとしても，SAT/SMTの式における変数の増加は，SPN上でトランジションを増加した場合と同じであるため，直接的な手法よりもかなり効率的に抑えることができる．さらに，SPNに対するパーフェクトサンプリング手法を直接適用できるためアルゴリズムそのものが極めてシンプルに構成でき，実装面においても非常に有利である．一方で棄却サンプリング法を利用しているため，最終的に得られた定常分布からのサンプルを棄却するケースがありサンプリングの効率性を上げるための調整が必要となり，この点において改良の余地がある． GSPN は SPN と比較すると実システムの表現において格段に表現能力が上がるため，今回の成果は応用面において非常に高い成果であるとが考えられる．
Current Status of Research Progress	Current Status of Research Progress 3: Progress in research has been slightly delayed. Reason 令和2年度の計画では GSPN に加えて MRSPN のパーフェクトサンプリングについても検討する予定であった．こちらについては米国 Duke 大学のTrivedi教授の知見を得ながら進めようと計画していたが，新型コロナウィルスにより渡米ができなかったため当初計画していた部分が実行できなかった．そのため MRSPN に対するパーフェクトサンプリングの開発が位相近似を適用したものだけとなり，より効率的な MRSPN に特化したアルゴリズムの開発にはいたらなかった．
Strategy for Future Research Activity	令和3年度は，まず当初，令和2年度に計画していた MRSPN へのより効率的なパーフェクトサンプリング手法についての検討を行う．次に，FSPNで記述されたハイブリッドシステムへの適用を行う．FSPNでは連続量のトークンが存在するため最初に常微分方程式で記述された連続システム（確定的なシステム）に対する定常解析をSAT/SMTソルバで解くアプローチについて考察する．その後，連続システムに対するアルゴリズムとパーフェクトサンプリング手法をあわせることを検討する．連続システムでは，微分方程式に対してオイラー法などの数値解法による離散化したモデルに対してSAT/SMTソルバによるアプローチを展開する．また別の離散化として，連続量のビット表現による離散化も検討する．GSPN/MRSPNへの手法と同様にこれらの成果についても Python ならびに Julia パッケージとして配布可能にする．
Causes of Carryover	新型コロナウィルスで予定していた国際会議や国内研究集会が中止やオンライン開催となり，旅費および参加費が少額になったため．次年度使用額は令和３年度に行われる国際会議や研究集会の参加費に利用する．