Лекция 11. Bounded Model Checking. Выполнимость булевых формул SAT

Âåðèôèêàöèÿìîäåëåé ïðîãðàììËÅÊÒÎÐ:Âëàäèìèð Àíàòîëüåâè÷ ÇàõàðîâÂëàäèñëàâ Âàñèëüåâè÷ Ïîäûìîâ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.