#author("2019-03-28T19:52:21+09:00","default:Uedalab","Uedalab")
* Hybrid Automatonとは, [#i1a97e8b]
- ハイブリッドオートマトン(HA)とは, ハイブリッドシステムのモデリング手法の一つである
- 離散状態を表すノードと遷移を表すエッジから構成されるオートマトンである
- 連続状態を表すノードと遷移を表すエッジから構成されるオートマトンである
- 各ノードに連続変数の時間発展の記述を加えたものであり, ハイブリッドシステムのモデリング手法として広く使われている
- Hyroseの通常のシミュレーションが, シミュレーションの終了時点となる有限の時間やフェーズを指定してシミュレーションを行う
- つまり,
-- 初期ループで到達可能な全ての解軌道を求めることができる
-- 無限時間におけるシミュレーションに対応している
--- 無限時間における性質検証に利用可能である
-- 初期状態から到達可能な解軌道を全て求めることができる
-- 任意の有限時刻, フェーズまでのシミュレーションが容易に行うことができる
* 利用法 [#x0db50c2]
- オプションでHAを用いたシミュレーション(--hs)やHAへの変換(--ha)を指定して実行する
- HAを作成する為に抽象的なプログラムを用いる必要があり, HAを作成する(--ha)
- 後に各初期値を代入してシミュレーションを開始する(--hs)
** HA作成アルゴリズム [#n7ae85a5]
- HAの作成アルゴリズムでは, 到達可能範囲の不動点演算を行う
- 到達可能範囲が不動点に達すると, HAの作成が完了する
- 逆に, 収束しないとHAを作成することが出来ない
- HA作成アルゴリズムでは, プログラム解析に用いられる抽象実行の手法を取り入れる
-- 抽象度が低いHydLaプログラムでは, 到達可能範囲が拡散を続けるため, アルゴリズムの停止性は保証されない
* HAを用いたシミュレーション [#lcea7253]
** bouncing particleのHAを用いたシミュレーション [#s3fc3df6]
>
~ INIT <=> y > 0.
~ FALL <=> [](y"=-10).
~ BOUNCE <=> [](y-=0 => y'=-(4/5)*y'-).
~ INIT,FALL<<BOUNCE.
<
- 抽象実行を行うため, yの初期値を"y>0"として抽象度を高くして実行する
- 作成されるHAは次のようになる
&ref(./HAtest.dot.png);
- オプション(--hs)の場合, さらにこのHAに初期値を代入してすぐにシミュレーションを行うことができる
