ハイブリッドシステムのための区間解析に基づく高信頼実装技術

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

時間軸上を状態が連続変化するとともに、ある時点では状態・方程式系が離散変化するハイブリッドシステムを、簡潔に記述し、高信頼な実行を行うことを目指したハイブリッド並行制約プログラミング言語の実装技術として、下記の研究を行った。(a)ハイブリッド制約システム(以下「HCS」)の定式化と区間解析にもとづく実装初期状態から連続変化するハイブリッドシステムが、離散変化の判定条件を充たす時点と状態を求める問題をHCSとして定式化し、効率的な求解方法を開発してきた。本年度はまず、定式化を見なおし、既存の実数制約システムを、連続制約システム、HCSへと拡張していく枠組みとした。より広範なモデルを扱えるようになり、モデリングにおいて記述される種々の制約に対する分析への応用が期待できる。つぎに、昨年度開発した区間解析にもとづく実装を整備するとともに、計算した区間解中に理論解が唯一含まれるかどうかを保証する機能を実装した。(b)非線形なハイブリッドオートマトン(以下「HA」)の有界モデル検査法の開発HCSの求解を利用してハイブリッドシステムの到達性検証を行う手法を開発した。提案手法では、HAと危険領域とを入力とし、それらを方程式・不等式および微分方程式を命題に含んだ一階述語論理式の充足可能性判定問題に変換する。充足可能性判定手法として、(a)で述べた実装と、既存のSAT(命題論理式の充足可能性判定)求解系を接続した方法を設計、実装した。実装を用いて非線形HAを検証する実験をおこない、既存のPHAVerとHSolverでは求解できなかった問題を解の存在保証付きで求解することができた。(c)ハイブリッド並行制約プログラミング言語HydLaの開発HydLaプログラム中の制約階層を解決する方法(発表3)と、区間解析にもとづくシミュレーション方法(発表4)の開発に貢献した。