日本ソフトウェア科学会第 30 回大会 (2013 年度) 講演論文集

最強事後条件の計算を用いた
ハイブリッドオートマトンの帰納的検証
石井 大輔

Guillaume Melquiond

中島 震

ハイブリッドシステムの安全性検証は物理環境と結合されたシステムの開発において重要な技術である．本発表ではハイブリッドオートマトンを対象とした自動的な論理的分析手法を提案する．提案手法は従来のモデル検査法と較べて広範な問題に適用可能であり，記号パラメタや非線形式で記述されるモデルを扱うことができる．提案手法では，
まずハイブリッドオートマトンの実行トレースを逐次プログラムに変換し，その後，帰納法にもとづくプログラムのループ構造への変換と最強事後条件の計算により，安全性を証明するための検証条件群を生成する．検証条件をMathematica 等の算術ソルバーで妥当性判定することにより元モデルの安全性を示すことができる．提案するアルゴリズムは，展開する実行の長さの調整と，証明できなかった検証条件からループ不変条件を生成する処理をおこな
いながら，帰納的検証手法を自動化する．文献由来の例題群に対し実験を実施し，実用性を示す結果を得た．

とにより検証をおこなう．論理的分析法は，理論的な1 はじめに面では多くの研究がなされてきたものの，ツール実連続的ダイナミクスをともなう遷移系であるハイ用化の面では遅れていた．例外的な研究成果としてブリッドシステムは，物理環境と結合した組み込みシ

KeYmaera [16] があり，モデル検査アプローチでは扱

ステムの直截的なモデルであり，その高信頼な検証技えなかったパラメタを含む系や非線形系等，広範なク術の確立は重要かつチャレンジングな課題である．

ラスの問題が検証可能であることを示した．論理的分

ハイブリッドシステムの検証手法としてモデル検査

析法の欠点は，系が大きく複雑になると，検証プロセ

法と論理的分析法の 2 つのアプローチが提案されていスが自動的でなくなり，ユーザにモデルの理解と検証

る．モデル検査のアプローチでは，ハイブリッドオー

戦略の選択等の対話的作業を強いる点である．

トマトンを区分線形系等に抽象化し，状態の網羅的探本論文では，算術ソルバーを利用して半自動的にハ

索により検証をおこなう．モデル検査法は自動化する

イブリッドシステムの論理的分析をおこなうツールをことができ，HyTech [10]，PHAVer [6]，HybridSAL

提案する．提案手法はハイブリッドオートマトンの安[20] 等の多くのツールが開発され，実用的な問題に応

全性検証を対象とする．

用されてきた．2 つ目の論理的分析アプローチでは，

まず本論文では，ハイブリッドオートマトン (2 節)

演繹的推論に基づきハイブリッドシステムの検証に必の安全性を示すための有限長の検証条件を導出する健要となる検証条件を導出し，それらの妥当性を示すこ

全な方法を与える．提案手法では，ハイブリッドオー
トマトンの実行を直線的な逐次プログラムに変換しInductive Verification of Hybrid Automata with
Strongest Postcondition Calculus.
Daisuke Ishii, 東 京 工 業 大 学, Tokyo Institute ofTechnology.
Guillaume Melquiond, INRIA サクレ / パリ第 11 大学,
INRIA Saclay / Université Paris Sud 11.
Shin Nakajima, 国立情報学研究所, National Instituteof Informatics.

(3 節)，プログラムに対して帰納法を適用することによりループ構造を構成する (4 節)．すなわち，ハイブリッドオートマトンのすべての実行が，最大 m ス
テップの連続変化と離散変化の後，最大 n ステップ
周期で状態空間中のある領域を繰り返し訪れるようなループをなすことを示すためのプログラムを構成すϕ(0) = νt>0t̃)
= Fl (ϕ(t̃)) ∧ Il [ϕ(t̃)]∀t̃ ∈ [0, t] dϕ(dt

Gl1 ,l2 [ν1 ]t

Il2 [ν2 ]0⟨l, ν⟩ −→ ⟨l, ϕ(t)⟩図1Rl1 ,l2 [ν1 , ν2 ]⟨l1 , ν1 ⟩ −→ ⟨l2 , ν2 ⟩ハイブリッドオートマトンの操作的意味論

る．その後，最強事後条件の計算 (3. 2 節) を用いて逐次プログラムから検証条件を導出する．これらの検onẏ = rate iny ≤ highy=low

y = high, x′ = 0

sw-offẋ = 1, ẏ = rate in
0 ≤ x ≤ delay

証条件は実数上の算術式や常微分方程式を含んだ一階
x = delay

x = delay

述語論理式である．実際に数式処理系 Mathematica
sw-onẋ = 1, ẏ = rate out
0 ≤ x ≤ delay

を用い，線形および一部の非線形なハイブリッドオー
トマトンに関する検証条件が証明可能であることを示す．上記の検証プロセスを提案するアルゴリズムによ図2′

y = low , x = 0

offẏ = rate outy ≥ low

水槽の水位制御のモデル．

り自動化する (4. 2 節)．ただし (i) ループ構造を構成するために実行を展開するステップ数 m および n と，(ii) ループ構造の冒頭で成立すべきループ不変条件を

t

t

0

0

1
3
σ0 −→
σ1 −
→ σ2 −→··· −→ σ2k の形をした実行を長さ k の標準形と呼ぶ．

効率よく見つけるためにユーザの対話的作業を要す

本論文では，複数の離散変化が同時刻に起こらず，る．代数的手法によるループ不変条件の生成について最初に ⟨l0 , ν0 ⟩ −→ σ1 のように離散変化が起こらないも述べる (4. 3 節)．提案手法の実装を用い (5 節)，文と仮定する．一般的な実行に関する検証は今後の課題

献由来の例題群を検証した実験結果を述べる (6 節)．

とする．

2 ハイブリッドオートマトン
ハイブリッドオートマトン (hybrid automata) [9]0定義 2. 安全性 (不変性ともいう) を式 □P で表す．
ただし P は L × RV に関する条件である．式 P は，各実行の初期状態に関して成り立ち，各連続変化およはハイブリッドシステムを表す数理モデルである．

び離散変化において保存される．

定義 1. ハイブリッドオートマトンを以下の要素から

例 1 (水槽 [3] [13]).

なる 7 つ組 HA = ⟨L, V , Init, G, R, F, I⟩ で表す．

のハイブリッドオートマトンでモデリングする．ロ• ロケーションの有限集合 L = {l1 , . . . , lp }.

ケーション oﬀ および sw-on では水槽の出力孔から• 実変数の有限集合 V = {x1 , . . . , xq }. 変数への水が放出されるため，水位 y が一定速度 rateout で減

すべての付値の集合を RV で表す．

水位制御装置付きの水槽を図 2

少し，ロケーション on および sw-oﬀ では制御装置が• 初期条件 Init ⊆ L×RV ．

水を注入するため，y が一定速度 ratein で増加する．

• ガード条件の族 G = {Gl,l′ }l∈L,l′ ∈L ．ただし制御装置は y が値 low あるいは high に達するのに応Gl,l′ は RV に関する条件である.
• リセット関数の族 R = {Rl,l′ }l∈L,l′ ∈L ．ただし
Rl,l′ : RV → RV とする．
• ベ ク ト ル 場の 族 F = {Fl }l∈L ．た だ し Fl :RV → RV とする.
• ロケーション不変条件の族 I = {Il }l∈L ．ただし
Il は RV に関する条件である．
t1

t2

じてロケーション on と oﬀ を切り替える．さらにロケーション sw-on および sw-oﬀ によって上記の切り替えに遅延 delay が発生することを表している．安全性の例として，水位 y が限界値 min と max の間につねに収まっていることを，つぎのように記述できる．

□(min ≤ y ≤ max )また各定数パラメタについて下記のように制約する．

列 σ0 −→ σ1 −→ · · · を (有限長または無限長の) 実

min ≤ low ∧ high ≤ max ∧ low < high ∧行という．ただし σi ∈ L × RV と Init[σ0 ] がなりた

delay > 0 ∧ max ≥ high + ratein · delay ∧ti

つとする．−→ を ti > 0 のとき連続変化，ti = 0 のとき離散変化とよび，図 1 の 2 つのルールで定義する．

(1)

min ≤ low + rateout · delay(2)

3 ハイブリッドオートマトンの実行から逐次プログラムへの変換た形になっている．上記プログラムは途中でブロックする (skip に簡約されない) 実行や HA の異なるロケーションをたどる実行ももつことに注意されたい．

本節ではプログラム検証の技術を利用してハイブ

上記の ImpHA プログラムを用いて安全性の判定条件

リッドオートマトンの有限長・無限長の実行を扱うたを与えることができる．

めの準備をおこなう．まず，実行を記述するための簡補題 2. もし任意の上記の形の ImpHA プログラムに単な逐次言語を導入する．つぎに，各プログラム文とついて，初期プログラム状態 S0 が [[xs ]]S0 ∈ Init を

事前条件から導出される最強事後条件を説明する．

みたすとき，性質 P が終了プログラム状態においてなりたつならば，HA は安全性 □P をみたす (ただし

3. 1 逐次言語

Zeno 時刻が存在するならば最初の Zeno 時刻までに

ハイブリッドオートマトン HA について，逐次言語

関する)．

ImpHA を与える．ImpHA は 2 つのコマンド evolve
および trans と，それらの列からなる．コマンド

3. 2 最強事後条件

evolve は連続変化，trans は離散変化を記述する．

本節ではプログラム検証の基本概念である最強事

定義 3. 言語 ImpHA の構文を以下のように定める．

後条件 [11] [5] を用いて，ImpHA プログラムの安全性

s ::= skip | s; s | evolve t | transのための検証条件を導出する方法を説明する．

定義 4. プログラム状態 (S や Si で表す) は変数名か提案手法では到達性ではなく安全性の検証を目的

ら変数値への写像である．変数 xs は HA の実行におけとしており，プログラムが非ブロッキングであること

る「現在」状態 (∈ L×RV ) を表す．また当該状態を変を示す必要はない．そのため，最弱事前条件と最強事

数群 xs = ⟨xl , ·⟩ = ⟨·, xv ⟩ = ⟨·, (x1 , . . . , xi , . . . , xq )⟩.

後条件の計算は双対となる．本稿では前向き到達性ににより部分的に表すことができるものとする (いずれ対応する最強事後条件を用いるが，最弱事前条件を用かの変数値を更新した場合，上記の等価性が保たれる

いて検証を実施することも可能である．

よう他の変数値も暗黙的に書き換わる)．

補題 3 (最強事後条件と健全性). 任意の ImpHA プ

図 3 に ImpHA の操作的意味論を示す．[[e]]S は表

ログラム s について，もし初期状態が性質 P をみた

現 e 中の自由変数をプログラム状態 S が与える値ですならば，終了状態は SP (P, s) をみたす (s が skip

置き換えることを表す．S{x 7→ v} はプログラム状態に簡約可能とする)．ただし SP は図 4 のように定義

S を変数 x に値 v を与えるよう更新したプログラムする．

状態を表す．skip と連結構文のルールは典型的なものである．
任意の HA の有限長実行について対応する ImpHA
プログラムを与えることができる．
t1

補題 1. 以下の形をした任意の HA の実行 σ0 −→
0

tk

σ1 −
→ · · · −→ σ2k−1 に対し，下記の ImpHA プログ
ラムを与えることができる．

evolve t1 ; trans; · · · ; evolve tk
このプログラムは下記すべてをみたす実行をもつ．

証明. プ ロ グ ラ ム 状 態 S と S ′ に つ い て [[P ]]S とS, s ⇝∗ S ′ , skip がなりたつと仮定する．[[SP (P, s)]]S ′がなりたつことを示せばよい．それには s の構造に応じた SP の定義の各部が ImpHA の操作的意味論 (図3) を含意することを帰納的に確認すればよい．実際，
SP の定義の各部は (ImpHA の操作的意味論で前提としている) ハイブリッドオートマトンの操作的意味
論 (図 1) に基づいており，明らかである．

• 初期プログラム状態において xs = σ0 が成立．

例 2. 例 1 において xl = on ∧ y = low をみたす状• プログラムが skip に簡約される．

態を考える．長さ t の連続変化により到達する状態• 終了プログラム状態において xs = σ2k−1 が成立．

が y ≤ max をみたすことを証明する．補題 2 および

上記の HA の実行は標準形に 1 つ連続変化を加え

3 から，任意のプログラム状態について下記がなりたS1 , s1 ⇝ S2 , s2
S, (skip; s) ⇝ S, s
S1 , (s1 ; s3 ) ⇝ S2 , (s2 ; s3 )S, evolve 0 ⇝ S, skip
0t[[xs ]]S −→σ[[xs ]]S −→σ
S, evolve t ⇝ S{xs 7→ σ}, skip
S, trans ⇝ S{xs 7→ σ}, skip
図3

ImpHA の操作的意味論．

SP (P, skip) := P

SP (P, s1 ; s2 ) := SP (SP (P, s1 ), s2 )t̃)= Fxl (ϕ(t̃)) ∧ Ixl [ϕ(t̃)])SP (P, evolve t) := ∃ϕ P [xv ← ϕ(0)] ∧ ϕ(t) = xv ∧ (∀t̃ ∈ [0, t] dϕ(dt

SP (P, trans) := ∃⟨l′ , x′v ⟩ P [xs ← ⟨l′ , x′v ⟩] ∧ Gl′ ,xl [x′v ] ∧ xv = Rl′ ,xl (x′v ) ∧ Ixl [xv ]図4ImpHA プログラムの最強事後条件．

つことを示せばよい．

SP ((xl = on ∧ y = low ), evolve t) ⇒ y ≤ max

安全性検証のための前提条件を弱め，有限個のプログ
ラムをもとに検証を実施する手法を示す．

ここで左辺をみたすプログラム状態にいると仮定し，提案手法では，まず P + ⇒ P をみたす表明 P + を

y ≤ max がなりたつことを示す．SP の定義から，下仮定し，ハイブリッドオートマトン HA が下記をみ記のような関数 ϕ が存在する．

たすことを期待する．

(xl = on ∧ ϕy (0) = low ) ∧ ϕ(t) = (x, y)∧• HA の初期状態 Init から始まる高々m ステップt̃)
= Fxl (ϕ(t̃)) ∧ Ixl [ϕ(t̃)])(∀t̃ ∈ [0, t] dϕ(dt

長の任意の実行について，すべての途中状態が安上式中の微分方程式を解くことにより式 y =全で，P + をみたす状態に到達する．

low + ratein · t を求め，ロケーション不変条件 Ixl• P + をみたす状態から始まる高々n ステップ長のを展開して y ≤ high で置き換える．さらに制約 (2)

任意の実行について，すべての途中状態が安全を考慮し，線形算術によりゴール y ≤ max を証明す

で，P + をみたす状態に到達する．

ることができる．

上記を条件式としてエンコードし，妥当性判定するこ

注意 1. 検証条件を自動化ツールで扱う際，事前にでとにより安全性検証を実施する．本アプローチの成否

きる限り限量子を除去しておくのが望ましい．たとえは実行の長さ m および n と表明 P + を見つけること

ば SP (P, trans) は ∃l′ Q[l′ ] という形をしているが，ができるかどうかに依存する．

これは式 Q[l1 ] ∨ . . . ∨ Q[lp ] (l1 , . . . , lp で全ロケーショ

安全性の推論規則として，m = 0, n = 1 とした単ンを表す) と等しい．SP (P, evolve t) では，例 2 で純形を示す．

述べたように常微分方程式を閉形式に変換できれば，定理 1 (単純形). 下記の推論規則がなりたつ．
VC 0 : Init ⇒ P +∃ϕ を除去できる．

4 帰納的検証手法
本節では補題 2 および数学的帰納法にもとづきハ
イブリッドオートマトンの安全性検証をおこなうアル
ゴリズムについて述べる．

4. 1 帰納法による安全性検証
補題 2 では無限個のプログラムについて安全性を確認する必要があり，実用的ではなかった．本節では

VC 1 :
VC −1 :∀t ≥ 0 SP (P + , evolve t) ⇒ P∀t ≥ 0 SP (P + , evolve t; trans) ⇒ P +
HA |= □P

証明. VC 0 は初期状態が表明 P + をみたすことを確認している．VC −1 は連続変化と離散変化からなる任ti+1

0

意の実行 σi −−−→ σi+1 −→ σi+2 について，σi が P +をみたすとき，σi+2 もまた P + をみたすことを帰納的に確認している．VC 1 は上記連続変化の途中で安全性がつねになりたつことを確認している．

上記定理 1 の推論規則を任意の m, n について一般化する．
定理 2 (展開形). 下記の m + n + 2 個の最強事後条
件を考える．
SP 1≡ SP (Init ∧ ¬P + , evolve t1 )≡ SP (SP (SP 1 , trans) ∧ ¬P + , evolve t2 )
..
.

SP 2

≡ SP (SP (SP m−1 , trans) ∧ ¬P + ,evolve tm )SP 0
≡ SP (SP m , trans)
SP m+1 ≡ SP (P + , evolve t1 )
..
.
SP m

SP m+n ≡ SP (SP (SP m+n−1 , trans) ∧ ¬P + ,evolve tn )SP −1 ≡ SP (SP m+n , trans)
下記の推論規則がなりたつ．
VC 1:∀t1 ≥ 0

VC 2

VC m
VC 0
VC m+1

VC m+n
VC −1

:

:
:
:

:
:

∀t1 , t2 ≥ 0..
.

SP 1 ⇒ P
SP 2 ⇒ P

Input: HA; P ; mmax ∈ N≥0 ; nmax ∈ N>0
Output: true: HA |= □P ;false: mmax + nmax ステップ以下で □P を判定不可
1:
for m ∈ {0, . . . , mmax }; n ∈ {1, · · · , nmax } do
2:
P + := P3:
while P + ̸≡ false do
4:
if ¬∀i ∈ {0, . . . , m} Validate(VC i ) then
5:
break
6:
end if7:
if ∃j ∈ {m + 1, . . . , m + n, −1}¬Validate(VC j ) then8:
P + := P + ∧ Learn(VC j )
9:
else
10:
return true11:
end if12:
end while13:
end for14:
return false
図5

検証アルゴリズム.

つことを確認し，HA |= □P を判定する．アルゴリ
ズムは各 m ≤ mmax , n ≤ nmax について帰納的検証をおこなう (1 行目)．アルゴリズムはまず初期実行に∀t1 . . . tm ≥ 0∀t1 . . . tm ≥ 0∀t1 ≥ 0..
.

SP m ⇒ P
SP 0 ⇒ P +SP m+1 ⇒ P∀t1 . . . tn ≥ 0∀t1 . . . tn ≥ 0

SP m+n ⇒ P
SP −1 ⇒ P +ついて計算し (4 行目)，つぎにループ部について計算する (7 行目)．手続き Validate は引数の論理式が妥当であれば true を返し，妥当性を示すことができな
ければ false を返す．すべての検証条件の妥当性を示すことができれば検証が成功する (10 行目)．
ループ部の検証がうまくいかないとき，妥当性判定

HA |= □Pに失敗した検証条件の証明がうまくいくよう手続き

証明. 検証条件 VC 1 から VC 0 により，高々m ステッ

Learn によりループ不変条件を詳細化し (8 行目)，検プ長の初期の実行が領域 P+に到達することを確認

証を再度試みる．Learn がループ不変条件を強め過ぎしている．検証条件 VC m+1 から VC −1 により，領た場合には (3 行目)，内部のループから抜け出し別域 P + から始まる高々n ステップ長の実行がふたたびの m, n による検証を試み，それでも成功しなければ

領域 P

+

に到達することを確認している．

VC m+1 以外の検証条件では P + が不成立を仮定していることに注意されたい．これは n ステップ未満
で領域 P + にふたたび到達する場合を検証するための措置である．

4. 2 検証アルゴリズム
図 5 のアルゴリズムは，ハイブリッドオートマトン

HA，安全性 □P ，実行を展開する最大長 mmax , nmax
を入力とし，定理 2 中のすべての前提条件がなりた

false を返す．
アルゴリズムにおいて，初期実行の検証 (4–6 行目，
以下この手続きを BaseCase とよぶ) とループ部の検証 (7-11 行目，以下 Induction) は独立しており，これらの順序を逆にしてもかまわない．

4. 3 ループ不変条件の生成
手続き Learn の実装について述べる．ループ部の検証において条件 VC i ≡ ∀t1 . . . ti ≥ 0 SP (P + , s) ⇒ Pの検証に失敗したとする．このとき Learn(VC i ) は，
ループ不変条件を P + := P + ∧ Q と更新すれば VC iが妥当となるような式 Q を生成する．Learn は VC i

トン中の微分方程式は組み込み手続き DSolve を用いに代数的操作を施し，SP (Q, s) ⇒ VC i がなりたつて閉形式に変換している．

ような Q を求める．

Q に出現する現在状態を表す変数 xs は P

BaseCase と Induction の実装では，2 通りの最適+が成化を施した．まず，各 VC i を個別に妥当性判定する

立する時点での状態を表すべきであるが，VC i 内ののではなく，共通の前提条件を再利用するようにし

xs はプログラム s の終了時点での状態を表している．

た．VC i の妥当性を判定する際，アルゴリズムはまこの不一致を解決するため，Learn は，限量子除去

ず VC i が依拠するプログラム si の実行結果を表す(quantifier elimination, QE) を用い，Q から特定時

SP i を計算してから，SP i ⇒ P/P + を妥当性判定

点に依存する変数群を消去する．

する．すでに SP i を計算していれば，SP i−1 は効率

Q := QE(∀xs ∀t1 . . . ti
SP ((P+∧ x0 = xs ), s) ⇒ P )[x0 ← xs ]よく計算できる．つぎに，プログラム s が複数ロケー
ションにまたがる実行集合に対応している場合の計複数の実数変数と関数変数の限量子を含んだ式に対算を効率化した．実装では，最強事後条件をロケーする限量子除去は，一般に困難な問題である．提案手

ション毎に複製・管理し，妥当性判定を複数回おこな法における検証条件の単純化について注意 1 と次節

う (注意 1 を参照)．Validate を呼び出す回数は増えを参照されたい．

るが，一般に検証プロセス全体を効率化できる．

限量子除去の結果，しばしば論理和の形の大きな例 3. 実装を用いて例 1 の安全性 (1) を検証する例

式が求まり，このような式を Q として用いても検証を示す．アルゴリズムに従い，まず m = 0, n = 1 にがうまくいかないことがある．とくに Q の部分式がついて計算する．Init が P + ≡ P を含意することを

HA の実行において決して有効にならない挙動を表し示すべく BaseCase を実行すると，true が得られる.

ている場合，検証条件が必要以上に複雑になってい

つぎに Induction を実行し，連続変化と離散変化のシる．そこで次節の実験においては，下記の方法によりミュレーションをおこなう．Induction はロケーショ

Q の簡略化・強化をおこなった．

ン on, sw-oﬀ, oﬀ , sw-on 毎に最強事後条件・検証条件• 式の分割．Q を最上位の論理和演算子で分割し，1 つまたは複数の部分式を採用する．
• ロケーションの否定．Q を分割した際，結果にロケーション l に関する部分式が含まれるとき，部分式を式 xl ̸= l で置き換える．この方法はループ展開と組み合わせると有効である．

を生成し，それらの妥当性判定をおこなう．VC 1 の判定では，ロケーション on および oﬀ については成功するが，sw-oﬀ および sw-on については失敗する．
そこで，Learn により下記の補助式を生成する．

Qsw-oﬀ ≡min + x · ratein ≤ y + delay · ratein ≤max + x · ratein ∨ x = delay ∨y + delay · ratein < low + x · ratein

5 実装
前節までに説明した手法を記号的に算術式を扱うことが可能な数式処理系 Mathematica 8.0.4†1 を用

Qsw-on ≡min + x · rateout ≤ y + delay · rateout ≤max + x · rateout ∨ x = delay ∨high + x · rateout < y + delay · rateout

いて実装した†2 ．本実装では手続き Learn を完全には自動化しておらず，4. 3 節で述べた方法をユーザが手

ここで，4. 3 節の 2 つの方法を用いて 2 通りにループ動で適用する必要がある．Validate は Mathematica

不変条件を改良することができる．ロケーションの否の組み込み手続き FullSimplify, Reduce, FindInstance定を適用した場合，P + に下記の補助式を加えること

を用いて 3 通りに実装した．ハイブリッドオートマになる．

Q1 := xl ̸= sw-oﬀ ∧ xl ̸= sw-on†1 http://www.wolfram.com/mathematica/+†2 http://www.ueda.info.waseda.ac.jp/~ishii/pub/ 更新後の P を用い，m = 0, n = 2 とすると検証がmathybrid/ にて公開．
成功する．補助式の分割を適用した場合，式 Qsw-oﬀ

と Qsw-on を最上位の論理和で 3 つの部分式に分割し，のもと，検証が成功した．HyTech は効率よくこの問各補助式の最初の部分式 (Qsw-oﬀ,1 と Qsw-on,1 とす

題を検証することができた．KeYmaera ではループる) を用いることで検証が成功する．具体的には P +不変条件を追加しても検証できなかった．

に下記の補助式を加える．

温度制御 [3]. あるロケーションから複数のエッジがQ2 := (xl = sw-oﬀ ⇒ Qsw-oﬀ,1 ) ∧出ているハイブリッドオートマトンについて，ロケー(xl = sw-on ⇒ Qsw-on,1 )ション shutdown に決して到達しないことを検証する

すると m = 0, n = 1 のもと検証が成功する．

問題である．安全性条件に shutdown への離散変化のガード条件の否定を加え，強めるよう変更した後，実6 実験結果装を用いて検証することができた．Induction での妥提案手法の実用性を評価するため，複数の例題を

当性判定の失敗から Q1 ∨ Q2 ∨ Q3 という形の補助式

検証する実験を実施した．また，比較のために同じ例を得たが，各部分式を P + に加えただけでは検証が題を既存ツール (HyTech, PHAVer, KeYmaera) を成功しなかった．そこで Q1 ∧ (Q2 ∨ Q3 ) という形の用いて検証した．実験結果を表 1 に示す．各列は，各式を P + に加えたところ，m = 1, n = 1 のもと検証

HA のロケーション数，変数の数，ループ展開数 (初に成功した．HyTech は効率よくこの問題を検証する

期実行/ループ部)，ループ不変条件 P

+

を補助定理

で改良した回数，提案手法で検証条件の判定に要しことができた．KeYmaera ではループ不変条件を追加しても検証できなかった．

た CPU 時間，HyTech (バージョン 1.04f，H) ある

跳ね返るボール. 典型的な非線形ハイブリッドオー

いは PHAVer (バージョン 0.38，P) による検証に要

トマトンの例である．ボールの初期位置，初速，床のした時間，KeYmaera (バージョン 3.0) による検証

反発係数をパラメタ化し，反発係数が 1 以下ならばに要した時間，を示している (「–」は検証に失敗しボールの高さがボールの初期エネルギーを超えないたことを示す)．実験は 3.4GHz Intel Xeon プロセッ

ことを検証した．4 つの検証条件は Mathematica を

サと RAM 4GB を備えたマシン上で実施した．ただ用いて証明した．このようにパラメタ化したモデルはし，提案手法の実行時間はループ不変条件 P+の改良を終えてから検証にかかる時間のみを計測していることに注意されたい．

モデル検査器では検証できなかった．KeYmaera は同様のモデルを効率よく検証できた．
鉄道制御 [14] [8] [2]. 位置 z にいる鉄道が位置の上
限 m を越えないことを検証する問題である． [14] で

6. 1 例題のモデルに対し， [2] における解析に基づき，ガード

水槽 (例 1). 提案手法を用い，例 3 で述べたよう条件を詳細化した．m = 0, n = 1 のもと検証を実施に検証できる．流量を表すパラメタ変数による非線形

し，検証条件 VC 1 の判定失敗から P + を改良した後，項のため，モデル検査器はこの問題を扱うことができ成功した．本問題は [14] [8] においても独自の検証戦なかった．また KeYmaera でも検証することができ

略，モデル変換，不変条件生成を駆使して検証されてたが，モデルに (例 3 のものよりも複雑な) ループ不いる．モデル検査器では非線形式に起因して検証でき変条件を追加する必要がある [15]．
ガ ス バ ー ナ ー.

なかった．KeYmaera は [14] で述べられているよう

2 つ の ロ ケ ー ション L ={leaking, non-leaking} からなる線形ハイブリッドオーにパラメタ・制約式を変更したモデルを検証することができた．

トマトンの検証問題である．実装を用いると Induction

高速道路 [12]. n 台の自律走行する車からなる高速が最初の連続変化の検証に失敗した．Learn を用いて道路のモデルである．実装を用いて n = 9 と n = 19

ロケーション leaking に関する補助式を生成，P+にのインスタンスを検証することができた． [12] では同追加し，ロケーション non-leaking に関してはロケー

問題を専用手法を用いて検証している．PHAVer はションの否定を P + に追加した．すると m = 4, n = 2

n = 9 のインスタンスを検証できたが，n = 19 では

表1

実験結果．

例題

locs

vars

unrolllemmas

CPU 時間モデル検査器KeYmaera

水槽 (例 1)

4

2

0/1

2

0.85s

–

1.8s

ガスバーナー

2

3

4/2

3

2.22s

0.004s (H)

–

温度制御

4

3

1/1

4

2.82s

0.012s (H)–

跳ね返るボール

1

2

0/1

1

0.49s

–

0.9s

鉄道制御

2

3

0/1

1

4.48s

–

3.1s

高速道路 9

10

9

0/2

1

0.22s

0.22s (P)–高速道路 19

20

19

0/2

1

3.64s

–

–

使用メモリが限界に達し失敗した．KeYmaera では

ルではハイブリッドシステムを既存の検証フレーム

検証することができなかった．

ワークに変換して扱う．いずれのツールにおいても検証プロセスが完全には自動化されておらず，ユーザが6. 2 考察

付加的な情報を入力したり，対話的な定理証明をおこ

モデル検査器 HyTech および PHAVer を用いて 3なったりする必要がある．

つの例題を効率よく検証することができたが，他の問

Platzer らが開発した KeYmaera [16] [14] が近年，

題は検証できなかった．提案手法はいくつかの点で優実用的な検証ツールとして注目されている．KeY-

れているといえる．まず，提案手法はパラメタを含む

maera は独自のモデリング言語を備え，ハイブリッド

モデルを扱うことができる．跳ね返るボールの例はシステムを hybrid program として記述し，diﬀeren-

パラメタを含むためにモデル検査器で検証できなかっtial (algebraic) dynamic logic で仕様や検証条件を付た (具体化すれば検証できる)．つぎに，提案手法は加する．また，検証には独自の定理証明器を用いる

スケーラビリティが高い． [12] の実験では，PHAVer[14]．これに対して本研究では，標準的なハイブリッ

は高速道路の例を n = 15 までしか検証できていない．

ドオートマトンを対象とし，簡単な逐次言語と帰納法

KeYmaera を用いて多くのハイブリッドシステムにもとづく限られた検証戦略からなる「軽量な」検証を自動的に検証できるが，ハイブリッドオートマトン

手法を提案している．

としてモデル化したハイブリッドシステムに関してはハイブリッドシステムの多項式不変条件を生成する

検証がうまくいかないことが多い．水槽の例ではモデ

代数的手法 [18] [17] が提案されている．将来課題としルにループ不変条件を付加する必要があった．自動検て，これらを提案手法に組み込むことが考えられる．

証がうまくいかない場合，ユーザは定理証明器を対話提案手法は有界モデル検査法との類似性がある．無的に用いて演繹的な証明をおこなうこともできるが，限長の実行を扱う有界モデル検査法が提案されている

KeYmaera は 141 の推論ルールを備え，使いこなす

ものの (例 [4])，これらの手法は離散系に適用されるにのは習熟を要する [16]．本稿の提案手法も全自動化さとどまっている．多くのハイブリッドシステムの有界れていないものの，検証戦略の数は限られており，まモデル検査器は有限長の実行に関してのみ検証をおこた対話的作業を要するループ展開の試行やループ不変

なっている．Hybrid SAL Relational Abstracter [20]条件の導出を自動化することも可能だと考えている．

はハイブリッドシステムを離散系に抽象化して有界モデル検査をおこなうが，提案手法では抽象化せず直接

7 関連研究ハイブリッドシステムのための論理的分析ツールが複数提案されている [13] [1] [7] [8] [2] [19]．これらのツー

ハイブリッドシステムを扱う点が異なる．

8 まとめ
本稿では，多くの線形および非線形のハイブリッド
オートマトンの無限長の実行に関する安全検証が可能な，論理的分析アプローチによるツールを提案した．
提案手法では，多数の導出規則を用意して対話的な定理証明にもとづくツールを提供するのではなく，検証のための戦略を最強事後条件の計算と帰納法の適用とに絞り込み，自動的な検証プロセスの実現を目指した．実験結果では複数のベンチマーク問題を実用的な計算時間で検証可能なことを示した．提案手法では，一般のプログラム検証の場合と同様に不変条件を求める作業が必要となるが，証明に失敗した検証条件から Mathematica を用いて不変条件を生成する方法を示した．現状では不変条件生成においてユーザの対話的作業を必要としており，完全な自動化が今後の課題として挙げられる．
謝辞 本研究の一部は科研費 23-3810 の補助を得ておこなった．

参 考 文 献[ 1 ] Ábrahám-Mumm, E., Steﬀen, M., and Hannemann, U.: Verification of hybrid systems: Formalization and proof rules in PVS, ICECCS, 2001,
pp. 48–57.
[ 2 ] Abrial, J.-R., Su, W., and Zhu, H.: Formalizing
Hybrid Systems with Event-B, ABZ, LNCS 7316,
2012, pp. 178–193.
[ 3 ] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P.-H., Nicollin, X., Olivero, A.,
Sifakis, J., and Yovine, S.: The algorithmic analysis
of hybrid systems, Theoretical Computer Science,Vol. 138, No. 1(1995), pp. 3–34.
[ 4 ] De Moura, L., Ruess, H., and Sorea, M.:
Bounded model checking and induction: From refutation to verification, CAV, LNCS 2725, 2003,
pp. 14–26.
[ 5 ] Dijkstra, E. W.: Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, Vol. 18, No. 8(1975), pp. 453–

457.
[ 6 ] Frehse, G.: PHAVer: Algorithmic Verification ofHybrid Systems past HyTech, International Journal
on Software Tools for Technology Transfer (STTT),
Vol. 10, No. 3(2008), pp. 263–279.
[ 7 ] Ghosh, R., Tiwari, A., and Tomlin, C.: Automated symbolic reachability analysis: with application to delta-notch signaling automata, HSCC,
LNCS 2623, 2003, pp. 233–248.
[ 8 ] Hasuo, I. and Suenaga, K.: Exercises in Nonstandard Static Analysis of hybrid systems, CAV,LNCS 7358, 2012, pp. 462–478.
[ 9 ] Henzinger, T. A.: The Theory of Hybrid Automata, Verification of Digital and Hybrid Systems(NATO ASI Series F: Computer and Systems Sciences), Vol. 170(2000), pp. 265–292.
[10] Henzinger, T. A., Ho, P.-H., and Wong-Toi,
H.: HyTech: A model checker for hybrid systems,
STTT, Vol. 1(1997), pp. 110–122.
[11] Hoare, C. A. R.: An Axiomatic Basis for Computer Programming, Communications of the ACM,
Vol. 12, No. 10(1969), pp. 576–580 and 583.
[12] Jha, S. K., Krogh, B. H., Weimer, J. E., andClarke, E. M.: Reachability for Linear Hybrid
Automata Using Iterative Relaxation Abstraction,
HSCC, LNCS 4416, 2007, pp. 287–300.
[13] Manna, Z. and Sipma, H.: Deductive Verification of Hybrid Systems Using STeP, HSCC,
LNCS 1386, 1998, pp. 305–318.
[14] Platzer, A.: Logical Analysis of Hybrid Systems,
Springer, 2010.
[15] Platzer, A.: Guide for KeYmaera Hybrid Systems Verification Tool, http://symbolaris.com/info/
KeYmaera-guide.html, 2012.
[16] Platzer, A. and Quesel, J. D.: KeYmaera: A
hybrid theorem prover for hybrid systems, IJCAR,LNCS 5195, 2008, pp. 171–178.
[17] Rodriguez-Carbonell, E. and Tiwari, A.: Generating Polynomial Invariants for Hybrid Systems,
HSCC, LNCS 3414, 2005, pp. 590–605.
[18] Sankaranarayanan, S., Sipma, H., and Manna,Z.: Constructing invariants for hybrid systems,
HSCC, LNCS 2993, 2004, pp. 539–554.
[19] Su, W., Abrial, J.-R., and Zhu, H.: Complementary Methodologies for Developing Hybrid Systems
with Event-B, ICFEM, LNCS 7635, 2012, pp. 230–
248.
[20] Tiwari, A.: HybridSAL relational abstracter,
CAV, LNCS 7358, 2012, pp. 725–731.