• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 11J03810
Research Category

Grant-in-Aid for JSPS Fellows

Allocation TypeSingle-year Grants
Section国内
Research Field Software
Research InstitutionNational Institute of Informatics

Principal Investigator

石井 大輔  国立情報学研究所, アーキテクチャ科学研究系, 特別研究員(PD)

Project Period (FY) 2011 – 2013
Project Status Declined (Fiscal Year 2012)
Budget Amount *help
¥1,400,000 (Direct Cost: ¥1,400,000)
Fiscal Year 2012: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2011: ¥800,000 (Direct Cost: ¥800,000)
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

当初の予定通り,存在量化子付き数値制約のための区間計算による求解手法およびロボティクスへの応用と,ハイブリッドシステムの実行の周期性を判定し,無限実行ステップの安全性検証を行う代数的手法を開発した.ロボティクス応用では,ロボティクス研究者からの要望を受け,アーム間の衝突検出等の追加実験を行った.その他に予定していた区間計算による周期性判定の方法と,線形制約求解の高速化については今後の課題とする.

Report

(2 results)
  • 2012 Annual Research Report
  • 2011 Annual Research Report
  • Research Products

    (12 results)

All 2013 2012 2011 Other

All Journal Article (2 results) (of which Peer Reviewed: 2 results) Presentation (8 results) Remarks (2 results)

  • [Journal Article] Interval-Based Projection Method for Under-Constrained Numerical Systems2012

    • Author(s)
      石井大輔, Alexandre Goldsztejn, Christophe Jermann
    • Journal Title

      Constraints Journal

      Volume: 17(4) Issue: 4 Pages: 432-460

    • DOI

      10.1007/s10601-012-9126-y

    • Related Report
      2012 Annual Research Report
    • Peer Reviewed
  • [Journal Article] An Interval-based SAT Modulo ODE Solver for Model Checking Nonlinear Hybrid Systems2011

    • Author(s)
      石井大輔、上田和紀、細部博史
    • Journal Title

      International Journal on Software Tools for Technology Transfer (STTT)

      Volume: 13 Issue: 5 Pages: 449-461

    • DOI

      10.1007/s10009-011-0193-y

    • Related Report
      2011 Annual Research Report
    • Peer Reviewed
  • [Presentation] Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus2013

    • Author(s)
      石井大輔, Guillaume Melquiond, 中島震
    • Organizer
      10th International Conference on integrated Formal Methods (iFM'13)
    • Place of Presentation
      Turku, Finland(発表確定)
    • Related Report
      2012 Annual Research Report
  • [Presentation] Why3を用いたハイブリッドシステムの検証2012

    • Author(s)
      石井大輔, 中島震, G. Melquiond
    • Organizer
      第10回ディペンダブルシステムワークショップ(DSW'12)
    • Place of Presentation
      神戸・計算科学研究機構
    • Year and Date
      2012-12-11
    • Related Report
      2012 Annual Research Report
  • [Presentation] A Branch and Prune Algorithm for the Computation of Generalized Aspects of Parallel Robots2012

    • Author(s)
      Stephane Caro, Damien Chablat, Alexandre Goldsztejn, 石井大輔, Christophe Jermann
    • Organizer
      18th International Conference on Principles and Practice of Constraint Programming (CP'12)
    • Place of Presentation
      Quebec City, Canada
    • Year and Date
      2012-10-09
    • Related Report
      2012 Annual Research Report
  • [Presentation] 制約不足の数値制約充足問題のための区間計算に基づく射影手法2012

    • Author(s)
      石井大輔, Alexandre Goldsztejn, Christophe Jermann
    • Organizer
      日本ソフトウェア科学会第29回大会
    • Place of Presentation
      東京・法政大学
    • Year and Date
      2012-08-23
    • Related Report
      2012 Annual Research Report
  • [Presentation] HydLa : A High-Level Language for Hybrid Systems2012

    • Author(s)
      上田和紀, 松本翔太, 竹口輝, 細部博史, 石井大輔
    • Organizer
      Logics for System Analysis (LfSA'12)
    • Place of Presentation
      Berkeley, USA
    • Year and Date
      2012-07-07
    • Related Report
      2012 Annual Research Report
  • [Presentation] 区間制約プログラミングの研究事例2012

    • Author(s)
      石井大輔
    • Organizer
      電子情報通信学会・SS/MSS合同研究会
    • Place of Presentation
      高知市文化プラザかるぽーと(招待講演)
    • Year and Date
      2012-01-27
    • Related Report
      2011 Annual Research Report
  • [Presentation] Computation of generalized aspect of parallel manipulators2011

    • Author(s)
      石井大輔、A.Goldsztejn
    • Organizer
      The 4^<th> Small Workshop on Interval Methods
    • Place of Presentation
      仏ブルージュ・PRISME
    • Year and Date
      2011-06-14
    • Related Report
      2011 Annual Research Report
  • [Presentation] A parallelotope method for the simulation of nonlinear hybrid systems2011

    • Author(s)
      A.Goldsztejn、石井大輔
    • Organizer
      The 4^<th> Small Workshop on Interval Methods
    • Place of Presentation
      仏ブルージュ・PRISME
    • Year and Date
      2011-06-14
    • Related Report
      2011 Annual Research Report
  • [Remarks] Generalized Aspects of Parallel Robots

    • URL

      http://dsksh.com/aspects/

    • Related Report
      2012 Annual Research Report
  • [Remarks] Generalized Aspects of Parallel Robots

    • URL

      http://dsksh.com/aspects/

    • Related Report
      2011 Annual Research Report

URL: 

Published: 2011-12-12   Modified: 2024-03-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi