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

超準解析を用いたハイブリッドシステム検証

Research Project

Project/Area Number 15J05580
Research Category

Grant-in-Aid for JSPS Fellows

Allocation TypeSingle-year Grants
Section国内
Research Field Theory of informatics
Research InstitutionThe University of Tokyo

Principal Investigator

木戸 肩吾  東京大学, 情報理工学系研究科, 特別研究員(DC1)

Project Period (FY) 2015-04-24 – 2018-03-31
Project Status Completed (Fiscal Year 2017)
Budget Amount *help
¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 2017: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2016: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2015: ¥900,000 (Direct Cost: ¥900,000)
Keywords物理情報システム / ハイブリッドシステム / 遅延 / 形式手法 / 到達可能性解析 / 近似相模倣 / モデルベース開発 / 形式検証 / サイバーフィジカルシステム / 超準解析
Outline of Annual Research Achievements

採用当初は超準解析を用いたハイブリッドシステム検証に絞って研究を進めていたが,昨年度の報告書にも記述したように,昨年度からは制御論からのハイブリッドシステムへのアプローチもサーベイし,より広い視野でハイブリッドシステムの検証に向けて研究を行ってきた.本年度は,昨年度のカナダ・University of Waterlooへの研究訪問の際に着想を得て,センシングからアクチュエーションまでに遅延を含むハイブリッドシステムの到達可能性解析を,制御論的な議論により,遅延を含まない理想的なハイブリッドシステムの到達可能性解析に帰着する手法を提案した.本手法では,遅延を含むシステムと遅延を含まない理想的モデルの同時刻における状態を比べる距離を考え,増分安定性という安定性を仮定のもと制御論的な議論により近似相模倣という関係を作ることでその距離の過大近似を求める.本研究で扱う遅延は,物理的に離れたコントローラとプラントがネットワークで繋がれているネットワークコントロールシステムの分野で広く研究されているが,提案手法は特に増分安定性の仮定により非線形なシステムにも対応する点が特徴である.本結果は2018年7月に開催されるハイブリッドシステムに関する国際学会ADHS2018に採択された.
本手法をさらに拡張し,遅延を含むシステムと遅延を含まないモデルの同時刻における状態の差ではなく,比較する時刻にズレを許すことで,到達可能性解析やその他の時相論理式で表される性質の検証に関してより精度の高い結果を得ることができる手法も提案した.具体的には,Skorokhod距離と呼ばれる距離の過大近似を求められるようにシステム間の距離を定義し直し,その距離を近似相模倣により上から抑える手法となっている.こちらは物理情報システムに関する国際ワークショップCyPhy2017のポストプロシーディングスに投稿済みである(査読中).

Research Progress Status

29年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

29年度が最終年度であるため、記入しない。

Report

(3 results)
  • 2017 Annual Research Report
  • 2016 Annual Research Report
  • 2015 Annual Research Report
  • Research Products

    (9 results)

All 2018 2016 2015 Other

All Int'l Joint Research (3 results) Journal Article (2 results) (of which Int'l Joint Research: 2 results,  Peer Reviewed: 2 results,  Open Access: 1 results,  Acknowledgement Compliant: 1 results) Presentation (2 results) (of which Int'l Joint Research: 2 results) Remarks (2 results)

  • [Int'l Joint Research] University of Waterloo(カナダ)

    • Related Report
      2017 Annual Research Report
  • [Int'l Joint Research] University of Waterloo(カナダ)

    • Related Report
      2016 Annual Research Report
  • [Int'l Joint Research] Ecole Normale Superieure(フランス)

    • Related Report
      2015 Annual Research Report
  • [Journal Article] Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems2018

    • Author(s)
      Kengo Kido, Sean Sedwards and Ichiro Hasuo
    • Journal Title

      IFAC-PapersOnLine

      Volume: 印刷中

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis2016

    • Author(s)
      Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo
    • Journal Title

      Proc. Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, Lecture Notes in Computer Science

      Volume: 9583 Pages: 229-249

    • DOI

      10.1007/978-3-662-49122-5_11

    • ISBN
      9783662491218, 9783662491225
    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
  • [Presentation] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis2016

    • Author(s)
      Kengo Kido
    • Organizer
      17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)
    • Place of Presentation
      Hilton St. Petersburg Bayfront, St. Petersburg, Florida, USA
    • Year and Date
      2016-01-18
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis2015

    • Author(s)
      Kengo Kido
    • Organizer
      International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR 2015)
    • Place of Presentation
      Grand Hyatt hotel, Union Square, San Francisco, California, USA
    • Year and Date
      2015-07-19
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Remarks] 研究者個人webページ

    • URL

      http://group-mmm.org/~kkido/

    • Related Report
      2017 Annual Research Report
  • [Remarks] 木戸 肩吾 研究者ページ

    • URL

      http://www-mmm.is.s.u-tokyo.ac.jp/~kkido/

    • Related Report
      2015 Annual Research Report

URL: 

Published: 2015-11-26   Modified: 2024-03-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi