2014 Fiscal Year Annual Research Report
区間制約プログラミングと演繹的推論に基づくハイブリッドシステムの検証技術
| Project/Area Number |
25880008
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
石井 大輔 東京工業大学, 情報理工学(系)研究科, 助教 (00454025)
|
|---|
| Project Period (FY) |
2013-08-30 – 2015-03-31
|
| Keywords | ハイブリッドシステム / 制約プログラミング / 探索・論理・推論アルゴリズム / 区間解析 / 並列分散処理 / 国際研究者交流 |
|---|
| Outline of Annual Research Achievements |
区間計算を拡張した平行体計算に基づく非線形ハイブリッドシステムのシミュレーション手法をフランスCNRSのA. Goldsztejn研究員と共同で開発しており、実験と論文執筆を進めている。このシミュレーション手法を利用し、非線形ハイブリッドオートマトンに関して有界線形時相論理式で記述した性質を検証する手法を開発した。数値計算を用いる従来手法に較べ、提案手法では数値誤差の精度保証を行うため、高信頼な検証が可能になる。さらに、この検証手法を用いてハイブリッドオートマトンの高信頼な統計的モデル検査を行う実験を行い、平行体計算に基づく提案手法の有用性を示した。区間計算を用いたハイブリッドシステムの検証技術について調査し、その成果を記述した解説論文が計測自動制御学会の学会誌に掲載された。
非線形の実数方程式・不等式系を区間計算と探索に基づき求解するソルバーRealpaverをプロセスレベルで並列化する手法を開発した。昨年度開発した並列ソルバーに対し、X10言語のGLBライブラリを用いて負荷分散機構および終了判定機構の改良を施したところ、スーパーコンピュータTSUBAME2.5の50ノード・600コア上で、最大516倍の実行速度向上が得られた。昨年度の成果を制約プログラミングに関する国際会議CPにて発表した。
|
| Research Progress Status |
26年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
26年度が最終年度であるため、記入しない。
|
