Лекция 5. Model Checking для CTL. BDD - двоичные разрешающие диаграммы (1185527)
Текст из файла
Ìåòîäûâåðèôèêàöèèïðîãðàìì è ñõåìËÅÊÒÎÐÛ:Âëàäèìèð Àíàòîëüåâè÷ ÇàõàðîâÂëàäèñëàâ Âàñèëüåâè÷ Ïîäûìîâzakh@cs.msu.suËåêöèÿ 5.Âåðèôèêàöèÿ ìîäåëåé ïðîãðàìì1.2.3.4.5.6.Çàäà÷à model checking äëÿ CTLÒàáëè÷íûé àëãîðèòì model checkingäëÿ CTLModel checking äëÿ CTL âîãðàíè÷åíèÿõ ñïðàâåäëèâîñòèÄâîè÷íûå ðàçðåøàþùèå äèàãðàììû(BDDs)Ïîñòðîåíèå ðàçðåøàþùèõ äèàãðàììÏðåäñòàâëåíèå ìîäåëåé Êðèïêåäâîè÷íûìè ðàçðåøàþùèìèäèàãðàììàìèÇàäà÷à model checking äëÿ CTLÐàññìîòðèì ìíîæåñòâî àòîìàðíûõ âûñêàçûâàíèé AP .Ìîäåëüþ Êðèïêå M íàä ìíîæåñòâîì AP íàçîâåì ÷åòâåðêóM = (S, S0 , R, L) , â êîòîðîé:1) S êîíå÷íîå ìíîæåñòâî ñîñòîÿíèé ;2) S0 ⊆ S ìíîæåñòâî íà÷àëüíûõ ñîñòîÿíèé ;3) R ⊆ S × S îòíîøåíèå ïåðåõîäîâ , êîòîðîå îáÿçàíî áûòüòîòàëüíûì, ò.
å. äëÿ êàæäîãî ñîñòîÿíèÿ s ∈ S äîëæíîñóùåñòâîâàòü òàêîå ñîñòîÿíèå s 0 ∈ S , ÷òî èìååò ìåñòîR(s, s 0 ) ;4) L : S → 2AP ôóíêöèÿ ðàçìåòêè , êîòîðàÿ ïîìå÷àåòêàæäîå ñîñòîÿíèå ìíîæåñòâîì àòîìàðíûõ âûñêàçûâàíèé,èñòèííûõ â ýòîì ñîñòîÿíèè.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Ôîðìóëû ëîãèêè CTL ñòðîÿòñÿ èç àòîìàðíûõ âûñêàçûâàíèé(áàçîâûõ ñâîéñòâ) AP ïðè ïîìîùè áóëåâûõ ñâÿçîê¬, ∧, ∨, →, .
. . è äåñÿòè îñíîâíûõ îïåðàòîðîâ CTL:IAX è EX ,IAF è EF ,IAG è EG ,IAU è EU ,IAR è ER .Çàäà÷à model checking äëÿ CTLÏðèìåðû CTL ñïåöèôèêàöèé:I AG(Start→ AF Heat) ,Çàäà÷à model checking äëÿ CTLÏðèìåðû CTL ñïåöèôèêàöèé:I AG(Start→ AF Heat) ,I AG(Error→ A[¬Start R Error ]) ,Çàäà÷à model checking äëÿ CTLÏðèìåðû CTL ñïåöèôèêàöèé:I AG(Start→ AF Heat) ,I AG(Error→ A[¬Start R Error ]) ,I AG EX EX EX Heat,Çàäà÷à model checking äëÿ CTLÏðèìåðû CTL ñïåöèôèêàöèé:I AG(Start→ AF Heat) ,I AG(Error→ A[¬Start R Error ]) ,I AG EX EX EX HeatI,¬ EG(Error → AX Error ) ,Çàäà÷à model checking äëÿ CTLÏðèìåðû CTL ñïåöèôèêàöèé:I AG(Start→ AF Heat) ,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Ïóñòü çàäàíà ìîäåëü Êðèïêå M = (S, S0 , R, L) ,ïðåäñòàâëÿþùàÿ èíôîðìàöèîííóþ ñèñòåìó ñ êîíå÷íûììíîæåñòâîì ñîñòîÿíèé S , è ôîðìóëà òåìïîðàëüíîé ëîãèêè ϕ ,êîòîðàÿ âûðàæàåò íåêîòîðóþ æåëàåìóþ ñïåöèôèêàöèþ.Òðåáóåòñÿ íàéòè â ìíîæåñòâå S ïîäìíîæåñòâî Sϕ âñåõñîñòîÿíèé s , â êîòîðûõ âûïîëíÿåòñÿ ϕ , ò.å.
ìíîæåñòâîSϕ = {s ∈ S | M, s |= ϕ} ,è ïðîâåðèòü âûïîëíèìîñòü âêëþ÷åíèÿ S0 ⊆ Sϕ .Çàäà÷à model checking äëÿ CTLÏåðâûå àëãîðèòìû ðåøåíèÿ çàäà÷è âåðèôèêàöèè ìîäåëåéèñïîëüçîâàëè ÿâíîå ïðåäñòàâëåíèå ìîäåëåé Êðèïêå â âèäåðàçìå÷åííûõ îðèåíòèðîâàííûõ ãðàôîâ, äóãè êîòîðûõ çàäàâàëèïðè ïîìîùè ññûëîê. ýòîì ñëó÷àå âåðøèíû ïðåäñòàâëÿþò ñîñòîÿíèÿ èç S , äóãèãðàôà ñîîòâåòñòâóþò îòíîøåíèþ ïåðåõîäîâ R , à ðàçìåòêàâåðøèí îïðåäåëÿåòñÿ ôóíêöèåé L : S → 2AP .Àëãîðèòìû âåðèôèêàöèè ìîäåëåé, ðàáîòàþùèå ñ ÿâíûìïðåäñòàâëåíèåì ìîäåëåé, ïîëó÷èëè íàçâàíèå òàáëè÷íûõàëãîðèòìîâ , ïîñêîëüêó îíè èòåðàòèâíî çàïîëíÿëè òàáëèöóâûïîëíèìîñòè ïîäôîðìóë çàäàííîé ôîðìóëû CTL âî âñåõñîñòîÿíèÿõ ìîäåëè.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÏðèìåíÿÿ ðàâíîñèëüíûå çàìåíûIf ∧ g ≡ ¬(¬f ∨ ¬g ) ;If → g ≡ ¬f ∨ g ;I AX f≡ ¬ EX(¬f ) ;I EF f≡ E[True U f ] ;I AG f≡ ¬ EF(¬f ) ;I AF f≡ ¬ EG(¬f ) ;I A[f Ug ] ≡ ¬ E[¬g U (¬f ∧ ¬g )] ∧ ¬ EG ¬g ;I A[f Rg ] ≡ ¬ E[¬f U ¬g ] ;I E[f Rg ] ≡ ¬ A[¬f U ¬g ] ,âñÿêóþ CTL-ôîðìóëó ìîæíî çàïèñàòü ïðè ïîìîùè ñâÿçîê èîïåðàòîðîâ ¬ , ∨ , EX , EG è EU .
Òàêèì îáðàçîì, äîñòàòî÷íîóìåòü àíàëèçèðîâàòü ôîðìóëû øåñòè òèïîâ â çàâèñèìîñòè îòòîãî, ÿâëÿåòñÿ ëè ôîðìóëà g àòîìàðíîé èëè îíà ïðåäñòàâëåíàâ îäíîé èç ôîðì: ¬f1 , f1 ∨ f2 , EX f1 , EG f1 è E[f1 U f2 ] .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLAG(Start → AF Heat) ≡Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLAG(Start → AF Heat) ≡¬ EF ¬(Start → AF Heat) ≡Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLAG(Start → AF Heat) ≡¬ EF ¬(Start → AF Heat) ≡¬ E[True U ¬(Start → AF Heat)] ≡Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLAG(Start → AF Heat) ≡¬ EF ¬(Start → AF Heat) ≡¬ E[True U ¬(Start → AF Heat)] ≡¬ E[True U ¬(¬Start ∨ AF Heat)] ≡Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLAG(Start → AF Heat) ≡¬ EF ¬(Start → AF Heat) ≡¬ E[True U ¬(Start → AF Heat)] ≡¬ E[True U ¬(¬Start ∨ AF Heat)] ≡¬ E[True U ¬(¬Start ∨ ¬ EG ¬Heat)]Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÏóñòü çàäàíà ìîäåëü Êðèïêå M = (S, S0 , R, L) , è ìû õîòèìîïðåäåëèòü, â êàêèõ ñîñòîÿíèÿõ âûïîëíÿåòñÿ CTL-ôîðìóëà ϕ .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÏóñòü çàäàíà ìîäåëü Êðèïêå M = (S, S0 , R, L) , è ìû õîòèìîïðåäåëèòü, â êàêèõ ñîñòîÿíèÿõ âûïîëíÿåòñÿ CTL-ôîðìóëà ϕ .Ðàáîòà àëãîðèòìà çàêëþ÷àåòñÿ â ïðèïèñûâàíèè êàæäîìóñîñòîÿíèþ s ìíîæåñòâà label(s) òåõ ïîäôîðìóë ôîðìóëû ϕ ,êîòîðûå âûïîëíÿþòñÿ â ñîñòîÿíèè s .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÏóñòü çàäàíà ìîäåëü Êðèïêå M = (S, S0 , R, L) , è ìû õîòèìîïðåäåëèòü, â êàêèõ ñîñòîÿíèÿõ âûïîëíÿåòñÿ CTL-ôîðìóëà ϕ .Ðàáîòà àëãîðèòìà çàêëþ÷àåòñÿ â ïðèïèñûâàíèè êàæäîìóñîñòîÿíèþ s ìíîæåñòâà label(s) òåõ ïîäôîðìóë ôîðìóëû ϕ ,êîòîðûå âûïîëíÿþòñÿ â ñîñòîÿíèè s .Âíà÷àëå label(s) = L(s) .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÏóñòü çàäàíà ìîäåëü Êðèïêå M = (S, S0 , R, L) , è ìû õîòèìîïðåäåëèòü, â êàêèõ ñîñòîÿíèÿõ âûïîëíÿåòñÿ CTL-ôîðìóëà ϕ .Ðàáîòà àëãîðèòìà çàêëþ÷àåòñÿ â ïðèïèñûâàíèè êàæäîìóñîñòîÿíèþ s ìíîæåñòâà label(s) òåõ ïîäôîðìóë ôîðìóëû ϕ ,êîòîðûå âûïîëíÿþòñÿ â ñîñòîÿíèè s .Âíà÷àëå label(s) = L(s) .Äàëåå íà êàæäîì øàãå i îáðàáàòûâàþòñÿ ïîäôîðìóëû, âêîòîðûõ ãëóáèíà âëîæåííîñòè CTL-îïåðàòîðîâ ðàâíà i − 1 .Ïîñëå îáðàáîòêè ïîäôîðìóëó äîáàâëÿþò ê ìíîæåñòâó label(s)âñåõ òåõ ñîñòîÿíèé, â êîòîðûõ îíà âûïîëíèìà.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÏóñòü çàäàíà ìîäåëü Êðèïêå M = (S, S0 , R, L) , è ìû õîòèìîïðåäåëèòü, â êàêèõ ñîñòîÿíèÿõ âûïîëíÿåòñÿ CTL-ôîðìóëà ϕ .Ðàáîòà àëãîðèòìà çàêëþ÷àåòñÿ â ïðèïèñûâàíèè êàæäîìóñîñòîÿíèþ s ìíîæåñòâà label(s) òåõ ïîäôîðìóë ôîðìóëû ϕ ,êîòîðûå âûïîëíÿþòñÿ â ñîñòîÿíèè s .Âíà÷àëå label(s) = L(s) .Äàëåå íà êàæäîì øàãå i îáðàáàòûâàþòñÿ ïîäôîðìóëû, âêîòîðûõ ãëóáèíà âëîæåííîñòè CTL-îïåðàòîðîâ ðàâíà i − 1 .Ïîñëå îáðàáîòêè ïîäôîðìóëó äîáàâëÿþò ê ìíîæåñòâó label(s)âñåõ òåõ ñîñòîÿíèé, â êîòîðûõ îíà âûïîëíèìà.Ïî îêîí÷àíèè ðàáîòû àëãîðèòìà ìû îáíàðóæèì, ÷òîSϕ = {s : ϕ ∈ label(s)} .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÄëÿ ôîðìóë âèäà ¬f1 ìû ïîëàãàåì¬f1 ∈ label(s) ⇐⇒ f1 ∈/ label(s).Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÄëÿ ôîðìóë âèäà ¬f1 ìû ïîëàãàåì¬f1 ∈ label(s) ⇐⇒ f1 ∈/ label(s).Äëÿ ôîðìóë âèäà f1 ∨ f2 ìû ïîëàãàåìf1 ∨ f2 ∈ label(s) ⇐⇒ f1 ∈ label(s) èëè f2 ∈ label(s).Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÄëÿ ôîðìóë âèäà ¬f1 ìû ïîëàãàåì¬f1 ∈ label(s) ⇐⇒ f1 ∈/ label(s).Äëÿ ôîðìóë âèäà f1 ∨ f2 ìû ïîëàãàåìf1 ∨ f2 ∈ label(s) ⇐⇒ f1 ∈ label(s) èëè f2 ∈ label(s).Äëÿ ôîðìóë âèäà EX f1 ìû ïîëàãàåìEX f1 ∈ label(s) ⇐⇒ ∃s 0 : f1 ∈ label(s 0 ) è (s, s 0 ) ∈ R.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTL×òîáû ïðîàíàëèçèðîâàòü ôîðìóëó âèäà g = E[f1 U f2 ] , ìûâíà÷àëå âûäåëèì âñå ñîñòîÿíèÿ s 0 , ó êîòîðûõ f2 ∈ label(s 0 ) .Äàëåå áóäåì îòñòóïàòü èç íèõ íàçàä, èñïîëüçóÿ îòíîøåíèå,îáðàòíîå îòíîøåíèþ ïåðåõîäîâ R , äâèãàÿñü òîëüêî ïî òåìñîñòîÿíèÿì s , ó êîòîðûõ f1 ∈ label(s) .Âñå âûäåëåííûå òàêèì îáðàçîì ñîñòîÿíèÿ s 0 è s ïîìåòèìôîðìóëîé g .Äëÿ âûïîëíåíèÿ ýòîé ïðîöåäóðû òðåáóåòñÿ âðåìÿ O(|S| + |R|) .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLprocedure CheckEU(f1 , f2 )T := {s | f2 ∈ label(s)};for all s ∈ T do label(s) := label(s) ∪ {E[f1 U f2 ]};while T 6= ∅ dochoose s ∈ T ;T := T \ {s};for all t such that R(t, s) doif E[f1 U f2 ] ∈/ label(t) and f1 ∈ label(t) thenlabel(t) := label(t) ∪ {E[f1 U f2 ]};T := T ∪ {t};end if;end for all;end whileend procedureÐèñ.: Ïðîöåäóðà ðàçìåòêè ñîñòîÿíèé äëÿ ôîðìóëûE[f1 U f2 ]Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÑëó÷àé g = EG f1 ÷óòü áîëåå èçîùðåí.
×òîáû èññëåäîâàòü åãî,íåîáõîäèìî ðàçáèòü ãðàô íà íåòðèâèàëüíûå ñèëüíî ñâÿçíûåêîìïîíåíòû.Ñèëüíî ñâÿçíîé êîìïîíåíòîé (SCC) C íàçûâàåòñÿ íàèáîëüøèéïîäãðàô, ëþáàÿ âåðøèíà êîòîðîãî äîñòèæèìà èç âñÿêîé äðóãîéâåðøèíû ýòîãî ïîäãðàôà ïî îðèåíòèðîâàííîìó ïóòè, öåëèêîìñîäåðæàùåìóñÿ â C .Êîìïîíåíòà C ñ÷èòàåòñÿ íåòðèâèàëüíîé â òîì è òîëüêî òîìñëó÷àå, êîãäà îíà ñîäåðæèò áîëåå îäíîé âåðøèíû èëè âòî÷íîñòè îäíó âåðøèíó ñ öèêëîì-ïåòëåé, ïðîõîäÿùèì ÷åðåçíåå.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÏóñòü ìîäåëü M 0 ïîëó÷åíà èç M çà ñ÷åò óäàëåíèÿ èç S âñåõòåõ ñîñòîÿíèé, â êîòîðûõ íå âûïîëíÿåòñÿ f1 , èñîîòâåòñòâóþùåãî ñóæåíèÿ R è L .Òàêèì îáðàçîì, ìû ïîëó÷àåì ìîäåëü M 0 = (S 0 , R 0 , L0 ) , âêîòîðîé S 0 = {s ∈ S | M, s |= f1 } , R 0 = R|S 0 ×S 0 è L0 = L|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 ) .Òàáëè÷íûé àëãîðèòì 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 âûïîëíÿåòñÿ â êàæäîì ñîñòîÿíèè íà ïðîòÿæåíèè π .Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLËåììà 1. M, s |= EG f1 òîãäà è òîëüêî òîãäà, êîãäàñîáëþäåíû ñëåäóþùèå äâà óñëîâèÿ:Iñîñòîÿíèå s ñîäåðæèòñÿ â ìíîæåñòâå S 0 ;Iâ M 0 åñòü ïóòü, âåäóùèé èç s â íåêîòîðóþ âåðøèíó t ,ñîäåðæàùóþñÿ â íåòðèâèàëüíîé ñèëüíî ñâÿçíîéêîìïîíåíòå C ãðàôà (S 0 , R 0 ) .Äîêàçàòåëüñòâî.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
