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

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

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

î÷åíü ïðîñòîé: âñå ñâîäèòñÿ ê ðåøåíèþ õîðîøî èçâåñòíûõçàäà÷ òåîðèè ãðàôîâ (ïðîáëåìû äîñòèæèìîñòè âåðøèí,âûäåëåíèÿ ñèëüíî ñâÿçíûõ êîìïîíåíò);2. î÷åíü áûñòðûé: âðåìÿ âû÷èñëåíèÿ ïðîïîðöèîíàëüíîðàçìåðó âõîäíûõ äàííûõ.Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÄîñòîèíñòâà ïðåäëîæåííîãî àëãîðèòìà:1. î÷åíü ïðîñòîé: âñå ñâîäèòñÿ ê ðåøåíèþ õîðîøî èçâåñòíûõçàäà÷ òåîðèè ãðàôîâ (ïðîáëåìû äîñòèæèìîñòè âåðøèí,âûäåëåíèÿ ñèëüíî ñâÿçíûõ êîìïîíåíò);2. î÷åíü áûñòðûé: âðåìÿ âû÷èñëåíèÿ ïðîïîðöèîíàëüíîðàçìåðó âõîäíûõ äàííûõ.Íåäîñòàòêè ïðåäëîæåííîãî àëãîðèòìà:1.

î÷åíü ìåäëåííûé: âðåìÿ âû÷èñëåíèÿ ïðîïîðöèîíàëüíî÷èñëó ñîñòîÿíèé â ìîäåëè;2. î÷åíü çàòðàòíûé ïî îáúåìó ïàìÿòè: íåîáõîäèìî õðàíèòüñïèñîê âñåõ ñîñòîÿíèé ìîäåëè.Åñëè ñèñòåìà ñîñòîèò èç 16 ïðîöåññîâ, â êîòîðûõ èñïîëüçóþòñÿ16 áóëåâûõ ïåðåìåííûõ, òî ÷èñëî ñîñòîÿíèé ìîäåëè2256Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÊàê æå ðàáîòàòü ñ òàêèìè ìîäåëÿìè?Òàáëè÷íûé àëãîðèòì model checking äëÿ CTLÊàê æå ðàáîòàòü ñ òàêèìè ìîäåëÿìè?Íóæíî ïðîâîäèòü âû÷èñëåíèÿ íå ñ îòäåëüíûìè ñîñòîÿíèÿìèìîäåëè, à ñ öåëûìè ìíîæåñòâàìè ñîñòîÿíèé îäíîâðåìåííî!Åñëè ó íàñ åñòü äâà ìíîæåñòâà A è B , òî âðåìÿ âû÷èñëåíèÿîïåðàöèÿ A ∪ B ïðîïîðöèîíàëüíî ðàçìåðó ýòèõ ìíîæåñòâ, åñëèìíîæåñòâà ïðåäñòàâëåíû â âèäå ñïèñêîâ, ìàññèâîâ è ïð.Íî åñëè ìíîæåñòâà X ïðåäñòàâëåíû êîðîòêèìè îïèñàíèÿìèdescription(X ) , òî âðåìÿ âû÷èñëåíèÿ A ∪ B ìîæåò îêàçàòüñÿïðîïîðöèîíàëüíûì ðàçìåðó îïèñàíèé ýòèõ ìíîæåñòâ, à íåðàçìåðó ñàìèõ ìíîæåñòâ.Ýòà èäåÿ îòêðûâàåò íîâûé âèä àëãîðèòìîâ ðåøåíèÿ äèñðåòíûõçàäà÷ áîëüøîé ðàçìåðíîñòè ñèìâîëüíûå àëãîðèòìû .Íî äëÿ ýòîãî íàì ïîíàäîáÿòñÿ ñðåäñòâà ñèìâîëüíîãî îïèñàíèÿìíîæåñòâ äâîè÷íûõ âåêòîðîâ.Äâîè÷íûå ðàçðåøàþùèå äèàãðàììûÎäíà èç íàèáîëåå óäîáíûõ ìàòåìàòè÷åñêèõ ñòðóêòóð äëÿïðåäñòàâëåíèÿ ðàçìå÷åííûõ ñèñòåì ïåðåõîäîâ ñ êîíå÷íûì÷èñëîì ñîñòîÿíèé ýòî äâîè÷íûå ðàçðåøàþùèåäèàãðàììû (Binary Decision Diagrams, BDDs).1) Âíà÷àëå îáñóäèì, êàê èñïîëüçîâàòü äâîè÷íûå ðàçðåøàþùèåäèàãðàììû äëÿ ïðåäñòàâëåíèÿ áóëåâûõ ôóíêöèé.2) Äàëåå ïîêàæåì, êàê ýôôåêòèâíî âûïîëíÿòü ðàçëè÷íûåëîãè÷åñêèå îïåðàöèè, èñïîëüçóÿ BDDs.3)  çàêëþ÷åíèå ïîÿñíèì, êàê ïðè ïîìîùè BDDs êîìïàêòíîïðåäñòàâëÿòü ìîäåëè Êðèïêå.Îñíîâíûå îïðåäåëåíèÿÓïîðÿäî÷åííûå äâîè÷íûå ðàçðåøàþùèå äèàãðàììû (èëè,ñîêðàùåííî, OBDD ordered binary decision diagrams) ýòîêàíîíè÷åñêàÿ ôîðìà ïðåäñòàâëåíèÿ áóëåâûõ ôóíêöèé.Îíè çíà÷èòåëüíî áîëåå êîìïàêòíû, íåæåëè òðàäèöèîííûåíîðìàëüíûå ôîðìû, òàêèå êàê ÄÍÔ èëè ÊÍÔ.Êðîìå òîãî, ñ íèìè ìîæíî ðàáîòàòü î÷åíü ýôôåêòèâíî.Ïîýòîìó OBDDs íàøëè øèðîêîå ïðèìåíåíèå âî ìíîãèõïðèëîæåíèÿõ, îòíîñÿùèõñÿ ê àâòîìàòè÷åñêîìóïðîåêòèðîâàíèþ, ñèìâîëüíîìó èìèòàöèîííîìó ìîäåëèðîâàíèþ,âåðèôèêàöèè êîìáèíàöèîííûõ ëîãè÷åñêèõ ñõåì.Îñíîâíûå îïðåäåëåíèÿÂíà÷àëå ðàññìîòðèì äâîè÷íûå ðàçðåøàþùèå äåðåâüÿ .Äâîè÷íîå ðàçðåøàþùåå äåðåâî ýòî êîðíåâîåîðèåíòèðîâàííîå äåðåâî, âåðøèíû êîòîðîãî ðàçáèòû íà äâàêëàññà òåðìèíàëüíûå âåðøèíû è íåòåðìèíàëüíûå âåðøèíû .Êàæäàÿ íåòåðìèíàëüíàÿ âåðøèíà v ïîìå÷åíà ïåðåìåííîévar (v ) è èìååò äâå âåðøèíûïîñëåäîâàòåëÿ: low (v ) , êîòîðàÿñîîòâåòñòâóåò ñëó÷àþ, êîãäà ïåðåìåííàÿ var (v ) ðàâíà 0 , èhigh(v ) , êîòîðàÿ ñîîòâåòñòâóåò ñëó÷àþ, êîãäà ïåðåìåííàÿvar (v ) ðàâíà 1 .Êàæäàÿ èç òåðìèíàëüíûõ âåðøèí v èìååò ïîìåòêó value(v ) ,ðàâíóþ 0 èëè 1 .Îñíîâíûå îïðåäåëåíèÿÂíà÷àëå ðàññìîòðèì äâîè÷íûå ðàçðåøàþùèå äåðåâüÿ .Äâîè÷íîå ðàçðåøàþùåå äåðåâî ýòî êîðíåâîåîðèåíòèðîâàííîå äåðåâî, âåðøèíû êîòîðîãî ðàçáèòû íà äâàêëàññà òåðìèíàëüíûå âåðøèíû è íåòåðìèíàëüíûå âåðøèíû .Êàæäàÿ íåòåðìèíàëüíàÿ âåðøèíà v ïîìå÷åíà ïåðåìåííîévar (v ) è èìååò äâå âåðøèíûïîñëåäîâàòåëÿ: low (v ) , êîòîðàÿñîîòâåòñòâóåò ñëó÷àþ, êîãäà ïåðåìåííàÿ var (v ) ðàâíà 0 , èhigh(v ) , êîòîðàÿ ñîîòâåòñòâóåò ñëó÷àþ, êîãäà ïåðåìåííàÿvar (v ) ðàâíà 1 .Êàæäàÿ èç òåðìèíàëüíûõ âåðøèí v èìååò ïîìåòêó value(v ) ,ðàâíóþ 0 èëè 1 .Ðàññìîòðèì äâîè÷íîå ðàçðåøàþùåå äåðåâî äëÿ äâóõáèòîâîãîêîìïàðàòîðà, êîòîðûé îïèñûâàåòñÿ ôîðìóëîéf (a1 , a2 , b1 , b2 ) = (a1 ↔ b1 ) ∧ (a2 ↔ b2 ) .a1HH0H 1HHHb1b1@0@1@@@0@1@@a2a2a2a2 B B B B0B10B10B10B1BBBBBBBBb2b2b2b2b2b2b2b2CCCCCCCC0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 C C C C C C C C CCC CC CC C100100000000 1001Îñíîâíûå îïðåäåëåíèÿ×òîáû âûÿñíèòü, êàêîå çíà÷åíèå ïðèíèìàåò ôîðìóëà ïðèçàäàííîì íàáîðå çíà÷åíèé ïåðåìåííûõ, íóæíî ñïóñòèòñÿ ïîäåðåâó èç êîðíÿ äî òåðìèíàëüíîé âåðøèíû.Åñëè ïåðåìåííàÿ var (v ) èìååò çíà÷åíèå 0 , òî ñëåäóþùåéâåðøèíîé íà ïóòè èç êîðíÿ â òåðìèíàëüíóþ âåðøèíó áóäåòlow (x) .Åñëè æå var (v ) èìååò çíà÷åíèå 1 , òî ïîñëåäóþùåé âåðøèíîéíà ïóòè áóäåò high(x) .Òî çíà÷åíèå, êîòîðûì ïîìå÷åíà äîñòèãíóòàÿ òåðìèíàëüíàÿâåðøèíà, è áóäåò çíà÷åíèåì ôóíêöèè íà ýòîì íàáîðå.Îñíîâíûå îïðåäåëåíèÿ×òîáû âûÿñíèòü, êàêîå çíà÷åíèå ïðèíèìàåò ôîðìóëà ïðèçàäàííîì íàáîðå çíà÷åíèé ïåðåìåííûõ, íóæíî ñïóñòèòñÿ ïîäåðåâó èç êîðíÿ äî òåðìèíàëüíîé âåðøèíû.Åñëè ïåðåìåííàÿ var (v ) èìååò çíà÷åíèå 0 , òî ñëåäóþùåéâåðøèíîé íà ïóòè èç êîðíÿ â òåðìèíàëüíóþ âåðøèíó áóäåòlow (x) .Åñëè æå var (v ) èìååò çíà÷åíèå 1 , òî ïîñëåäóþùåé âåðøèíîéíà ïóòè áóäåò high(x) .Òî çíà÷åíèå, êîòîðûì ïîìå÷åíà äîñòèãíóòàÿ òåðìèíàëüíàÿâåðøèíà, è áóäåò çíà÷åíèåì ôóíêöèè íà ýòîì íàáîðå.Íàïðèìåð, îöåíêà ha1 := 1, a2 := 0, b1 := 1, b2 := 1i ïðèâîäèò êâèñÿ÷åé âåðøèíå, ïîìå÷åííîé 0 ; ñëåäîâàòåëüíî, ïðè òàêîìîçíà÷èâàíèè ôîðìóëà ëîæíà.ha1 := 1, a2 := 0, b1 := 1, b2 := 1ia1HH0H 1HHHb1b1@0@1@@@0@1@@a2a2a2a2 B B B B0B10B10B10B1BBBBBBBBb2b2b2b2b2b2b2b2CCCCCCCC0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 C C C C C C C C CCC CC CC C100100000000 1001Îñíîâíûå îïðåäåëåíèÿÄâîè÷íûå ðàçðåøàþùèå äåðåâüÿ íå äàþò î÷åíü êîìïàêòíîãîïðåäñòàâëåíèÿ áóëåâûõ ôóíêöèé.

Ïî ñóòè äåëà, îíè èìåþòòî÷íî òàêîé æå ðàçìåð, êàê è òàáëèöà èñòèííîñòè.Îäíàêî òàêèå äåðåâüÿ îáû÷íî áûâàþò ÷ðåçâû÷àéíîèçáûòî÷íûìè. Íàïðèìåð, äåðåâî äâóõáèòîâîãî êîìïàðàòîðàñîäåðæèò âîñåìü ïîääåðåâüåâ, êîðíè êîòîðûõ ïîìå÷åíû b2 , íîòîëüêî òðè èç íèõ ïîïàðíî ðàçëè÷íû.Çà ñ÷åò ýòîãî ìû ìîæåì äîáèòüñÿ áîëåå êîìïàêòíîãîïðåäñòàâëåíèÿ äëÿ áóëåâûõ ôóíêöèé, êàê òîëüêî ñêëåèì âñåèçîìîðôíûå ïîääåðåâüÿ. ðåçóëüòàòå ïîëó÷èòñÿ îðèåíòèðîâàííûé àöèêëè÷åñêèé ãðàô,êîòîðûé è íàçûâàåòñÿ äâîè÷íîé ðàçðåøàþùåé äèàãðàììîé .a1HH0H 1HHHb1b1@0@1@@@0@1@@a2a2a2a2 B B B B0B10B10B10B1BBBBBBBBb2b2b2b2b2b2b2b2CCCCCCCC0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 C C C C C C C C CCC CC CC C100100000000 1001a1HH0H 1HHHb1b1@0@1@@@0@1@@a2a2a2a2 B B B B0B10B10B10B1BBBBBBBBb2b2b2b2b2b2b2b2CCCCCCCC0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 C C C C C C C C CCC CC CC C100100000000 1001a1HH0H 1HHHb1b1@0@1@@@0@1@@a2a2a2a2 B B B B0B10B10B10B1BBBBBBBBb2b2b2b2b2b2b2b2CCCCCCCC0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 0 C1 C C C C C C C C CCC CC CC C100100000000 1001Îñíîâíûå îïðåäåëåíèÿÄâîè÷íàÿ ðàçðåøàþùàÿ äèàãðàììà ýòî êîðíåâîéîðèåíòèðîâàííûé àöèêëè÷åñêèé ãðàô, âåðøèíû êîòîðîãîðàçáèòû íà äâà êëàññà òåðìèíàëüíûå âåðøèíû èíåòåðìèíàëüíûå âåðøèíû.Êàê è â ñëó÷àå äâîè÷íûõ ðàçðåøàþùèõ äåðåâüåâ, êàæäàÿíåòåðìèíàëüíàÿ âåðøèíà v ïîìå÷åíà ïåðåìåííîé var (v ) èèìååò äâå âåðøèíûïîñëåäîâàòåëÿ: low (v ) è high(v ) .

Êàæäàÿòåðìèíàëüíàÿ âåðøèíà ïîìå÷åíà ëèáî 0 , ëèáî 1 .Îñíîâíûå îïðåäåëåíèÿÂñÿêàÿ äâîè÷íàÿ ðàçðåøàþùàÿ äèàãðàììà B ñ êîðíåì ââåðøèíå v îïðåäåëÿåò áóëåâó ôóíêöèþ fv (x1 , . . . , xn )ñëåäóþùåãî âèäà:1.  ñëó÷àå, êîãäà v òåðìèíàëüíàÿ âåðøèíà, ìû ñ÷èòàåì,÷òîa). åñëèb). åñëèvalue(v ) = 1 , òî fv (x1 , . .

. , xn ) = 1 ,value(v ) = 0 , òî fv (x1 , . . . , xn ) = 0 .2.  ñëó÷àå, êîãäà v íåòåðìèíàëüíàÿ âåðøèíà èvar (v ) = xi ìû èìååìfv (x1 , . . . , xn ) = (¬xi ∧flow (v ) (x1 , . . . , xn ))∨(xi ∧fhigh(v ) (x1 , . . . , xn )).Îñíîâíûå îïðåäåëåíèÿa1v1@10@v2b1b1v30110v4v5v7a2@@01@@b2b2 v106@@01 1@ 0@v8Îñíîâíûå îïðåäåëåíèÿa1v1@10@v2b1b1v30110v4v5v7a2@@01@@b2b2 v106@@01 1@ 0@v8fv7 = 1 fv8 = 0Îñíîâíûå îïðåäåëåíèÿa1v1@10@v2b1b1v30110v4v5v7a2@@01@@b2b2 v106@@01 1@ 0@v8fv5 = ¬b2fv5 = b2fv7 = 1 fv8 = 0Îñíîâíûå îïðåäåëåíèÿa1v1@10@v2b1b1v30110v4v5v7fv4 = (¬a2 ∧ ¬b2 ) ∨ (a2 ∧ b2 )a2@@01@@b2b2 v106@@01 1@ 0@v8fv5 = ¬b2fv5 = b2fv7 = 1 fv8 = 0Îñíîâíûå îïðåäåëåíèÿa1v1@10@v2b1b1v30110v4v5v7a2@@01@@b2b2 v106@@01 1@ 0@v8fv4 = (¬a2 ∧ ¬b2 ) ∨ (a2 ∧ b2 )= (a2 ↔ b2 )fv5 = ¬b2fv5 = b2fv7 = 1 fv8 = 0Îñíîâíûå îïðåäåëåíèÿa1v1@10@v2b1b1v30110v4v5v7a2@@01@@b2b2 v106@@01 1@ 0@v8fv2 = ¬b1 ∧ (a2 ↔ b2 )fv3 = b1 ∧ (a2 ↔ b2 )fv4 = (¬a2 ∧ ¬b2 ) ∨ (a2 ∧ b2 )= (a2 ↔ b2 )fv5 = ¬b2fv5 = b2fv7 = 1 fv8 = 0Îñíîâíûå îïðåäåëåíèÿa1fv1 = (¬a1 ∧ fv2 ) ∨ (a1 ∧ fv3 )v1@1@0v2b1b1v30110v4v5v7a2@@01@@b2b2 v106@@01 1@ 0@v8fv2 = ¬b1 ∧ (a2 ↔ b2 )fv3 = b1 ∧ (a2 ↔ b2 )fv4 = (¬a2 ∧ ¬b2 ) ∨ (a2 ∧ b2 )= (a2 ↔ b2 )fv5 = ¬b2fv5 = b2fv7 = 1 fv8 = 0Îñíîâíûå îïðåäåëåíèÿa1v1@1@0v2b1b1v30110v4v5v7a2@@01@@b2b2 v106@@01 1@ 0@v8fv1 = (¬a1 ∧ fv2 ) ∨ (a1 ∧ fv3 )= (a1 ↔ b1 ) ∧ (a2 ↔ b2 )fv2 = ¬b1 ∧ (a2 ↔ b2 )fv3 = b1 ∧ (a2 ↔ b2 )fv4 = (¬a2 ∧ ¬b2 ) ∨ (a2 ∧ b2 )= (a2 ↔ b2 )fv5 = ¬b2fv5 = b2fv7 = 1 fv8 = 0Îñíîâíûå îïðåäåëåíèÿÂî ìíîãèõ ïðèëîæåíèÿõ âàæíî èìåòü êàíîíè÷åñêîåïðåäñòàâëåíèå áóëåâûõ ôóíêöèé, êîòîðîå îáëàäàåò òåìñâîéñòâîì, ÷òî äâå áóëåâû ôóíêöèè ëîãè÷åñêè ýêâèâàëåíòíûòîãäà è òîëüêî òîãäà, êîãäà îíè èìåþò èçîìîðôíûåïðåäñòàâëåíèÿ.

Ýòî ñâîéñòâî óïðîùàåò ðåøåíèå çàäà÷èñðàâíåíèÿ äâóõ áóëåâûõ ôóíêöèé â èòåðàòèâíûõ àëãîðèòìàõ.Îñíîâíûå îïðåäåëåíèÿÂî ìíîãèõ ïðèëîæåíèÿõ âàæíî èìåòü êàíîíè÷åñêîåïðåäñòàâëåíèå áóëåâûõ ôóíêöèé, êîòîðîå îáëàäàåò òåìñâîéñòâîì, ÷òî äâå áóëåâû ôóíêöèè ëîãè÷åñêè ýêâèâàëåíòíûòîãäà è òîëüêî òîãäà, êîãäà îíè èìåþò èçîìîðôíûåïðåäñòàâëåíèÿ. Ýòî ñâîéñòâî óïðîùàåò ðåøåíèå çàäà÷èñðàâíåíèÿ äâóõ áóëåâûõ ôóíêöèé â èòåðàòèâíûõ àëãîðèòìàõ.Äâå BDDs ñ÷èòàþòñÿ èçîìîðôíûìè , åñëè ñóùåñòâóåò òàêîåâçèìíî îäíîçíà÷íîå îòîáðàæåíèå h , êîòîðîå ñîïîñòàâëÿåòòåðìèíàëüíûå âåðøèíû îäíîé èç íèõ òåðìèíàëüíûì âåðøèíàìäðóãîé, à òàêæå íåòåðìèíàëüíûå âåðøèíû îäíîé íåòåðìèíàëüíûì âåðøèíàì äðóãîé, òàê ÷òî äëÿ êàæäîéòåðìèíàëüíîé âåðøèíû v ñïðàâåäëèâî ðàâåíñòâîvalue(v ) = value(h(v )) , à äëÿ êàæäîé íåòåðìèíàëüíîé âåðøèíûv âûïîëíÿþòñÿ ñîîòíîøåíèÿ var (v ) = var (h(v )) ,h(low (v )) = low (h(v )) è h(high(v )) = high(h(v )) .Ïîñòðîåíèå ðàçðåøàþùèõ äèàãðàììÁðèàí ïîêàçàë, êàê ïîñòðîèòü êàíîíè÷åñêèå ïðåäñòàâëåíèÿáóëåâûõ ôóíêöèé, íàëàãàÿ äâà îãðàíè÷åíèÿ íà ñòðóêòóðóäâîè÷íûõ ðàçðåøàþùèõ äèàãðàìì.R.

Bryant. Graph-based algorithms for boolean functionmanipulation. IEEE Transactions on Computers, 35(8):677691,1986.Ïîñòðîåíèå ðàçðåøàþùèõ äèàãðàììÁðèàí ïîêàçàë, êàê ïîñòðîèòü êàíîíè÷åñêèå ïðåäñòàâëåíèÿáóëåâûõ ôóíêöèé, íàëàãàÿ äâà îãðàíè÷åíèÿ íà ñòðóêòóðóäâîè÷íûõ ðàçðåøàþùèõ äèàãðàìì.R. Bryant.

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

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