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

• Project/Area Number: 20700033
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: Waseda University
• Principal Investigator: 石井 大輔 Waseda University, 理工学術院, 助手 (00454025)
• Project Period (FY): 2008 – 2010
• Project Status: Completed (Fiscal Year 2010)
• Budget Amount: ¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000); Fiscal Year 2010: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2009: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2008: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: プログラム言語 / 探索・論理・推論アルゴリズム / ハイブリッドシステム / 区間解析 / 制約プログラミング / 探索・論理, 推論アルゴリズム

Research Abstract

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

Research Products

• [Journal Article] ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法 (2008)
  • Author(s): 石井大輔, 上田和紀, 細部博史
  • Journal Title: 情報処理学会論文誌数理モデル化と応用 1(1) Pages: 149-159
  • NAID: 110006827845
  • Peer Reviewed
• [Presentation] ハイブリッドシステムモデリング言語HydLaの統合処理系 (2010)
  • Author(s): 高田賢士郎, 廣瀬賢一, 大谷順司, 石井大輔, 細部樽史, 上田和紀
  • Organizer: 第12回プログラミンゲおよびプログラミング言語ワークショップ(PPL' 10)
  • Place of Presentation: 香川県琴平温泉
• [Presentation] ハイブリッドシステムモデリング言語HydLaの区間制約に基づく全解シミュレーション実行処理系 (2010)
  • Author(s): 大谷順司, 廣瀬賢一, 石井大輔, 細部博史, 上田和紀
  • Organizer: 情報処理学会創立50周年記念(第72回)全国大会
  • Place of Presentation: 東京大学
• [Presentation] 制約概念に基づくハイブリッドシステムモデリング言語HydLaの実装 (2009)
  • Author(s): 廣瀬賢一, 大谷順司, 石井大輔, 細部博史, 上田和紀
  • Organizer: 第11回プログラミングおよびプログラミング言語ワークショップ(PPL'09)
  • Place of Presentation: 岐阜県・高山市
  • Year and Date: 2009-03-10
• [Presentation] Simulation of Hybrid Systems based on Hierarchical Interval Constraints (2009)
  • Author(s): D. Ishii, K. Ueda, and H. Hosobe
  • Organizer: 2nd International Conference on Simulation Tools and Techniques (SIMUTools'09)
  • Place of Presentation: イタリア・ローマ
  • Year and Date: 2009-03-04
• [Presentation] Interval-based Solving of Hybr id Constraint Systems (2009)
  • Author(s): Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe, Alexandre Goldsztejn
  • Organizer: The 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS'09)
  • Place of Presentation: スペイン・サラゴサ
• [Presentation] An Interval-based SAT Modulo ODE Solver for Model Checking Nonlinear Hybrid Systems (2009)
  • Author(s): Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe
  • Organizer: Workshop on Verified Software : Theory, Tools, and Experiments (VSTTE'09)
  • Place of Presentation: オランダ・アイントホーフエン
• [Presentation] 制約階層によるハイブリッドシステムのモデリング手法 (2009)
  • Author(s): 廣瀬賢一, 大谷順司, 石井大輔, 細部博史, 上田和紀
  • Organizer: 日本ソフトウェア科学会第26回大会
  • Place of Presentation: 島根大学
• [Presentation] 不確実値を持つハイブリッドシステムの高信頼なシミュレーション手法 (2009)
  • Author(s): 大谷順司, 廣瀬賢一, 石井大輔, 上田和紀
  • Organizer: 第6回ディペンダブルシステムシンポジウム
  • Place of Presentation: 大阪大学
• [Presentation] 微分制約論理式によるハイブリッドシステムのモデリングと検証 (2009)
  • Author(s): 石井大輔, 上田和紀, 細部博史
  • Organizer: 電子情報通信学会コンカレント工学研究会
  • Place of Presentation: 横浜
• [Presentation] 制約概念に基づくハイブリッドシステムモデリング言語HydLa (2008)
  • Author(s): 上田和紀, 石井大輔, 細部博史
  • Organizer: 第5回システム検証の科学技術シンポジウム(SSV'08)
  • Place of Presentation: 筑波・筑波大学
  • Year and Date: 2008-11-17
• [Presentation] 制約概念に基づくハイブリッドシステムモデリング言語 (2008)
  • Author(s): 上田和紀, 石井大輔, 細部博史
  • Organizer: 日本ソフトウェア科学会第25回大会
  • Place of Presentation: 東京・筑波大学
  • Year and Date: 2008-09-11
• [Presentation] 区間演算を用いたODE Solverにおける任意精度演算の導入とパラメタ最適化 (2008)
  • Author(s): 廣瀬賢一, 石井大輔, 上田和紀
  • Organizer: FIT2008第7回情報科学技術フォーラム
  • Place of Presentation: 慶応大学
  • Year and Date: 2008-09-03
• [Presentation] ハイブリッドシステムの高信頼シミュレーションへの区間ニュートン法の適用 (2008)
  • Author(s): 石井大輔, 上田和紀, 細部博史
  • Organizer: 第6回ディペンダブルシステムワークショップ(DSW' 08summer)
  • Place of Presentation: 北海道・函館
  • Year and Date: 2008-07-03
• [Presentation] 数式処理・Quantifier Eliminationを用いたハイブリッドシステムのZeno状態の導出手法 (2008)
  • Author(s): 大野善之, 石井大輔, 上田和紀
  • Organizer: 人工知能学会第22回全国大会
  • Place of Presentation: 北海道・旭川市
  • Year and Date: 2008-06-11
• [Remarks]
  • URL: http://code.google.com/p/hcslib/http://code.google.com/p/hydlogic/