2013 Fiscal Year Annual Research Report
区間制約プログラミングと演繹的推論に基づくハイブリッドシステムの検証技術
| Project/Area Number |
25880008
|
|---|
| Research Category |
Grant-in-Aid for Research Activity Start-up
|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
石井 大輔 東京工業大学, 情報理工学(系)研究科, 助教 (00454025)
|
|---|
| Project Period (FY) |
2013-08-30 – 2015-03-31
|
| Keywords | ハイブリッドシステム / 制約プログラミング / 区間解析 / 並列計算 / 演繹的推論 / 国際研究者交流: フランス、スウェーデン |
|---|
| Research Abstract |
(a) 数値制約充足問題を求解する区間制約ソルバーと (b) ハイブリッドシステムの演繹的検証器との深化発展を目指し，下記の3項目を実施した．
1. 区間制約ソルバーの並列化：区間制約ソルバーRealpaverの探索に基づく求解処理をプロセスレベルで並列化する手法を開発した．提案手法では求解ワーカを各コア上に配置し，まず1ワーカから全ワーカへ探索木を展開・分散し，その後ワーカ間で動的負荷分散しながら求解を行う．提案手法をX10言語で実装し，SGI UV1000の256コアを用いて約120倍の速度向上，TSUBAME2の50ノード・600コアを用いて約200倍の速度向上が得られることを確認している．成果について情報処理学会HPC研究会にて発表した．
2. 数式処理に基づくハイブリッドシステムの演繹的検証：昨年度から継続し，数式処理系Mathematicaにハイブリッドオートマトンをエンコードし，帰納法に基づき安全性検証を実施する手法の開発に取り組んだ．研究成果を国際会議iFM (Integrated Formal Methods) および日本ソフトウェア科学会全国大会にて発表し，後者に関して高橋奨励賞を受賞した．
3. 区間制約プログラミングに基づく非線形ハイブリッドシステムの到達領域の計算手法：昨年度から継続し，区間計算を拡張した平行体計算に基づく非線形ハイブリッドシステムのシミュレーション手法の開発に取り組んだ．提案手法により離散変化計算におけるラッピング効果を軽減し，複数の例題についてシミュレーション可能な離散変化数が数百倍に向上することを確認した．本研究は仏CNRSのA. Goldsztejn研究員と共同で実施している．研究成果を電子情報通信学会のMSS研究会にて発表した．また本研究に関してスウェーデン・ハルムスタッド大学のW. Taha教授らと議論を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究計画に従い，区間制約ソルバーの並列化を行い，数百コアを用いて提案手法による速度向上が得られることを示した．
数式処理に基づく演繹的検証手法に関しては，ループ不変条件を対話的に生成する必要があり，これを自動化する方法を検討予定だったが未着手である．
非線形ハイブリッドシステムの到達領域の計算手法に関しては，計画通り平行体による近似計算手法を開発し，高精度な区間計算を可能にした．
|
| Strategy for Future Research Activity |
前年度から継続し，(a) 並列区間制約ソルバーと，(b) 区間制約ソルバーおよび数式処理系を基本技術としたハイブリッドシステムの検証器について，下記のように開発を進める．
(a) 前年度は探索空間を分散することによる並列化に取り組んだが，今年度は求解パラメタをポートフォリオ方式で冗長化することによる並列化に取り組み，さらに前年度成果とのハイブリッド手法に取り組む．これらの手法により開発中のソルバーをさらに高速化し，ロボティクスの到達範囲計算を実施する．
(b) バックエンドソルバーとして区間制約ソルバーおよび数式処理系を用いた検証器の開発に，2つのアプローチで取り組む．まず区間制約ソルバーおよび数式処理系を統合した演繹的検証のアプローチに取り組む．区間制約ソルバーを用いてパラメタ入りハイブリッドシステムの状態空間を計算する手法を検討する．本手法を前年度成果の演繹的検証の枠組みに組み込み， 安全性検証を実施可能にする．つぎに統計的モデル検査のアプローチに取り組む．前年度成果の平行体計算による非線形ハイブリッドシステムのシミュレーション手法を利用し，与えられた問題について，サンプル軌道群のシミュレーション・検証とその結果の統計的評価を行う手法を開発する．上記2つのアプローチにより，広範な非線形ハイブリッドシステムの安全性および、その他安定性等の性質に関する、検証を実施可能にすることを目指す．
|
