Safety and Liveness Properties

08-15

來自專欄霧雨魔法店45 人贊了文章

在程序運行時, 我們會特別在意程序的一些性質(Program properties), 例如程序正確, 程序停機, 無異常等等. 對於我們關心的程序性質, 將可以分為兩類:

Safety Properties, 在程序運行中不會進入非預期的狀態(如非法調用參數, 數組下標越界等運行錯誤).
Liveness Properties, 在程序運行中預期狀態一定會到達(如停機, 獲取資源請求一定有返回結果等等).

下面將介紹程序性質的拓撲結構, 最後展示對於任意程序性質, 均可將其分解為其Safety分量(safety component)與Liveness分量(liveness component)的交.

定義1: 轉移系統(transition system)

轉移系統由一個狀態集合 $Sigma$ 與轉移關係 $osubseteqSigma imesSigma$ 構成, 形如 $langleSigma, o angle$ .

其中狀態表示程序執行的當前狀態, 一般由當前執行程序位置(指令指針)與程序符號值(內存空間)構成. 轉移關係由程序語義定義.

定義2: 軌跡(trace)

$egin{align} &Sigma^{*} = igcup_{k=0}^{}Sigma^{k}\ &Sigma^{overrightarrow{*}} = left{ sigma=(sigma_1sigma_2cdotssigma_k)in Sigma^{*};|;forall i<|sigma|:sigma_i osigma_{i+1} ight} \ &Sigma^{overrightarrow{omega}} = left{ sigma=(sigma_1sigma_2sigma_3cdots)in Sigma^{omega};|;forall i:sigma_i osigma_{i+1} ight}\ &Sigma^{overrightarrow{infty}} = Sigma^{overrightarrow{*}}cupSigma^{overrightarrow{omega}} end{align}$

( $|sigma|$ 為 $sigma$ 的長度)

顯然 $Sigma^{overrightarrow{*}}subseteqSigma^{overrightarrow{infty}}$ , 其中 $sigmainSigma^{overrightarrow{infty}}$ 稱為trace.

定義3: 拼接(concatenation), 前綴(prefix), 後綴(suffix), 拓展(extension)

對於 $u=(u_1cdots u_n)inSigma^{overrightarrow{*}}$ , $v=(v_1,v_2cdots)inSigma^{overrightarrow{infty}}$ , $u_{n} o v_1$ , 記 $uv=(u_1cdots u_n,v_1,v_2cdots)$ 為 $u$ 與 $v$ 的拼接.

對於 $U, Vsubseteq Sigma^{overrightarrow{infty}}$ , 記 $UV=left{ uv;|;uin U,vin V ight}$ .

若 $exists v:uv=w$ 則稱 $u$ 為 $w$ 的前綴, $v$ 為 $w$ 的後綴, 記作 $upreceq w$ , 稱 $w$ 為 $u$ 的拓展, 記作 $wsucceq u$ .

空串為 $epsilon$ , 其中有 $|varepsilon|=0$ , $epsilonsigma=sigmaepsilon=sigma$ .

定義4: Prefix與Extension Closed

令 $VsubseteqSigma^{overrightarrow{infty}}$

若 $forall upreceq vin V$ 有 $uin V$ , 則稱 $V$ 為prefix closed.
若 $forall wsucceq vin V$ 有 $win V$ , 則稱 $V$ 為extension closed.

定義5: Limit Closed與Finite Witnesses

令 $VsubseteqSigma^{overrightarrow{infty}}$

若 $forall win Sigma^{overrightarrow{infty}}$ , 對於任意有限長度 $upreceq w$ 均滿足 $uin V$ 那麼有 $win V$ , 則稱 $V$ 為limit closed.
若 $forall win V$ , 存在有限長度 $upreceq w$ 使得 $uin V$ , 則稱 $V$ 為finite witnesses.

命題1: $VsubseteqSigma^{overrightarrow{infty}}$ 為prefix closed(extension closed)集, 則 $Sigma^{overrightarrow{infty}}setminus V$ 為extension closed(prefix closed)集.

證明:

若 $Sigma^{overrightarrow{infty}}setminus V$ 為非extension closed集, 則 $exists wsucceq vin Sigma^{overrightarrow{infty}}setminus V: w otin Sigma^{overrightarrow{infty}}setminus V$ 即 $win V$ . 因為 $V$ 為prefix closed, 故 $wsucceq vin V$ . 矛盾, 故 $Sigma^{overrightarrow{infty}}setminus V$ 為extension closed集.

類似地, 若 $V$ 為extension closed集, 則 $Sigma^{overrightarrow{infty}}setminus V$ 為prefix closed集.

命題2: $VsubseteqSigma^{overrightarrow{infty}}$ 為limit closed(finite witnesses)集, 則 $Sigma^{overrightarrow{infty}}setminus V$ 為finite witnesses(limit closed)集.

證明:

若 $Sigma^{overrightarrow{infty}}setminus V$ 為非finite witnesses集, 則 $exists win Sigma^{overrightarrow{infty}}setminus V: forall upreceq w: u otin Sigma^{overrightarrow{infty}}setminus V$ ( $u$ 長度有限) 即 $forall upreceq w: uin V$ . 因為 $V$ 為limit closed, 故 $win V$ . 矛盾, 故 $Sigma^{overrightarrow{infty}}setminus V$ 為finite witnesses集.

類似地, 若 $V$ 為finite witnesses集, 則 $Sigma^{overrightarrow{infty}}setminus V$ 為limit closed集.

定義6: Topology space on $Sigma^{overrightarrow{infty}}$ : $(Sigma^{overrightarrow{infty}}, au)$

$au$ 為開集族(open sets), $au = left{ WSigma^{overrightarrow{infty}};|;WsubseteqSigma^{overrightarrow{*}} ight}$ .

命題3: $au$ 為開集族

證明:

? $emptyset=WSigma^{overrightarrow{infty}}in au$ , 其中 $W=emptyset$ .

? $Sigma^{infty}=WSigma^{overrightarrow{infty}}in au$ , 其中 $W={epsilon}$ .

? $W_{alpha}subseteqSigma^{overrightarrow{*}}$ , $alphain I$ , 有 $igcup_{alphain I}^{}(W_{alpha}Sigma^{overrightarrow{infty}})=WSigma^{overrightarrow{infty}}in au$ , 其中 $W=left( igcup_{alphain I}^{}W_{alpha} ight)subseteqSigma^{overrightarrow{*}}$ .

? $U, Vsubseteq Sigma^{overrightarrow{*}}$ , 定義 $U_{V}={uin U;|;exists vin V: vpreceq u}subseteq U$ , 類似地定義 $V_{U}$ .

$egin{align} &win USigma^{overrightarrow{infty}}cap VSigma^{overrightarrow{infty}}\ Leftrightarrow;&exists uin U, vin V: x, yin Sigma^{overrightarrow{infty}}, w=ux=vy\ Leftrightarrow;&win V_USigma^{overrightarrow{infty}}; ext{or};win U_VSigma^{overrightarrow{infty}};(upreceq v; ext{or};vpreceq u) end{align}$

因此有 $USigma^{overrightarrow{infty}} cap VSigma^{overrightarrow{infty}}=U_VSigma^{overrightarrow{infty}} cup V_USigma^{overrightarrow{infty}}$ , 設 $W=U_V cup V_UsubseteqSigma^{overrightarrow{*}}$ , 那麼

$USigma^{overrightarrow{infty}} cap VSigma^{overrightarrow{infty}}=WSigma^{overrightarrow{infty}}in au$ .

故 $(Sigma^{overrightarrow{infty}}, au)$ 為 $Sigma^{overrightarrow{infty}}$ 上的一個拓撲.

引理1: $VsubseteqSigma^{overrightarrow{infty}}$ 為閉集當且僅當:

$forall win Sigma^{overrightarrow{infty}}$ 若對於任意有限長度 $upreceq w$ 存在 $vsucceq u$ 使得 $vin V$ , 那麼 $win V$ .

證明:

$(Rightarrow)$ 若 $VsubseteqSigma^{overrightarrow{infty}}$ 為閉集, 則存在 $UsubseteqSigma^{overrightarrow{*}}$ 滿足 $Sigma^{overrightarrow{infty}}setminus V=USigma^{overrightarrow{infty}}$ , 若 $win Sigma^{overrightarrow{infty}}, w otin V$ , 那麼 $win USigma^{overrightarrow{infty}}$ , 存在長度有限前綴 $upreceq w, uin U$ , 有 $forall vsucceq u: vin USigma^{overrightarrow{infty}}$ 即 $v otin V$ , 故逆否命題 $(forall (win Sigma^{overrightarrow{infty}}, ext{finite};upreceq w): exists vsucceq u: vin V) o win V$ 成立.

$(Leftarrow)$ 令 $U=left{ uinSigma^{overrightarrow{*}};|; forall vsucceq u: v otin V ight}$ , 顯然 $USigma^{overrightarrow{infty}}subseteqSigma^{overrightarrow{infty}}setminus V$ . 若 $w otin V$ 則有 $exists ext{finite};upreceq w: forall vsucceq u: v otin V$ , 那麼 $uin U$ 故 $exists v:uv=w$ 即 $win USigma^{overrightarrow{infty}}$ , $Sigma^{overrightarrow{infty}}setminus Vsubseteq USigma^{overrightarrow{infty}}$ . 因此 $USigma^{overrightarrow{infty}}=Sigma^{overrightarrow{infty}}setminus V$ 為開集, 即 $V$ 為閉集.

命題4: open and closed set

令 $VsubseteqSigma^{overrightarrow{infty}}$

$V$ 為閉集當且僅當 $V$ 為prefix closed與limit closed.
$V$ 為開集當且僅當 $V$ 為extension closed與finite witnesses.

證明:

? $(Rightarrow)$ 若 $V$ 為閉集, 對於任意 $upreceq vin V$ , 設 $u^{}$ 為 $u$ 的任意有限前綴 $u^{}preceq u$ , 有 $vsucceq u succeq u^{}$ , 根據引理1得 $uin V$ 即 $V$ 為prefix closed.

由引理1直接可得 $V$ 為limit closed.

$(Leftarrow)$ 若 $V$ 為prefix closed與limit closed, 若 $w otin V$ 即 $win Sigma^{overrightarrow{infty}}setminus V$ , 由命題1和命題2得, $Sigma^{overrightarrow{infty}}setminus V$ 為extension closed與finite witnesses, 由finite witnesses存在有限長度 $upreceq w$ 使得 $uin Sigma^{overrightarrow{infty}}setminus V$ , 又由extension closed對於任意 $vsucceq u$ 均有 $vin Sigma^{overrightarrow{infty}}setminus V$ 即 $v otin V$ , 故其逆否命題 $(forall (win Sigma^{overrightarrow{infty}}, ext{finite};upreceq w): exists vsucceq u: vin V) o win V$ 成立. 由引理1得 $V$ 為閉集.

? $V$ 為開集當且僅當 $V$ 為extension closed與finite witnesses.

$Leftrightarrow$ $Sigma^{overrightarrow{infty}}setminus V$ 為prefix closed與limit closed. (命題1和命題2)

$Leftrightarrow$ $Sigma^{overrightarrow{infty}}setminus V$ 為閉集 (proved above)

$Leftrightarrow$ $V$ 為開集

命題5: closure與interior

令 $VsubseteqSigma^{overrightarrow{infty}}$

$cl(V)=left{ winSigma^{overrightarrow{infty}} ;|; forall ext{finite};upreceq w:exists vsucceq u: vin V ight}$ .
$int(V)=left{ winSigma^{overrightarrow{infty}} ;|; exists ext{finite};upreceq w:forall vsucceq u: vin V ight}$ .

證明:

? 令 $C(V)=left{ winSigma^{overrightarrow{infty}} ;|; forall ext{finite};upreceq w:exists vsucceq u: vin V ight}$ , $forall win Sigma^{overrightarrow{infty}}$ 若對於任意有限長度 $upreceq w$ 存在 $vsucceq u$ 使得 $vin C(V)$ , 由 $C(V)$ 的定義存在 $v^{}succeq u$ 使得 $v^{}in V$ , 故 $win C(V)$ 由引理1得 $C(V)$ 為閉集.

令 $Vsubseteq Gamma subseteqSigma^{overrightarrow{infty}}$ , $Gamma$ 為閉集, 設 $win C(V)$ 那麼有 $forall ext{finite};upreceq w:exists vsucceq u: vin V subseteq Gamma$ , 又由 $Gamma$ 為閉集, 根據引理1得 $win Gamma$ 即 $C(V)subseteqGamma$ .

故 $C(V)$ 為 $V$ 的closure.

? 令 $I(V)=left{ winSigma^{overrightarrow{infty}} ;|; exists ext{finite};upreceq w:forall vsucceq u: vin V ight}$ , 設 $win I(V)$ 那麼 $exists ext{finite};upreceq w:forall vsucceq u: vin V$ , 由 $I(V)$ 的定義 $forall vsucceq u: vin I(V)$ , 故 $win uSigma^{overrightarrow{infty}}subseteq I(V)$ 且 $uSigma^{overrightarrow{infty}}$ 為開集, $I(V)=igcup_{win I(V)}^{}uSigma^{overrightarrow{infty}}$ 因此 $I(V)$ 為開集.

令 $winDeltasubseteq V$ , $Delta$ 為開集, 故存在 $U subseteqSigma^{overrightarrow{*}}$ 滿足 $win USigma^{overrightarrow{infty}} subseteq Delta$ , 因此 $exists uin U: upreceq w$ , 故 $forall vsucceq u: vin USigma^{overrightarrow{infty}} subseteq Deltasubseteq V$ , 根據 $I(V)$ 定義有 $win I(V)$ 即 $Deltasubseteq I(V)$ .

故 $I(V)$ 為 $V$ 的interior.

定義7: safety property與liveness property

若 $forall winleft(Sigma^{overrightarrow{infty}}setminus W ight): exists ext{finite};upreceq w; ext{s.t.};forall v:uvinleft(Sigma^{overrightarrow{infty}}setminus W ight)$ 則稱 $W$ 為safety property.
若 $forall ext{finite};u:exists v; ext{s.t.};uvin W$ 則稱 $W$ 為liveness property.

注: safety property的含義為若某trace違反safety property則能通過其有限長度的前綴識別. liveness property的含義為對於任意的有限長度的trace, 總存在拓展滿足liveness property.

命題6: $W$ 為safety property當且僅當 $W$ 為閉集.

證明:

$W$ 為safety property

$egin{align} &Leftrightarrow forall winleft(Sigma^{overrightarrow{infty}}setminus W ight): exists ext{finite};upreceq w; ext{s.t.};forall v:uvinleft(Sigma^{overrightarrow{infty}}setminus W ight)\ &Leftrightarrow left(forall w otin W ight) oleft(exists ext{finite};upreceq w; ext{s.t.};forall u^{}succeq u:u^{}inleft(Sigma^{overrightarrow{infty}}setminus W ight) ight)\ &Leftrightarrow left(forall ext{finite};upreceq w; ext{s.t.};exists u^{}succeq u:u^{}in W ight) o win W quad ext{[contrapositive]}\ &Leftrightarrow W; ext{is closed};quad ext{[lemma 1]}\ end{align}$

命題7: $V$ 為liveness property當且僅當 $V$ 稠密.

證明:

$(Rightarrow)$ $V$ 為liveness property. 設 $Vsubseteq Gamma$ , $Gamma$ 為閉集. 若存在 $winSigma^{overrightarrow{infty}}setminus Gamma$ 即 $w otinGamma$ , 由引理1得存在有限長度 $upreceq w$ 對於任意 $vsucceq u$ 使得 $v otin V$ . 又由 $V$ 為liveness property, 故存在 $vsucceq u$ 滿足 $vin Vsubseteq Gamma$ , 矛盾. 故 $Sigma^{overrightarrow{infty}}setminus Gamma=emptyset$ 即 $Gamma=Sigma^{overrightarrow{infty}}$ , $V$ 稠密.

$(Leftarrow)$ $V$ 稠密. 若 $V$ 不為liveness property, 則存在有限長度 $u$ 使得 $forall vsucceq u$ 均有 $v otin V$ , 因此 $uSigma^{overrightarrow{infty}}subseteqSigma^{overrightarrow{infty}}setminus V$ 即 $VsubseteqSigma^{overrightarrow{infty}}setminus uSigma^{overrightarrow{infty}}$ , 又 $Sigma^{overrightarrow{infty}}setminus uSigma^{overrightarrow{infty}}$ 為閉集, 而 $V$ 稠密, 故 $Sigma^{overrightarrow{infty}}setminus uSigma^{overrightarrow{infty}}=Sigma^{overrightarrow{infty}}$ , $uSigma^{overrightarrow{infty}}=emptyset$ 即 $u$ 不存在, 矛盾. 故 $V$ 為liveness property.

定義8: safety component與liveness component

$safe(V)=cl(V)$ .
$live(V)=Sigma^{overrightarrow{infty}}setminus left( cl(V)setminus V ight)$ .

引理2: $(X, au)$ 為Topology space, $Ysubseteq X$ 則 $Xsetminus (cl(Y)setminus Y)$ 稠密.

證明:

設 $Xsetminus (cl(Y)setminus Y)subseteq Z$ , $Z$ 為閉集.

$Xsetminus Z subseteq cl(Y) setminus Y$

又由 $Ysubseteq cl(Y)$ 故

$Ysubseteq cl(Y)setminus(Xsetminus Z)$

$Xsetminus Z$ 為閉集故 $cl(Y)setminus(Xsetminus Z)$ 亦為閉集, 那麼有 $cl(Y)setminus(Xsetminus Z) subseteq cl(Y)$ 即 $Xsetminus Z=emptyset$ , $Z=X$ . 因此 $Xsetminus (cl(Y)setminus Y)$ 稠密.

推論1: $V$ 為safety property當且僅當 $safe(V)=V$ .

證明:

由命題6得, $V$ 為safety property當且僅當 $V$ 為閉集, 故 $V=cl(V)overset{mathrm{def}}{=}safe(V)$ .

推論2: 對於任意 $VsubseteqSigma^{overrightarrow{infty}}$ , $safe(V)$ 為safety property.

證明:

$safe(V)overset{mathrm{def}}{=}cl(V)$ 為閉集, 由命題6得, $safe(V)$ 為safety property.

推論3: $V$ 為liveness property當且僅當 $live(V)=V$ .

證明:

由命題7得, $V$ 為liveness property當且僅當 $V$ 稠密, 故 $cl(V)=Sigma^{overrightarrow{infty}}$ $live(V)overset{mathrm{def}}{=}Sigma^{overrightarrow{infty}}setminus left( cl(V)setminus V ight)=Sigma^{overrightarrow{infty}}setminus left( Sigma^{overrightarrow{infty}}setminus V ight)=V$ .

推論4: 對於任意 $VsubseteqSigma^{overrightarrow{infty}}$ , $live(V)$ 為liveness property.

證明:

$live(V)overset{mathrm{def}}{=}Sigma^{overrightarrow{infty}}setminus left( cl(V)setminus V ight)$ 由引理2得其稠密, 由命題7得, $live(V)$ 為liveness property.

引理3: $(X, au)$ 為Topology space, $Ysubseteq X$ 則

$Y=cl(Y)cap(Xsetminus (cl(Y)setminus Y))$

證明:

$egin{align} cl(Y)cap(Xsetminus (cl(Y)setminus Y))&=(Xcap cl(Y))setminus ((cl(Y)setminus Y)cap cl(Y))\ &=cl(Y)setminus (cl(Y)setminus Y)\ &=Y end{align}$

定理1: property decomposition

對於任意性質 $P$ , 其均可分解為safety component與liveness component的交.

$P=safe(P)cap live(P)$

證明:

$egin{align} P&=safe(P)cap live(P)\ &overset{mathrm{def}}{=}cl(P)capleft(Sigma^{overrightarrow{infty}}setminus (cl(P)setminus P) ight)\ &=Pquad ext{[lemma 3]} end{align}$

一個例子:

程序total correctness可以分解為partial correctness(safety component)與termination(liveness component).

$UpsilonsubseteqSigma$ 為初始狀態.
$OmegasubseteqSigma$ 為終止狀態.
$PsisubseteqUpsilon imesOmega$ 為partial correctness relation.
$Phioverset{mathrm{def}}{=}left{ (s,s^{});|;(sinUpsilon) Rightarrow((s o^{*}s^{})wedge (s^{}inOmega)wedge (s,s^{})inPsi) ight}$ 為total correctness relation.

partial correctness:

$forall s,s^{}inSigma:left((s o^{*}s^{})wedge (sinUpsilon)wedge (s^{}inOmega)) ight)Rightarrow left( (s,s^{})inPsi ight)$

termination:

$forall sigmainSigma^{overrightarrow{*}}:left( sigma_0 inUpsilon ight)Rightarrowleft(exists l=|sigma|:sigma_linOmega ight)$

total correctness:

$forall sigmainSigma^{overrightarrow{*}}:left(exists l=|sigma|:(sigma_1,sigma_l)inPhi ight)$

證明:

$egin{align} &forall sigmainSigma^{overrightarrow{*}}:left( sigma_0 inUpsilon ight)& ext{[initial states]}\ Rightarrow;&sigma_0 inUpsilonwedgeexists l=|sigma|:sigma_linOmega& ext{[termination]}\ Rightarrow;&(sigma_0, sigma_l)inPsi& ext{[partial correctness]}\ Rightarrow;&(sigma_0, sigma_l)inPhi& ext{[proving total correctness]}\ end{align}$

好久都沒寫新文章啦, 最近了解了一下程序性質的拓撲結構覺得還蠻有趣的, 所以來寫個小文章介紹一下. 有機會將來再深入介紹一下在此之上與Linear temporal logic(LTL)的一些有趣的性質, 在model checking中有著比較多的應用.

謝謝大家的閱讀~