Лекция 11. Bounded Model Checking. Выполнимость булевых формул SAT (1185511)
Текст из файла
Âåðèôèêàöèÿìîäåëåé ïðîãðàììËÅÊÒÎÐ:Âëàäèìèð Àíàòîëüåâè÷ ÇàõàðîâÂëàäèñëàâ Âàñèëüåâè÷ Ïîäûìîâzakh@cs.msu.suËåêöèÿ 11.Îãðàíè÷åííàÿ âåðèôèêàöèÿìîäåëåé ïðîãðàìì(Bounded model checking)1.2.3.4.Ðàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèèìîäåëåé ïðîãðàììÇàäà÷à ïðîâåðêè âûïîëíèìîñòèáóëåâûõ ôîðìóë (SAT) è ñïîñîáû ååðåøåíèÿÇàäà÷à îãðàíè÷åííîé âåðèôèêàöèèìîäåëåé ïðîãðàìì (BMC)Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÐàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèè ìîäåëåéïðîãðàììÍåîñïîðèìûé òåçèñ îñíîâå êàæäîãî ñïîñîáà ðåøåíèÿ çàäà÷è âåðèôèêàöèèìîäåëåé ïðîãðàìì ëåæèò íåêîòîðàÿ çàäà÷à äèñêðåòíîéìàòåìàòèêè è ìåòîäû åå ðåøåíèÿ.Ðàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèè ìîäåëåéïðîãðàììÍåîñïîðèìûé òåçèñ îñíîâå êàæäîãî ñïîñîáà ðåøåíèÿ çàäà÷è âåðèôèêàöèèìîäåëåé ïðîãðàìì ëåæèò íåêîòîðàÿ çàäà÷à äèñêðåòíîéìàòåìàòèêè è ìåòîäû åå ðåøåíèÿ.1.
Òàáëè÷íûé è òåîðåòèêî-àâòîìàòíûé ìåòîäû . Ìîäåëèïðåäñòàâëÿþòñÿ â âèäå ãðàôà. Âåðèôèêàöèÿ ìîäåëèñâîäèòñÿ ê ïðîâåðêå äîñòèæèìîñòè çàäàííîãî ìíîæåñòâàâåðøèí è êîìïîíåíò ñâÿçíîñòè â ãðàôå.Ðàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèè ìîäåëåéïðîãðàììÍåîñïîðèìûé òåçèñ îñíîâå êàæäîãî ñïîñîáà ðåøåíèÿ çàäà÷è âåðèôèêàöèèìîäåëåé ïðîãðàìì ëåæèò íåêîòîðàÿ çàäà÷à äèñêðåòíîéìàòåìàòèêè è ìåòîäû åå ðåøåíèÿ.1. Òàáëè÷íûé è òåîðåòèêî-àâòîìàòíûé ìåòîäû . Ìîäåëèïðåäñòàâëÿþòñÿ â âèäå ãðàôà.
Âåðèôèêàöèÿ ìîäåëèñâîäèòñÿ ê ïðîâåðêå äîñòèæèìîñòè çàäàííîãî ìíîæåñòâàâåðøèí è êîìïîíåíò ñâÿçíîñòè â ãðàôå.2. Ñèìâîëüíûé ìåòîä . Ìîäåëè ïðåäñòàâëÿþòñÿ â âèäåROBDD. Âåðèôèêàöèÿ ìîäåëè ñâîäèòñÿ ê âû÷èñëåíèþíåïîäâèæíûõ òî÷åê îïåðàòîðîâ íà êîíå÷íûõ ìíîæåñòâàõïîñðåäñòâîì îïåðàöèé íàä ROBDD.Ðàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèè ìîäåëåéïðîãðàìì1. Òàáëè÷íûé è òåîðåòèêî-àâòîìàòíûé ìåòîäû .Ïðåèìóùåñòâà. Óñòðîåí ïðîñòî è ðàáîòàåò áûñòðî.Òðóäíîñòè.
Ïðèìåíèì òîëüêî ê ìîäåëÿì íåáîëüøîãîðàçìåðà (108 − 1010 ñîñòîÿíèé).Ðàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèè ìîäåëåéïðîãðàìì1. Òàáëè÷íûé è òåîðåòèêî-àâòîìàòíûé ìåòîäû .Ïðåèìóùåñòâà. Óñòðîåí ïðîñòî è ðàáîòàåò áûñòðî.Òðóäíîñòè. Ïðèìåíèì òîëüêî ê ìîäåëÿì íåáîëüøîãîðàçìåðà (108 − 1010 ñîñòîÿíèé).2. Ñèìâîëüíûé ìåòîä .Ïðåèìóùåñòâà. Ïðèìåíèì ê ìîäåëÿì áîëüøîãî ðàçìåðà(10100 è áîëåå ñîñòîÿíèé).Òðóäíîñòè. Òðåáóåò òîíêîé íàñòðîéêè âûáîðàïîäõîäÿùåé àáñòðàêöèè ïðè ïîñòðîåíèè ìîäåëè,îïòèìàëüíîãî óïîðÿäî÷åíèÿ ïåðåìåííûõ ïðè ïîñòðîåíèèROBDD, áîëüøîãî îáúåìà ïàìÿòè äëÿ åå õðàíåíèÿ.Ðàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèè ìîäåëåéïðîãðàìì1.
Òàáëè÷íûé è òåîðåòèêî-àâòîìàòíûé ìåòîäû .Ïðåèìóùåñòâà. Óñòðîåí ïðîñòî è ðàáîòàåò áûñòðî.Òðóäíîñòè. Ïðèìåíèì òîëüêî ê ìîäåëÿì íåáîëüøîãîðàçìåðà (108 − 1010 ñîñòîÿíèé).2. Ñèìâîëüíûé ìåòîä .Ïðåèìóùåñòâà. Ïðèìåíèì ê ìîäåëÿì áîëüøîãî ðàçìåðà(10100 è áîëåå ñîñòîÿíèé).Òðóäíîñòè. Òðåáóåò òîíêîé íàñòðîéêè âûáîðàïîäõîäÿùåé àáñòðàêöèè ïðè ïîñòðîåíèè ìîäåëè,îïòèìàëüíîãî óïîðÿäî÷åíèÿ ïåðåìåííûõ ïðè ïîñòðîåíèèROBDD, áîëüøîãî îáúåìà ïàìÿòè äëÿ åå õðàíåíèÿ.¾Ñ óìíûì - õëîïîòíî, ñ äóðàêîì - ïëîõî.Íóæíî ÷òî-òî ñðåäíåå.Äà ãäå æ åãî âçÿòü?¿Ðàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèè ìîäåëåéïðîãðàììÈäåÿÍà ïðàêòèêå ÷àùå âñåãî ïðèõîäèòñÿ ïðîâåðÿòü ïðîñòûåòðåáîâàíèÿ áåçîïàñíîñòè è æèâîñòè, íàðóøåíèå êîòîðûõïîäòâåðæäàåòñÿ îáíàðóæåíèåì ñðàâíèòåëüíî êîðîòêîãîêîíòð-ïðèìåðà òðàññû äëèíû 10 − 100.Safety counterexample'Liveness counterexample$''s0sky- t- t- t- t - y&$$s0y- t- ?t- t- t- ts`%&sk%Ðàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèè ìîäåëåéïðîãðàììÈäåÿÏðåäïîëàãàåìûé êîíòð-ïðèìåð ìîæíî îïèñàòü áóëåâîéôîðìóëîé, óòâåðæäàþùåé î òîì, ÷òî â ìîäåëè ñóùåñòâóåòïîñëåäîâàòåëüíîñòü ïåðåõîäîâ s0 → s1 → · · · → sk çàäàííîéäëèíû k , ïðîõîäÿùåé ÷åðåç ñîñòîÿíèÿ îïðåäåëåííîãî âèäà.Safety counterexample'Liveness counterexample$''s0sky- t- t- t- t - y&$$s0y- t- ?t- t- t- ts`%&sk%Ðàçíîîáðàçèå ìåòîäîâ âåðèôèêàöèè ìîäåëåéïðîãðàììÈäåÿÏîñòðîåííàÿ ôîðìóëà ϕ äîëæíà áûòü âûïîëíèìà â òîì èòîëüêî òîì ñëó÷àå, êîãäà â ìîäåëè åñòü ¾êîðîòêàÿ¿ òðàññà,êîòîðàÿ ÿâëÿåòñÿ êîíòð-ïðèìåðîì äëÿ ïðîâåðÿåìîãî ñâîéñòâà.Îäíàêî òàêàÿ ôîðìóëà ìîæåò çàâèñåòü îò äåñÿòêîâ òûñÿ÷ïåðåìåííûõ (÷èñëî ïåðåìåííûõ ñîñòîÿíèÿ × äëèíàêîíòð-ïðèìåðà), è ïîýòîìó ïðîâåðèòü åå âûïîëíèìîñòü ïðèïîìîùè ROBDD ïðàêòè÷åñêè íåâîçìîæíî íå õâàòèò ïàìÿòè.Íàì íóæíû ñïåöèàëüíûå ìåòîäû è ñðåäñòâà ðåøåíèÿ çàäà÷èSAT ïðîâåðêè âûïîëíèìîñòè áóëåâûõ ôîðìóë. ÷åì æå ñîñòîèò ýòà çàäà÷à è êàê îíà ðåøàåòñÿ?Çàäà÷à ïðîâåðêè âûïîëíèìîñòè áóëåâûõôîðìóë (SAT) è ñïîñîáû åå ðåøåíèÿÏðîáëåìà âûïîëíèìîñòè äëÿ áóëåâûõ ôîðìóë (SAT): äëÿïðîèçâîëüíîé çàäàííîé áóëåâîé ôîðìóëû ϕ(x1 , x2 , .
. . , xn )âûÿñíèòü, ñóùåñòâóåò ëè òàêîé íàáîð çíà÷åíèé ïåðåìåííûõx1 = σ1 , x2 = σ2 , . . . , xn = σn , äëÿ êîòîðîãî âåðíî ðàâåíñòâîϕ(σ1 , σ2 , . . . , σn ) = 1Çàäà÷à ïðîâåðêè âûïîëíèìîñòè áóëåâûõôîðìóë (SAT) è ñïîñîáû åå ðåøåíèÿÏðîáëåìà âûïîëíèìîñòè äëÿ áóëåâûõ ôîðìóë (SAT): äëÿïðîèçâîëüíîé çàäàííîé áóëåâîé ôîðìóëû ϕ(x1 , x2 , . . .
, xn )âûÿñíèòü, ñóùåñòâóåò ëè òàêîé íàáîð çíà÷åíèé ïåðåìåííûõx1 = σ1 , x2 = σ2 , . . . , xn = σn , äëÿ êîòîðîãî âåðíî ðàâåíñòâîϕ(σ1 , σ2 , . . . , σn ) = 1Çàìå÷àíèå 1.Ìîæíî ñ÷èòàòü, ÷òî â ôîðìóëå ϕ(x1 , x2 , . . . , xn ) èñïîëüçóþòñÿòîëüêî îïåðàöèè ¬, ∧, ∨ .Çàäà÷à ïðîâåðêè âûïîëíèìîñòè áóëåâûõôîðìóë (SAT) è ñïîñîáû åå ðåøåíèÿÏðîáëåìà âûïîëíèìîñòè äëÿ áóëåâûõ ôîðìóë (SAT): äëÿïðîèçâîëüíîé çàäàííîé áóëåâîé ôîðìóëû ϕ(x1 , x2 , . .
. , xn )âûÿñíèòü, ñóùåñòâóåò ëè òàêîé íàáîð çíà÷åíèé ïåðåìåííûõx1 = σ1 , x2 = σ2 , . . . , xn = σn , äëÿ êîòîðîãî âåðíî ðàâåíñòâîϕ(σ1 , σ2 , . . . , σn ) = 1Çàìå÷àíèå 1.Ìîæíî ñ÷èòàòü, ÷òî â ôîðìóëå ϕ(x1 , x2 , . . . , xn ) èñïîëüçóþòñÿòîëüêî îïåðàöèè ¬, ∧, ∨ .Çàìå÷àíèå 2.Ìîæíî ñ÷èòàòü, ÷òî ôîðìóëà ϕ(x1 , x2 , . . . , xn ) ýòîêîíúþíêòèâíàÿ íîðìàëüíàÿ ôîðìà âèäà^δ3CNF =(xiδi ∨ xj j ∨ xkδk )(i,j,k)∈IÇàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÈëëþñòðàöèÿ ê çàìå÷àíèþ 2.Φ(. . . x1 → x2 . . .
)Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÈëëþñòðàöèÿ ê çàìå÷àíèþ 2.Φ(. . . x1 → x2 . . . )Φ(. . . y . . . ) ∧ (y ≡ (x1 → x2 ))Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÈëëþñòðàöèÿ ê çàìå÷àíèþ 2.Φ(. . . x1 → x2 . . . )Φ(. . . y . . . ) ∧ (y ≡ (x1 → x2 ))Φ(. . . y . . . ) ∧ (y ∨ x1 ∨ x2 ) ∧ (y ∨ x1 ∨ x2 ) ∧ (y ∨ x1 ∨ x2 ) ∧ (ȳ ∨ x1 ∨ x2 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÈëëþñòðàöèÿ ê çàìå÷àíèþ 2.Φ(. . . x1 → x2 . . . )Φ(. . .
y . . . ) ∧ (y ≡ (x1 → x2 ))Φ(. . . y . . . ) ∧ (y ∨ x1 ∨ x2 ) ∧ (y ∨ x1 ∨ x2 ) ∧ (y ∨ x1 ∨ x2 ) ∧ (ȳ ∨ x1 ∨ x2 )Òàêèì îáðàçîì, ëþáóþ áóëåâó ôîðìóëó ñ n ïåðåìåííûìè è mîïåðàöèÿìè ìîæíî ïðåîáðàçîâàòü â ðàâíîâûïîëíèìóþ 3-ÊÍÔñ n + m ïåðåìåííûìè è 4m äèçúþíêòàìè-ñîìíîæèòåëÿìè.Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÊàê èçâåñòíî, ïðîáëåìà âûïîëíèìîñòè 3-ÊÍÔ ÿâëÿåòñÿNP-ïîëíîé çàäà÷åé.Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÊàê èçâåñòíî, ïðîáëåìà âûïîëíèìîñòè 3-ÊÍÔ ÿâëÿåòñÿNP-ïîëíîé çàäà÷åé. ñâåòå ñîâðåìåííûõ ìàòåìàòè÷åñêèõ çíàíèé ýòî îçíà÷àåò, ÷òî1.
íåò ýôôåêòèâíîé ïðîöåäóðû ãàðàíòèðîâàííîãî ðåøåíèÿçàäà÷è âûïîëíèìîñòè 3-ÊÍÔ;Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÊàê èçâåñòíî, ïðîáëåìà âûïîëíèìîñòè 3-ÊÍÔ ÿâëÿåòñÿNP-ïîëíîé çàäà÷åé. ñâåòå ñîâðåìåííûõ ìàòåìàòè÷åñêèõ çíàíèé ýòî îçíà÷àåò, ÷òî1. íåò ýôôåêòèâíîé ïðîöåäóðû ãàðàíòèðîâàííîãî ðåøåíèÿçàäà÷è âûïîëíèìîñòè 3-ÊÍÔ;2. ñêîëü-íèáóäü ýôôåêòèâíûé ìåòîä ðåøåíèÿ çàäà÷èâûïîëíèìîñòè 3-ÊÍÔ ìîæíî èñïîëüçîâàòü äëÿ ðåøåíèÿáîëüøîãî ÷èñëà ðàçíîîáðàçíûõ çàäà÷ êîìáèíàòîðèêè,äèñêðåòíîé ìàòåìàòèêè, àëãåáðû, òåîðèè ôîðìàëüíûõÿçûêîâ è äð.Âîò ïîýòîìó ïðîãðàììû ðåøåíèÿ çàäà÷è âûïîëíèìîñòè 3-ÊÍÔ(SAT-solvers) ïîëüçóþòñÿ áîëüøèì ñïðîñîì.Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÍàèáîëåå ðàñïðîñòðàíåííûå ïîäõîäû ê ðåøåíèþ çàäà÷è SATI ìåòîä DPLL ñ ðàçðåøåíèåì êîíôëèêòîâ,I ìåòîä ñëó÷àéíîãî áëóæäàíèÿ.Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÍàèáîëåå ðàñïðîñòðàíåííûå ïîäõîäû ê ðåøåíèþ çàäà÷è SATI ìåòîä DPLL ñ ðàçðåøåíèåì êîíôëèêòîâ,I ìåòîä ñëó÷àéíîãî áëóæäàíèÿ.DPLL (DavisPutnamLogemannLoveland algorithm) ýòîïåðåáîðíûé ïîèñê íàáîðà çíà÷åíèé ïåðåìåííûõ, íà êîòîðîìâûïîëíÿåòñÿ 3-ÊÍÔ, ïóòåì ïîñëåäîâàòåëüíîãî âûáîðàïîäõîäÿùèõ çíà÷åíèé äëÿ îòäåëüíûõ ïåðåìåííûõ è óïðîùåíèÿ3-ÊÍÔ â ñîîòâåòñòâèè ñ âûáðàííûìè çíà÷åíèÿìè.Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿw(x1 ∨ x2 )∧ (x1 ∨ x3 )∧ (x2 ∨ x4 ∨ x5 )∧(x1 ∨ x2 ∨ x4 )∧(x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿwx1 = 0w(x1 ∨ x2 )∧ (x1 ∨ x3 )∧ (x2 ∨ x4 ∨ x5 )∧(x1 ∨ x2 ∨ x4 )∧(x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿwx1 = 0w(0 ∨ x2 )∧ (0 ∨ x3 )∧ (x2 ∨ x4 ∨ x5 )∧(0 ∨ x2 ∨ x4 )∧ (x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿwx1 = 0x2 ∧w(x2 ∨ x4 ∨ x5 )∧ (x2 ∨ x4 )∧(x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿwx1 = 0x2 ∧w(x2 ∨ x4 ∨ x5 )∧ (x2 ∨ x4 )∧(x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿwx1 = 0wx2 = 1(1 ∨ x4 ∨ x5 )∧(1 ∨ x4 )∧(1 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿwx1 = 0wx2 = 1(x4 ∨ x5 )∧x4 ∧x5Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿwx1 = 0wx2 = 1x4 = 0 , x5 = 0(x4 ∨ x5 )∧x4 ∧x5Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿwx1 = 0wx2 = 1x4 = 0 , x5 = 0(0 ∨ 0)Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿw@@@x1 = 1Rw@(x1 ∨ x2 )∧ (x1 ∨ x3 )∧ (x2 ∨ x4 ∨ x5 )∧(x1 ∨ x2 ∨ x4 )∧(x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿw@@@x1 = 1Rw@(1 ∨ x2 )∧ (1 ∨ x3 )∧ (x2 ∨ x4 ∨ x5 )∧(1 ∨ x2 ∨ x4 )∧ (x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿw@@@x1 = 1Rw@x3 = 1x3 ∧ (x2 ∨ x4 ∨ x5 )∧(x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿw@@@x1 = 1Rw@x3 = 1(x2 ∨ x4 ∨ x5 )∧(x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿw@@@x1 = 1Rw@x3 = 1x2 = 0w(x2 ∨ x4 ∨ x5 )∧(x2 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿw@@@x1 = 1Rw@x3 = 1x2 = 0w(0 ∨ x4 ∨ x5 )∧(0 ∨ x5 )Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿw@@@x1 = 1Rw@x3 = 1x2 = 0w1Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÑîâðåìåííûå èíñòðóìåíòàëüíûå ñðåäñòâà ðåøåíèÿ çàäà÷è SATMiniSAT, BoolSAT, ArgoSAT, BCSAT, etc.êîìáèíèðóþò îñíîâíîé àëãîðèòì (DPLL, random walking) èíåñêîëüêî ïðèåìîâ, ñîêðàùàþùèõ ïåðåáîð, îáíàðóæåíèå èðåãèñòðàöèÿ êîíôëèêòîâ, íåõðîíîëîãè÷åñêèé îòêàò, ñëó÷àéíûéïåðåçàïóñê è äð. ðåçóëüòàòå ïîñòîÿííîãî è èíòåíñèâíîãî ñîâåðøåíñòâîâàíèÿýòè ñðåäñòâà ñïîñîáíû ïðîâåðÿòü âûïîëíèìîñòü 3-ÊÍÔ,ñîäåðæàùèõ ìèëëèîíû äèçúþíêòîâ è ñîòíè òûñÿ÷ ïåðåìåííûõ.Çàäà÷à SAT è ñïîñîáû åå ðåøåíèÿÑòðåìèòåëüíûé ïðîãðåññ â ðåøåíèè çàäà÷è SATÇàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)×òîáû âîñïîëüçîâàòüñÿ SAT-ðåøàòåëÿìè, íóæíî óìåòü ñâîäèòüèññëåäóåìóþ çàäà÷ó ê çàäà÷å SAT, ò.å.
ïîñòðîèòü òàêîéòðàíñëÿòîð Tr : Problems → 3-ÊÍÔ , ÷òîáû äëÿ ëþáîéêîíêðåòíîé çàäà÷è P èç êëàññà Problems áûëî âåðíîP èìååò ïîëîæèòåëüíîå ðåøåíèå ⇔ Tr (P) âûïîëíèìàÿ 3-ÊÍÔÇàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)×òîáû âîñïîëüçîâàòüñÿ SAT-ðåøàòåëÿìè, íóæíî óìåòü ñâîäèòüèññëåäóåìóþ çàäà÷ó ê çàäà÷å SAT, ò.å.
ïîñòðîèòü òàêîéòðàíñëÿòîð Tr : Problems → 3-ÊÍÔ , ÷òîáû äëÿ ëþáîéêîíêðåòíîé çàäà÷è P èç êëàññà Problems áûëî âåðíîP èìååò ïîëîæèòåëüíîå ðåøåíèå ⇔ Tr (P) âûïîëíèìàÿ 3-ÊÍÔÈçâåñòíî, ÷òî çàäà÷ó model checking äëÿ PLTL íåâîçìîæíîýôôåêòèâíî ñâåñòè ê çàäà÷å SAT (ïî÷åìó? ).Çàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)×òîáû âîñïîëüçîâàòüñÿ SAT-ðåøàòåëÿìè, íóæíî óìåòü ñâîäèòüèññëåäóåìóþ çàäà÷ó ê çàäà÷å SAT, ò.å. ïîñòðîèòü òàêîéòðàíñëÿòîð Tr : Problems → 3-ÊÍÔ , ÷òîáû äëÿ ëþáîéêîíêðåòíîé çàäà÷è P èç êëàññà Problems áûëî âåðíîP èìååò ïîëîæèòåëüíîå ðåøåíèå ⇔ Tr (P) âûïîëíèìàÿ 3-ÊÍÔÈçâåñòíî, ÷òî çàäà÷ó model checking äëÿ PLTL íåâîçìîæíîýôôåêòèâíî ñâåñòè ê çàäà÷å SAT (ïî÷åìó? ).Ïîýòîìó ïðèõîäèòñÿ îãðàíè÷èâàòüñÿ óïðîùåííûì âàðèàíòîìçàäà÷è model checking bounded model checking (BMC) :I ïðîâåðêå ïîäëåæàò òîëüêî ôîðìóëû âèäà Eϕ , ãäå ϕ ôîðìóëà ïóòè â ïîçèòèâíîé íîðìàëüíîé ôîðìå (îòðèöàíèÿïðèìåíÿþòñÿ òîëüêî ê ýëåìåíòàðíûì âûñêàçûâàíèÿì);I ïðîâåðêà ïðîâîäèòñÿ òîëüêî íà íà÷àëüíûõ îòðåçêàõ òðàññôèêñèðîâàííîé äëèíû k â ìîäåëè M .M |=k EϕÇàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)Ìû áóäåì ðàññìàòðèâàòü êîíå÷íûå ïóòè äâóõ òèïîâ,ïîðîæäåííûå êîíå÷íûìè ïîñëåäîâàòåëüíîñòÿìè ñîñòîÿíèés0 , s1 , .
. . , skk -ïóòü(`, k)-ïóòü'$''s0sky- t- t- t- t - y&$$s0y- t- ?t- t- t- ts`sk%&Åñëè π = s0 , s1 , . . . , s` , . . . , sk ýòî (`, k)-ïóòü, òî çàïèñü πbáóäåò îáîçíà÷àòü áåñêîíå÷íûé ïóòüπb = s0 , s1 , . . . , s` , s`+1 , . . . , sk , s` , s`+1 , . . . , sk , . . .%Çàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)Îïðåäåëåíèå îãðàíè÷åííîé âûïîëíèìîñòèπ |=k ϕ1. Åñëè π ýòî (`, k) -ïóòü, òî π |=k ϕ ⇔ πb |= ϕ.Çàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)Îïðåäåëåíèå îãðàíè÷åííîé âûïîëíèìîñòèπ |=k ϕ1.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
