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 340 download [Information]
Last-modified: 2017-03-02 (Thu) 03:21:30 (205d)