Лекция 5. Model Checking для CTL. BDD - двоичные разрешающие диаграммы (1185527), страница 2
Текст из файла (страница 2)
Äîïóñòèì, ÷òî M, s |= EG f1 . ßñíî, ÷òîs ∈ S 0 . Ðàññìîòðèì òàêîé áåñêîíå÷íûé ïóòü π , èñõîäÿùèé èç s, ÷òî f1 âûïîëíÿåòñÿ â êàæäîì ñîñòîÿíèè íà ïðîòÿæåíèè π .Òàê êàê ìîäåëü M êîíå÷íà, ïóòü π âñåãäà ìîæíî ïðåäñòàâèòü ââèäå π = π0 π1 , ãäå π0 êîíå÷íûé íà÷àëüíûé îòðåçîê, à π1 áåñêîíå÷íûé ñóôôèêñ π , îáëàäàþùèé òåì ñâîéñòâîì, ÷òîêàæäîå ñîñòîÿíèå â π1 âñòðå÷àåòñÿ â íåì áåñêîíå÷íî ÷àñòî.ßñíî, ÷òî π0 ñîäåðæèòñÿ â S 0 .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLËåììà 1. M, s |= EG f1 òîãäà è òîëüêî òîãäà, êîãäàñîáëþäåíû ñëåäóþùèå äâà óñëîâèÿ:Iñîñòîÿíèå s ñîäåðæèòñÿ â ìíîæåñòâå S 0 ;Iâ M 0 åñòü ïóòü, âåäóùèé èç s â íåêîòîðóþ âåðøèíó t ,ñîäåðæàùóþñÿ â íåòðèâèàëüíîé ñèëüíî ñâÿçíîéêîìïîíåíòå C ãðàôà (S 0 , R 0 ) .Äîêàçàòåëüñòâî.
Äîïóñòèì, ÷òî M, s |= EG f1 . ßñíî, ÷òîs ∈ S 0 . Ðàññìîòðèì òàêîé áåñêîíå÷íûé ïóòü π , èñõîäÿùèé èç s, ÷òî f1 âûïîëíÿåòñÿ â êàæäîì ñîñòîÿíèè íà ïðîòÿæåíèè π .Òàê êàê ìîäåëü M êîíå÷íà, ïóòü π âñåãäà ìîæíî ïðåäñòàâèòü ââèäå π = π0 π1 , ãäå π0 êîíå÷íûé íà÷àëüíûé îòðåçîê, à π1 áåñêîíå÷íûé ñóôôèêñ π , îáëàäàþùèé òåì ñâîéñòâîì, ÷òîêàæäîå ñîñòîÿíèå â π1 âñòðå÷àåòñÿ â íåì áåñêîíå÷íî ÷àñòî.ßñíî, ÷òî π0 ñîäåðæèòñÿ â S 0 .Îáîçíà÷èì ñèìâîëîì C ìíîæåñòâî ñîñòîÿíèé, ÷åðåç êîòîðûåïðîõîäèò π1 .
Î÷åâèäíî, ÷òî C ñîäåðæèòñÿ â S 0 .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÄîêàçàòåëüñòâî.Ïîêàæåì, ÷òî ìåæäó ëþáîé ïàðîé ñîñòîÿíèé èç C ïðîõîäèòïóòü, öåëèêîì ëåæàùèé â C .Ðàññìîòðèì ïðîèçâîëüíûå ñîñòîÿíèÿ s1 è s2 èç C . Âûáåðåìíåêîòîðîå âõîæäåíèå s1 â π1 . Ó÷èòûâàÿ òî, êàêèì îáðàçîì áûëâûáðàí ïóòü π1 , ìû ìîæåì óòâåðæäàòü, ÷òî îäíî èç âõîæäåíèéñîñòîÿíèÿ s2 ðàñïîëàãàåòñÿ íà ïóòè π1 åùå äàëüøå.Îòðåçîê ìåæäó âûáðàííûìè âõîæäåíèÿìè ñîñòîÿíèé s1 è s2öåëèêîì ëåæèò â C . Ýòîò îòðåçîê ïðåäñòàâëÿåò ñîáîé ïóòü èçs1 â s2 , ëåæàùèé â C .Òàêèì îáðàçîì, C ëèáî ÿâëÿåòñÿ ñèëüíî ñâÿçíîé êîìïîíåíòîé,ëèáî ñîäåðæèòñÿ â îäíîé èç òàêèõ êîìïîíåíò.
 ëþáîì ñëó÷àåîáà çàÿâëåííûõ óñëîâèÿ ëåììû âûïîëíÿþòñÿ.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLËåììà 1. M, s |= EG f1 òîãäà è òîëüêî òîãäà, êîãäàñîáëþäåíû ñëåäóþùèå äâà óñëîâèÿ:Iñîñòîÿíèå s ñîäåðæèòñÿ â ìíîæåñòâå S 0 ;Iâ M 0 åñòü ïóòü, âåäóùèé èç s â íåêîòîðóþ âåðøèíó t ,ñîäåðæàùóþñÿ â íåòðèâèàëüíîé ñèëüíî ñâÿçíîéêîìïîíåíòå C ãðàôà (S 0 , R 0 ) .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLËåììà 1. M, s |= EG f1 òîãäà è òîëüêî òîãäà, êîãäàñîáëþäåíû ñëåäóþùèå äâà óñëîâèÿ:Iñîñòîÿíèå s ñîäåðæèòñÿ â ìíîæåñòâå S 0 ;Iâ M 0 åñòü ïóòü, âåäóùèé èç s â íåêîòîðóþ âåðøèíó t ,ñîäåðæàùóþñÿ â íåòðèâèàëüíîé ñèëüíî ñâÿçíîéêîìïîíåíòå C ãðàôà (S 0 , R 0 ) .Äîêàçàòåëüñòâî.À òåïåðü äîïóñòèì, ÷òî óñëîâèÿ ëåììû ñîáëþäåíû.Ðàññìîòðèì ïóòü π0 èç s â t .
Îáîçíà÷èì π1 êîíå÷íûé ïóòüäëèíû ≥ 1 , èñõîäÿùèé èç t è âíîâü âîçâðàùàþùèéñÿ â t .Òàêîé ïóòü π1 íàâåðíÿêà ñóùåñòâóåò, ò.ê. ñîñòîÿíèå t ëåæèò âíåòðèâèàëüíîé ñèëüíî ñâÿçíîé êîìïîíåíòå.Âñå ñîñòîÿíèÿ â áåñêîíå÷íîì ïóòè π = π0 π1ω óäîâëåòâîðÿþò f1 .Ïîñêîëüêó π îäèí èç äîïóñòèìûõ ïóòåé, èñõîäÿùèõ èç s âìîäåëè M , ìû óáåæäàåìñÿ â òîì, ÷òî M, s |= EG f1 . Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÀëãîðèòì äëÿ ñëó÷àÿ g = EG f1 âûòåêàåò èç ëåììû.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÀëãîðèòì äëÿ ñëó÷àÿ g = EG f1 âûòåêàåò èç ëåììû.Âíà÷àëå ñòðîèì ñîêðàùåííóþ ìîäåëü Êðèïêå M 0 = (S 0 , R 0 , L0 ) ,êàê ýòî áûëî îïèñàíî âûøå.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÀëãîðèòì äëÿ ñëó÷àÿ g = EG f1 âûòåêàåò èç ëåììû.Âíà÷àëå ñòðîèì ñîêðàùåííóþ ìîäåëü Êðèïêå M 0 = (S 0 , R 0 , L0 ) ,êàê ýòî áûëî îïèñàíî âûøå.Äàëåå ðàçáèâàåì ãðàô (S 0 , R 0 ) íà ñèëüíî ñâÿçíûå êîìïîíåíòû,ïðèìåíÿÿ îäèí èç ýôôåêòèâíûõ àëãîðèòìîâ ðåøåíèÿ ýòîéçàäà÷è (íàïðèìåð, àëãîðèòì Òàðüÿíà).
Ýòîò àëãîðèòì èìååòñëîæíîñòü O(|S 0 | + |R 0 |) .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÀëãîðèòì äëÿ ñëó÷àÿ g = EG f1 âûòåêàåò èç ëåììû.Âíà÷àëå ñòðîèì ñîêðàùåííóþ ìîäåëü Êðèïêå M 0 = (S 0 , R 0 , L0 ) ,êàê ýòî áûëî îïèñàíî âûøå.Äàëåå ðàçáèâàåì ãðàô (S 0 , R 0 ) íà ñèëüíî ñâÿçíûå êîìïîíåíòû,ïðèìåíÿÿ îäèí èç ýôôåêòèâíûõ àëãîðèòìîâ ðåøåíèÿ ýòîéçàäà÷è (íàïðèìåð, àëãîðèòì Òàðüÿíà).
Ýòîò àëãîðèòì èìååòñëîæíîñòü O(|S 0 | + |R 0 |) .Çàòåì âûäåëÿåì òå ñîñòîÿíèÿ, êîòîðûå ïðèíàäëåæàò ñèëüíîñâÿçíûì êîìïîíåíòàì. Ïîòîì âîçâðàùàåìñÿ íàçàä, èñïîëüçóÿîáðàùåíèå R 0 , è âûäåëÿåì, òàêèì îáðàçîì, âñå òå ñîñòîÿíèÿ,êîòîðûå ëåæàò íà ïóòÿõ, ïðîõîäÿùèõ ïî ñîñòîÿíèÿì,ïîìå÷åííûì f1 .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÂñå âû÷èñëåíèå ìîæíî âûïîëíèòü çà âðåìÿ O(|S| + |R|) .Ïðîöåäóðà CheckEG , äîáàâëÿþùàÿ EG f1 ê ìíîæåñòâó label(s)äëÿ êàæäîãî s , â êîòîðîì âûïîëíÿåòñÿ EG f1 , ïðè óñëîâèè, ÷òîôîðìóëà f1 óæå áûëà êîððåêòíî îáðàáîòàíà.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLprocedure CheckEG(f1 )S 0 := {s | f1 ∈ label(s)};SCC :=SCC S 0 };S {C | CT := C ∈SCC {s | s ∈ C };for all s ∈ T do label(s) := label(s) ∪ {EG f1 };while T 6= ∅ dochoose s ∈ T ;T := T \ {s};for all t such that t ∈ S 0 and R(t, s) doif EG f1 ∈/ label(t) thenlabel(t) := label(t) ∪ {EG f1 };T := T ∪ {t}; íåòðèâèàëüíàÿâend if;end for all;end whileend procedureÐèñ.: Ïðîöåäóðà ðàçìåòêè ñîñòîÿíèé äëÿ ôîðìóëûEG f1Òàáëè÷íûé àëãîðèòì model checking äëÿ CTL×òîáû ïðîâåðèòü CTL-ôîðìóëó ϕ , íóæíî ïðèìåíÿòü àëãîðèòìðàçìåòêè ñîñòîÿíèé êî âñåì åå ïîäôîðìóëàì, íà÷èíàÿ ñ ñàìûõêîðîòêèõ è íàèáîëåå ãëóáîêî âëîæåííûõ ïîäôîðìóë, èïðîäâèãàòüñÿ íàðóæó, ïîêà íå áóäåò îõâà÷åíà ôîðìóëà ϕ .Ñëåäóÿ òàêîé ñõåìå âû÷èñëåíèÿ, ìîæíî áûòü óâåðåííûì â òîì,÷òî êàê òîëüêî ìû ïðèíèìàåìñÿ çà íåêîòîðóþ ïîäôîðìóëóôîðìóëû ϕ , âñå åå ïîäôîðìóëû óæå áûëè îáðàáîòàíû.Êîëü ñêîðî êàæäûé ïðîõîä òðåáóåò âðåìåíè O(|S| + |R|) , àôîðìóëà ϕ ìîæåò ñîäåðæàòü íå áîëåå |ϕ| ðàçëè÷íûõïîäôîðìóë, âñÿ ðàáîòà àëãîðèòìà ïðîâîäèòñÿ çà âðåìÿO(|ϕ|(|S| + |R|)) .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÒåîðåìà.
Ñóùåñòâóåò àëãîðèòì ïðîâåðêè âûïîëíèìîñòèïðîèçâîëüíîé CTL-ôîðìóëû ϕ â ñîñòîÿíèè s íà ìîäåëèM = (S, R, L) çà âðåìÿ O(|ϕ|(|S| + |R|)) .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÏîÿñíèì ðàáîòó àëãîðèòìà âåðèôèêàöèè ìîäåëåé äëÿ CTL íàïðèìåðå ìèêðîâîëíîâîé ïå÷è.Êàæäîå ñîñòîÿíèå ìîäåëè ïîìå÷åíî ñïèñêîì, â êîòîðûéâêëþ÷åíû âñå òå àòîìàðíûå âûñêàçûâàíèÿ, êîòîðûå èñòèííû âýòîì ñîñòîÿíèè, à òàêæå îòðèöàíèÿ âñåõ òåõ àòîìàðíûõâûñêàçûâàíèé, êîòîðûå ëîæíû â ýòîì ñîñòîÿíèè. Ïîìåòêè íàäóãàõ îáîçíà÷àþò äåéñòâèÿ, ïðèâîäÿùèå ê ïåðåõîäàì.Ïðîâåðèì íà ýòîé ìîäåëè CTL-ôîðìóëóAG(Start → AF Heat),ýêâèâàëåíòíóþ ôîðìóëåϕ = ¬ E[True U ¬(¬Start ∨ ¬ EG ¬Heat)]1'$¬Start¬Close¬Heat¬Error&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'''$$@¬StartClose¬Heat¬ErrorStart¬Close¬HeatErrorãîòîâî¬StartCloseHeat¬Error%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó?5'StartClose¬HeatError&ñáðîñïå÷ü?6$'StartClose¬Heat¬Error%&ñòðÿïíþ7$'ïîäîãðåòü-StartCloseHeat¬Error%&$%Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLϕ = ¬ E[True U ¬(¬Start ∨ ¬ EG ¬Heat)]Âûäåëèì ïîäôîðìóëû:If1 = ¬StartIf2 = ¬HeatIf3 = EG f2If4 = ¬(f1 ∨ ¬f2 )If5 = E[True U f4 ]Iϕ = ¬f5Ïðîâåðÿåì ïîäôîðìóëó1'$¬Startf1 = ¬Start&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@¬StartStartãîòîâî¬Start%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöóñáðîñïå÷ü5?'6?$'StartStartñòðÿïíþ7$'ïîäîãðåòü$Start&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'f1 = ¬Start$¬Startf1&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 432? $?''$'$@¬Startf1Startãîòîâî¬Startf1%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöóñáðîñïå÷ü5?'6?$'StartStartñòðÿïíþ7$'ïîäîãðåòü$Start&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'$¬Heatf2 = ¬Heat&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@¬Heat¬HeatãîòîâîHeat%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'¬Heatñáðîñïå÷ü6?$'¬Heatñòðÿïíþ7$'ïîäîãðåòü$Heat&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'f2 = ¬Heat$¬Heatf2&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'''$$@¬Heatf2¬Heatf2ãîòîâîHeat%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'¬Heatf2&ñáðîñïå÷ü6?$'¬Heatf2%&ñòðÿïíþ7$'ïîäîãðåòü$Heat%&%Ïðîâåðÿåì ïîäôîðìóëó1'$f2f3 = EG f2&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@f2f2ãîòîâîf2%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'f2ñáðîñïå÷ü6?$'f2ñòðÿïíþ7$'$ïîäîãðåòü&%&%&%Ïðîâåðÿåì ïîäôîðìóëó'1$f2f3 = EG f2&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@'''$23? $4?$'$@f2f2ãîòîâîf2%&%&%&&%%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó'5?f2ñáðîñïå÷ü6?$'f2ñòðÿïíþ7$'$ïîäîãðåòü&%&%&%Ïðîâåðÿåì ïîäôîðìóëó'1'$$f2f3 = EG f2&%&%I@ñòðÿïàòü6$$@ îòêðûòü 'çàïóñòèòü îòêðûòüçàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@''$'$'$23? $4?$''$@f2f2ãîòîâîf2%%&%&%&%%&%&%&66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó''5??f2ñáðîñïå÷ü$'6?$f2ñòðÿïíþ7$'$ïîäîãðåòü&%&%&%Ïðîâåðÿåì ïîäôîðìóëó'1'f3 = EG f2$$f2f3&%&%I@ñòðÿïàòü6$$@ îòêðûòü 'çàïóñòèòü îòêðûòüçàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@''$'$'$234? $?$''$@f2f3f2f3ãîòîâîf2f3%%&%&%&%%&%&%&66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó''5??f2f3&ñáðîñïå÷ü$'6?$f2ñòðÿïíþ7$'$ïîäîãðåòü%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'f4 = ¬(f1 ∨ ¬f3 )$f1f3&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 432? $?''$'$@f1f3f3ãîòîâîf1f3%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'ñáðîñïå÷ü6?$'$ïîäîãðåòüf3&ñòðÿïíþ7$'%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'f4 = ¬(f1 ∨ ¬f3 )$f1f3&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 432? $?''$'$@f1f3f3ãîòîâîf4f1f3%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'f3f4&ñáðîñïå÷ü6?$'ñòðÿïíþ7$'$ïîäîãðåòüf4%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'$f5 = E[True U f4 ]&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@f4ãîòîâî%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'f4ñáðîñïå÷ü6?$'f4ñòðÿïíþ7$'$ïîäîãðåòü&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'$f5f5 = E[True U f4 ]&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?''$'$@f4f5ãîòîâîf5f5%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'f4f5&ñáðîñïå÷ü6?$'f4f5%&ñòðÿïíþ7$'ïîäîãðåòü-$f5%&%Ïðîâåðÿåì ïîäôîðìóëó1'$f5ϕ = ¬f5ϕ = AG(Start → AF Heat)&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@f5f5ãîòîâîf5%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'f5ñáðîñïå÷ü6?$'f5ñòðÿïíþ7$'ïîäîãðåòü$f5&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'ϕ = ¬f5$f56|= ϕϕ = AG(Start → AF Heat)&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'''$$@f56|= ϕf56|= ϕãîòîâîf56|= ϕ%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'ñáðîñïå÷ü6?$'f56|= ϕf56|= ϕ&%&ñòðÿïíþ7$'ïîäîãðåòü-$f56|= ϕ%&%Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÒàêèì îáðàçîì, M, 1 6|= AG(Start → AF Heat) .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÒàêèì îáðàçîì, M, 1 6|= AG(Start → AF Heat) .Çàäà÷à.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
