2012 Fiscal Year Annual Research Report
非線形ハイブリッドシステムのための区間制約プログラミングにもとづくモデル検査技術
| Project/Area Number |
11J03810
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
石井 大輔 国立情報学研究所, アーキテクチャ科学研究系, 特別研究員(PD)
|
|---|
| Project Period (FY) |
2011 – 2013-03-31
|
| Keywords | ハイブリッドシステム / 制約プログラミング / 区間解析 / プログラム検証 / satisfiability modulo theories |
|---|
| Research Abstract |
並列ロボットを非線形数値制約として簡潔にモデリングし,区間制約プログラミング技術(branch and pruneアルゴリズム)を用いて安全な可動範囲の内部近似・外部近似を自動的に計算,可視化する手法および実装を開発した.本年度はとくに求解ヒューリスティックの分析・改善,応用的なロボットの解析手法(アーム間の衝突検出,障害物との衝突検出等)の開発に取り組んだ.提案手法により複数の未解決問題を解くことができた.提案手法では,任意の等式・不等式制約を連立した形式で諸々の問題を記述でき,また実装した区間制約ソルバーを用いて高速・自動的に結果を得ることができるため,既存手法に較べ簡便かつ高信頼である.本研究はナント大学のA. Goldsztejn研究員およびC. Jermann准教授と共同で進めた.研究成果を国際会議CPで発表し好評を得た.
上記研究と並行し,プログラム検証技術に基づくハイブリッドシステムの検証手法を開発した.提案手法はハイブリッドオートマトンの実行を有限ステップ展開,抽象解釈し,周期的な構造になっていることと安全性条件を確認し,帰納的に検証を行う.本年度は提案手法の理論面を整備するとともに,Mathematicaを用いてツール実装および実験を行った.非線形ハイブリッドオートマトンの無限ステップの実行に関する安全性検証を半自動的に行うことを可能にし,既存ツールでは扱えなかった複数の検証事例を示した.またプログラム検証技術の多くはユーザがツールを対話的に利用する必要があり自動的ではなかったが,提案手法によりその負荷を軽減した.本研究は国立情報学研究所の中島震教授およびINRIASaclayのG. Melquiond研究員と共同で進めた.研究成果を国際会議iFMに投稿し受理された.
ハイブリッドシステムを区間計算および記号計算に基づき扱う統合的かつ実用的な枠組みの実現を進めている.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の予定通り,存在量化子付き数値制約のための区間計算による求解手法およびロボティクスへの応用と,ハイブリッドシステムの実行の周期性を判定し,無限実行ステップの安全性検証を行う代数的手法を開発した.ロボティクス応用では,ロボティクス研究者からの要望を受け,アーム間の衝突検出等の追加実験を行った.その他に予定していた区間計算による周期性判定の方法と,線形制約求解の高速化については今後の課題とする.
|
