2011 Fiscal Year Annual Research Report
非線形ハイブリッドシステムのための区間制約プログラミングにもとづくモデル検査技術
| Project/Area Number |
11J03810
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
石井 大輔 国立情報学研究所, アーキテクチャ科学研究系, 特別研究員(PD)
|
|---|
| Keywords | ハイブリッドシステム / 制約プログラミング / 区間解析 / プログラム検証 / satisfiability modulo theories |
|---|
| Research Abstract |
4月から12月にかけて仏パリの研究所INRIA Saclayを訪問し、当地およびナント大学の研究者と共同で研究活動を行った。帰国後は提案手法に関する実験作業および論文執筆に取り組んだ。従来行ってきたハイブリッドシステムと区間制約プログラミングの研究を進めるとともに、新たに演繹的プログラム検証技術を取り組み、統合的かつ実用的な枠組みの実現に向かっていると考えている。
INRIA Saclayにて所属したProvalチームでは、演繹的なプログラム検証フレームワークWhy3を拡張した、ハイブリッドシステムの安全性を検証するための枠組みを開発した。線形ハイブリッドオートマトンの無限ステップの実行に関する検証が可能な実装を行い、複数の例題を検証可能であることを示した。現在、提案手法に関する論文を準備中である。提案手法により、線形系の範囲では、これまで主流であった到達範囲の近似計算に基づく手法より広い範囲の問題を扱うことができた。今後、提案手法をより広範な系に適用し、実用的なツールを実現したいと考えている。
上記研究と並行し、区間制約プログラミングに関してナント大学と共同研究を行った。算術制約充足問題において、under-constrainedな場合(変数に対して制約が不足し、解が1点に定まらず集合となる場合)の解領域の射影を区間集合により精度よく近似する手法を提案した。提案手法では、従来手法に4点の改良を施し高速かつ汎用なソルバーを実現した。とくに、区間幅を増減させて区間内の解の存在保証を自動的に行う方法や、区間同士の重なりを考慮して探索空間を削減する方法等を提案した。提案手法を論文にまとめ、ジャーナルConstraintsに投稿した(条件付き採録の結果を得ている)。また、上記の枠組みを並列マニピュレータの可動範囲解析に応用した実験を行った。上記の研究に関して電子情報通信学会の研究会にて招待講演を行い好評を得た。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画通り、ハイブリッドシステムの無限実行ステップの検証手法と、存在量化子付き算術制約のための区間計算による求解手法を開発した。成果のアウトプットは24年度に予定している(論文1件、学会発表2件を投稿中)。
|
| Strategy for Future Research Activity |
計画通り、区間計算による求解手法をハイブリッドシステムの検証器に組み込み、非線形ハイブリッドシステムの多様な検証の実現を目指す。
|
