Computer Aided Verification 計算機輔助驗證 Model Checking (Part II) 模型檢驗 (二) CTL, TCTL, and Symbolic Model Checking) (Chapters: 4, 17, 5, 6 of “Model Checking” book) Pao-Ann Hsiung Department of Computer Science and Information Engineering National Chung Cheng University, Taiwan 熊博安 國立中正大學 資訊工程研究所 These slide contents are adapted from the slides of Professor Farn Wang.

Contents CTL Model Checking Timed Automata (TA) Timed Computation Tree Logic (TCTL) TCTL Model Checking Clock Zones, DBM, BDD Symbolic Model Checking Counterexample & Witnesses

模型檢驗（Model Checking） 模型檢驗問題的定義： 給定一個有限狀態結構 M 與一個時態邏輯公式φ，請問M是φ的一個模型嗎？

模型檢驗（Model Checking） 狀態空間分析 規則系統行為 有限但極大(天文數字)之狀態空間 狀態空間表示法：有向圖 節點：系統狀態 箭頭：狀態轉換 規則系統行為 有限但極大(天文數字)之狀態空間 執行 完成 等待

CTL模型檢驗的演算法 給定M 與φ 1. 將Closure(φ)中的公式，由小到大排列 φ0 φ1 φ2 … φn 對所有0 i<j  n，φj 不是φi 的子公式！ 2. 依序由i=0 到 n，對所有M 中的狀態 s，計算 M, s┝φi (第七頁的方法) 3. 如果M的啟始狀態是 s0，且M, s0┝φ， 則回答“是”;否則回答“否”!

Closure(φ) 是所有φ的子公式所成的集合 φ 的子公式為φ φψ 、 φψ 的子公式為φ 、ψ φψ的子公式為φ 、ψ φUψ的子公式為φ 、ψ 、  φUψ φUψ的子公式為φ 、ψ 、 φUψ φ、 φ 的子公式為φ φ 的子公式為φ 、 φ φ 的子公式為φ 、 φ φ的子公式為φ 、  φ φ的子公式為φ 、  φ

CTL模型檢驗的演算法（續） 若φi 為 true，則 M,s┝φi 若φi 為 φ，則 M,s┝φi iff not M,s┝φ 若φi 為φψ，則 M,s┝φi iff M,s┝φ 或M,s┝ψ 若φi 為 φUψ，則由所有滿足ψ 的狀態開始，沿著滿足φ的所有的反向路徑上的狀態，都滿足φUψ 若φi 為 φ，找出 M 中所有狀態都滿足φ的Strongly Connected Components（SCC）。由這些SCC開始，沿著滿足φ的所有的反向路徑上的狀態，都滿足φ。 注意： φUψ  (( φ U (φψ)) ψ)

CTL模型檢驗的演算法（續） 若φi為φUψ，則由所有滿足ψ 的狀態開始，沿著滿足φ的所有的反向路徑上的狀態，都滿足φUψ。 For all state s with M,s┝ψ, M,s┝ φUψ holds Repeat until no more change can be made: For all (s', s), if M,s'┝φ and M,s┝ φUψ, then M,s'┝ φUψ 此一計算一定會停止，因為每一個φUψ都是被有限長度路徑所滿足。Repeat迴圈只需循環到最長的最短路徑長度。

CheckEU(f1, f2) for  f1U f2

CTL模型檢驗的演算法（續） 若φi 為 φ，找出 M 中所有狀態都滿足φ的Strongly Connected Components（SCC）。由這些SCC開始，沿著滿足φ的所有的反向路徑上的狀態，都滿足φ。 將M中，不滿足φ的狀態都刪掉。 執行transitive closure以計算剩餘狀態間的路徑。 Reach[s,s’]=1如果由s到s’之間，有一條路徑 Reach[s,s’]=0如果由s到s’之間，沒有路徑 For all s, M,s┝ φ iff s’(Reach[s,s’]  Reach[s’,s’])

CTL模型檢驗的演算法（續） 在M（剩餘的M）中，所有狀態都滿足φ。 執行 transitive closure: For all s, s do if (s, s)M, Reach[s, s] := 1; else Reach[s, s] := 0; For s, s do For all s do Reach[s, s] := Reach[s, s]  (Reach[s, s]  Reach[s, s]);

Strongly Connected Components (SCC) A strongly connected component (SCC) C is a maximal sub-graph such that every node in C is reachable from every other node in C along a directed path entirely contained within C. s1 s2 s3 s4 s5 Two SCC: {s1, s2, s3} {s4}

CheckEG( f1) for  f1

Microwave Oven Example

Microwave Oven Example (Start  ◇Heat) ◇(Start  Heat) S(Start) = {2, 5, 6, 7} S(Heat) = {1, 2, 3, 5, 6} SCC(Heat) = {1, 2, 3, 5} S(Heat) = {1, 2, 3, 5} S(Start  Heat) = {2, 5} S(◇(Start  Heat)) = {1,2,3,4,5,6,7} S(◇(Start  Heat)) = 

Fairness Constraints F = {P1, …, Pk} // fairness constraints Fair SCC C  Pi  F, state ti  (C  Pi). CheckFairEG(f1): Fair SCCs Define “fair”: atomic proposition, true at a state s iff there is a fair path starting at s. M, s┝ p  fair, M, s┝ (f1  fair), CheckEUFair(f1, f2) = CheckEU(f1, f2fair) = M, s┝  (f1 U (f2  fair))

Microwave Oven (with Fairness) (Start  ◇Heat) F = {◇(Start  Close  Error)} S(Start) = {2, 5, 6, 7} S(Heat) = {1, 2, 3, 5, 6} SCC(Heat) = {1, 2, 3, 5} is NOT fair S(Heat) = { } S(◇(Start  Heat)) = { } S(◇(Start  Heat))={1,2,3,4,5,6,7}

Model Checking Real-Time Systems Timed Automata (TA) Real-Time Properties: Timed Computation Tree Logic (TCTL) Given a real-time system S modeled by a set of TA {A1, A2, …, An} and a real-time property specified by a TCTL formula , check if S satisfies  (S┝  ?).

 ::= p | x  c | x-y  y | 1 | 12 Timed Automata真時自動機 狀態條件敘述（state predicate）： 以proposition集合P與時鐘變數集合X，建構而成  ::= p | x  c | x-y  y | 1 | 12 pP; x, y X; c,dN; ‘’{ ,  , ,  , } 範例： 男性  未婚  年齡  30 孤單  男性  未婚  今日+2  收假日 戰機巡航模式  x+5  回報週期

 ::= p | x  c | xcy+d | 1 | 12 Timed Automata真時自動機 狀態條件敘述（state predicate）： 以proposition集合P與時鐘變數集合X，建構而成  ::= p | x  c | xcy+d | 1 | 12 pP; x, y X; c,dN; ‘’{ ,  , ,  , } 縮寫： true  x = x 12  ((1)(2)) 1 2  (1)2 (P, X)： 所有由P、X建構而成的狀態條件敘述之集合

Timed Automata真時自動機 A = Q, q0, P, X, , E, ,  Q : 有限控制點的集合 (set of control locations) q0 : 啟始控制點 (initial location) P : 命題的集合 (set of propositions) X : 時鐘變數的集合 (set of clock variables)  : Q (P,X)；各控制點的恆定條件 (invariant) EQQ : 控制點轉換的集合 (set of transitions)  : E (P, X)；各轉換的激發條件 (triggering condition)  : E 2X : 在轉換時，要被reset成零（歸零）的時鐘變數的集合 (set of clocks to be reset)

A=Q, q0, P, X, , E, ,  Q={監控，命中} E={(監控,監控),(監控,命中)} q0=監控  (監控 ,監控)= z =50 P = { }, X = {x, y}  (監控 ,命中)= true  (監控)= x  500z  50  (監控 ,監控)= {z}  (命中)= true  (監控 ,命中)= {} 監控 x  500ms z  50ms x:=0; z:=0 命中 z=50ms z:=0

Parallel Composition of TA A1=Q1, q01, P1, X1, 1, E1, 1, 1, A2=Q2, q02, P2, X2, 2, E2, 2, 2 A1 ∥A2 =  Q1  Q2, q0, P1  P2 X1  X2 , E, 1  2, 1  2  q0: a merge of q01 and q02 (q, q') = 1(q)  2(q') E: set of interleaved transitions with synchronization transitions identified

A Manufacturing Example

Manufacturing Ex: D-Robot TA

Manufacturing Ex: G-Robot TA

Manufacturing Ex: Station TA

Manufacturing Ex: Box TA

Model of Manufacturing System M = D-Robot || G-Robot || Station || Box Transitions with same labels are identified as one in M. E.g.: g-put in G-Robot, Station, and Box E.g.: d-pick in D-Robot, Station, and Box

真時自動機的語意 A = Q, q0, P, X, , E, ,  狀態 s = (q,) q  Q  : P  {true, false}  X R+ ; 定義所有Boolean變數的真假值 定義所有時鐘變數的非負實數讀值 ┝ (q) ; 時鐘讀值與proposition設定，須滿足控制點的恆定條件

真時自動機的語意 A=Q, q0, P, X, , E, ,   ┝ ： 滿足一個狀態條件敘述 　　(state predicate)   ┝ p iff  (p) = true  ┝ x  c iff  (x)  c  ┝ x - y  d iff  (x) - v(y)  d  ┝ 1 iff not  ┝ 1  ┝ 12 iff ┝ 1 或 ┝ 2 狀態 s = (q,) ； s ┝  iff  ┝ 

真時自動機的語意 兩個狀態的符號定義 給定一個 R+，    是一個新函數 (  )(p) =  (p) (  )(x) =  (x)   給定一個 Y X ， Y是一個新函數 (Y)(p) =  (p) (Y)(x) = 0 iff x Y (Y)(x) =  (x) iff x Y 給定 s = (q,) 與 Y  X ， sY = (q,Y)

真時自動機的語意 從直觀上看， dense-time自動機的計算（computation），應該是 對映到R+ （非負實數集合）的一個狀態序列； 具有狀態的稠密性；

真時自動機的語意 A=Q, q0, P, X, , E, ,  一個轉換 (transition) 的符號定義 給定s = (q,) 與 s' = (q', ') ， ss'（狀態 s與狀態 s'間，有一個轉換）iff (q, q')  E s┝  (q, q') s (q, q')┝  (q')

真時自動機的語意 A=Q, q0, P, X, , E, ,  的計算 (computation) s0-run: s0 s1 s2 ... sk ... ... ... 對所有k  0， sk 是具有如(q,)格式的狀態。 存在一個monotonically increasing、divergent的非負實數序列 t0 t1 t2 ... tk ... ... ... 對所有k  0， 對所有 t[0, tk+1tk ]， sk t┝ (q) Either sk  (tk+1tk ) = sk+1 or sk  (tk+1tk )  sk+1

Timed Computation Tree Logic (TCTL) 範例：從現在的狀態開始，有一種可能將來，七天會發薪水。 7發薪水 範例：從現在開始，無論將來如何，十年內要結婚。  10 結婚

TCTL（續） 範例：在任何計算狀態，敵機出現，都可能在五秒內擊落。 (發現敵機   5 擊落敵機)) 範例： 在任何狀態，不管如何計算，敵機都會在五秒內擊落。 (發現敵機   5 擊落敵機))

TCTL（續） 範例：從任何狀態開始，都有一種計算，時間會無限增加。 1true 範例：從任何狀態開始，對所有計算，時間都會無限增加。 1true

φ ::=  | φ1 | φ1φ2 | φ1U cφ2 |  cφ1 TCTL的語法 φ ::=  | φ1 | φ1φ2 | φ1U cφ2 |  cφ1   (P, X)：所有由P、X建構而成的狀態條件敘述之集合; c  N; ‘’  {, , , , }

TCTL的語法 縮寫： φ1φ2  ((φ1)(φ2)) φ1 φ2  (φ1)φ2 φ1φ2  ((φ1)(φ2)) φ1 φ2  (φ1)φ2  cφ   trueU cφ  cφ    c φ φ1U cφ2  ( ((φ2)U c(φ1φ2))   cφ2)  cφ   trueU cφ

TCTL的語意 A=Q, q0, P, X, , E, ,  A,(q,)┝φ; 狀態 (q,) 滿足φ A,(q,)┝ ； 定義如state predicate 者 A,(q,)┝ φ1 iff not A,(q,)┝φ1 A,(q,)┝ φ1φ2 iff A,(q,)┝φ1 或 A,(q,)┝φ2 A,(q,)┝ φ1U cφ2 iff ... A,(q,)┝  cφ1 iff ...

TCTL的語意 A=Q, q0, P, X, , E, ,  A,(q,)┝ φ1U cφ2 iff 存在 (q,)-run：s0 s1 s2 ... sk ... ... ... ，與 monotonically increasing、divergent的非負實數序列：t0 t1 t2 ......與 k  0，與 t [0, tk+1  tk]， tk+t t0  c A,sk+t┝φ2 對所有k  h  0與 t’ [0,th+1  th]， A, sh+t’┝φ1 對所有 t’ [0 ,t)，A, sk+t’┝φ1

TCTL的語意 A = Q, q0, P, X, , E, ,  A,(q,)┝  cφ1 iff 存在 (q,)-run：s0 s1 s2 ... sk ... ... ... ，與 monotonically increasing、divergent的非負實數序列：t0 t1 t2 ...... 對所有k  0，與 t [0, tk+1  tk]， 若 tk+t t0  c，則 A,sk+t┝φ1

A ┝φ iff  ， 若┝(q0)，則A,(q0, ) ┝φ TCTL模型檢驗問題 定義： A ┝φ（A滿足φ ；A是φ的一個模型） 給定一個A=Q, q0, , E, , 與一個TCTL公式φ， A ┝φ iff  ， 若┝(q0)，則A,(q0, ) ┝φ TCTL模型檢驗問題： 請問A是φ的一個模型嗎？

TCTL模型檢驗問題的反思 如何在無限、稠密的狀態空間中，分割出有限的discrete狀態空間？ 工程經驗： 在任何即時系統中，雖然面對無限的大自然環境，在電腦的觀測中，還是以有限的flag、switch來描述，並控制系統的行為。

TCTL模型檢驗問題的反思 平交道監視器的範例 x:=0; x=300 x=100 x:=0; 在即時系統中，用clock來控制! 遙遠 1/2 公里內 x=300 x=100 x:=0; 火車剛剛通過 在平交道上 在即時系統中，用clock來控制!

TCTL模型檢驗問題的反思 Real-time systems 的自動驗證，真的是必要的嗎？ 還是只是學術上的假象？ 目前的一個困境： 在即時系統的製作上，工業界的工程師並不把系統看做real-time automata 最傳統的作法，還是periodic model 在真時工業案例中，也缺乏強有力的理由，非用real-time automata不可。

TCTL模型檢驗問題 如何將無限的狀態空間， 切割為有限、且等價行為的狀態子空間？

TCTL模型檢驗問題 符號定義： 假設在A與φ中，使用最大的常數是CA:φ 。

TCTL模型檢驗問題 Infinite States  Finite Regions q = q' Two states are in the same region, i.e., (q, )  (q', ')，若 q = q' 對所有 p  P，(p) = '(p) 對所有x  X，(x) 與'(x) 在小於CA:φ時， 整數部分相等。 若  (x)  C  '(x)  C ，則 (x) = '(x) 對所有x, y  X， (x) 與 '(x) 小於CA:φ時，小數部分的順序相同。 若  (x)  C   '(x)  C ，則 (x)  (x)  (y) (y) iff '(x) '(x)  '(y) '(y)

TCTL模型檢驗問題 當CA:φ=7 且有兩個clock: x、y

2 Clocks with cx= 2, cy= 1 28 Clock Regions: 6 corner points, 14 open line segments, 8 open regions

TCTL模型檢驗問題 Equivalent States: (q, )  (q', ')，若 小數部分的順序相同。 q = q' 立於相同的控制點。 對所有 p  P，(p) = '(p) 可以判斷所有 Boolean 變數的真假值。 對所有x  X，(x) 與'(x) 在小於CA:φ時，整數部分相等 可以判斷所有 x  c不等式的真假值。 對所有x, y  X，(x) 與'(x) 在小於CA:φ時， 小數部分的順序相同。 可以判斷哪一個不等式 x  c會先發生變化。

TCTL模型檢驗問題 定理：對所有 ，若(q, )  (q', ')，則 A, (q, ) ┝  iff A, (q', ') ┝  直觀證明：若存在 (q, ) 則可以由(q', ')建立： (q',  ') 等價片段 等價片段 等價片段 等價片段 等價片段 等價片段 等價片段

TCTL模型檢驗問題 Region graph 以 s  s' 的等價關係，將狀態空間分割成有限數目的子空間。 [s]、 [s']之間的transition， 可以代表自動機上的狀態轉換， 也可以代表時間的前進。

TCTL模型檢驗問題 可以證明，以region graph就可以充分必要的回答TCTL的模型檢驗問題。 但須加上一個附加的clock變數 z， A,(q,)┝ φ1U cφ2 iff A,(q, [z])┝ φ1U cφ2  [z]與 完全一樣，除了 [z](z)= 0 A,(q, [z])┝ φ1U cφ2 iff存在由(q, [z])開始的region序列 r0 r1 r2 ... rk r0 r1 r2 ... rk-1 都滿足φ1 rk 滿足φ2 與 z  c 。

TCTL的驗證問題複雜度 TCTL與真時自動機的模型檢驗問題是PSPACE-complete。 TCTL的satisfiability問題，是undecidable。

Clock Zones Finite representation of infinite state-space Conjunction of inequalities such as: x < c | x ≤ c | x – y < c | x – y ≤ c x, y  X, c  Z General form of a clock zone: x0 = 0  0  i  j  n (xi – xj ~ cij) ~  {< , ≤}

Clock Zones (Operations) Clock zones are closed under 3 operations: Let z1, z2 be two clock zones, Y  X, t  0 Intersection: z1  z2 is a clock zone (Conjunction of conjunctions) Clock Reset: z1(Y:=0) is a clock zone (Proof on pages 284 ~ 287) Time Elapse: z1 + t is a clock zone (See next page)

Clock Zones (Time Elapse)

Zones = Symbolic States Zone: (s, z), where s: location, z: clock zone represents a symbolic state. Successor Clock Zone: z' = succ(z, e), where z: clock zone, e: transition (successor clock zone obtained from z after time elapse and executing transition e) Successor Zone: (s', succ(z, e)), where e: ss'

Clock Zone (succ(z, e)) To obtain Successor Clock Zone (succ(z, e)) Intersect z with  (s) Let time elapse in s (operator te()) Intersect with  (s) Intersect with  (e) Reset all clocks from  (e) succ(z, e) = ((te(z (s))  (s)   (e))[ :=0]) Closed under , te(), reset, also a clock zone!!!

a transition: (s, z)  (s', succ(z, e)) Zone Graph Zone Graph is a transition system Z(A) States = zones of A Initial state = (s, [X := 0]) For each transition e of A: a transition: (s, z)  (s', succ(z, e)) Zone reachability State reachability

Difference Bound Matrix (DBM) DBM is a matrix to represent a clock zone 0 – x1 < c, i.e., x1 > c x1 <  x1 – xn  r xn  d

DBM (Example) x1  x2 < 2  0 < x2  2  1  x1

DBM (Uniqueness) A zone is not uniquely represented by a DBM Zone: x1  x2 < 2  0 < x2  2  1  x1 x1  x2 < 2 and x2  2  x1 < 4

xixj ~ij dij and xjxk ~jk djk  xixk ~ik dik DBM (Canonical Form) Canonical (unique) form of DBM for a zone Tightening operation: xixj ~ij dij and xjxk ~jk djk  xixk ~ik dik where dik = dij + djk ~ik =  if both ~ij and ~jk are  < otherwise Apply tightening operations to a DBM until no more change is possible!

DBM (Emptiness) Check if all elements on main diagonal are ( 0) Yes  nonempty No  empty or unsatisfiable Empty or unsatisfiable  At least 1 negative entry on main diagonal E.g. xi  xi  1  0  1  FALSE!!!

DBM (3 operations: Intersection) Intersection: D = D1  D2 (all DBMs) Let D1(i, j) = ~1 c1 and D2(i, j) = ~2 c2 D(i, j) = (min(c1, c2), ~) where ~ = ~1 if c1 < c2 ~ = ~2 if c2 < c1 ~ = ~1 if c1 = c2 and ~1 = ~2 ~ = < if c1 = c2 and ~1  ~2

DBM (3 operations: Clock Reset) Clock Reset: D' = D [Y := 0], Y  X defined as follows: D'(i, j) = ( 0) if xi, xj  Y D'(i, j) = D(0, j) if xi  Y and xj  Y D'(i, j) = D(i, 0) if xj  Y and xi  Y D'(i, j) = D(i, j) if xj  Y and xi  Y

DBM (3 operations: Time Elapse) Time Elapse: D' = te(D) defined as follows: D'(i, 0) = (< ), for any i  0 D'(i, j) = D(i, j), for i = 0 or j  0

DBM (3 operations) All 3 operations can be efficiently implemented DBM must be canonalized (using tightening) before any of the 3 operations (intersection, clock reset, and time elapse) After any of the 3 operations, a DBM might no longer be canonical! Last step: Reduce to canonical form!!!

DBM (Zone Graph Construction) Clock zones: represented by DBM Succesor clock zones succ(z, e): computed by the 3 operations: intersection, reset, and time elapse on DBM instead of on clock zones

DBM (Zone Graph Construction) Initial state: (s0, Z0), Z0: x = 0  y = 0 Zone D0

DBM (Zone Graph Construction) Invariant  (s0) is 0 ≤ x  0 ≤ y ≤ 5

DBM (Zone Graph Construction) Step 1: Intersection D0 with  (s0) gives D0 Step 2: Let time elapse: te(D0   (s0) )

DBM (Zone Graph Construction) Step 3: Intersect with  (s0) again

DBM (Zone Graph Construction) Trigger (a) = y  3

DBM (Zone Graph Construction) Step 4: Intersect with trigger (a)

DBM (Zone Graph Construction) Step 5: Reset clock y in DBM Z1 = 3 ≤ x ≤ 5  3 ≤ x  y ≤ 5  y = 0

DBM (Zone Graph Construction) Successor of (s0, Z0) is (s1, Z1) Repeat the same 5 steps: (s0, 4 ≤ y ≤ 5  4 ≤ y  x ≤ 5  x = 0) (s1, 0 ≤ x ≤ 1  0 ≤ x  y ≤ 1  y = 0) (s0, 5 ≤ y ≤ 8  5 ≤ y  x ≤ 8  x = 0) (s1, x = 0  y = 0), which is contained in the 2nd zone, thus no more new zones can be generated!!! No more change! Stop! Zone Graph!

Binary Decision Diagram (BDD) BDD: A canonical form representation for Boolean formulas. Motivation: Too much space redundancy in traditional representations BDD is more compact than truth tables, conjunctive normal form, disjunctive normal form, binary decision trees, etc. BDD has a canonical form BDD operations are efficient

BDD (Binary Decision Tree)

BDD (redundancy in BDT) Binary Decision Trees (BDT): Same size as truth tables Lots of redundancy: Out of 8 subtrees rooted at b2 only 3 are distinct!!! Merge isomorphic subtrees  BDD BDD is a rooted, DAG with 2 types of vertices: terminal and nonterminal Each nonterminal v is labeled with var(v) and has two successors: low(v) and high(v) Each terminal vertex is labeled 0 or 1

BDD (Boolean Function) BDD B with root v determines Boolean function fv(x1, …, xn) as follows: If v is a terminal vertex fv(x1, …, xn) = value(v)  {0, 1} If v is a nonterminal vertex with var(v) = xi: fv(x1, …, xn) = ( xi  flow(v)(x1, …, xn) )  ( xi  fhigh(v)(x1, …, xn))

BDD (Canonical Form) Canonical Form: Two boolean functions are logically equivalent iff they have isomorphic representations Why Canonical Form? Simplifies equivalence checking and satisfiability checking BDD Canonical Form: Same variable order along all paths from root to terminal No isomorphic subtrees or redundant vertices

BDD (Canonical Form) For requirement 1 (same variable order): Total ordering < on all variables If u has a nonterminal successor v, then var(u) < var(v) For requirement 2 (no redundancy): Apply 3 transformations repeatedly: Remove duplicate terminals Remove duplicate non-terminals Remove redundant tests

BDD (Canonical Form) Remove duplicate terminals: Eliminate all but one terminal vertex with a given label and redirect hanging arcs. Remove duplicate non-terminals: If var(u) = var(v), low(u) = low(v), high(u) = high(v), then eliminate u or v. Redirect hanging arcs. Remove redundant tests: If low(v) = high(v), then eliminate v and redirect incoming arcs to low(v).

BDD (Canonical Form) Apply 3 transformations repeatedly in a bottom-up manner Time: O(|BDD|) Gives Ordered BDD (OBDD) Order: a1 < b1 < a2 < b2 OBDD for two-bit comparator example

Ordered BDD (OBDD) Since OBDDs are canonical, it is easy to: check equivalence = check BDD isomorphism check satisfiability = check BDD isomorphism with OBDD(0) Size of OBDD depends critically on VARIABLE ORDERING!!! 2-bit comparator example: Change variable order to: a1 < a2 < b1 < b2 11 vertices instead of 8 for a1 < b1 < a2 < b2

OBDD (Variable Ordering) a1 < a2 < b1 < b2 In general, for n-bit comparator: a1 < b1 < …< an < bn gives 3n + 2 vertices a1 < …< an < b1<…< bn gives 3  2n  1 vertices

OBDD (Variable Ordering) Infeasible to find an optimal variable ordering! Checking a particular ordering is optimal is NP-complete! There are Boolean functions with exponential size OBBDs for any ordering! Eg: nth output of a combinational circuit to multiply two n bit integers

OBDD (Variable Ordering) Heuristics to find a good variable ordering: Depth-First Traversal of circuit gives a good variable order Intuition: related variables should be grouped together in the order Dynamic Reordering: to save time and space, not to find an optimal ordering.

f = ( x  f |x:=0)  (x  f |x:=1) OBDD (Operations) All 16 two-argument logical operations can be implemented efficiently on OBDDs. Time Complexity = O(|OBDD1|  |OBDD2|) Key Idea: Shannon Expansion f = ( x  f |x:=0)  (x  f |x:=1) Let f, f ' = OBDDs, v, v' = roots, x = var(v), x' = var(v') Apply(f, f ', *, ): a uniform algorithm for all 16 operations *

OBDD (Apply Algorithm) If v, v' are terminals, f * f ' = value(v) * value(v') If x = x', then use Shannon Expansion: f * f ' = ( x  (f |x:=0 * f '|x:=0))  ( x  f |x:=1 * f '|x:=1)) If x < x', then Shannon Expansion simplifies: f * f ' = ( x  (f |x:=0* f '))  (x  f |x:=1 * f ')) (∵ f '|x:=0 = f '|x:=1 = f ' does not depend on x) If x' < x, same as previous.

OBDD (Efficiency) A problem generates 2 sub-problems Use dynamic programming to avoid exponential algorithm # sub-graphs = |OBDD(f )| A sub-problem depends on 2 sub-graphs # sub-problems ≤ |OBDD(f1)|  |OBDD(f2)| Result Cache: computed sub-problems in canonical form Modern BDD package: millions of vertices!

OBDD (Representing Kripke Structures) State variables: a, b Add new state variables: a', b' s1s2: (a  b  a'  b') Full system: (a  b  a'  b')  (a  b  a'  b')  (a  b  a'  b')

Symbolic Model Checking Symbolic = Manipulation of Boolean formulas Symbolic  Operate on entire sets of states instead of individual states and transitions

Fixpoint Representations M(S, R, L): Finite Kripke Structure P(S): power set of S Least element in P(S): False = empty set Greatest element in P(S): True = S Predicate transformer:  : P(S)  P(S) 0(Z) = Z,  i+1(Z) =  i(Z)  is monotonic if P  Q   (P)   (Q)

Fixpoint Representations Fixpoint characterization of temporal logic operators A set S'  S is a fixpoint of a function  : P(S)  P(S) if  (S') = S'. (S: set of states, P(S): power set of S) A monotonic predicate transformer  on P(S) always has: a least fixpoint:  Z. (Z) a greatest fixpoint:  Z. (Z)

Least Fixpoint False   (False)   2(False)  … No. of iterations  |S| Last iteration:  (Q) = Q =  Z. (Z)  Z. (Z)  (False) False

Least Fixpoint Algorithm

Greatest Fixpoint True   (True)   2(True)  … No. of iterations  |S| Last iteration:  (Q) = Q =  Z. (Z) True = S  (True) 2 (True)  Z. (Z)

Greatest Fixpoint Algorithm

Fixpoint Characterizations  =  Z .  Z  =  Z .   Z  =  Z .   Z  =  Z .   Z [1 U 2] =  Z . 2  (1  Z) [1 U 2] =  Z . 2  (1  Z)    Z   Z

Approximations for [p U q]

Symbolic Model Checking for CTL Kripke Structures are represented symbolically using OBDDs. Quantified Boolean Formulas QBF(V): every propositional variable in V is a formula f, f  g, f  g are formulas, if f and g are v f and v f are formulas, if f is and vV Every QBF formula can be represented by an OBDD x f = f |x=0  f |x=1 x f = f |x=0  f |x=1

Symbolic Model Checking Algorithm Check(a CTL formula) returns an OBDD that represents all system states satisfying the formula Inductive definition of Check() as follows: If f = a (a proposition), Check(f ) returns the set of states satisfying a. If f = f1 f2 or f = f1, use Apply(Check(f1), Check(f2), *)

Symbolic Model Checking Algorithm Check(f ) = CheckEX(Check(f )) Check([f U g]) = CheckEU(Check(f ), Check(g)) Check(f ) = CheckEG(Check(f )) CTL formula OBDD

CheckEX(f ) f is true in a state if it has a successor in which f is true. CheckEX(f (v)) = v'[f (v')  R(v, v')] = [f (v')  R(v, v')]|v'=0  [f (v')  R(v, v')]|v'=1 R is the transition relation OBDD Given OBDDs for f and R, we can compute an OBDD for v'[f (v')  R(v, v')]

CheckEU(f ) Least fixpoint characterization: [1 U 2] =  Z . 2  (1  Z) Use Lfp() to compute Q0=False, Q1, …, Qi, … that converges to [1 U 2] Given OBDDs for 1, 2, and Qi, we can compute Qi+1. Qi+1= 2  (1  Qi) Qi+1= Qi  Qi=  Z . 2  (1  Z)

CheckEG(f ) Greatest fixpoint characterization  =  Z .   Z Use Gfp() to compute Q0=True, Q1, …, Qi, … that converges to  Given OBDDs for 1 and Qi, we can compute Qi+1. Qi+1 =    Qi Qi+1= Qi  Qi=  Z .   Z

Fairness in Symbolic Model Checking Fairness Constraints F = {P1, …, Pn}  =  Z .   k = 1…n[ U(Z  Pk)] Set of all states which are start of some fair computation is fair(v) = CheckFair(True) CheckFairEX(f (v)) = CheckEX(f (v)  fair(v)) CheckFairEU(f(v), g(v)) = CheckEU(f(v), g(v)  fair(v))

Counterexamples & Witnesses Counterexample: If  is false, produce a path to a state in which  holds. Witness: If  is true, produce a path to a state in which  holds. Counterexample() = Witness( ) Thus, need consider only witnesses: , U, and .

Witnesses Construct SCC graph G(V, E), where each node in V is an SCC, and an edge exists if there is a transition from a state in one SCC to a state in another SCC. SCC graph contains no cycle (because all cycles are in SCC graph nodes) Each infinite path has a suffix in an SCC graph node.

Witness for  with F = {P1,…,Pk}  =  Z .   k = 1…n[ U(Z  Pk)] For each P, compute an increasing sequence of approximations Q0P  Q1P  Q2P  …, where QiP is the set of states from which a state in Z  P can be reached in  i steps. Start with an initial state s satisfying  . Look for a successor t of s in Q0P, PF. If no such t, keep looking in Q1P, Q2P, … If t  QiP and i > 0, find a successor of t in Qi-1P, and continue until i = 0, thus we have a path from s to some state u in   P. Continue with other PF to obtain s'. Find a path from s' to t (cycle).

Witness for  in first SCC

Witness for  spans 3 SCC

Witnesses for U and  fair = {s | state s satisfies True with F} Witness for  [ f U g] with F = Witness for  [ f U (g  fair)] Witness for [ f ] with F = Witness for [ f  fair]

An ALU Example

An ALU Example Pipeline circuit First cycle of instruction: read operands from register file into operand registers Second cycle: compute result and store in first pipe register Third to r + 1 cycle: result is passed through remaining pipeline registers Last cycle: result is written to register file

An ALU Example Only after r + 2 cycles, the result of an operation is written back to register file. Input signal stall  invalid instruction (e.g., cache miss)  no change to destination reg Assume: 1 pipe register, XOR op only CTL specification has 2 parts: Destination register updated correctly All other registers should not change

Spec Part 1 (Dest reg updated correctly) An ALU Example Spec Part 1 (Dest reg updated correctly) Use n operator for n cycle delays src1opi = (src1addr  2 reg0,i)  (src1addr  2 reg1,i) src2opi = (src2addr  2 reg0,i)  (src2addr  2 reg1,i) resulti = (destaddr  3 reg0,i)  (destaddr  3 reg1,i)

Spec Part 2 (No change in other registers) An ALU Example Spec Part 2 (No change in other registers) ((stall  destaddr)  (2reg0,i 3reg0,i)) ((stall  destaddr)  (2reg1,i 3reg1,i))

An ALU Example (Experiment Results) 8-bit wide pipeline 4 general registers 1 pipeline register 1 operation More than 1020 states 41,000 OBDD nodes Verification time: 22 mins of Sun 3 Substantial improvement over explicit-state model checking