_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.