ltl模型检测总结ppt-ltlmodelchecking

ltl模型检测总结ppt-ltlmodelchecking内容摘要：

1,1,I1,F1, A2=,S2,2,I2,F2. Define A1A2= ,S,,I,F where S = S1 x S2 x {0,1,2}  = ? I = I1 x I2 x {0} F = S1 x S2 x {2} Intersection  = { ((s1,s2,i),a,((s1’,s2’,i)) | i {0,1}, (s1,a,s1’)1, (s2,a,s2’)2 }  { ((s1,s2,0),a,((s1’,s2’,1)) | (s1,a,s1’)1, (s2,a,s2’)2, s1F1 }  { ((s1,s2,1),a,((s1’,s2’,2)) | (s1,a,s1’)1, (s2,a,s2’)2, s2F2 }  { ((s1,s2,2),a,((s1’,s2’,0)) | (s1,a,s1’)1, (s2,a,s2’)2 } Intersection Theorem L(A1  A2 ) = L(A1 )  L(A2) Complementation The set of BAs is closed under plementation. Given A=,S,,I,F. There exists a BA B such that L(B) =  \L(A) Generalized Buchi Automaton Definition A GBA is a quintuple ,S,,I,F – : A finite set of symbols – S : A finite set of states –  S x  x S : A transition relation – I  S : A set of initial states – F  2S : A set of sets of acceptance states Accepting Run Definition An accepting run of A is a run  of A such that for each fF, inf()f. Union Given two automaton A1=,S1,1,I1,F1, A2=,S2,2,I2,F2. Suppose that S1 and S2 are disjoint. Define A1A2= ,S,,I,F where S = S1 S2  = 1 2 I = I1 I2 F = { f  S2 | f F1 }  { f  S1 | f F2 } Union Theorem L(A1A2 ) = L(A1 )  L(A2) Intersection Given two automaton A1=,S1,1,I1,F1, A2=,S2,2,I2,F2. Define A1A2= ,S,,I,F where S = S1 x S2  = { ((s1,s2),a,((s1’,s2’))| (s1,a,s1’)1, (s2,a,s2’)2 } I = I1 x I2 F = { f x S2 | f F1}  { S1 x f| f F2} Intersection Theorem。