ltl模型檢測總結(jié)ppt-ltlmodelchecking(編輯修改稿)
2024-11-04 20:45 本頁面
【文章內(nèi)容簡介】 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
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1