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.
Last-modified: 2019-03-28 (Thu) 10:52:21 (1853d)