↑
● 補題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∃Ｕφ2 | φ1∀Ｕφ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'もそうである．
● 反復計算の例
φ∃Ｕφ'
R = 【φ】
R' = 【φ'】
R0 = R'
Ri+1 = Ri∪(R|>Ri)
【φ∃Ｕφ'】 = ∪i Ri
∀□φ = ¬(true∃Ｕ¬φ)
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]
●補足
∃Ｕの解釈は，上述のように，反復計算によって求めることができる．
しかし，∀Ｕの方は，反復計算では単純には求めることができない．
1)にあるように，timed automatonの場合は，
region automatonを作ることができるので，
有限モデル検査の場合と同様にして，
region automaton上における反復計算を行うことにより，
∀Ｕの解釈を求めることができる．
2)や3)では，以下のように，∀Ｕを∃Ｕに帰着させることにより，
最終的に∀Ｕの解釈を反復計算によって求める方法が与えられている．
cを正の定数としたとき，【φ∀Ｕφ'】は以下を満たす最小のXである．
X = 【φ'】∪(【φ∨φ'】∀Ｕ≦c X)
ここで，【φ】∀Ｕ≦c【φ'】は，以下を満たす．
【φ】∀Ｕ≦c【φ'】 = 【¬z. ((¬φ')∃Ｕ(¬(φ∨φ')∨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.