非線形ハイブリッドシステムのための区間制約プログラミングにもとづくモデル検査技術

点击翻译按钮获取中文摘要

並列ロボットを非線形数値制約として簡潔にモデリングし,区間制約プログラミング技術(branch and pruneアルゴリズム)を用いて安全な可動範囲の内部近似・外部近似を自動的に計算,可視化する手法および実装を開発した.本年度はとくに求解ヒューリスティックの分析・改善,応用的なロボットの解析手法(アーム間の衝突検出,障害物との衝突検出等)の開発に取り組んだ.提案手法により複数の未解決問題を解くことができた.提案手法では,任意の等式・不等式制約を連立した形式で諸々の問題を記述でき,また実装した区間制約ソルバーを用いて高速・自動的に結果を得ることができるため,既存手法に較べ簡便かつ高信頼である.本研究はナント大学のA. Goldsztejn研究員およびC. Jermann准教授と共同で進めた.研究成果を国際会議CPで発表し好評を得た.上記研究と並行し,プログラム検証技術に基づくハイブリッドシステムの検証手法を開発した.提案手法はハイブリッドオートマトンの実行を有限ステップ展開,抽象解釈し,周期的な構造になっていることと安全性条件を確認し,帰納的に検証を行う.本年度は提案手法の理論面を整備するとともに,Mathematicaを用いてツール実装および実験を行った.非線形ハイブリッドオートマトンの無限ステップの実行に関する安全性検証を半自動的に行うことを可能にし,既存ツールでは扱えなかった複数の検証事例を示した.またプログラム検証技術の多くはユーザがツールを対話的に利用する必要があり自動的ではなかったが,提案手法によりその負荷を軽減した.本研究は国立情報学研究所の中島震教授およびINRIASaclayのG. Melquiond研究員と共同で進めた.研究成果を国際会議iFMに投稿し受理された.ハイブリッドシステムを区間計算および記号計算に基づき扱う統合的かつ実用的な枠組みの実現を進めている.