Hybrid Automaton

Hybrid Automatonとは, †

  • ハイブリッドオートマトン(HA)とは, ハイブリッドシステムのモデリング手法の一つである
  • 連続状態を表すノードと遷移を表すエッジから構成されるオートマトンである
  • 各ノードに連続変数の時間発展の記述を加えたものであり, ハイブリッドシステムのモデリング手法として広く使われている
  • Hyroseの通常のシミュレーションが, シミュレーションの終了時点となる有限の時間やフェーズを指定してシミュレーションを行う
  • つまり,
    • 初期ループで到達可能な全ての解軌道を求めることができる
    • 無限時間におけるシミュレーションに対応している
      • 無限時間における性質検証に利用可能である
    • 任意の有限時刻, フェーズまでのシミュレーションが容易に行うことができる
↑

利用法 †

  • オプションでHAを用いたシミュレーション(--hs)やHAへの変換(--ha)を指定して実行する
  • HAを作成する為に抽象的なプログラムを用いる必要があり, HAを作成する(--ha)
  • 後に各初期値を代入してシミュレーションを開始する(--hs)
↑

HA作成アルゴリズム †

  • HAの作成アルゴリズムでは, 到達可能範囲の不動点演算を行う
  • 到達可能範囲が不動点に達すると, HAの作成が完了する
  • 逆に, 収束しないとHAを作成することが出来ない
  • HA作成アルゴリズムでは, プログラム解析に用いられる抽象実行の手法を取り入れる
    • 抽象度が低いHydLaプログラムでは, 到達可能範囲が拡散を続けるため, アルゴリズムの停止性は保証されない
↑

HAを用いたシミュレーション †

↑

bouncing particleのHAを用いたシミュレーション †

INIT <=> y > 0.

FALL <=> [](y"=-10).

BOUNCE <=> [](y-=0 => y'=-(4/5)*y'-).

INIT,FALL<<BOUNCE.

  • 抽象実行を行うため, yの初期値を"y>0"として抽象度を高くして実行する
  • 作成されるHAは次のようになる HAtest.dot.png
  • オプション(--hs)の場合, さらにこのHAに初期値を代入してすぐにシミュレーションを行うことができる
Attach file: fileHAtest.dot.png 1243 download [Information]
Last-modified: 2019-03-28 (Thu) 10:52:21 (1850d)