HydLaWiki
Hybrid Automaton
Start:
* Hybrid Automatonとは, [#i1a97e8b]
- ハイブリッドオートマトン(HA)とは, ハイブリッドシステム...
- 連続状態を表すノードと遷移を表すエッジから構成されるオ...
- 各ノードに連続変数の時間発展の記述を加えたものであり, ...
- Hyroseの通常のシミュレーションが, シミュレーションの終...
- つまり,
-- 初期ループで到達可能な全ての解軌道を求めることができる
-- 無限時間におけるシミュレーションに対応している
--- 無限時間における性質検証に利用可能である
-- 任意の有限時刻, フェーズまでのシミュレーションが容易に...
* 利用法 [#x0db50c2]
- オプションでHAを用いたシミュレーション(--hs)やHAへの変...
- HAを作成する為に抽象的なプログラムを用いる必要があり, H...
- 後に各初期値を代入してシミュレーションを開始する(--hs)
** HA作成アルゴリズム [#n7ae85a5]
- HAの作成アルゴリズムでは, 到達可能範囲の不動点演算を行う
- 到達可能範囲が不動点に達すると, HAの作成が完了する
- 逆に, 収束しないとHAを作成することが出来ない
- HA作成アルゴリズムでは, プログラム解析に用いられる抽象...
-- 抽象度が低いHydLaプログラムでは, 到達可能範囲が拡散を...
* HAを用いたシミュレーション [#lcea7253]
** bouncing particleのHAを用いたシミュレーション [#s3fc3d...
>
~ 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に初期値を代入して...
End:
* Hybrid Automatonとは, [#i1a97e8b]
- ハイブリッドオートマトン(HA)とは, ハイブリッドシステム...
- 連続状態を表すノードと遷移を表すエッジから構成されるオ...
- 各ノードに連続変数の時間発展の記述を加えたものであり, ...
- Hyroseの通常のシミュレーションが, シミュレーションの終...
- つまり,
-- 初期ループで到達可能な全ての解軌道を求めることができる
-- 無限時間におけるシミュレーションに対応している
--- 無限時間における性質検証に利用可能である
-- 任意の有限時刻, フェーズまでのシミュレーションが容易に...
* 利用法 [#x0db50c2]
- オプションでHAを用いたシミュレーション(--hs)やHAへの変...
- HAを作成する為に抽象的なプログラムを用いる必要があり, H...
- 後に各初期値を代入してシミュレーションを開始する(--hs)
** HA作成アルゴリズム [#n7ae85a5]
- HAの作成アルゴリズムでは, 到達可能範囲の不動点演算を行う
- 到達可能範囲が不動点に達すると, HAの作成が完了する
- 逆に, 収束しないとHAを作成することが出来ない
- HA作成アルゴリズムでは, プログラム解析に用いられる抽象...
-- 抽象度が低いHydLaプログラムでは, 到達可能範囲が拡散を...
* HAを用いたシミュレーション [#lcea7253]
** bouncing particleのHAを用いたシミュレーション [#s3fc3d...
>
~ 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に初期値を代入して...
Page:
