Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://www.intsys.msu.ru/staff/mironov/modelchk.pdf Äàòà èçìåíåíèÿ: Mon Mar 8 14:04:13 2010 Äàòà èíäåêñèðîâàíèÿ: Mon Oct 1 21:58:14 2012 Êîäèðîâêà:

Model Checking
..



1 1.1 1.2 . . . . . . . . . . . . . . . . 1.3 . . . . . . . . . . . . . . . . 1.3.1 . 1.3.2 . . . . . . . . . . . 1.3.3 . . . . 2 2.1 . . . . . . . . . . . . . . . . . 2.1.1 . . . . . . . . 2.1.2 . . . . . . . . . . . . 2.1.3 . . . . 2.2 . . . . . . . . . . . . . . . . . 2.2.1 . . . . . . . . 2.2.2 . . . 2.3 . . . . . . . . . . 2.4 . . . . . . . . . . . . 2.4.1 . . . 2.4.2 . . . . . . . . . . . . . 2.4.3 , . . . . . . . . . . . . . 2.4.4 Fairness . . . . . . . . . . . . . . . 4 4 6 7 7 8 10 12 12 12 13 14 16 16 17 18 18 18 19 21 24 26 26 27 27

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

...... ...... ...... ...... ...... ...... ...... ...... ...... ...... ...... ...... ......

3 3.1 . . . . . . . . . . . 3.2 CTL . . . . . . . . . . . . . . . . . . . . . . 3.2.1 CTL­ . . . . . . . . . . . . . . . . . 1


3.3

3.4

3.5

CTL­ . . . . . . . . . . . . CTL­ . . . . . . . , CTL­ . . . . . . . . . . . . . . . . . . . Model checking CTL . . . . . . . . . . . . . . . . 3.3.1 MC-CTL . . . . . . . . . . . . . . . . 3.3.2 fair MC-CTL . . . . . . . . . . . . . . . 3.4.1 . . . . . . . . . . . . 3.4.2 Q FP . . . 3.4.3 fair-MC-CTL fairness CTL­ . . . . . . . . . . . . . . . µ­ . . . . . . . . . . . . . . . . . . . . . . 3.5.1 µ­ . . . . . . . . . . . . . . . . . . . 3.5.2 µ­ . . . . . . . . . . . . . . 3.5.3 µ­ 3.5.4 CTL µ­ . . . . . . .

3.2.2 3.2.3 3.2.4

28 29 30 31 31 34 35 35 37 38 39 40 41 42 44 46

4 Mo del Checking 4.1 . . . . . . . . . . . . . . . . . . . . 4.2 SMC-CTL . . . . . . . . . . . . . 4.3 Binary Decision Diagrams . . . . . . . . . 4.3.1 BDD . . . . . . . . . . . 4.3.2 BDD . . . . . . . . . . . 4.3.3 BDD . . . 4.3.4 BDD . . . . . . . . . 5 LTL 5.1 5.2 LTL- . . . . . . . . . 5.3 Model checking LTL . . . . 5.3.1 S . . . . . . . . . . 5.3.2 S â S . . . . . . . 5.3.3 MC-LTL . . . . 5.4 . . . . . . . . 5.4.1 5.4.2 . . . 2

..... ..... ..... ..... ..... ..... .....

. . . . . . .

46 47 49 49 51 51 53 60 60 62 62 62 67 71 72 72 74

...... ...... ...... ...... ...... ...... ..... ......

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .


5.4.3 5.4.4 5.4.5 5.4.6

. . . . . . B . . . . . .

...... MC-LTL ...... ......

74 75 79 81

3


1
. , , . , Model Checking.

1.1



( ) . , · , · , · .

4


. [1]. . 1. , .. . 2. , . , . 3. . 4. . . 5. , . 6. , ( ). 7. , .. . , , . , - , , , . . 5


1.2



. ( ) , , . : , ( ), , . ([2], . 41), , . , , . . , , · , · , · , · , · , . , . . 6


1.3



. 1. . 2. ( ). 3. . , ­ . , , .. , . .

1.3.1



, ( ) , · , ( ), , · , , . . , , . , 7


· , · , . . 1. , .. . 2. , · , , · , .. .

1.3.2



­ . , , · , · ,

n i=1

i­

8


, , . , · , , , , · ( : ). . 1. (), · , · ­ . , , , · , · . , .

9


2. , · - , · , .. .

1.3.3



, : 1. mo del checking (MC), , , 2. , ( MC) , . , , . Mo del checking MC , · , · , , . 10


, MC , .. , . , ( ), : 1. 2. , 3. .

11


2
, , .

2.1
2.1.1




, · T y pes , T y pes D · V ar , x V ar (x) T y pes · F un, , f F un ­ (f ), (1 , . . . , k ) 1 , . . . , k , T y pes, 12 (2.1)


­ , f , f : D1 â . . . â Dk D , . e (e). · x V ar (x). · T y pes D . . · ­ e1 , . . . , ek , ­ f , ( (e1 ), . . . , (ek )) f (e1 , . . . , ek ) . , e, V ar(e).

2.1.2



e ­ . , e, , x e (x) D (x) . e e (e), : · e = x V ar, (e) 13


· e D , (e) e · e = f (e1 , . . . , ek ) (e) = f ( (e1 ), . . . , (ek )) e1 e2 , (e1 ) = (e2 ) e1 = e2 , e1 e2 .

2.1.3



T y pes bool, 0 1. bool. e , (e) = 1, , (e) = 0. F un ¬, , , · ¬ bool bool · (bool, bool) bool , , , . e ¬e e. , , , . 14


e1 , . . . , ek e1 e2 . . . ek e1 e2 . . . ek ¨ e1 (e2 (. . . ek ) . . .) e1 (e2 (. . . ek ) . . .) .


e1 .. ek

.








e1 .. ek



.



. e1 , e2 · e1 e2 ¨ e1 e2 · e1 e2 ¨ (e1 e2 ) (e2 e1 ). {ei | i I } (i) I (2.2) (i) ei (i) ei ei1 . . . ei
k

ei1 . . . e

i

k

{i1 , . . . , ik } ­ i I , (i). , (2.2) 1 0 . 15


2.2
2.2.1




( ). , . v Op(v ) : : . Op(v ) I nit (2.3) I nit ­ , . : Op(v ) x := e (2.4)

x ­ , e ­ , x. : O p (v ) = b ­ . : Op(v ) = halt b (2.5)

(2.3), (2.4), . (2.5) : " +", ­ " -". halt . , , , . , , . . . . 16


· (2.4) e x. · (2.5) b, ­ 1, " +", ­ - " -". · halt .

2.2.2



G, , . , S tart(G). . 1. . . S tart(G) , , . 2. · v , · a1 , a2 , , a v , a2 - v , a a2 , · Op(v ), Op(v ) (2.4), · b?, Op(v ) (2.5), a2 " +" · b?, Op(v ) (2.5), a2 " -". 3. 17
1

1


· v halt, · a v , a, 1?

2.3



. , : · : ­ , ­ , · : , .

2.4
2.4.1



S = ( P , Q, , L, Q0 )

() S (2.6)

. 1. P ­ , . 2. Q ­ , S . 18


3. ­ Q (.. Q â Q), . 4. L ­ L : Q â P {0, 1} , : q Q p P p · q , L(q , p) = 1, · q , L(q , p) = 0. L(q , p) q (p). 5. Q0 Q ­ . , · , · (q , q ) q q . : q Q (q ) = {q Q | (q , q ) } -1 (q ) = {q Q | (q , q ) }
def def

2.4.2



(2.6) ­ = ( q0 , q 1 , . . . ) (2.7)

, i 0 qi+1 (qi ). (2.7) , , . , 19


, , . , , . , , q ( q ), (.. 0) q. : · (2.7) q Q q , q = qi i 0 · (2.7) q , q qq ,


q>q ,


qq ,


q

, i, j , , q = qi , , , i j, . ­ = ( q0 , . . . , qn ) , ­ q0 (2.8) ­ (2.8), qn = (qn , (2.8) i > j, i j, i j

qn . , n = 0. ­ q
n+1

, ... )

20


, · , (q0 , . . . , qn , q
n+1

, ... )

­ (2.8), q0 = qn , . ­ , , · · ... inf ( ) {q Q | q }

2.4.3

,

= {1 , . . . , k } ­ . : i = 1, . . . k · Gi
i i

· Vi , ^ · Vi Vi {ati }

ati ­ , Gi ^ ^ · V V1 . . . Vk . x V x . 21


· ­ , V , · ( , ) ­ V ( , ) : x V · (x) · x (x) . i = 1, . . . , k c Gi E dg es(Gi ). E dg es(Gi ) i (), V , . i () : · n n · X V same(X ) ( x = x)
x X

i () : · x := e,


i ( ) =

def

ati = n ati = n x =e same(Vi \ {x}



)



22


· b?,


i () =

def

ati = n ati = n b same(Vi )



, i () ( , ) , · , ^ , x Vi (x), · ^ x Vi (x). , , . 1. V . 2. V . 3. ( , ) , · 1 . . . k , , · 1 . . . k , , i = 1, . . . , k i i ()
E dg es(Gi )

4. ( , p) (p).

23


5. ,


I nit1 . . . I nitk at1 = S tart(G1 ) ... atk = S tart(Gk )



I nit1 , . . . , I nitk ­ .

2.4.4

Fairness

S , , , (.. ) S. , S , . S , , , S . fairness. , , fair . fairness. 1. S , , . 2. · (1 ) (2 ), · 2 1 . 24


S , , · 1 2 , · 2 1 . 3. , . S , , · , · . fairness F {Fi | i = 1, . . . , k }, i = 1, . . . , k fairness i = 1, . . . , k inf ( ) Fi = Fi Q (2.9)

.. , F .

25


3
3.1

, , . ( ). , : 1. 2. - , , . , , .. " " : · ­ , , 26


· ­ . · CTL (Computational Tree Logic), · LTL (Linear Temporal Logic). . , , .. q p q (p) {0, 1}. P . . 1. P . 2. 1 0 . 3. , , ¬ , , (3.1)

. (3.1) . , , 2.1.3. , , , 2.1.3.

3.2
3.2.1

CTL
CTL­

CTL : 27


· CTL, CTL : AX AF AG

6 EX EF EG

· , CTL, CTL 4 : AU( , ) EU( , ) AR( , ) ER( , ) (AX, ..) CTL­. CTL CTL­.

3.2.2

CTL­

S = (P , Q, , L, Q0 ) ­ . q Q CTL­ q () q 1 0, : 1. = p P , q () S 2. q (1) = 1, 3.
def

q (0) = 0
def

def

· q ( ) = q ( ) · q ( ) = q ( ) q ( ) · q ( ) = q ( ) q ( )
def def

4. , CTL-, : · q (AX ) = 1, q (q ) q ( ) = 1 (3.2)

· q (EX ) = 1, q (q ), , (3.2) 28


· q (AF ) = 1, q q , , (3.2) · q (EF ) = 1, q q , , (3.2) · q (AG ) = 1, q q (3.2) · q (EG ) = 1, q , , q (3.2) · q (AU( , )) = 1, q q , ,
q ( ) = 1, q < q q ( ) = 1




(3.3)

· q (EU( , )) = 1, q q , , (3.3) · q (AR( , )) = 1, q q


q ( ) = 1, q < q : q ( ) = 1




(3.4)

· q (ER( , )) = 1, q , , q (3.4). CTL- S Q = {q Q | q () = 1}
def

(3.5)

3.2.3

CTL­

CTL­ , q q () = q ( ) CTL­ , = . 29


, : · : = , · AX = EX · EF = EU(1, ) · AF = EG · AG = EF EU( , ) · AU(, ) = EG · AR(, ) = EU(, ) · ER(, ) = AU(, ) , CTL­ CTL­ , CTL­: EX, EG, EU (3.6)


= ,

=

3.2.4

, CTL­

1. EF ( Start Ready ) ( , Start , Ready ­ ) 2. AG ( Request AF Acknowledgement ) ( , - ) 3. AG ( AF DeviceEnabled ) ( DeviceEnabled ) 30


4. AG ( EF Restart ) ( , Restart)

3.3
3.3.1

Model checking CTL
MC-CTL

mo del checking CTL ( MC-CTL) , · S = (P , Q, , L, Q0 ), · CTL­ Q . , CTL­ (3.6). Q . 1. = p P , Q S . 2. 1 0, Q Q . 3. , ,

Q Q \ Q , Q Q , Q Q


4. = EX , Q = {q Q | (q ) Q = }.

31


5. = EU( , ), Q Q Q, Q := Q , Q := Q : while (Q = ) { q Q , q Q q -1 (q ) q Q ? q Q Q q Q } 6. = EG . . Q Q , q1 , q2 Q q1 q2 . ( ) (strongly connected component, SCC). ( ) SCC, O(|Q| + | |). Q, Q1 . Q1 Q, SCC Q. , q (EG ) = 1 , Q q . (3.7)

32


Q , q , {q | q q }


(3.8)

. , (3.8), Q , , , SCC Q . 0 , q . , (3.7) SCC C Q , 0 Q q q q C,


(3.9)

, (3.9) (3.7), .. = 0 ·
def 1

(3.10)

1 ­ q q , C , : Q . , Q . (a) Q SCC, Q , SCC. Q := Q . (b) , . , O(|| · |S |) || ­ , |S | = |Q| + | |, .. · ||, · |S |­ . 33


3.3.2

fair MC-CTL

F fairness (2.9), fair- CTL­ q , q F (). fair- 3.2.2 : · , "", "fair" · q Q CTL, fair q , q F () = 0. QF {q Q | q F ( ) = 1}. , q F (EG ) = 1 , fair SCC C , q C, 0 q q , 0 QF SCC C QF fair, Fi F , q F (EG1) (3.12) Fi C = QF


(3.11)

1 , fair q . q (f air) 34


, O(|F | · |S |) |F | ( F ) , SCC, fair. f air , q (3.12). Fair- : 1. q F (p) = q (p f air). 2. q F (EX ) = q (EX( f air)) 3. q F (EU( , )) = q (EU( , ( f air)). , CTL­ q F () O(|| · |S | · |F |)

3.4
3.4.1




Q ­ , 2Q ­ . 2Q ­ F : 2Q 2Q : A, B 2
Q

(3.13)

AB



F (A) F (B )

35


, . A Q (3.13), A = F (A) " " FP (fixpoint). (3.13), , , - -. F . F (Z ) FP. FP F (Z ) · ( µZ.F (Z )), FP F (Z ), · ( Z.F (Z )), FP F (Z ). F (Z ) (3.13) FP, µZ.F (Z ) =
i0

F i () = F i0 () F i (Q) = F j0 (Q)
i0 def

Z.F (Z ) =

i0 j0 , F i (A) = F (. . . (F (A))).
i

FP (3.13)

36


: A :=


( FP) Q ( FP)


B := A do while (B = A) A := F (A)

return A

3.4.2

Q FP
3.3.1 Q , , EG EU. , -

:

1. A A : 2Q 2Q ( A Q ­ ), B 2Q A B A B , 2. EX : 2Q 2
Q

B 2Q EX(B ) = {q Q | (q ) B = } , CTL­ , :

def

QEX = EX(Q ) QEG = Z. Q EX(Z ) QEU(
, )

(3.14)

= µZ. Q (Q EX(Z )) 37


, , EG EU, FP.

3.4.3

fair-MC-CTL fairness CTL­

fairness (2.9) CTL­, .. i = 1, . . . , k Fi = Qi i CTL (3.15) Q Q
F EG F EG




= Z.

Q
k i=1



EX EU Q , Z Qi

(3.16)



. (3.16) , , . 1. , QF EG (3.16), , QF FP EG (3.16), .. QF = EG


Q
k i=1



EX EU Q , QF Q EG

i



, q , fair Q . 2. , Z ­ FP (3.16), .. Z=


Q





k i=1

EX EU Q , Z Qi



q Z fair Q , .. Z QF . EG 38


, · fair-MC-CTL QF , EG q F (EG ) (3.15), · , (3.17) 1, fair Q q (3.10), , GFP (3.16): · FP EU Q , Z Q1 Q1 Q1 Q2 . . . 0 0 0 , 1 Q q q1 Z Q1 · 2 Q q1 q2 Z Q2 · .. , , 1 , 2 , . . . (3.17)

3.5

µ­

CTL ( , , PDL) , µ­. , , MC-CTL µ­. 39


µ­ , .. ( P , Q, {a | a T }, L, Q0 ) (3.18)

T ­ , , a T a Q2 .

3.5.1

µ­

, RV , (). µ­ ( µ­) µ . , 3.1, 1. RV
µ

2. a T µ­ [a]
µ



a µ

3. Z µ­ µZ. µ Z. µ

µ­ : · Z µ­ Z ­ , · , , , [a] , a

Z Z , Z ( ), Z 40


· µZ. Z. , ­ Z ( Z µ ) , ­ , . µ­ , µZ. Z. , Z , . µ­ .

3.5.2

µ­
: RV 2Q (3.19)

(3.18)

µ­ (3.18) (3.19) () Q : 1. p P (p) = Qp
def

2. (3.19) 3. · (1) = Q,
def def def

(0) =

def

· ( ) = Q \ ( ) · ( ) = ( ) ( ) · ( ) = ( ) ( ) 4. · ( a ) = {q Q | a (q ) ( ) = } · ([a] ) = {q Q | a (q ) ( )} 5. · (µZ. ) = µZ. A [Z := A]( ) 41
def def def def


· ( Z. ) = Z. A [Z := A]( ) A [Z := A]( ) (3.20)

def

(3.13), Q Q [Z := Q ]( ) [Z := Q ] , Z , [Z := Q ] Q . (3.20) . , () , . , ( ) (3.18) . (3.18). µ­ (3.18), = . , [ a] = a a = [a] µZ. = Z.( Z ) Z. = µZ.( Z ) (3.21)

( Z ) Z Z .

3.5.3

µ­

() 3.5.2 . O(|S ||| ), S ­ , (). µZ. Z. , , 42


0 1, Q Q, Q (µZ. ) Q ( Z. ) () µZ. . 1. , (3.21). . , . 2. M µ ( ), , . M A B , , A 0. , A , B . 3.
M : B := A do while A := [Z := A ]( ) B = A

return A



[Z := A ]( ) (3.22)

, 3.5.2. M , . 43


, (3.22) ( ) M , µZ . , [Z := A ]( ) (3.23)

( ), A . , , , , 3.5.2. , A . Z. . O(|S |d ), d ­ , 1 , . . . , k , µ , i = 1, . . . , k - 1 · i
+1

i

· i µ, i+1 , i , i+1 µ.

3.5.4

CTL µ­

a ­ T . CTL­ , CTL­ (3.6), µ­ µ , , CTL­, µ­, : 44


1. EX a 2. EU( , ) µZ. ( a Z ) 3. EG Z.( a Z ) S ­ (2.6). Sµ (3.18) , S , , , a = . , CTL­ Q S µ Sµ . , MC-CTL µ-.

45


4 Model Checking
4.1
:V D (4.1)

Q

V ­ , D ­ . e, V , Qe Q, : Qe = { Q | (e) = 1} Q Q e, , Q = Qe (4.2)
def

, e Q ( e Q ). Q Q (4.2) , e Q . 46


, , Qe1 Q Qe1 Q Q \ Qe
e2 e2

= Qe1 e = Qe1 e = Q¬e

2 2

, - , .

4.2

SMC-CTL

SMC-CTL (Symbolic Model Checking), , CTL- S , · (4.1) · (V , V ), V , {( , ) Q2 | ( , ) = 1} ( (V , V ) 2.4.3) · p Qp e(p) e(), Q . , , CTL­ (3.6). SMC-CTL , C , : 47


· C (, , ) · C , 0 1 · C (.. , e1 , e2 C C , e, e1 e2 , e1 e
2

· C EX, e C EX(e) = V ( (V , V ) e )
def

(4.3)

e e x V x. SMC-CTL C , e() . 1. = p P , e(p) . 2. , e() , . 3. CTL-, e() : e(EX ) = EX(e( )) e(EG ) = Z. e( ) EX(Z ) e(EU( , )) = µZ. e( ) (e( ) EX(Z ))

48


, 3.4.1, .. 1 ( ) 0 ( ) e := e 2 1 do while (e2 = e1 ) e1 := F (e1 ) e1 := return e1 F (Z ) µZ Z .


4.3
4.3.1

Binary Decision Diagrams
BDD

C , 4.2, , BDD (Binary Decision Diagram). BDD (4.1), x V bool. V ­ bool, · (4.1) ^ V {0, 1} (4.4) ^ V V x V , - bool, |x| bool, |x| ­ , (x), · (4.1) BDD, (4.4).

49


, x V bool. BDD , 2.1.1. BDD , BDD . BDD e Root(e), . BDD - . 0 1. . v l(v ) V . , 0, - 1. BDD BDD, . · , (l(v )), · , , . BDD , , , · , · , · BDD , BDD . , BDD , .

50


4.3.2

BDD

BDD BDD . . 1. BDD v1 , v2 : · l(v1 ) = l(v2 ), · v1 v2 , v1 v2 . · v1 , · , v1 , v2 . 2. BDD v , , v v1 , · v , · v v1 . 3. BDD v (.. v , ), . BDD , . BDD , .

4.3.3

BDD

V R.

51


BDD R, v1 v2 l(v1 ) < l(v2 ) , BDD V , . M (4.1), R V . BDD, M R, siz e(M , R) , M ,
k

( xi y i )
i=1

· siz e(M , R1 ) = 3k + 2, R1 x1 < y1 < . . . < xk < yk · siz e(M , R2 ) = 3 · 2k - 1, R2 x1 < . . . < xk < y1 < . . . < yk R V M , R V siz e(M , R) siz e(M , R ) NP­.

52


BDD . , , BDD, , , · BDD, · BDD.

4.3.4

BDD

BDD. , , BDD. 0 1 BDD, 0 1, , . e ­ BDD. v vb ( b = 0 1) v b. [x := b]e (4.5) ( x V b = 0 1) BDD, e x , v , v , vb . , e, (4.5) vb . (4.5) e. 53


, ([x := b]e) = ( [x := b]) (e) [x := b] x, b. BDD e e e : 0 1, 1 - 0. . BDD e1 , e2 e1 e2 . BDD e1 , e2 , e1 e2 e1 , e2 : 0 e = 0, 0 e = e, 1 e = e, 1e=1

BDD e1 e2 . Root(e1 ) Root(e2 ) x y . x = y , BDD x, · 0 BDD ([x := 0]e1 ) ([x := 0]e2 ) · 1 BDD ([x := 1]e1 ) ([x := 1]e2 ) x < y , BDD x, 54


· 0 BDD ([x := 0]e1 ) e2 · 1 BDD ([x := 1]e1 ) e2 y < x, BDD . , BDD ( [x := b]ei ) BDD, .. BDD, BDD. , BDD, BDD . , , BDD O(|e1 | · |e2 |). BDD EX(e), (4.3), (), BDD f (X , Y ) g (Y , Z ) ( X, Y , Z ­ , f X Y , g ­ Y Z ) BDD Y f (X, Y ) g (Y , Z ) (4.6)

Y y1 . . . y
k

55


Y (y1 , . . . , yk ). BDD e y e BDD [y := 0]e [y := 1]e (4.6) Rel_Pro d f , g , Y . C ache, ( f , g , Y , Rel_Pro d(f , g , Y ) ) Rel_Pro d . Rel_Pro d . Rel_Pro d (f , g , Y ) := 1. f = 0 g = 0, return 0 2. f = 1 g = 1, return 1 3. (f , g , Y , h) C ache return h 4. : · a := maxvar (f ) ( f ) · b := maxvar (g ) · c := max (a, b) · h0 := Rel_Pro d ([c := 0]f , [c := 0]g , Y ) · h1 := Rel_Pro d ([c := 1]f , [c := 1]g , Y ) · h :=


h0 h1 c Y (z h1 ) (z h0 )

· (f , g , Y , h) C ache · return (h)

56


. , · (X, Y ) Y e(Y )


(4.7)

( MC), · i , Y BDD (4.7) . , = 1 . . . n ( , , , , 2.4.3), BDD (4.7) BDD
n i=1

i ( X , Y ) Y e(Y )





(4.8)

, , , y i fi (X ) = (yj = xj
j =i





i

)

(4.8)
n i=1

yi fi (X ) yi e(x1 , . . . , xi-1 , yi , xi+1 , . . . , xn )





(4.9)

, , , , . 57


, , BDD. , , 1 , . . . , n , = 1 . . .
n

i {1, . . . , n} Y (i ) Y , i . Y Y1 . . . Yn , def Y1 = Y (1 ) Y2 = Y (2 ) \ Y
def def 1

Y3 = Y (3 ) \ (Y1 Y2 ) ... Yn = Y (n ) \ (Y1 . . . Y
def n-1

)

BDD (4.7) BDD




1

Y1 Y


2



2



. . . Yn


-1



n Yn e(Y )


n-1





BDD BDD en , . . . , e1 , i = n, . . . , 1 ei = Y
def


i



i ei


+1

,

e

def n+1

= e(Y )



BDD en , . . . , e1 BDD . NP-. , , , , . 1. C . 58


2. y , - Y ( ), C , "",
C, Y ( ) y

max

|Y ( )|
C, Y ( ) y

|Y ( )|

3. , Y ( ) . 4. C . 5. C .

59


5 LTL
5.1

() : · ­ , X , F , G ­ · ­ , U( , ) R( , ) ­ (X, ..) . = (q0 , q1 , . . .) ­ S . i 0 i "" : i = (qi , q
i+1

, . . .)

() 1 0, : 1. = p P , () = q0 () ( S ) 2. (1) = 1, (0) = 0
def

60


3. 4. · (X ) = 1 ( ), · (F ) = 1, i 0 : i ( ) = 1 · (G ) = 1, i 0 i ( ) = 1 · (U( , )) = 1, i 0 :
i ( ) = 1, j < i j ( ) = 1
def

(5.1)

· (R( , )) = 1, i 0


( ) = 1, i j < i : j ( ) = 1 ( = ), () = ( ) , · F = 1U · X = X · G = F · U(, ) = R(, ) , , ¬, , X, U. , U( , ) = XU( , ) XR( , )



R( , ) =

61


5.2

LTL-

LTL­ A E , ­ . S q LTL­ q q () : · q (A ) = 1, q ( ) = 1 (5.2)

· q (E ) = 1, q , , (5.2). , A = E CTL­ LTL­, , 1. CTL­ AG(EFp) LTL­ 2. LTL­ A(FGp) CTL­ 3. LTL­, CTL­.

5.3
5.3.1

Model checking LTL
S

, {¬, , X, U}. C l() ( ) , : 62


1. C l() 2. U( , ) C l(), XU( , ) C l() C l() . p P , , P . S , · K : C l() {0, 1} : K ( ) = K ( ) K ( ) = K ( ) K ( ) K ( ) K (U( , )) = K ( ) K (XU( , )) (5.3)

(5.4)

· K, K S K K , X C l() K (X ) = K ( ) (5.5)

· p P K p K K (p), · K , K () = 1 · S fairness, (F
U( , )

| U( , ) C l())

C l() U( , ) F
def U( , )

= {K : C l() {0, 1} | K (U( , )) K ( )} 63


, = (K0 , . . .) S fair , · i 0, · U( , ) C l() Ki (U( , ))
j i

Kj ( )

. K S fair , K , K () = () . : fair = (K0 , . . .) S C l(), i 0 Ki ( ) = i ( ) (5.6)

. 1. p P


Ki (p) = i (p)

2. Ki ( ) = Ki ( ) = i ( ) = i ( ) 3. Ki ( ) = Ki ( ) Ki ( ) = = i ( ) i ( ) = i ( ) 4. Ki (X ) = K
i+1

( ) = i+1 ( ) = i (X )

5. Ki (U( , )) = i (U( , )) : Ki (U( , )) i (U( , )) 64 (5.7)


Ki (U( , )) i (U( , )) (5.7) , .. Ki (U( , )) = 1 i (U( , )) = 0 (5.9) (5.10) (5.8)

, (5.10) i ( ) = 0 i ( XU( , )) = 0 (5.11) (5.12)

, , Ki ( ) = 0 Ki ( ) i+1 (U( , )) = 0 (5.4), (5.9), (5.13) , Ki ( ) K .. Ki ( ) = 1 K
i+1 i+1

(5.13) (5.14)

(U( , )) = 1

(5.15)

(5.16) (5.17)

(U( , )) = 1

(5.14) (5.16) , i+1 (U( , )) = 0 (5.18)

(5.17) (5.18) (5.9) (5.10) i i+1. , (5.9) (5.10), i j i.

65


, (5.9) (5.10) (5.13), j i (5.13), i j . (5.9), , ­ fair. (5.8). i (U( , )) i ( ) . . . i k 0. (5.8) , (5.19) Ki (U( , )) (5.20)
+k-1

( ) i+k ( )

(5.19)

, (5.19) Ki ( ) . . . K K K K K
i+k-1 i+k-1 i+k-1 i+k i+k-1

( ) K

i+ k

( )

(5.21)

( ) K

i+k

(U( , )) = K

i+k-1

(XU( , ))

( ) K i+ k ( ) ( ) Ki+k-1 (XU( , )) (U( , ))

.. (5.21) K
i+ k - 1

(U( , ))

, (5.20).

66


5.3.2

S â S



S = (P , Q, , L, Q0 ), S â S , · (q , K ), ­ q Q, ­ K ­ S , ­ p P q (p) = K (p)

· S â S (q , K ) (q , K ) q q K K · ­ (q , K ) S â S , ­ p P p (q , K ) K (p) (= q (p)). S = (P , Q, , L, Q0 ) ­ . = (q0 , . . .) S fair = (K0 , . . .) S , C l(), fair, i0 0 : i i0 .. ii .. ii
0 0

i 0

K i ( ) = i ( )

(5.22)

Ki (U( , )) Ki ( )

i (U( , )) i ( ) i ( ) = 0

i (U( , )) = 1,

, .. i0 (U( , )) = 1 , i i0 : 67 i ( ) = 1


ii
0

i ( ) = 0

= (q0 , . . .) S â S â S , .. ((q0 , K0 ), (q1 , K1 ), . . .) (5.23)

S â S fair, fair S . S fair S â S . , fair (5.23) (5.22), = (q0 , . . .). (5.22) . 1. p P Ki (p) = qi (p) = i (p)

2. Ki ( ) = Ki ( ) = i ( ) = i ( ) 3. Ki ( ) = Ki ( ) Ki ( ) = = i ( ) i ( ) = i ( ) 4. Ki (X ) = K
i+1

( ) =

i+1

( ) = i (X )

5. Ki (U( , )) = Ki ( ) = = Ki ( ) Ki (XU( , )) Ki ( ) = Ki ( ) K

i+1





(U( , )) ( ) ( ) K



=


=


K ( ) i

K Ki ( ) K



i+1 i+1

i+1

(XU( , ))




=

Ki ( ) K ( ) K = i Ki ( ) K

i+1 i+1

( ) ( ) K

=

i+1

(XU( , ))

68


Ki ( ) K ( ) K = i Ki ( ) K = ... =





i+1 i+1

( ) ( ) K


i+2

=

(U( , ))

=

i i i .. i i

( ) ( ) ( ) . ( ) ( )





i+1 i+1

( ) ( )

i+2

( )

... ...

i+k-1 i+k

( ) i+k ( ) ( ) Ki+k+1 (U( , ))



k ­ . , i (U( , )) Ki (U( , )) , , ­ fair, Ki (U( , ))
j i

Kj ( ) =
j i

j ( )

C S â S fair, · (q , K ) C , · U( , ) C l() K (U( , ))
(q ,K )C

K ( )

(5.24)

, (q , K ) S â S . 1. fair (q , K ). 69


2. (q , K ) (q , K ), fair SCC. , (1) (2). fair (q , K ), (q , K ) , , {(q , K ) | (q , K ) (q , K )}


(5.25)

. (5.25) , , , SCC C . , C - fair SCC, .. · (q1 , K1 ) C , · U( , ) C l() K1 (U( , ))
(q2 ,K2 )C

K2 ( )

(5.26)

(q1 , K1 ) (5.25). C , C (q1 , K1 ) (q1 , K1 ). "" , (q1 , K1 ). (5.4) (5.5), , ­ fair , , · ­ fair , K1 (U( , ))
(q2 ,K2 )·

K2 ( )

(5.27)

· C , (5.27) (5.26). , (2) (1). 0 (q , K ) (q , K ) C , C ­ fair SCC. 1 (q , K ) (q , K ) C . , 0 · 1 fair (q , K ). 70


5.3.3

MC-LTL

MC-LTL Q = {q Q | q ( ) = 1} Q ­ , ­ LTL­ . MC-LTL , E. A = E QA QE . , q (E) = 1 , q : () = 1 (5.28)

, fair S â S (q , K0 ). (5.22) i = 0 = , : () = 0 () = K0 () (5.28) : (q , K ) S â S , , 1. K () = 1, 2. (q , K ) fair . , (q , K ) fair SCC. , QE , MC-CTL 3.3.1. O(|S | · 2|| ). , MC-LTL fair-MC-LTL PSPACE­.

71


, (5.28) fair-MC-CTL ( ), (q , K ) S â S , 1. K () = 1, 2. (q , K )F (EG1) = 1.

5.4
5.4.1




( ) ­ B = (A, Q, , Q0 , F ) (5.29) : 1. A ­ , 2. Q ­ , 3. ­ Q â A â Q, 4. Q0 Q ­ 5. F = (F1 , . . . , Fn ) ­ fair , i = 1, . . . , n Fi Q. . a (q , a, q ) q q . , a . q q a q q .

72


L( ) , , .. q
a0 0

-

q

a1 1

-

q

a2 2

-

...

(5.30)

L( ) = (a0 , a1 , a2 , . . .). inf ( ) , . fair, i = 1, . . . , n inf ( ) Fi =

B ­ L(B ) A, fair , .. L(B ) = {L( ) | ­ fair q Q0 } B1 B2 , L(B1 ) = L(B2 ). B (5.29) B1 = (A, Q1 , 1 , Q0 , F1 ) 1 , F1 . B1 , , : · Q1 = Q â {0, 1, . . . , n} · Q0 = Q0 â {0} 1 · F1 = (Q â {n}) · 1 (q , j ) (q , j ) , q q k q Fk j = k - 1 j = 0 j = n j 73

a a


5.4.2




§ ¦

a

? # - q1 ! "

a b

b - q2

¤ ¥

: · A = {a, b} · Q = {q1 , q2 } · Q0 = {q1 } ( , ) · F = ({q1 }) ( fair ) (b · a) . , F fair , , , F.

5.4.3


Bi = (A, Qi , i , Q0 , Fi ) i

B1 , B2 , (i = 1, 2)

B1 B2 , B1 B2 , : L(B1 B2 ) = L(B1 ) L(B2 ) (5.31)

B1 B2 , , : · Q = Q1 â Q2 â {0, 1, 2} 74


· Q0 = Q0 â Q0 â {0} 1 2 · F = Q1 â Q2 â {2} · (q1 , q2 , j ) (q1 , q2 , j ) , qi q
a i a

(i = 1, 2), 1 2 0 j j = 0 q1 F1 j = 1 q2 F2 j = 2

j=



F1 = Q1 , B1 B2 : · Q = Q1 â Q2 , Q0 = Q0 â Q0 , 1 2 F = Q1 â F2 .

· (q1 , q2 ) (q1 , q2 ) , qi q
a i a

(i = 1, 2)

5.4.4

MCLTL

MC-LTL , · S = (P , Q, , L, Q0 ), · LTL­ A , q Q0 q (A) = 1 (5.32) .. , - S , () = 1. 75 (5.33)


5.3.2, fair K S , K () = (). () = 1, , , K , , . = (q0 , . . .) L( ) = (L(q0 ), . . .) P {0, 1}, i 0 p P L(qi )(p) = qi (p). = (K0 , . . .) L( ) = (L(K0 ), . . .) P {0, 1}, i 0 p P L(Ki )(p) = Ki (p). (5.22) , L( ) = L( ). S L(S ) L( ), ­ S ( S fairness, fair ). , (5.32) L(S ) L(S ) (5.34)

, (5.34) (5.32), .. (5.34) , = (q0 , . . .) q0 Q0 fair = (K0 , . . .) S , , K0 () = 1 i 0, p P 76 qi (p) = Ki (p) (5.35)


(5.35) , ((q0 , K0 ), . . .) fair S â S , , 5.3.2, (5.22), (5.33). (5.34) L(S ) L(S ) = L(S ) L(S ) = (a0 , . . .) P {0, 1} : (a0 , . . .) L(S ) (a0 , . . .) L(S ). , , · {q0 , . . .}, · (qi , qi+1 ), · p P , i 0 qi (p) = ai (p). (q0 , . . .) . · fair S , · fair S . , (a0 , . . .) = L( ) = L( ) · () = 1, (a0 , . . .) L(S ) · () = 0, (a0 , . . .) L(S ). , (5.32) (5.36). (5.36) 77
def

(5.36)


· BS B , L(BS ) = L(S ), L(B ) = L(S )

· BS B . S = (P , Q, , L, Q0 ) BS , L(S ) = L(BS ), , , · init ( BS ), · init Q0 . q q , L(q ), .. P {0, 1} F fair BS S . , BS fair . S fair (.. S fair), F B . : 1. (5.29) 2. q Q0 q C , C ­ SCC Q, C F = 3. q Q0 q F , . , (5.36) 2, 3.

78


2, SCC , 2, . 3, BS B " " ("on-the-fly"). , B , BS . BS B (qs , q ), qs ­ BS , q ­ B . qs BS , BS , , qs , a , , · qs qs , · q q q B . BS B , , 3, BS B .
a a

5.4.5

B

B S , S , . S . , , . , q C l(), q New(q ) Old(q ). S . S . q p P q (p) 1, p q , 0 ­ p q . C l() U( , ) fair FU(,) , q , U( , ) q q .

79


: q , q , fair , q . def q0 = {} = New(q0 ). q , New(q ) = ( , ). 1. New(q ) , X, New(q ) Old(q ), (a) = , New(q ) (b) = , · q q New Old, , q , , q , · New(q ), · New(q ). (c) = U( , ), , , X , .. · q q , q , · New(q ) · X New(q ) (d) = R , , X , .. · q q , q , · New(q ) · X New(q ) q : 80


· q 0, p, p, q · q 1, · q , , New(q ) (b), (c), (d) q . 2. New(q ) X, (a) , q = q : New(q ) New(q ) Old(q ) = Old(q ) q , q (b) · q = { | X New(q )} = New(q ) q q , · New(q ) . S , .

5.4.6



MC-LTL (5.32) (5.34), . : B1 B2 L(B1 ) L(B2 ). , PSPACE-. Bi (i = 1, 2) ( A, Qi , i , Q0 , Fi ) i 81


S ( {p1 , p2 }, Q1 â Q2 , , L, Q0 â Q0 ) 1 2 · (q1 , q2 ) (q1 , q2 ), a, , qi q 1, 2) · (q1 , q2 )(pi ) = 1 qi F
i a i

(i =

(i = 1, 2).

, L(B1 ) L(B2 ) : · S LTL­ A(GFp1 GFp2 ) · S CTL­ AGAFp2 fairness, CTL­ AGAFp1 .

82



[1] International Standard ISO/IEC 9126. Information Technology - Software Product Evaluation - Quality Characteristics and Guidelines for their Use. International Organization for Standardization, International Electrotechnical Commission, Geneva, 1991. [2] . , , 1993. [3] E. Clarke, O. Grumb erg, D. Peled: Model checking. MIT Press, 2001.

83