専攻名（専攻分野）
Department 研究指導名 Research guidance
氏名 Name 学籍番号 Student ID
number
指 導 教 員 Advisor
印 Seal
研究題目 Title
Date of submission: 1 / 31 / 2012 (MM / DD / YYYY)
修 士 論 文 概 要 書
Summary of Master’s Thesis
CD 5110B058 – 2 情報理工学専攻
並列知識情報処理
渋谷 俊
上田 和紀
ハイブリッド制約言語プログラムのハイブリッドオートマトンへの変換
1 研究の背景と目的
ハイブリッドシステムとは時間の経過に伴って状態が連 続変化したり離散変化したりする系であり，制御工学や生 命工学などのモデルを記述するのに適している．
HydLaは制約概念に基づくハイブリッドシステムモデ
リング言語であり，HydLa処理系Hyroseは精度保証され たシミュレーションを行ってシステム検証に役立てること を目標としている．これまでのHyroseはシミュレーショ ン終了までの実行時間や状態変化のステップ数を指定して 実行し，その時点までの結果を得ていた．このためHydLa プログラムを無限時間まで実行した時の性質がどのように なるか明らかでなかった．
本論文の目的はHydLaによるシステム検証を目標とし
てHydLaプログラムを記号実行によりハイブリッドオー
トマトンに変換を行い，生成されたオートマトンの性質に ついて考察する．
ハイブリッドシステム[2]とは時間の経過に伴って状態 が連続変化したり，状態や方程式系自体が離散変化したり するシステムを指す．ハイブリッドシステムは物理学や制 御工学，生命工学などの分野で，システムの目標状態への 到達可能性検証や，仕様を満たすようなパラメータ調整に 重要な役割を果たす．ハイブリッドシステムを用いたツー ルに制約を用いたものや，ハイブリッドオートマトンを用 いたものがある．
HydLa[3]は上田研究室で開発されている制約概念に基
づくハイブリッドシステムモデリング言語である．宣言 型で論理式を記述するため記法が最小限で済む，制約ベー スで時刻の関数を用いて方程式を定義する，制約階層に より制約を簡潔に記述できるといった特徴がある．ガード 条件が成立したときに後件の制約を評価する条件付き制 約を用いてif文のように条件を記述する．HydLa処理系 Hyrose[4][5]はHydLaプログラムから制約階層に従って解 候補モジュール集合を生成し，離散変化を表すPointPhase と連続変化を表すIntervalPhaseのシミュレーションを，各 フェーズで極大で無矛盾な解候補モジュール集合から非決 定的に採用してシミュレーションを行うことを交互に繰り
INIT <=> f=0.
INC <=> [](f’=1).
DROP <=> [](f- = 2 => f=0).
INIT, (INC << DROP).
図1 ノコギリ波のHydLaプログラム
返し，各変数の解軌道を出力する．
ノコギリ波とは時間経過で増加し，一定の値に達すると 値をリセットする波である．ノコギリ波の形状をHydLa プログラムで表したものが図1となる．変数fは波の高 さ，f’はf の一階微分，f-はf の左極限値を表す．制 約INITは時相演算子alwaysを付けていないためシミュ レーション時刻 0 の初期値に関する制約，INC は時間 と共に波が高くなる制約，DROP は波の高さが一定に達 した時にリセットする制約であり，INCとDROPは時相
演算子 alwaysを付けているため時刻 0以降の制約であ
る．制約階層を用いて DROPをINCより優先するように している．このプログラムの解候補モジュール集合群は
{INIT,INC,DROP}，{INIT,DROP}となる．解候補モジュー
ル集合{INIT,INC,DROP}を採用しているフェーズで制約
DROPのガード条件f- = 2が成立すると，後件のf=0が 評価される．この時，制約INCとDROPは矛盾するため，
解候補モジュール集合{INIT,INC,DROP}は採用できなく なる．
Hyroseで実行した結果の変数fの解軌道をプロットし
たものを図2に示す。波の高さが時間と共に増え，一定に
図2 ノコギリ波の実行結果
達するとリセットされるのがわかる．
ハイブリッドオートマトン[1]は状態を表すノードと遷 移を表すエッジから成り立つ．連続変化がノード，離散変 化がエッジに対応し，時間経過ごとにノード間を遷移する
ことで，ハイブリッドシステムを表す．
2 ハイブリッドオートマトン変換アル ゴリズム
HydLaの実行に基づいてHydLaプログラムを変換し，
ハイブリッドオートマトンに変換する．HydLaはフェー ズの切り替わりに各変数のフェーズ終了時の値を変数表に 格納し引き継いでいる．次フェーズでは変数表の各変数の 値を前フェーズ終了時の値(左極限値)として扱い，採用す る解候補モジュール集合を決定し，無矛盾性判定や条件付 き制約の成立判定(閉包計算)した結果，シミュレーショ ンに用いる制約群を決定している．同じ種類のフェーズ (PointPhaseまたはIntervalPhase )で異なる時間のフェー ズでも同じ変数表を用いてフェーズの実行を行うと，同じ 解候補モジュール集合が採用され，条件付き制約の成立が 判定された結果，同一の制約群を用いて解軌道が計算され るため，一致する．
ハイブリッドオートマトンを生成するにあたって，各 ノードとエッジを
• 各フェーズで採用している解候補モジュール集合
• 各フェーズで成立しているガード条件
• 初期値に関する制約であるか について場合分けを行う．
各フェーズで採用している解候補モジュール集合につい て場合分けするのは，HydLaの実行は各フェーズにおい て極大で無矛盾な解候補モジュール集合を採用するため，
採用する解候補モジュール集合はフェーズごとに異なるた めである．各フェーズで成立しているガード条件について 場合分けするのは，HydLaの実行は同じ解候補モジュー ル集合を採用していても，条件付き制約の成立によって後 件の制約を評価するかが決定され，シミュレーションに用 いる制約群が異なるためである．初期値に関する制約であ るかについて場合分けするのは，ハイブリッドオートマト ンの初期値に関する制約はHydLaプログラムの時刻0の PointPhaseの実行に対応する．時相演算子alwaysが付い ている制約は時刻0以降に使用し，付いていない制約は時 刻0の時点だけで使用するため，このalwaysが付いてい ない制約を考慮するためである．
これらの点に着目しながらHydLaプログラムのシミュ レーションをハイブリッドオートマトンの生成が終了する まで実行し，実行結果としてハイブリッドオートマトンに 必要な情報を集め，変換を行う．まず時刻0のPointPhase と直後のIntervalPhaseを実行し，ハイブリッドオートマ トンの初期値と初期ノードを生成する．この初期ノード の変数表を特徴変数について解析し，変数表とガード条件 を比較し，次にこの初期ノードから実行可能なPointPhase をすべて実行し，さらに各PointPhaseの直後から始まる
IntervalPhaseを実行し，エッジとノードのペアを生成す
る．これ以降も同様に生成されたノードから次に実行可
能なPointPhaseをすべて実行するが，すでに生成された
ノードと採用する解候補モジュール集合と成立する条件 付き制約の組み合わせが一致するノードは同じであると し，PointPhase とIntervalPhaseの実行を行わない．この ように実行する可能性のある PointPhase とその直後の IntervalPhaseのペアをオンザフライに実行し，遷移可能な すべての解候補モジュール集合と成立する条件付き制約の 組み合わせを取得する．
3 変換アルゴリズムの実装
Hyroseに変換アルゴリズムを実装した．この変換アル
ゴリズムで扱うプログラムのガード条件は変数と定数が対 応する等式のみとする．
ノコギリ波のHydLaプログラムを変換アルゴリズムに 従って変換する．変換したハイブリッドオートマトンを図 3に示す．採用している解候補モジュール集合と成立して いるガード条件をラベルとして記入している．どんなに時
図3 ノコギリ波のHydLaプログラムを変換したハイブ リッドオートマトン
間が経過しても波の高さが増加とリセットを繰り返すこと がわかる．
4 まとめと今後の課題
ハイブリッド制約言語プログラムをハイブリッドオート マトンに変換する手法を提案し，Hyrose上で実装を行い 例題を用いて変換を確認した．またHydLaプログラムを ハイブリッドオートマトンに変換することでHydLaプロ グラムの無限時間までの性質を定性的に評価できるように なったことを確認した．
今後の課題として変換後のハイブリッドオートマトンを 検証器で用いる形に変換し，既存のツールを用いて検証を 行いたい．
参考文献
[1] T. Henzinger : The Theory of Hybrid Automata,in Proc. LICS’96, IEEE Com- puter Society Press, 1996, pp. 278–292.
[2] J. Lunze : Handbook of Hybrid Systems Control: Theory, Tools, Applications, Cambridge University Press, 2009.
[3] 上田和紀,石井大輔,細部博史:ハイブリッド制約言語HydLaの宣言的意味論, コンピュータソフトウェア, Vol. 28 No. 1, 2011, pp. 306–311.
[4] 渋谷俊,高田賢士郎,細部博史,上田和紀:ハイブリッドシステムモデリング 言語HydLaの実行アルゴリズム,コンピュータソフトウェア, Vol. 28 No. 3, 2011, pp. 167–172.
[5] 松本 翔太,櫻庭 翔,高田 賢士郎,細部 博史,上田 和紀:ハイブリッドシステム モデリング言語HydLaの実装,日本ソフトウェア科学会第28回大会, 2011.
