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

Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 22.Çàäà÷à âåðèôèêàöèè ìîäåëåéïðîãðàìì.Ïîäôîðìóëû Ôèøåðà-Ëàäíåðà.Òàáëè÷íûé ìåòîä âåðèôèêàöèèìîäåëåé ïðîãðàìì.Àëãîðèòì âåðèôèêàöèè ìîäåëåéïðîãðàìì.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÇàäà÷à model checking äëÿ PLTLÄëÿ çàäàííîé ôîðìóëû PLTL ϕ è êîíå÷íîé LTS M ïðîâåðèòü M |= ϕ.Ïî÷åìó çàäà÷à model checking íåïðîñòà? Ïîòîìó ÷òîIâûïîëíèìîñòü ôîðìóë PLTL ïðîâåðÿåòñÿ íà áåñêîíå÷íûõèíòåðïðåòàöèÿõ,I LTS M èìååòñÿ áåñêîíå÷íî ìíîãî èíòåðïðåòàöèé (òðàññ).Ïî÷åìó çàäà÷à model checking èìååò ýôôåêòèâíîå ðåøåíèå?Ïîòîìó ÷òîIâñå ýòî áåñêîíå÷íîå ìíîæåñòâî áåñêîíå÷íûõ èíòåðïðåòàöèé¾óïàêîâàíî¿ â êîíå÷íóþ ñòðóêòóðó LTS M .ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÇàìûñåë òàáëè÷íîãî ìåòîäà1.

Âìåñòî ïðîâåðêè âûïîëíèìîñòè ϕ âî âñåõ èíòåðïðåòàöèÿõëó÷øå çàíÿòüñÿ ïîèñêîì êîíòðìîäåëè èíòåðïðåòàöèè I ,â êîòîðîé íå âûïîëíÿåòñÿ ϕ.2. Âûïîëíèìîñòü âñÿêîé ôîðìóëû ψ ïîëíîñòüþ îïðåäåëÿåòñÿâûïîëíèìîñòüþ åå ïîäôîðìóë. Ïîýòîìó (íå)âûïîëíèìîñòüôîðìóë ìîæíî ïðîâåðÿòü èíäóêòèâíî.3. (Íå)âûïîëíèìîñòü ôîðìóëû íà îäíîé èç òðàññ LTS M ,íà÷èíàþùåéñÿ â ñîñòîÿíèè s , ýòî ñâîéñòâî ñîñòîÿíèÿ s .Çíà÷èò, ïðîâåðÿÿ (íå)âûïîëíèìîñòü âñåõ ïîäôîðìóëôîðìóëû ϕ äëÿ âñåõ ñîñòîÿíèé LTS M , ìîæíî âû÷èñëèòüìíîæåñòâî S ϕ âñåõ òåõ ñîñòîÿíèé, â êîòîðûõ íåâûïîëíÿåòñÿ ôîðìóëà ϕ. Åñëè S0 ∩ S ϕ 6= ∅, òî M 6|= ϕ.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÂñïîìîãàòåëüíûå îïðåäåëåíèÿ è îáîçíà÷åíèÿÄëÿ çàäàííîé LTS M = hAP, S, S0 , −→, ρi, òðàññûtr = si0 , si1 , .

. . , sin , sin+1 , . . . â LTS M è ôîðìóëû PLTL ϕ áóäåìèñïîëüçîâàòü çàïèñüItr |= ϕ äëÿ îáîçíà÷åíèÿ îòíîøåíèÿ âûïîëíèìîñòèI (tr ), 0 |= ϕ;Itr [j] äëÿ îáîçíà÷åíèÿ j -ãî ñîñòîÿíèÿ sij â òðàññå tr ;Itr |j äëÿ îáîçíà÷åíèÿ òðàññû tr 0 = sij , sij+1 , . . . , ÿâëÿþùåéñÿñóôôèêñîì òðàññû tr , íà÷èíàþùåéñÿ ñîñòîÿíèåì sij .ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÓòâåðæäåíèå 1.Äëÿ ëþáîé LTS M è ôîðìóëà PLTL ϕ âåðíîM 6|= ϕ⇐⇒ñóùåñòâóåò òàêàÿ íà÷àëüíàÿ òðàññà tr , tr ∈ Tr0 (M),äëÿ êîòîðîé tr 6|= ϕ.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Òàêèì îáðàçîì, âìåñòî çàäà÷è M |= ϕ ìû áóäåì ðàññìàòðèâàòüäðóãóþ çàäà÷ó:íàéòè â LTS M íà÷àëüíóþ òðàññó tr , äëÿ êîòîðîé tr 6|= ϕ.Åñëè òàêîé òðàññû íàéòè íå óäàñòñÿ, òî âåðíî M |= ϕ.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÏðèâåäåíèå ôîðìóëû ê ïîçèòèâíîé ôîðìåÏðèìåíÿÿ ðàâíîñèëüíûå ïðåîáðàçîâàíèÿ, óïðîñòèì ôîðìóëó ϕ.Óäàëåíèå èìïëèêàöèè → è òåìïîðàëüíûõ îïåðàòîðîâíà îñíîâàíèè çàêîíîâ âçàèìíîé çàâèñèìîñòèÝòàï 1.,G F|= ψ → ψ ≡ ¬ψ ∨ χ;|= Fψ ≡ true Uψ ;|= Gψ ≡ false Rψ .Ýòàï 2.

Ïðîäâèæåíèå ¬ âãëóáü ôîðìóëû íà îñíîâàíèè çàêîíîâäâîéñòâåííîñòè|= ¬(ψ&χ) ≡ ¬ψ ∨ ¬χ;|= ¬(ψ ∨ χ) ≡ ¬ψ&¬χ;|= ¬¬ψ ≡ ψ ;|= ¬Xψ ≡ X¬ψ ;|= ¬(ψUχ) ≡ ¬ψR¬χ;|= ¬(ψRχ) ≡ ¬ψU¬χ.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÓòâåðæäåíèå 2. ðåçóëüòàòå ïðèìåíåíèÿ ðàâíîñèëüíûõ ïðåîáðàçîâàíèé ýòàïîâ1 è 2 ëþáàÿ ôîðìóëà PLTL ϕ ïðèâîäèòñÿ ê ðàâíîñèëüíîéôîðìóëå ϕ0 , ïðåäñòàâëåííîé â ïîçèòèâíîé ôîðìå, â êîòîðîéIèñïîëüçóþòñÿ òîëüêî ëîãè÷åñêèå ñâÿçêè ∨, &, ¬ èòåìïîðàëüíûå îïåðàòîðû X, F, G,Iñâÿçêà ¬ ïðèìåíÿåòñÿ òîëüêî ê àòîìàðíûì âûñêàçûâàíèÿìp, p ∈ AP .Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÏðèâåäåíèå ôîðìóëû ê ïîçèòèâíîé ôîðìåÏðèìåð.ϕ = G(free & Xbusy → XF(pr1 ∨ pr2 )).Ýòàï 1.ϕ0 = false R (¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 ))).Ýòàï 2.ϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÏóñòü ϕ1 ôîðìóëà PLTL â ïîçèòèâíîé ôîðìå.

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

å.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 ,ò.