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

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

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