R. Alur, C. Courcoubetis, N. Halbwacks, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science 138, 1995, pp.3-34. ● ハイブリッド・システム(hybrid system) H = (Loc, Var, Lab, Edg, Act, Inv) Loc: (状態遷移グラフの)頂点の有限集合. 頂点はロケーション(location)という. Var: 実数値をとる変数の有限集合 付値(valuation)とは,X∈Varに対してv(x)∈Rとなる関数. 付値の全体をVと書く. 状態(state)は,ロケーションl∈Locと付値v∈Vの組(l,v). 状態の全体をΣと書く. Lab: 同期ラベル(synchronization label)の有限集合 足踏ラベル(stutter label)τが含まれる. Edg: 遷移(transition)の有限集合. 各遷移eは,e=(l,a,μ,l')という形をしている. l∈Loc: ソース・ロケーション(source location) l'∈Loc: ターゲット・ロケーション(target location) a∈Lab: 同期ラベル μ⊆V×V: 遷移関係(transition relation) 各ロケーションl∈Locに対して,制御変数(controlled variable) の有限集合Con⊆Varが存在して, (l,τ,IdCon,l) という形の足踏遷移が許される.IdConは,Con以外の変数に対しては 付値が等しくなるような遷移関係. (v,v')∈μに対して,(l',v')を(l,v)の遷移後継(transition successor) という. Act: 各ロケーションにアクティビティ(activity)の集合を与える関数. アクティビティとは,非負実数R≧0からVへの関数. 各ロケーションのアクティビティ(activity)は, 時間に対して不変(time-invariant)と仮定する. すなわち,l∈Loc,f∈Act(l),t∈R≧0に対して, (f+t)∈Act(l) と仮定する.ただし,t'∈R≧0に対して (f+t)(t') = f(t+t'). なお,l∈Loc,f∈Act(l),x∈Varに対して,関数f^xを次のように定義する. f^x(t)= f(t)(x) Inv: l∈Locに対してInv(l)⊆Vを与える.不変述語(invariant). ● 時間決定的(time-determinisitic)なハイブリッド・システム l∈Locとv∈Vに対して,f(0)=vを満たすf∈Act(l)は高々一つ. このようなfを, φl[v] と書く. ● ハイブリッド・システムの実行(run) 離散的(瞬間的)な遷移 時間の経過 t0 t1 t2 ρ = σ0 |→ σ1 |→ σ2 |→ ... f0 f1 f2 ただし, σi = (li,vi) ∈ Σ ti ∈ R≧0 fi ∈ Act(li) 以下の条件を満たす. 1. fi(0) = vi. 2. 0≦t≦ti に対して,fi(t) ∈ Inv(li). 3. σi+1 は,σ'i = (li,fi(ti)) の遷移後継. σ'i を σi の時間後継(time successor)という. σi+1 を σi の後継(successor)という. ハイブリッド・システム H の実行の全体を [H] と書く. ● 例 サーモスタット ___ ___ / \ / \ / l0 \ x = m / l1 \ │ │ -----------------> │ │ │ . │ │. │ x = M │ x = -Kx │ │x = K(h - x)│ ------> │ │ │ │ \ x ≧ m / <----------------- \ x ≦ M / \ / x = M \ /  ̄ ̄ ̄  ̄ ̄ ̄ この場合, f∈Act(l0) iff d f^x(t) -------- = -K f^x(t) d t iff f^x(t) = θexp(-Kt) f∈Act(l1) iff d f^x(t) -------- = K(h - f^x(t)) d t iff f^x(t) = θexp(-Kt) + h(1 - exp(-Kt)) v∈Inv(l0) iff v(x) ≧ m v∈Inv(l1) iff v(x) ≦ M (l0,a,μ0,l1): (v,v')∈μ0 iff v(x) = v'(x) = m (l1,a,μ1,l0) (v,v')∈μ0 iff v(x) = v'(x) = M ● ハイブリッド・システムの合成(composition) H1 = (Loc1, Var, Lab1, Edg1, Act1, Inv1) H2 = (Loc2, Var, Lab2, Edg2, Act2, Inv2) H1×H2 = (Loc1×Loc2, Var, Lab1∪Lab2, Edg, Act, Inv) ((l1,l2),a,μ,(l1',l2'))∈Edg iff (l1,a1,μ,l1')∈Edg1 (l2,a2,μ,l2')∈Edg1 a1=a2=a または (a1=a, not a1∈Lab2, a2=τ) または (a2=a, not a2∈Lab1, a1=τ) μ=μ1∩μ2 Act(l1,l2) = Act1(l1)∩Act2(l2) Inv(l1,l2) = Inv1(l1)∩Inv2(l2) ● 線形ハイブリッド・システム(linear hybrid system) l∈Locに対して,Act(l)が . x = k_x という形の微分方程式の集合によって定義される. 各x∈Varに対して上のような微分方程式が与えられる. k_x∈Zは整定数. k_xをAct(l,x)と書く.xのレート(rate)という. l∈Locに対して,Inv(l)は線形の論理式によって定義される. e∈Edgに対して,遷移関係μは,次のような ガード付きの非決定的な代入によって定義される. ψ ⇒ {x := [αx,βx] | x∈Var} これは次の条件を意味する. (v,v')∈μ iff v(ψ) ∧ ∀x∈Var. v(αx)≦v'(x)≦v(βx) ψは線形論理式(linear formula)であり,ガード(guard)という. αxとβxも線形式(linear term). αx=βxのとき,これをμ(e,x)と書く. ● 時間オートマトン(timed automaton) 線形ハイブリッド・システムの特殊な場合. 変数は,クロック(clock)または命題(proposition). クロック: Act(l,x) = 1. μ(e,x) = αx = βx ∈ {0,x}. すなわち,遷移関係は,変数の値を0にするか,変化させない. ガードや不変述語の中の線形の式は, x#c または x-y#c という形で,cは整定数,#は等号か不等号. Act(l,x)が1に限らない場合,歪んだクロック(skewed clock)という. 命題: Act(l,x) = 0. μ(e,x) = αx = βx ∈ {0,1}. ● マルチレートの時間システム(multirate timed system) 線形ハイブリッド・システムの特殊な場合. 変数は,歪んだクロックまたは命題. nレート(n-rate): レートの数がn. ● インテグレータ・システム(integrator system) 線形ハイブリッド・システムの特殊な場合. 変数は,インテグレータ(integrator)または命題. インテグレータ: Act(l,x)∈ {0,1}. μ(e,x) = αx = βx ∈ {0,x}. ● 例 相互排除プロトコル(Fischer's protocol) repeat repeat await k=0 k := i delay b until k=i Critical section k := 0 forever 二番目のプロセスの速度は一番目のプロセスの1.1倍. x>b ∧ k≠1 ┌──────────────┐ ↓ │ __ __ __ x>b __ / 1 \ / 2 \ / 3 \ ∧ / 4 \ │ . │k=0 │ . │k:=1 │ . │k=1 │ . │ →│ x=1 │─→ │ x=1 │─→ │ x=1 │─→ │ x=1 │ \ / x:=0 \xb ∧ k≠2 ┌──────────────┐ ↓ │ __ __ __ x>b __ / A \ / B \ / C \ ∧ / D \ │ . │k=0 │ . │k:=2 │ . │k=2 │ . │ →│ y=1.1│─→ │ y=1.1│─→ │ y=1.1│─→ │ y=1.1│ \ / y:=0 \y │ x = 1 │ y = 0 │ . │ │ . │ z = 0 │ y = 1 │ │ y = 1 │ ------> │ . │ x≧30 │ . │ \ z = 1 / <----------------- \ z = 0 / \ x≦1 / x := 0 \ /  ̄ ̄ ̄  ̄ ̄ ̄ x: 各ロケーションにおける経過時間 y: 経過時間 z: ガス漏れの累積時間 インテグレータ・システムである. 検証事項: y ≧ 60 ⇒ 20z ≦ y ● 線形ハイブリッド・システムに対する到達可能性問題 σ,σ'∈Σに対して,σからσ'に至る実行が存在するとき, * σ |-> σ' と書き,σ'はσから到達可能(reachable)であるという. 時間オートマトンの到達可能性問題は決定可能である[ACD93]. 線形ハイブリッド・システムは,遷移のガードと不変述語が, k∈Zに対して, x≦k または k≦x という形をしているとき,単純(simple)であるという. ● 定理3.1 単純な線形ハイブリッド・システムの到達可能性問題は決定可能である. すなわち,クロックのレートが複数個あってもよい(マルチレートでよい). 時間オートマトンに帰着する. クロックのレートをすべて1に合わせる. それに従って,ガードと不変述語の定数も合わせる. すなわち,xをk_x×xで置き換える.(単純ではなくなる.) propositionについては,そのまま. ● 定理3.2 2レートの時間システムの到達可能性問題は決定不能である. 非決定性2カウンタ機械の停止問題に帰着する. レートが1のクロックとレートが2のクロックを用いる. y: レート1 0が始まり,1になると0に戻る. カウンタ機械の1ステップを表現する. x1, x2: レート1 カウンタの値nを,クロックの値1/2^nで表現する. 時間システムの時刻iの状態によって,カウンタ機械の状態を表現する. 時刻iにおいて,x=1/2^nとする(xはx1またはx2). カウンタの値を変えない場合: x = 1 ⇒ x := 0 時刻i+1において再び1/2^nになる. カウンタの値を増やす場合: z: レート1 z': レート2 x = 1 ⇒ x := 0; z := 0 i i+1-1/2^n ? i+1 -------------------------------------------------- y 0 0 x 1/2^n 0 0 1/2^n+1 z 0 1/2^n z' 0 1/2^n 時刻?で,x := 0; z' := 0. 時刻i+1で,z=z'をチェック. カウンタの値を減らす場合: z: レート1 z': レート2 時刻?で,x := 0; z := 0. x = 1 ⇒ x := 0; z' := 0 i-1 ? i-1/2^n i i+1-1/2^n-1 ------------------------------------------------------------- y 0 0 x 1/2^n 0 0 z 0 1/2^n-1 z' 0 1/2^n-1 時刻i+1で,z=z'をチェック. z = 1 ⇒ x := 0 ● ハイブリッド・システムの検証 状態の集合をリージョン(region)という. R: リージョン R⊆Σ ● 前向きの解析(forward analysis) ↑ Rの状態の時間後継の全体 = ∪ (l,_l↑) l∈Loc R_lは,Rのロケーションlへの射影. post[R] Rの状態の遷移後継の全体 post[R] = ∪ (l',post_e[R_l]) e=(l,l')∈Edg ● 命題4.1 I: リージョン Iの状態から到達可能な状態からなるリージョンは, 以下の方程式の最小不動点である. X = ↑ ● 補題4.1 線形ハイブリッド・システムに対して, Pが付値の線形集合(linear set)ならば,

_l↑ post_e[P] も線形集合となる. 制御変数(control variable)pcを導入することにより, リージョンを線形論理式によって表現することができる. ψ_lがR_lを表現するとすると, ∨ (pc=l ∧ ψ_l) pc∈Loc Rが,線形論理式で表現できれば, ↓ post[R] も線形論理式で表現できる. しかし,不動点がそうなるとは限らない. ● 後向きの解析(backward analysis) ↓ Rの状態を時間後継として持つ状態の全体 pre[R] Rの状態を遷移後継として持つ状態の全体 ● 命題4.2 R: リージョン Rの状態へ到達可能な状態からなるリージョンは, 以下の方程式の最小不動点である. X = ↓ ● 補題4.2 補題4.1と同様. ● 近似的な解析(approximate analysis) 二つの問題とその解決法 線形不等式の選言(合併) ⇒ convex hull 不動点計算 ⇒ widening リージョンをpolyhedronで近似する. polyhedron: 線形不等式の有限集合で表現できる. そして,polyhedraの合併をconvex hullで近似する. P|_|P' = {λx+(1-λ)x' | x∈P, x'∈P', λ∈[0,1]} P∇P': widening P|_|P' ⊆ P∇P' polyhedraの無限増加列 P0,P1,P2,... に対して, Q0 = P0 Qn+1 = Qn∇Pn+1 と定義すると,Q0,Q1,... は有限で収束する. P∇P'の例 Pの線形制約のうちでP'が満たすもののみから定義されるpolyhedra 線形制約の数は減るばかりなので,有限で収束する. ● 最小化 π: Σの分割 R∈πが安定(stable)であるとは, 任意のR'∈πに対して, R∩pre[↓]≠φ ⇒ R⊆pre[↓] πがバイシミュレーション(bisimulation)であるとは, 任意のR∈πが安定. RF⊆Σがπをリスペクト(respect)するとは, RFがπのリージョンの合併になっている. 最小化手続(minimization procedure) RF⊆Σがリスペクトする分割を計算しながら, Iから到達可能なリージョンの集合を求める. 最終的に,RFがIから到達可能かどうかを調べる. π := {RF, Σ−RF} α := {R | R∩I≠φ} Iから到達可能なリージョンの集合 β := φ そのうちπに対して安定であることが わかっており,しかも, 継続のリージョンが調べられている リージョンの集合 while α≠β do choose R∈(α−β) let α' := split[π](R) より安定になるようにRを分割 if α'={R} then 分割の必要がない β := β∪{R} α := α∪{R'∈π | R|->R'} else α := α−{R} if ∃R'∈α' such that R'∩I≠φ then α := α∪{R'} fi β := β−{R'∈π | R|->R'} π := (π−{R})∪α' fi od return there is R∈α such that R⊆RF split[π](R) R'=pre[↓]∩RかつR'⊂Rを満たすR"∈πが存在すれば, split[π](R) := {R, R−R'} そうでなければ, split[π](R) := {R} ● TCTL 実時間時相論理を用いることにより,到達可能性だけでなく, 様々な性質を表現する. TCTL(timed computational tree logic) C: Varと共通部分を持たないクロックの集合 ψ: 状態論理式 VarとCの変数に関する線形論理式 TCTL論理式 φ ::= ψ | ¬φ | φ1∨φ2 | z.φ | φ1∃Uφ2 | φ1∀Uφ2 z∈C 位置(position) Cの変数による量化(quantification)を解釈するために導入. t0 t1 ρ: σ0 |→ σ1 |→ ... を実行とする. σi = (li,vi) π=(i,t): ρの中の位置 t≦ti 位置は辞書式順序で順序付けられる. ρ(π) = (li,φ_li[vi](t)) δ_ρ(π) = t + Σ tj jR' σ∈R|>R' iff σの時間後継σ'で,σ'∈pre[R']が成り立ち, σ'とσの間にあるすべての状態がR∪R'に含まれる ようなものが存在する. ● 補題4.3 RとR'が線形リージョンならば,R|>R'もそうである. ● 反復計算の例 φ∃Uφ' R = 【φ】 R' = 【φ'】 R0 = R' Ri+1 = Ri∪(R|>Ri) 【φ∃Uφ'】 = ∪i Ri ∀□φ = ¬(true∃U¬φ) R0 = 【φ】 Ri+1 = Ri∩¬(true|>¬Ri) 【∀□φ】 = ∩i Ri ∀◇≦cφ = z.∀◇(φ∧z≦c) R = 【φ】 R0 = 【z>c】 Ri+1 = Ri∪((¬R)|>Ri) 【∀◇≦cφ】 = ¬∪i Ri[z:=0] ●補足 ∃Uの解釈は,上述のように,反復計算によって求めることができる. しかし,∀Uの方は,反復計算では単純には求めることができない. 1)にあるように,timed automatonの場合は, region automatonを作ることができるので, 有限モデル検査の場合と同様にして, region automaton上における反復計算を行うことにより, ∀Uの解釈を求めることができる. 2)や3)では,以下のように,∀Uを∃Uに帰着させることにより, 最終的に∀Uの解釈を反復計算によって求める方法が与えられている. cを正の定数としたとき,【φ∀Uφ'】は以下を満たす最小のXである. X = 【φ'】∪(【φ∨φ'】∀U≦c X) ここで,【φ】∀U≦c【φ'】は,以下を満たす. 【φ】∀U≦c【φ'】 = 【¬z. ((¬φ')∃U(¬(φ∨φ')∨z>c))】 一般のhybrid automatonの場合, 反復計算は止まることが保証されていないが, もし止まったならば,求まった解釈は正しいものである. 1) R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2--34, May 1993. 2) Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244, June 1994. 3) R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic Symbolic Verification of Embedded Systems. IEEE Transactions on Software Engineering 22:181-201, 1996.