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

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

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

 òàêîì ñëó÷àå ðàçëîæåíèå Øåííîíàóïðîùàåòñÿ è ïðèíèìàåò âèäf ∗ f 0 = (¬x ∧ (f |x←0 ∗ f 0 )) ∨ (x ∧ (f |x←1 ∗ f 0 )),à ROBDD äëÿ f ∗ f 0 âû÷èñëÿåòñÿ ðåêóðñèâíî, êàê è âïðåäûäóùåì ñëó÷àå.Ïîñòðîåíèå ðàçðåøàþùèõ äèàãðàììIÅñëè x < x 0 , òî f 0 |x←0 = f 0 |x←1 = f 0 , ïîñêîëüêó f 0 íåçàâèñèò îò x .  òàêîì ñëó÷àå ðàçëîæåíèå Øåííîíàóïðîùàåòñÿ è ïðèíèìàåò âèäf ∗ f 0 = (¬x ∧ (f |x←0 ∗ f 0 )) ∨ (x ∧ (f |x←1 ∗ f 0 )),à ROBDD äëÿ f ∗ f 0 âû÷èñëÿåòñÿ ðåêóðñèâíî, êàê è âïðåäûäóùåì ñëó÷àå.IÅñëè x 0 < x , òî ñõåìà âû÷èñëåíèé áóäåò àíàëîãè÷íàïðåäûäóùåìó ñëó÷àþ.Ïîñòðîåíèå ðàçðåøàþùèõ äèàãðàìì×òîáû ïðåäîòâðàòèòü ýêñïîíåíöèàëüíîå ðàçðàñòàíèåâû÷èñëåíèé, ïðèìåíÿåòñÿ ìåòîä äèíàìè÷åñêîãîïðîãðàììèðîâàíèÿ.Êàæäàÿ ïîäçàäà÷à ñîîòâåòñòâóåò ïàðå ROBDD, ÿâëÿþùèõñÿïîäãðàôàìè èñõîäíûõ ROBDD äëÿ f è f 0 . Òàêèì îáðàçîì,êîëè÷åñòâî ïîäçàäà÷ îãðàíè÷åíî ïðîèçâåäåíèåì ðàçìåðîâOBDD äëÿ f è f 0 .Õýø-òàáëèöà ïîä íàçâàíèåì êýø ðåçóëüòàòîâ èñïîëüçóåòñÿ äëÿõðàíåíèÿ â ïàìÿòè ðàíåå âû÷èñëåííûõ ïîäçàäà÷.Ïåðåä ðåêóðñèâíûì îáðàùåíèåì, ìû ïðîñìàòðèâàåì ýòîò êýøè ïðîâåðÿåì, áûëà ëè óæå ðåøåíà ïðåäúÿâëåííàÿ ïîäçàäà÷à.Åñëè ýòî òàê, òî ðåçóëüòàò âûáèðàåòñÿ èç êýøà; èíà÷åâûïîëíÿåòñÿ ðåêóðñèâíîå îáðàùåíèå, è ïîñòðîåííàÿ ROBDDïîìåùàåòñÿ â êýø ðåçóëüòàòîâ.Ïîñòðîåíèå ðàçðåøàþùèõ äèàãðàììÁóëåâî îòðèöàíèå ìîæíî ðåàëèçîâàòü, ïðèìåíÿÿ Apply.

Íîïðîùå âû÷èñëèòü ROBDD äëÿ ¬f , ïîìåíÿâ ìåñòàìè çíà÷åíèÿâ òåðìèíàëüíûõ âåðøèíàõ OBDD äëÿ f .Ïîñòðîåíèå ðàçðåøàþùèõ äèàãðàììÁóëåâî îòðèöàíèå ìîæíî ðåàëèçîâàòü, ïðèìåíÿÿ Apply. Íîïðîùå âû÷èñëèòü ROBDD äëÿ ¬f , ïîìåíÿâ ìåñòàìè çíà÷åíèÿâ òåðìèíàëüíûõ âåðøèíàõ OBDD äëÿ f .Áûë ðàçðàáîòàí ðÿä îáîáùåíèé ýòîãî ìåòîäà äëÿïðåäñòàâëåíèÿ ñåìåéñòâà áóëåâûõ ôóíêöèé, èìåþùèõ îáùèåïîäãðàôû.Äëÿ âñåõ ôóíêöèé ýòîãî ñåìåéñòâà äåéñòâóåò îäèí è òîò æåïîðÿäîê ðàñïîëîæåíèÿ ïåðåìåííûõ.Åñëè èñïîëüçóåòñÿ ïîäîáíîå îáîáùåíèå, òî äâå ôóíêöèèñåìåéñòâà áóäóò ðàâíû â òîì è òîëüêî òîì ñëó÷àå, êîãäà îíèèìåþò îäèí è òîò æå êîðåíü.Ñëåäîâàòåëüíî, âðåìÿ, òðåáóåìîå äëÿ ïðîâåðêè ðàâåíñòâà äâóõôóíêöèé, îãðàíè÷åíî ïîñòîÿííîé âåëè÷èíîé.Ñîâðåìåííûå ïàêåòû OBDD ìîãóò ýôôåêòèâíî ðàáîòàòü ñãðàôàìè, èìåþùèìè ìèëëèîíû âåðøèí.ROBDD ïðåäñòàâëåíèå ìîäåëåé ÊðèïêåOBDD óäîáíû äëÿ ïîëó÷åíèÿ êîìïàêòíûõ ïðåäñòàâëåíèéîòíîøåíèé íà êîíå÷íûõ îáëàñòÿõ.Âñÿêîå n -ìåñòíîå îòíîøåíèå Q íà ìíîæåñòâå {0, 1} ìîæíîïðåäñòàâèòü â âèäå OBDD äëÿ åãî õàðàêòåðèñòè÷åñêîéôóíêöèè :fQ (x1 , .

. . , xn ) = 1 ⇐⇒ Q(x1 , . . . , xn ) = true.ROBDD ïðåäñòàâëåíèå ìîäåëåé Êðèïêå×òîáû ïîñòðîèòü ROBDD ïðåäñòàâëåíèå n -ìåñòíîãîîòíîøåíèÿ Q íà êîíå÷íîé îáëàñòè D , ñîäåðæàùåé íå áîëåå 2mýëåìåíòîâ, íóæíî çàêîäèðîâàòü âñå ýëåìåíòû ìíîæåñòâà Däâîè÷íûìè âåêòîðàìè, âîñïîëüçîâàâøèñü êàêîé-íèáóäüáèåêöèåé φ : {0, 1}m → D .b ìåñòíîñòè m × n ïîÄàëåå îïðåäåëÿåòñÿ áóëåâî îòíîøåíèå Qñëåäóþùåìó ïðàâèëó:b 1 , .

. . , x n ) = Q(φ(x 1 ), . . . , φ(x n )),Q(xãäå x i âåêòîð, ñîñòîÿùèé èç m áóëåâûõ ïåðåìåííûõ, ïðèïîìîùè êîòîðîãî çàêîäèðîâàíà ïåðåìåííàÿ xi , ïðèíèìàþùàÿçíà÷åíèÿ èç D .Òåïåðü îòíîøåíèå Q ìîæíî ïðåäñòàâèòü â âèäå ROBDD äëÿb.õàðàêòåðèñòè÷åñêîé ôóíêöèè fQb îòíîøåíèÿ QROBDD ïðåäñòàâëåíèå ìîäåëåé Êðèïêå×òîáû îòûñêàòü ROBDD ïðåäñòàâëåíèå ìîäåëè ÊðèïêåM = (S, R, L) , íóæíî îïèñàòü ìíîæåñòâî S , îòíîøåíèå R èîòîáðàæåíèå L .Çàêîäèðóåì ñîñòîÿíèÿ ìíîæåñòâà S áóëåâûìè âåêòîðàìèäëèíû m .Èñïîëüçóåì ôóíêöèþ φ : {0, 1}m → S äëÿ îòîáðàæåíèÿáóëåâûõ âåêòîðîâ â ìíîæåñòâî ñîñòîÿíèé S .ROBDD ïðåäñòàâëåíèå ìîäåëåé Êðèïêå×òîáû îòûñêàòü ROBDD ïðåäñòàâëåíèå ìîäåëè ÊðèïêåM = (S, R, L) , íóæíî îïèñàòü ìíîæåñòâî S , îòíîøåíèå R èîòîáðàæåíèå L .Çàêîäèðóåì ñîñòîÿíèÿ ìíîæåñòâà S áóëåâûìè âåêòîðàìèäëèíû m .Èñïîëüçóåì ôóíêöèþ φ : {0, 1}m → S äëÿ îòîáðàæåíèÿáóëåâûõ âåêòîðîâ â ìíîæåñòâî ñîñòîÿíèé S .Äëÿ ïðåäñòàâëåíèÿ îòíîøåíèÿ ïåðåõîäîâ ïîòðåáóþòñÿ äâàêîìïëåêòà áóëåâûõ ïåðåìåííûõ: îäíî äëÿ ïðåäñòàâëåíèÿñîñòîÿíèÿ, êîòîðûì íà÷èíàåòñÿ ïåðåõîä, à äðóãîå äëÿïðåäñòàâëåíèÿ ñîñòîÿíèÿ, â êîòîðîì ïåðåõîä îêàí÷èâàåòñÿ.Åñëè îòíîøåíèå ïåðåõîäîâ R çàêîäèðîâàíî áóëåâîé ôóíêöèåéb x 0 ) , òî îòíîøåíèå R çàäàåòñÿ OBDD äëÿR(x,õàðàêòåðèñòè÷åñêîé ôóíêöèè fRb .Ïðåäñòàâëåíèå ìîäåëåé ÊðèïêåÔóíêöèþ ðàçìåòêè L ìîæíî ðàññìàòðèâàòü êàê îòîáðàæåíèåèç ìíîæåñòâà àòîìàðíûõ âûñêàçûâàíèé â ìíîæåñòâî âñåõïîäìíîæåñòâ ïðîñòðàíñòâà ñîñòîÿíèé S : êàæäîå àòîìàðíîåâûñêàçûâàíèå p îòîáðàæàåòñÿ â ìíîæåñòâî Lp = {s | p ∈ L(s)}òåõ ñîñòîÿíèé, â êîòîðûõ îíî âûïîëíÿåòñÿ.Ìíîæåñòâà Lp ìîæíî ïðåäñòàâèòü â âèäå OBDD ïðè ïîìîùèêîäèðîâàíèÿ φ .Ïðåäñòàâëåíèå ìîäåëåé ÊðèïêåÐàññìîòðèì ìîäåëü ñ äâóìÿ ñîñòîÿíèÿìè'$$'$ab&%s I?'$R%a ¬b&%1s2Ïåðåõîä èç ñîñòîÿíèÿ s1 â ñîñòîÿíèå s2 áóäåì ïðåäñòàâëÿòüêîíúþíêöèåé(a ∧ b ∧ a0 ∧ ¬b 0 ).Áóëåâà ôîðìóëà äëÿ âñåãî îòíîøåíèÿ ïåðåõîäîâ èìååò âèä(a ∧ b ∧ a0 ∧ ¬b 0 ) ∨ (a ∧ ¬b ∧ a0 ∧ ¬b 0 ) ∨ (a ∧ ¬b ∧ a0 ∧ b 0 ).Ýòà ôîðìóëà ñîäåðæèò òðè äèçúþíêòèâíûõ ñëàãàåìûõ,ïîñêîëüêó ìîäåëü Êðèïêå ñîäåðæèò òðè ïåðåõîäà.

Äàëåå ýòàôîðìóëà ïðåîáðàçóåòñÿ â OBDD äëÿ íàèáîëåå êîìïàêòíîãîïðåäñòàâëåíèÿ îòíîøåíèÿ ïåðåõîäîâ.ÓïðàæíåíèÿÐàññìîòðèòå âñå âîçìîæíûå óïîðÿäî÷åíèÿ ïåðåìåííûõ x, y , z èäëÿ êàæäîãî èç íèõ ïîñòðîéòå óïîðÿäî÷åííûå äâîè÷íûåðàçðåøàþùèå äèàãðàììû, ÿâëÿþùèåñÿ êàíîíè÷åñêèìèïðåäñòàâëåíèÿìè ôóíêöèé f (x, y , z) è g (x, y , z) , êîòîðûåçàäàíû ñëåäóþùèìè òàáëèöàìè.xyzf (x, y , z)g (x, y , z)1111000011001100101010100101000111101000ÓïðàæíåíèÿÂûáåðèòå íàèëó÷øåå óïîðÿäî÷åíèå ïåðåìåííûõ x, y , z èïîñòðîéòå OBDD, ÿâëÿþùèåñÿ ïðåäñòàâëåíèåì ñëåäóþùèõôóíêöèéIF1 (x, y , z) = ¬f (x, y , z) ;IF2 (x, y , z) = f (x, y , z) ∧ g (x, y , z) ;IF3 (x, y , z) = f (x, y , z) ∨ g (x, y , z) ;IF4 (x, y , z) = F2 (x, y , z) ⊕ F3 (x, y , z) .Ïðîâåðüòå, ÿâëÿåòñÿ ëè âûáðàííûé Âàìè ïîðÿäîêðàñïîëîæåíèÿ ïåðåìåííûõ îïòèìàëüíûì äëÿ ïðåäñòàâëåíèÿïåðå÷èñëåííûõ ôóíêöèé â âèäå OBDD.ÓïðàæíåíèÿÍàïèøèòå ïðîãðàììû, ðåàëèçóþùèåàëãîðèòìûReduce è Apply.ÊÎÍÅÖ ËÅÊÖÈÈ 5..

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

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