| 研究課題/領域番号 |
17K00098
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2020-03-31
|
| キーワード | BDD / d-DNNF / 投射モデル計数 / 量的情報流解析 |
|---|
| 研究実績の概要 |
平成３０年度は、プログラムの動的量的情報流解析への応用のために、与えられた命題論理式と投射変数集合に対するすべての投射モデル集合を表すデータ表現を生成するツールの開発を行った。これまでは投射モデル数のみを求めるソルバを開発してきたが、動的情報流解析に応用するためには特定の論理式に対して異なる追加条件を加えては繰り返し計数する必要がある。そこで、論理式と投射変数集合からモデル計数・列挙が容易になる表現をあらかじめ生成しておくことで、追加条件が与えられてから計数結果が得られるまでの実行時間の短縮を図る。与えられた命題論理式から、論理関数の簡潔な表現として知られる2分決定図（Binary Decision Diagram）やd-DNNF（deterministic decomposable negation normal form）に変換する手法やツールはすでに存在していたが、投射モデル集合を表現するBDDやd-DNNFを生成するツールが存在しなかった。平成３０年度は、これまでに利用してきた投射モデル計数技術を活用して、投射モデル集合を表現するBDDおよびd-DNNFを生成するツールを開発した。BDDについては命題論理式の通常のモデル集合のための既存の構成ツールに投射モデル計数の手法を組み込むことで実現した。d-DNNFについては、我々の研究グループで開発した投射モデル計数GPMCの計算過程が自然にd-DNNF形式と対応することを利用することで実現した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
投射モデル集合を表現するBDDおよびd-DNNFを生成するツールの開発と、それを実際にプログラムの動的情報流解析に利用して一定の有用性を確認した。また、これまでの成果を整理して実装した投射モデル計数ソルバGPMCを自身のWEBページで公開した。
|
| 今後の研究の推進方策 |
平成30年度はBDDおよびd-DNNF構成ツールの開発に注力したが、引き続き投射モデル計数ソルバの高速化に取り組む。まず、成分キャッシュの削除ヒューリスティクスの検討のための実験を行う。次に、最近Lagniezらによって発表された投射モデル計数アルゴリズムとの性能比較を行い、GPMCやその他ソルバを組み合わせたポートフォリオ型などの並列ソルバを検討する。
|
| 次年度使用額が生じた理由 |
本年度の研究成果を年度内にまとめきれず成果発表や論文執筆まで至らなかった。次年度にそれらの成果の発表および論文投稿を計画している。
|
