2016 Fiscal Year Research-status Report
連続・離散ハイブリッド領域のための区間制約プログラミング技術
| Project/Area Number |
15K15968
|
|---|
| Research Institution | University of Fukui |
|---|
Principal Investigator |
石井 大輔 福井大学, 学術研究院工学系部門, 講師 (00454025)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | ハイブリッドシステム / 制約プログラミング / 区間制約 / 探索・論理・推論アルゴリズム |
|---|
| Outline of Annual Research Achievements |
ハイブリッドシステムの高信頼な解析を可能にすることを目標に、下記の3項目を実施した。
(a) 非線形式で記述されるハイブリッドオートマトンと、その振る舞いに関する性質記述とを入力とし、振る舞いのシミュレーションと性質の成否判定を区間計算により高信頼に実施するためのツールHySIAの整備を行った。HySIAを用いて、これまでに提案してきた専用の区間計算手法の性能を評価したり、非線形ハイブリッドシステムを複数例示したりして良好な実験結果を得た。
(b) ハイブリッドシステムの専用モデリング言語や対話的インターフェースを備えるAcumenツール上に、信号時相論理に基づくモニタリング機能と統計的モデル検査機能を実装した。これにより、Acumen付属の多数の例題に対し、Acumenのシミュレーションエンジン切り替え機能を使って、柔軟な検証を行う環境を実現した。
(c) これまで開発してきた区間制約充足問題用の並列ソルバーを改変し、最適化問題用の並列ソルバーを構築した。一部の問題インスタンスについて良好な速度向上を得た。また並列化にあたっては、並列探索用の負荷分散ライブラリに暫定的な最適値をワーカ間で伝播する機能を追加するアプローチをとっているため、ライブラリを一般の最適化問題の並列求解にも利用することができる。
(d) 産業界で用いられている MATLAB/Simulink の大規模・複雑なモデルを調査した。モデルに対し、静的解析のみを用いた検証は難しく、数値シミュレーションに基づく検証手法や、区間解析による部分的な静的解析が有用であることを確認した。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
実績 (a) で開発したツールHySIAは使用アルゴリズム・実装がともに複雑なものとなり、ツール自体の信頼性を確保しながら開発を進めるのが難しくなった。そこで実績 (b) では既存のツールAcumenを利用して見通しのよい再実装に取り組み、今後 (a) と同等の機能を実装する予定である。
当初予定していたベクトル場の区間近似計算や、ハイブリッドシステム検証器の並列化は実施していない。
並列区間制約ソルバーは最適化問題を扱えるよう拡張した。
|
| Strategy for Future Research Activity |
下記2項目に取り組み、並列ハイブリッドシステム検証器の開発を進め、応用実験を行う。
(a) ハイブリッドシステムのモニタリング機能と統計的モデル検査機能の開発を進め、新しい頑強度の定義、統計的評価手法、区間解析手法などを新たに実装し、大規模・複雑なモデルを扱うことが可能なツールの実現を目指す。
(b) 区間制約最適化問題とハイブリッドシステム検証について、1000コア程度までスケール可能な並列化に取り組む。
|
| Causes of Carryover |
実際の使用額と予算が正確に一致しなかったため。
|
| Expenditure Plan for Carryover Budget |
消耗品の購入等に充てる予定である。
|
