Лекция 22. Задача верификации моделей программ. Подформулы Фишера-Ладнера... (Лекции 2014), страница 2

å. äóãàìè ãðàôà ÿâëÿþòñÿ âñå òàêèå ïåðåõîäû LTS M ,êîòîðûå ïîçâîëÿþò ïîäòâåðäèòü âñå îáåùàíèÿ Xψ âûïîëíèòüψ â ñëåäóþùèé ìîìåíò âðåìåíè.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÒåïåðü ïðîâåäåì ðàñêðàñêó âåðøèí ãðàôà Γϕ1 ,M = (V , E ).Ðàññìîòðèì ìíîæåñòâî (Until-Release)-ïîäôîðìóëURSubϕ1 = {χ01 Uχ001 , . .

. , χ0k Uχ00k , χ0k+1 Rχ00k+1 , . . . , χ0k+m Rχ00k+m }.Êàæäîé ôîðìóëå ψi èç ìíîæåñòâà URSubϕ1 ñîïîñòàâèìèíäèâèäóàëüíûé öâåò i .Ðàñêðàñèì â öâåò i âñå âåðøèíû (s, B), äëÿ êîòîðûõ âûïîëíåíîõîòÿ áû îäíî èç äâóõ óñëîâèéâ ñëó÷àå, êîãäà ψi = χ0i Uχ00i :1) χ00i ∈ B ,/ B.2) X(χ0i Uχ00i ) ∈â ñëó÷àå, êîãäà ψi = χ0i Rχ00i :1) χ00i ∈/ B,2) X(χ0i Rχ00i ) ∈ B .Áåñêîíå÷íûé ìàðøðóò(si1 , Bi1 ), (si2 , Bi2 ), .

. . , (sin , Bin ), . . .â ãðàôå Γϕ1 ,M íàçîâåì ðàäóæíûì, åñëè â íåì áåñêîíå÷íî ÷àñòîâñòðå÷àþòñÿ âåðøèíû êàæäîãî öâåòà 1, 2, . . . , k .ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÎñíîâíàÿ òåîðåìàÄëÿ ëþáîé ôîðìóëû PLTL ϕ1 â ïîçèòèâíîé ôîðìå è LTSM = hAP, S, S0 , −→, ρiM 6|= ϕ1mâ ãðàôå Γϕ1 ,M ñóùåñòâóåò õîòÿ áû îäèí ðàäóæíûé ìàðøðóò,èñõîäÿùèé èç âåðøèíû v0 = (s0 , B0 ), â êîòîðîé s0 ∈ S0 èϕ1 ∈/ B0 .ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÄîêàçàòåëüñòâî.(⇑) Ïðåäïîëîæèì, ÷òî â ãðàôå Γϕ1 ,M åñòü ðàäóæíûé ìàðøðóò(s0 , B0 ), (s1 , B1 ), .

. . , (sn , Bn ), (sn+1 , Bn+1 ), . . .óêàçàííîãî âèäà, â êîòîðîì ϕ1 ∈/ B0 .Òîãäà ñîãëàñíî îïðåäåëåíèþ ñèñòåìû Õèíòèêêè Γϕ1 ,M â LTS Måñòü íà÷àëüíàÿ òðàññàtr |0 |= B0tr = ys0tr |1 |= B1tr |2 |= B2- y- ys1s2- r r rtr |n |= Bn- ysntr |n+1 |= Bn+1- y- r r rsn+1Ïîêàæåì, ÷òî äëÿ ëþáîé ôîðìóëû ψ, ψ ∈ FLSubϕ1 , è äëÿëþáîãî n, n ≥ 0, âåðíîtr |n |= ψ ⇐⇒ ψ ∈ Bn .ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÄîêàçàòåëüñòâî.Åñëè óäàñòñÿ ïîêàçàòü, ÷òîtr |n |= ψ ⇐⇒ ψ ∈ Bn(∗)òî, ó÷èòûâàÿ ϕ1 ∈/ B0 , ïðèäåì ê çàêëþ÷åíèþ tr 6|= ϕ1 .Äëÿ äîêàçàòåëüñòâà ñîîòíîøåíèÿ (∗) âîñïîëüçóåìñÿ èíäóêöèåéïî ÷èñëó ñâÿçîê â ôîðìóëå ψ .Áàçèñ èíäóêöèè.p ∈ AP .p ∈ Bn ⇐⇒ p ∈ ξ(sn ) ⇐⇒ tr |n |= p .¬p ∈ Bn ⇐⇒ p ∈/ Bn ⇐⇒ p ∈/ ξ(sn ) ⇐⇒ tr |n 6|= p ⇐⇒ tr |n |= ¬p.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÄîêàçàòåëüñòâî.Èíäóêòèâíûé ïåðåõîä.1. Ëîãè÷åñêèå ñâÿçêè & è ∨.ψ1 &ψ2 ∈ Bn ⇐⇒ ψ1 ∈ Bn è ψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 è tr |n |= ψ1⇐⇒ tr |n |= ψ1 &ψ1 .2.

Òåìïîðàëüíûé îïåðàòîðXX.ψ ∈ Bn ⇐⇒ ψ ∈ Bn+1 ⇐⇒ tr |n+1 |= ψ ∈ Bn+1 ⇐⇒ tr |n |= Xψ.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÈíäóêòèâíûé ïåðåõîä.3. Òåìïîðàëüíûé îïåðàòîð.R3.1. Ïîêàæåì ψ1 Rψ2 ∈ Bn =⇒ tr |n |= ψ1 Rψ2 .Çàìåòèì, ÷òî ñîãëàñíî îïðåäåëåíèþ ñîãëàñîâàííîãî ìíîæåñòâàψ1 Rψ2 ∈ B ⇐⇒ ψ2 ∈ B è ïðè ýòîì ψ1 ∈ B èëè X(ψ1 Rψ2 ) ∈ B.Ïóñòü ψ1 Rψ2 ∈ Bn . Òîãäà âîçìîæíû 2 ñëó÷àÿ.Âàðèàíò 1.(ψ1 Rψ2 ) ∈ Bn+i äëÿ ëþáîãî i, i ≥ 0.XÒîãäà ïî îïðåäåëåíèþ Γϕ1 ,M â êàæäîì ìíîæåñòâå Bn+i , i ≥ 0,ñîäåðæèòñÿ ôîðìóëà ψ1 Rψ2 è, ñëåäîâàòåëüíî, ψ2 ∈ Bn+i .Òîãäà ïî èíäóêòèâíîìó ïðåäïîëîæåíèþ tr |n+i |= ψ2 äëÿ ëþáîãîi, i ≥ 0.

Ñëåäîâàòåëüíî, tr |n |= ψ1 Rψ2 .rrrtr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1- yn+2- ytr |n+i |= ψ2- yn+i-r r rÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÈíäóêòèâíûé ïåðåõîä.Âàðèàíò 2.X(ψ1 Rψ2 ) ∈/ Bn+k äëÿ íåêîòîðîãî k, k ≥ 0.Òîãäà ñóùåñòâóåò òàêîå k0 , ÷òî X(ψ1 Rψ2 ) ∈/ Bn+k0 íîX(ψ1 Rψ2 ) ∈ Bn+i äëÿ ëþáîãî i, 0 ≤ i < k0 .Òîãäà ïî îïðåäåëåíèþ ãðàôà Γϕ1 ,M â êàæäîì ìíîæåñòâå Bn+i ,0 ≤ i ≤ k0 , ñîäåðæèòñÿ ôîðìóëà ψ1 Rψ2 .Òîãäà ïî îïðåäåëåíèþ ñîãëàñîâàííûõ ìíîæåñòâ ψ2 ∈ Bn+i äëÿëþáîãî i, 0 ≤ i ≤ k0 , è, êðîìå òîãî, ψ1 ∈ Bn+k0 .Òîãäà ïî èíäóêòèâíîìó ïðåäïîëîæåíèþ tr |n+i |= ψ2 äëÿ ëþáîãî0 ≤ i ≤ k0 è tr |n+k0 |= ψ1 . Çíà÷èò, tr |n |= ψ1 Rψ2 .rrrtr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1- ytr |n+k0 −1 |= ψ2n+2- ytr |n+k0 |= ψ1tr |n+k0 |= ψ2- y-n+kÈòàê, â îáîèõ ñëó÷àÿõ ψ1 Rψ2 ∈ Bn =⇒ tr |n |= ψ1 Rψ2 .r r rÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÈíäóêòèâíûé ïåðåõîä.3.2.

Ïîêàæåì ψ1 Rψ2 ∈/ Bn =⇒ tr |n 6|= ψ1 Rψ2 .Ïóñòü ψ1 Rψ2 ∈/ Bn . Ò. ê. ψ1 Rψ2 ∈ URSubϕ1 ýòîé ôîðìóëåñîîòâåòñòâóåò íåêîòîðûé öâåò j .Ïîñêîëüêó ðàññìàòðèâàåìûé ìàðøðóò(s0 , B0 ), (s1 , B1 ), . . . , (sn , Bn ), (sn+1 , Bn+1 ), . . .ÿâëÿåòñÿ ðàäóæíûì, òî âåðøèíû, îêðàøåííûå â öâåò j ,âñòðå÷àþòñÿ â ýòîì ìàðøðóòå áåñêîíå÷íî ÷àñòî.Çíà÷èò, ñóùåñòâóåò òàêîå k, k ≥ 0, ÷òî âåðøèíà (sn+k , Bn+k ) ïåðâàÿ, îêðàøåííàÿ â öâåò j âåðøèíà, ñëåäóþùàÿ â ýòîìðàäóæíîì ìàðøðóòå âñëåä çà âåðøèíîé (sn , Bn ).Èìåþòñÿ äâå ïðè÷èíû, ïî êîòîðûì âåðøèíà (sn+k , Bn+k )îêàçàëàñü îêðàøåííîé â öâåò j :I ψ2 ∈/ Bn+k ,I X(ψ1 Rψ2 ) ∈ Bn+k ,Ðàññìîòðèì êàæäûé èç ýòèõ ñëó÷àåâ ïî îòäåëüíîñòè.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÈíäóêòèâíûé ïåðåõîä.Âàðèàíò 1. ψ2 ∈/ Bn+k .Ò.

ê. âñå âåðøèíû (sn+i , Bn+i ), 0 ≤ i < k íå îêðàøåíû â öâåò j ,äëÿ êàæäîãî èç ìíîæåñòâ Bn+i , 0 ≤ i < k , âåðíû ñîîòíîøåíèÿèψ2 ∈ Bn+i(ψ1 Rψ2 ) ∈/ Bn+i .XÒîãäà ïî îïðåäåëåíèþ ãðàôà Γϕ1 ,M äëÿ êàæäîãî ìíîæåñòâàBn+i , 0 ≤ i < k , âåðíî ñîîòíîøåíèå ψ1 Rψ2 ∈/ Bn+i . À îòñþäàñëåäóåò, ÷òî ψ1 ∈/ Bn+i äëÿ ëþáîãî i, 0 ≤ i < k .Òîãäà ïî èíäóêòèâíîìó ïðåäïîëîæåíèþtr |n+i |= ψ2 è tr |n+i 6|= ψ1 äëÿ ëþáîãî i, 0 ≤ i < k ,tr |n+k 6|= ψ2 .rrrtr |n 6|= ψ1 tr |n+1 6|= ψ1tr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k−1 6|= ψ1tr |n+k−1 |= ψ2- y- yn+2À ýòî îçíà÷àåò, ÷òî tr |n 6|= ψ1 Rψ2 .tr |n+k 6|= ψ2- yn+k-r r rÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÈíäóêòèâíûé ïåðåõîä.Âàðèàíò 2.X(ψ1 Rψ2 ) ∈ Bn+k .Ò. ê.

âñå âåðøèíû (sn+i , Bn+i ), 0 ≤ i < k íå îêðàøåíû â öâåò j ,äëÿ êàæäîãî èç ìíîæåñòâ Bn+i , 0 ≤ i < k , âåðíû ñîîòíîøåíèÿèψ2 ∈ Bn+i(ψ1 Rψ2 ) ∈/ Bn+i .XÒîãäà ïî îïðåäåëåíèþ ãðàôà Γϕ1 ,M äëÿ êàæäîãî ìíîæåñòâàBn+i , 0 ≤ i ≤ k , âåðíî ñîîòíîøåíèå ψ1 Rψ2 ∈/ Bn+i . À îòñþäàñëåäóåò, ÷òî ψ1 ∈/ Bn+i äëÿ ëþáîãî i, 0 ≤ i < k è ψ2 ∈/ Bn+k .Òîãäà ïî èíäóêòèâíîìó ïðåäïîëîæåíèþtr |n+i |= ψ2 è tr |n+i 6|= ψ1 äëÿ ëþáîãî i, 0 ≤ i < k ,tr |n+k 6|= ψ2 .rrrtr |n 6|= ψ1 tr |n+1 6|= ψ1tr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k−1 6|= ψ1tr |n+k−1 |= ψ2- y- yn+2È âî âòîðîì ñëó÷àå tr |n 6|= ψ1 Rψ2 .tr |n+k 6|= ψ2- yn+k-r r rÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÈíäóêòèâíûé ïåðåõîä.Òàêèì îáðàçîì, åñëè ψ1 Rψ2 ∈/ Bn , òî tr |n 6|= ψ1 Rψ2 . èòîãå, äëÿ ëþáîé ôîðìóëû âèäà ψ1 Rψ2 è äëÿ ëþáîéâåðøèíû (sn , Bn ) íàøåãî ðàäóæíîãî ìàðøðóòà âåðíîñîîòíîøåíèåψ1 Rψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 Rψ2 .4. Òåìïîðàëüíûé îïåðàòîð.UÄëÿ äîêàçàòåëüñòâà ñîîòíîøåíèÿψ1 Rψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 Rψ2ïðèìåíÿþòñÿ ðàññóæäåíèÿ, àíàëîãè÷íûå òåì, êîòîðûå áûëèèñïîëüçîâàíû äëÿ èññëåäîâàíèÿ îïåðàòîðà R.Ñàìîñòîÿòåëüíî.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÇàâåðøèâ îáîñíîâàíèå èíäóêòèâíîãî ïåðåõîäà, ìû òåì ñàìûìçàâåðøèëè äîêàçàòåëüñòâî ïåðâîé ÷àñòè òåîðåìû:M 6|= ϕ1⇑â ãðàôå Γϕ1 ,M ñóùåñòâóåò õîòÿ áû îäèí ðàäóæíûé ìàðøðóò,èñõîäÿùèé èç âåðøèíû v0 = (s0 , B0 ), â êîòîðîé s0 ∈ S0 èϕ1 ∈/ B0 .Ïîêàæåì, ÷òî â òîì ñëó÷àå, êîãäà èìååò ìåñòî M 6|= ϕ1 , âãðàôå Γϕ1 ,M èç íåêîòîðîé âåðøèíû v0 = (s0 , B0 ), â êîòîðîés0 ∈ S0 è ϕ1 ∈/ B0 , èñõîäèò õîòÿ áû îäèí ðàäóæíûé ìàðøðóò.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÏóñòü M 6|= ϕ1 .

Òîãäà â LTS M ñóùåñòâóåò òàêàÿ íà÷àëüíàÿòðàññà tr , äëÿ êîòîðîé tr 6|= ϕ1 . Ðàññìîòðèì ýòó òðàññó tr .Äëÿ êàæäîãî i, i ≥ 0, ïîëîæèìBi = {ψ : ψ ∈ FLSubϕ1 , tr |i |= ψ .}Ñîãëàñíî óòâåðæäåíèþ 4, âñå ïîñòðîåííûå ìíîæåñòâà Biÿâëÿþòñÿ ñîãëàñîâàííûìè.Ïîêàæåì, ÷òî ïîñëåäîâàòåëüíîñòü ïàð(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), . .

.îáðàçóåò èñêîìûé ðàäóæíûé ìàðøðóò â ãðàôå Γϕ1 .ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÄåéñòâèòåëüíî,1. Äëÿ ëþáîãî n, n ≥ 0, âåðíî tr [n] −→ tr [n + 1], ïîñêîëüêó tr ìàðøðóò â LTS M .2. Äëÿ ëþáîãî n, n ≥ 0 è äëÿ ëþáîé ôîðìóëûâåðíîXψ ∈ Bn ⇐⇒ ψ ∈ Bn+1ψ ∈ XSubϕ1 ,XïîñêîëüêóXψ ∈ Bn ⇐⇒ tr |n |= Xψ ⇐⇒ tr |n+1 |= ψ ⇐⇒ ψ ∈ Bn+1 .3. tr [0] ∈ S0 (ò. ê.

tr íà÷àëüíàÿ òðàññà â M ) è ϕ1 ∈/ B0 (ò. ê.tr |0 6|= ϕ1 ).Çíà÷èò, ïîñëåäîâàòåëüíîñòü(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .ÿâëÿåòñÿ ìàðøðóòîì â ãðàôå Γϕ1 ,M , èñõîäÿùèì èç íóæíîéâåðøèíû.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈ4. Îñòàëîñü ïîêàçàòü, ÷òî ìàðøðóò(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . .

, (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .ÿâëÿåòñÿ ðàäóæíûì.Ðàññìîòðèì ïðîèçâîëüíîå ÷èñëî n, n ≥ 0 è ïðîèçâîëüíóþôîðìóëó ψi ∈ URSubϕ1 . Ïîêàæåì, ÷òî ñóùåñòâóåò òàêîåk, k ≥ 0, ÷òî âåðøèíà (tr [n + k], Bn+k ) îêðàøåíà â öâåò i .ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÎãðàíè÷èìñÿ ðàññìîòðåíèåì Until-ôîðìóëû ψi = χ0 Uχ2 .(Äëÿ ôîðìóë âèäà ψi = χ0 Rχ2 äîêàçàòåëüñòâî ïðîâåäèòåñàìîñòîÿòåëüíî. )1.

Åñëè tr |n 6|= X(χ1 Uχ2 ), òî X(χ1 Uχ2 ) ∈/ Bn , è,ñëåäîâàòåëüíî, âåðøèíà (tr [n], Bn ) îêðàøåíà â öâåò j .2. À åñëè tr |n |= X(χ1 Uχ2 ), òî tr |n+1 |= χ1 Uχ2 . Òîãäàñóùåñòâóåò òàêîå k, k ≥ 1, ÷òî tr |n+k |= χ2 . Ïîýòîìóχ2 ∈ Bn+k , è âåðøèíà (tr [n + k], Bn+k ) îêðàøåíà â öâåò j .Òàêèì îáðàçîì, âåðøèíû öâåòà j âñòðå÷àþòñÿ â íàøåììàðøðóòå áåñêîíå÷íî ÷àñòî. Ïîñêîëüêó ψi áûëà ïðîèçâîëüíîé(Until-Release)-ôîðìóëîé, ýòî îçíà÷àåò, ÷òî íàø ìàðøðóò âãðàôå Γϕ1 ,M ÿâëÿåòñÿ ðàäóæíûì.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÍî êàê ïðîâåðèòü, ÷òî èç çàäàííîé âåðøèíû â ãðàôå Γϕ1 ,Míå èñõîäèò íè îäíîãî ðàäóæíîãî ìàðøðóòà?Îðèåíòèðîâàííûé ãðàô Γ íàçûâàåòñÿ ñèëüíî ñâÿçíûì , åñëèäëÿ ëþáîé ïàðû âåðøèí v è u â ãðàôå Γ ñóùåñòâóåò ìàðøðóòèç v â u è ìàðøðóò èç u â v .Âñÿêèé ìàêñèìàëüíûé ñèëüíî ñâÿçíûé ïîäãðàô ãðàôà Γíàçûâàåòñÿ êîìïîíåíòîé ñèëüíîé ñâÿçíîñòè .Êîìïîíåíòó ñèëüíîé ñâÿçíîñòè ãðàôà (ñèñòåìû Õèíòèêêè)Γϕ1 ,M áóäåì íàçûâàòü ðàäóæíîé, åñëè â íåé ñîäåðæàòñÿâåðøèíû âñåõ öâåòîâ.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÒåîðåìà.Èç âåðøèíû v â ãðàôå Γϕ1 ,M èñõîäèò ðàäóæíûé ìàðøðóò òîãäàè òîëüêî òîãäà, êîãäà ñóùåñòâóåò ìàðøðóò , âåäóùèé èçâåðøèíû v õîòÿ áû â îäíó èç âåðøèí õîòÿ áû îäíîé ðàäóæíîéêîìïîíåíòû ñèëüíîé ñâÿçíîñòè.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.

Çäåñü âñå î÷åâèäíî.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌôîðìóëà PLTL ϕ è LTSM = hAP, S, S0 , −→, ρi.Èñõîäíûå äàííûå:1. Ïîñòðîèòü ðàâíîñèëüíóþ ïîçèòèâíóþ ôîðìó ϕ1 .2. Ïîñòðîèòü ñèñòåìó Õèíòèêêè Γϕ1 ,M .3. Âûäåëèòü ìíîæåñòâî ïîäôîðìóë URSubϕ1 è ðàñêðàñèòüâåðøèíû ãðàôà Γϕ1 ,M .4.

Âûäåëèòü ðàäóæíûå êîìïîíåíòû ñèëüíîé ñâÿçíîñòè âãðàôå Γϕ1 ,M .5. Âûäåëèòü ìíîæåñòâî V 0 âñåõ âåðøèí ãðàôà Γϕ1 ,M , èçêîòîðûõ äîñòèæèìû ðàäóæíûå êîìïîíåíòû ñèëüíîéñâÿçíîñòè.6. Âûäåëèòü ìíîæåñòâî V 00 âñåõ âåðøèí (s0 , B0 ), äëÿ êîòîðîéâûïîëíÿåòñÿ s0 ∈ S0 , ϕ1 ∈/ B0 .0007. Âû÷èñëèòü V = V ∩ V .Ðåçóëüòàò:M |= ϕ ⇐⇒ V = ∅.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÏðèìåð.ϕ = p UqLTS M :'s1'- iξ(s1 ) = {p} 6&s0$s2?i$ξ(s2 ) = {q}%yξ(s0 ) = {p}'s3&- iξ(s3 ) = {p} 6&$s4?iξ(s4 ) = {p}%%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÏðèìåð.ϕ = F(p Uq)1.