Лекция 5. Model Checking для CTL. BDD - двоичные разрешающие диаграммы (1185527), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

Ïðîâåðüòå âûïîëíèìîñòü â ìîäåëè ìèêðîâîëíîâîéïå÷è âûïîëíèìîñòü äðóãèõ ñïåöèôèêàöèé:I AG(Error→ A[¬Start R Error ]) ,I AG EX EX EX HeatI,¬ EG(Error → AX Error ) ,I AG(A[¬Start UClose]) .Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòèÒåïåðü ìû ïîêàæåì, êàê îáîáùèòü àëãîðèòì âåðèôèêàöèèìîäåëåé äëÿ ëîãèêè CTL, ÷òîáû îõâàòèòü îãðàíè÷åíèÿñïðàâåäëèâîñòè.Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòèÒåïåðü ìû ïîêàæåì, êàê îáîáùèòü àëãîðèòì âåðèôèêàöèèìîäåëåé äëÿ ëîãèêè CTL, ÷òîáû îõâàòèòü îãðàíè÷åíèÿñïðàâåäëèâîñòè.Ðàññìîòðèì ñïðàâåäëèâóþ ìîäåëü Êðèïêå M = (S, R, L, F ) , âêîòîðîé F = {P1 , .

. . , Pk } ìíîæåñòâî îãðàíè÷åíèéñïðàâåäëèâîñòè , ãäå Pi ⊆ S äëÿ âñåõ i, 1 ≤ i ≤ k .Ïóñòü π = s0 , s1 , . . . ïóòü â M . Ââåäåì ñëåäóþùóþõàðàêòåðèñòèêó ïóòè:inf (π) = {s | s = si äëÿ áåñêîíå÷íî ìíîãèõ i}.Áóäåì ãîâîðèòü, ÷òî π ñïðàâåäëèâûé ïóòü, åñëè äëÿ âñÿêîãîîãðàíè÷åíèÿ ñïðàâåäëèâîñòè Pi èç F âûïîëíÿåòñÿ ñîîòíîøåíèåinf (π) ∩ Pi 6= ∅ .Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòèÑåìàíòèêà CTL íà ñïðàâåäëèâûõ ìîäåëÿõ Êðèïêå î÷åíü ïîõîæàíà ñåìàíòèêó CTL íà îáû÷íûõ ìîäåëÿõ Êðèïêå.Ìû áóäåì èñïîëüçîâàòü çàïèñü M, s |=F ϕ äëÿ îáîçíà÷åíèÿòîãî, ÷òî ôîðìóëà ñîñòîÿíèÿ ϕ èñòèííà â ñîñòîÿíèè s íàñïðàâåäëèâîé ìîäåëè Êðèïêå M .Èçìåíåíèÿ âíîñÿòñÿ òîëüêî â íåêîòîðûå ïóíêòû îïðåäåëåíèÿîòíîøåíèÿ âûïîëíèìîñòè äëÿ CTL.IM, s |=F p ⇔ åñòü F -ñïðàâåäëèâûé ïóòü, èñõîäÿùèé èç s ,è ïðè ýòîì p ∈ L(s) ;IM, s |=F E(ϕ) ⇔ â ìîäåëè M åñòü òàêîé F -ñïðàâåäëèâûéïóòü π èç ñîñòîÿíèÿ s , ÷òî M, π |= ϕ ;IM, s |=F A(ϕ) ⇔ äëÿ êàæäîãî ñïðàâåäëèâîãî ïóòè π âìîäåëè M èç ñîñòîÿíèÿ s âåðíî ñîîòíîøåíèå M, π |= g1 .Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòèÁóäåì ãîâîðèòü, ÷òî ñèëüíî ñâÿçíàÿ êîìïîíåíòà C ãðàôà Mÿâëÿåòñÿ ñïðàâåäëèâîé îòíîñèòåëüíî îãðàíè÷åíèéñïðàâåäëèâîñòè F , â òîì è òîëüêî òîì ñëó÷àå, êîãäà äëÿêàæäîãî Pi ∈ F ñóùåñòâóåò ñîñòîÿíèå ti ∈ C ∩ Pi .Âíà÷àëå ïðèâåäåì àëãîðèòì äëÿ ïðîâåðêè EG f1 íàñïðàâåäëèâîé ìîäåëè.Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòèprocedure CheckFair EG(f1 )S 0 := {s | f1 ∈ label(s)}; íåòðèâèàëüíàÿ ñïðàâåäëèâàÿFair SCCS := {C | CT := C ∈Fair 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 procedureSCCâ S 0 };Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòè×òîáû óñòàíîâèòü êîððåêòíîñòü ýòîãî àëãîðèòìà, ïîòðåáóåòñÿëåììà, àíàëîãè÷íàÿ ëåììå 1.Êàê è ïðåæäå, áóäåì ïîëàãàòü, ÷òî ìîäåëü M 0 ïîëó÷åíà èç Mçà ñ÷åò óäàëåíèÿ èç S âñåõ òåõ ñîñòîÿíèé, â êîòîðûõ f1 íåâûïîëíÿåòñÿ ñïðàâåäëèâî .Òàêèì îáðàçîì, M 0 = (S 0 , R 0 , L0 , F 0 ) , ãäåS 0 = {s ∈ S | M, s |=F f1 } , R 0 = RS 0 ×S 0 , L0 = LS 0 èF 0 = {Pi ∩ S 0 | Pi ∈ F } .Ëåììà 2.

Ñîîòíîøåíèå M, s |=F EG f1 âåðíî òîãäà è òîëüêîòîãäà, êîãäà ñîáëþäåíû ñëåäóþùèå äâà óñëîâèÿ:Iñîñòîÿíèå s ñîäåðæèòñÿ â ìíîæåñòâå S 0 ,Iâ M 0 èìååòñÿ ïóòü, âåäóùèé èç s â íåêîòîðóþ âåðøèíó t ,ñîäåðæàùóþñÿ â íåòðèâèàëüíîé ñïðàâåäëèâîé ñèëüíîñâÿçíîé êîìïîíåíòå C ãðàôà (S 0 , R 0 ) .Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòèÄëÿ ïðîâåðêè äðóãèõ CTL-ôîðìóë íà ñïðàâåäëèâûõ ìîäåëÿõÊðèïêå ââåäåì â ðàññìîòðåíèå âñïîìîãàòåëüíîå àòîìàðíîåâûñêàçûâàíèå fair = EG true . Íåòðóäíî çàìåòèòü, ÷òî äëÿëþáîãî ñîñòîÿíèÿ s âåðíîM, s |=F fair ⇔ èç s èñõîäèò ñïðàâåäëèâûé ïóòü.Ðàçìåòèòü ñîñòîÿíèÿ ýòèì íîâûì àòîìàðíûì âûñêàçûâàíèåììîæíî ïðè ïîìîùè ïðîöåäóðû CheckFairEG (true).Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòèÄëÿ ïðîâåðêè äðóãèõ CTL-ôîðìóë íà ñïðàâåäëèâûõ ìîäåëÿõÊðèïêå ââåäåì â ðàññìîòðåíèå âñïîìîãàòåëüíîå àòîìàðíîåâûñêàçûâàíèå fair = EG true .

Íåòðóäíî çàìåòèòü, ÷òî äëÿëþáîãî ñîñòîÿíèÿ s âåðíîM, s |=F fair ⇔ èç s èñõîäèò ñïðàâåäëèâûé ïóòü.Ðàçìåòèòü ñîñòîÿíèÿ ýòèì íîâûì àòîìàðíûì âûñêàçûâàíèåììîæíî ïðè ïîìîùè ïðîöåäóðû CheckFairEG (true).×òîáû ïðîâåðèòü ñîîòíîøåíèå M, s |=F p äëÿ íåêîòîðîãîp ∈ AP , ïðîâåðÿåì ñîîòíîøåíèå M, s |= p ∧ fair ïðè ïîìîùèîáû÷íîé ïðîöåäóðû âåðèôèêàöèè ìîäåëåé.Äëÿ ïðîâåðêè ñîîòíîøåíèÿ M, s |=F EX f1 îáðàùàåìñÿ ê çàäà÷åàíàëèçà ñîîòíîøåíèÿ M, s |= EX(f1 ∧ fair ) .È, íàêîíåö, ÷òîáû ïðîâåðèòü ñîîòíîøåíèå M, s |=F E[f1 U f2 ]àíàëèçèðóåì ñîîòíîøåíèå M, s |= E[f1 U (f2 ∧ fair )] ,îáðàòèâøèñü ê ïðîöåäóðå CheckEU(f1 , f2 ∧ fair ) .Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòèÒåîðåìà.

Ñóùåñòâóåò àëãîðèòì ïðîâåðêè âûïîëíèìîñòèïðîèçâîëüíîé CTL-ôîðìóëû ϕ â ñîñòîÿíèè s íà ìîäåëèM = (S, R, L, F ) â ðàìêàõ ñïðàâåäëèâîé ñåìàíòèêè çà âðåìÿO(|ϕ|(|S| + |R|)|F |) .Àíàëèç ñëîæíîñòè òàêîâ æå, êàê è ïðè îòñóòñòâèèñïðàâåäëèâîñòè.Âðåìÿ, íåîáõîäèìîå íà êàæäîì ýòàïå ðàáîòû àëãîðèòìà,ñîñòàâëÿåò O((|S| + |R|)|F |) .Òàê êàê ÷èñëî òàêèõ ýòàïîâ íå ïðåâîñõîäèò |ϕ| , îáùàÿñëîæíîñòü ïî âðåìåíè ðàâíà O(|ϕ|(|S| + |R|)|F |) .Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòè×òîáû ïîñìîòðåòü, êàêîå âëèÿíèå îêàçûâàåò ñïðàâåäëèâîñòü,îáðàòèìñÿ âíîâü ê ôîðìóëå AG(Start → AF Heat) èëè, êðàâíîñèëüíîé åé ôîðìóëåϕ = ¬ E[True U (Start ∧ EG ¬Heat)]íà ìîäåëè ìèêðîâîëíîâîé ïå÷è.Îäíàêî íà ýòîò ðàç áóäåì ðàññìàòðèâàòü òîëüêî òå ïóòè, íàïðîòÿæåíèè êîòîðûõ ïîëüçîâàòåëü ïðàâèëüíî ðàáîòàåò ñìèêðîâîëíîâîé ïå÷üþ áåñêîíå÷íî ÷àñòî.

Ýòî îçíà÷àåò, ÷òîäîëæíî áåñêîíå÷íî ÷àñòî âûïîëíÿòüñÿ óñëîâèåStart ∧ Close ∧ ¬Error .Èòàê, F = {P} , ãäå P = {s | s |= Start ∧ Close ∧ ¬Error } .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Âûäåëèì ïîäôîðìóëû:If0 = fair = EG trueIf1 = Start ∧ f0If2 = ¬(Heat ∧ f0 )If3 = EG f2If4 = f1 ∧ f3If5 = E[True U f4 ∧ f0 ]Iϕ = ¬f5Ïðîâåðÿåì ïîäôîðìóëó1'$¬Startf0 = EG true&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@¬StartStartãîòîâî¬Start%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöóñáðîñïå÷ü5?'6?$'StartStartñòðÿïíþ7$'ïîäîãðåòü$Start&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'f0 = EG true$¬Startf0&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'''$$@¬Startf0Startf0ãîòîâî¬Startf0%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöóñáðîñïå÷ü5?'6?$'Startf0Startf0&%&ñòðÿïíþ7$'ïîäîãðåòü-$Startf0%&%Ïðîâåðÿåì ïîäôîðìóëó1'f0 = EG true$¬Startf0f1 = (Start ∧ f0 )&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'''$$@¬Startf0Startf0ãîòîâî¬Startf0%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöóñáðîñïå÷ü5?'6?$'Startf0Startf0&%&ñòðÿïíþ7$'ïîäîãðåòü-$Startf0%&%Ïðîâåðÿåì ïîäôîðìóëó1'f0 = EG true$¬Startf0f1 = (Start ∧ f0 )&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'''$$@¬Startf0Startf0f1ãîòîâî¬Startf0%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöóñáðîñïå÷ü5?'6?$'Startf0f1Startf0f1&%&ñòðÿïíþ7$'ïîäîãðåòü-$Startf0f1%&%Ïðîâåðÿåì ïîäôîðìóëó1'$¬Heatf2 = ¬(Heat ∧ f0 )&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@¬Heat¬HeatãîòîâîHeat%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'¬Heatñáðîñïå÷ü6?$'¬Heatñòðÿïíþ7$'ïîäîãðåòü$Heat&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'f2 = ¬(Heat ∧ f0 )$¬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'$$f2f3 = EG f2&%&%I@ñòðÿïàòü6$$@ îòêðûòü 'çàïóñòèòü îòêðûòüçàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@''$'$'$23? $4?$''$@f2f2ãîòîâîf2%%&%&%&%%&%&%&66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó''5??f2ñáðîñïå÷ü$'6?$f2ñòðÿïíþ7$'$ïîäîãðåòü&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'$f1f4 = f1 ∧ f3&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@f1ãîòîâîf1%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'ñáðîñïå÷ü6?$'ñòðÿïíþ7$'$ïîäîãðåòü&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'$f1f4 = f1 ∧ f3f5 = E[True U f4 ∧ f0 ]&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@f1ãîòîâîf1%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'ñáðîñïå÷ü6?$'ñòðÿïíþ7$'$ïîäîãðåòü&%&%&%Ïðîâåðÿåì ïîäôîðìóëó1'f4 = f1 ∧ f3$f1ϕf5 = E[True U f4 ∧ f0 ]&%I@ñòðÿïàòü6$çàïóñòèòü îòêðûòü@ îòêðûòü 'çàêðûòüïå÷üäâåðöóäâåðöó @ äâåðöó@ 423? $?'$''$@ϕ = ¬f5f1ϕãîòîâîϕf1ϕ%&%&%&%66îòêðûòüçàêðûòüçàïóñòèòüíà÷àòüäâåðöóäâåðöó5?'ñáðîñïå÷ü6?$'ñòðÿïíþ7$'ïîäîãðåòüϕ&ϕ%&-$ϕ%&%Model checking äëÿ CTL â îãðàíè÷åíèÿõñïðàâåäëèâîñòèÒàêèì îáðàçîì,S(¬ E[True U (Start ∧ EG ¬Heat)]) = {1, 2, 3, 4, 5, 6, 7} .À ýòî îçíà÷àåò, ÷òî M, 1 |=F AG(Start → AF Heat) , ò.å.ïðîãðàììà ìèêðîâîëíîâîé ïå÷è óäîâëåòâîðÿåò ñïåöèôèêàöèèïðàâèëüíîãî ïîâåäåíèÿ ïðè çàäàííûõ îãðàíè÷åíèÿõñïðàâåäëèâîñòè.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÄîñòîèíñòâà ïðåäëîæåííîãî àëãîðèòìà:1.

Характеристики

Список файлов лекций