Лекции В.А. Захарова, страница 36

å.XSubϕ1 = {ψ : ψ = Xχ, ψ ∈ FLSubϕ1 }.Ïðèìåð.Ïóñòüϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ÒîãäàXSubϕ1= {Xϕ1 , X¬busy ,X(true U(pr1 ∨ pr2 ))}.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀ(Until-Release)-ïîäôîðìóëûÏóñòü ϕ1 ôîðìóëà PLTL â ïîçèòèâíîé ôîðìå è FLSubϕ1 ìíîæåñòâîì ïîäôîðìóë ÔèøåðàËàäíåðà ôîðìóëû ϕ1 .Òîãäà çàïèñü URSubϕ1 áóäåò îáîçíà÷àòü ìíîæåñòâî âñåõ òåõïîäôîðìóë ÔèøåðàËàäíåðà, êîòîðûå íà÷èíàþòñÿ îïåðàòîðîìU (Until) èëè R (Release), ò. å.USubϕ1= {ψ : ψ = χ1 Uχ2 , ψ ∈ FLSubϕ1 }∪{ψ : ψ = χ1 Rχ2 , ψ ∈ FLSubϕ1 }.Ïðèìåð.Ïóñòüϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ÒîãäàUSubϕ1= {ϕ1 , true U(pr1 ∨ pr2 )}.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÑîãëàñîâàííûå ìíîæåñòâà ïîäôîðìóëÏóñòü ϕ1 ôîðìóëà PLTL â ïîçèòèâíîé ôîðìå, è FLSubϕ1 ìíîæåñòâî ïîäôîðìóë ÔèøåðàËàäíåðà äëÿ ϕ1 .Òîãäà ñîãëàñîâàííûì ìíîæåñòâîì ïîäôîðìóë ôîðìóëû ϕ1íàçûâàåòñÿ âñÿêîå ïîäìíîæåñòâî B , B ⊆ FLSubϕ1 ,óäîâëåòâîðÿþùåå ñëåäóþùèì óñëîâèÿì:1.true∈ B,false∈/ B,2. äëÿ ëþáîãî àòîìàðíîãî âûñêàçûâàíèÿp, p ∈ AP ∩ FLSubϕ1 , âûïîëíÿåòñÿ â òî÷íîñòèäâóõ âêëþ÷åíèé: ëèáî p ∈ B , ëèáî ¬p ∈ B ;îäíî èç3.

ψ ∨ χ ∈ B ⇐⇒ ψ ∈ B èëè χ ∈ B ,4. ψ&χ ∈ B ⇐⇒ ψ ∈ B è χ ∈ B ,5. ψ Uχ ∈ B ⇐⇒ χ ∈ B èëè {ψ, X(ψ Uχ)} ⊆ B ,6. ψ Rχ ∈ B ⇐⇒ χ ∈ B è ïðè ýòîì ψ ∈ B èëè X(ψ Rχ) ∈ B .ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÑîãëàñîâàííûå ìíîæåñòâà ïîäôîðìóëÑîãëàñîâàííûå ìíîæåñòâà ïîäôîðìóë ýòî ìàêñèìàëüíûåìíîæåñòâà ôîðìóë, êîòîðûå íå ñîäåðæàò ¾ÿâíûõ¿ïðîòèâîðå÷èé, ò. å. òàêèõ ïðîòèâîðå÷èé, êîòîðûå ìîæíîîáíàðóæèòü â òåêóùèé ìîìåíò âðåìåíè.Íàïðèìåð, ìíîæåñòâî, ñîñòîÿùåå èç äâóõ ôîðìóëXpX¬p çàâòðà ÿ ïîéäó íà ëåêöèþ, çàâòðà ÿ íå ïîéäó íà ëåêöèþ,ìîæåò áûòü ñîãëàñîâàííûì (õîòÿ è ïðîòèâîðå÷èâûì),ïîñêîëüêó ñåãîäíÿ âîçìîæíîå ïðîòèâîðå÷èå, ñîäåðæàùååñÿ âýòèõ âûñêàçûâàíèÿõ, íå ïðîÿâëÿåòñÿ.Ñîãëàñîâàííîå ìíîæåñòâî ïîäôîðìóë ÿâëÿåòñÿ àíàëîãîìñåìàíòè÷åñêîé òàáëèöû îíî âûðàæàåò íàøå ïîæåëàíèåñäåëàòü âñå óòâåðæäåíèÿ, ñîäåðæàùèåñÿ â ýòîì ìíîæåñòâå,èñòèííûìè, à âñå óòâåðæäåíèÿ, íå ñîäåðæàùèåñÿ â íåì, ëîæíûìè.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÑîãëàñîâàííûå ìíîæåñòâà ïîäôîðìóëÏðèìåð.ÏóñòüFLSubϕ1= {free, busy , pr1 , pr2 , ¬free, ¬busy , ¬pr1 , ¬pr2 ,pr1 ∨ pr2 ,true U(pr1 ∨ pr2 ),X¬busy , X(true U(pr1 ∨ pr2 )),¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 )),ϕ1 , Xϕ1 }.Òîãäà îäíèì èç ñîãëàñîâàííûõ ìíîæåñòâ ïîäôîðìóë ôîðìóëûϕ1 ÿâëÿåòñÿ ìíîæåñòâîB = {true, pr1 , ¬pr2 , ¬free, busy , X¬busy ,true U(pr1 ∨ pr2 ), X(true U(pr1 ∨ pr2 )), ϕ1 }.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÓòâåðæäåíèå 4.Ïóñòü I ïðîèçâîëüíàÿ òåìïîðàëüíàÿ èíòåðïðåòàöèÿ, è ϕ1 ïðîèçâîëüíàÿ ôîðìóëà â ïîçèòèâíîé ôîðìå.Òîãäà äëÿ ëþáîãî ìîìåíòà âðåìåíè n ìíîæåñòâî ôîðìóëBn = {ψ : ψ ∈ FLSubϕ1 è I , n |= ψ}ÿâëÿåòñÿ ñîãëàñîâàííûì.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.

Íåïîñðåäñòâåííî èç îïðåäåëåíèÿñîãëàñîâàííîãî ìíîæåñòâà.À âåðíî ëè îáðàòíîå óòâåðæäåíèå: êàæäîå ñîãëàñîâàííîåìíîæåñòâî ôîðìóë âûïîëíèìî â íåêîòîðîé èíòåðïðåòàöèè âíà÷àëüíûé ìîìåíò âðåìåíè?ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÓòâåðæäåíèå 5.Ïóñòü ϕ1 ôîðìóëà PLTL â ïîçèòèâíîé ôîðìå. Òîãäà1. äëÿ ëþáîé ïàðû B 0 ⊆ AP ∩ FLSubϕ1 , B 00 ⊆ XSubϕ1 ,ñóùåñòâóåò òàêîå ñîãëàñîâàííîå ìíîæåñòâî ïîäôîðìóë B ,äëÿ êîòîðîãî âåðíî B ∩ AP = B 0 , B ∩ XSubϕ1 = B 00 ;2. äëÿ ëþáîé ïàðû B1 è B2 ñîãëàñîâàííûõ ìíîæåñòâïîäôîðìóë Ôèøåðà-Ëàäíåðà ϕ1 âåðíû ñîîòíîøåíèÿB1 = B2 ⇐⇒ B1 ∩ AP = B2 ∩ AP èB1 ∩ XSubϕ1 = B1 ∩ XSubϕ1 .Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Óòâåðæäåíèå 6.Åñëè ϕ1 ñîäåðæèò n ëîãè÷åñêèõ ñâÿçîê è òåìïîðàëüíûõîïåðàòîðîâ, òî ÷èñëî ðàçëè÷íûõ ñîãëàñîâàííûõ ìíîæåñòâïîäôîðìóë Ôèøåðà-Ëàäíåðà íå ïðåâîñõîäèò âåëè÷èíû 23n .ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÌÎÄÅËÅÉ ÏÐÎÃÐÀÌÌÏóñòü çàäàíà ôîðìóëû PLTL ϕ è êîíå÷íàÿ LTSM = hAP, S, S0 , −→, ρi.Íóæíî ïðîâåðèòü âûïîëíèìîñòü M |= ϕ.Äëÿ ýòîãî1.

ôîðìóëà ϕ ïðèâîäèòñÿ ê ïîçèòèâíîé ôîðìå ϕ1 ,2. äëÿ ôîðìóëû ϕ1 ñòðîÿòñÿIIIIìíîæåñòâî ïîäôîðìóë ÔèøåðàËàäíåðà FLSubϕ1 ,ìíîæåñòâî Next-ïîäôîðìóë XSubϕ1 ,ìíîæåñòâî U-ïîäôîðìóë FLSubϕ1 ,ñîâîêóïíîñòü Conϕ1 âñåõ âîçìîæíûõ ñîãëàñîâàííûõìíîæåñòâ ïîäôîðìóë ÔèøåðàËàäíåðà.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÌÎÄÅËÅÉ ÏÐÎÃÐÀÌÌÑèñòåìîé Õèíòèêêè äëÿ ôîðìóëû PLTL ϕ1 è LTS Míàçûâàåòñÿ ðàñêðàøåííûé îðèåíòèðîâàííûé ãðàôGϕ1 ,M = (V , E ) ñ ìíîæåñòâîì âåðøèí V è ìíîæåñòâîì äóã E ,êîòîðûå óñòðîåíû òàê:V = {(s, B) : s ∈ S, B ∈ Conϕ1 , ρ(s) = B ∩ AP},ò. å.

âåðøèíàìè ãðàôà ÿâëÿþòñÿ âñåâîçìîæíûå ïàðû(ñîñòîÿíèå s , ñîãëàñîâàííîå ìíîæåñòâî B ),äëÿ êîòîðûõ ðàçìåòêà ρ(s) ñîñòîÿíèÿ s ïîäòâåðæäàåòèñòèííîñòü âñåõ àòîìàðíûõ âûñêàçûâàíèé ìíîæåñòâà B ;E= {h(s 0 , B 0 ), (s 00 , B 00 )i : s 0 −→ s 00è äëÿ ëþáîé Next-ïîäôîðìóëûâåðíî Xψ ∈ B 0 ⇐⇒ ψ ∈ B 00 },Xψ, Xψ ∈ XSubϕ1 ,ò. å. äóãàìè ãðàôà ÿâëÿþòñÿ âñå òàêèå ïåðåõîäû 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 .