6 Представления неподвижной точки в CTL. Алгоритм символьной верификации моделей в CTL

Âåðèôèêàöèÿìîäåëåé ïðîãðàììËÅÊÒÎÐ:Âëàäèìèð Àíàòîëüåâè÷ Çàõàðîâzakh@cs.msu.suËåêöèÿ 6.Ñèìâîëüíûé àëãîðèòìâåðèôèêàöèè ìîäåëåé äëÿ CTL1.Ïðåäïîñûëêè äëÿ ñèìâîëüíûõàëãîðèòìîâ âåðèôèêàöèè2.Ïðåäñòàâëåíèÿ íåïîäâèæíîéòî÷êè3.Íåïîäâèæíûå òî÷êè èòåìïîðàëüíûå îïåðàòîðû4.Ñèìâîëüíàÿ âåðèôèêàöèÿìîäåëåé äëÿ CTLÏðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;2. Äëÿ ROBDD èìåþòñÿ ýôôåêòèâíûå ïðîöåäóðûf (x̄) = g (x̄) ,f (x̄){xi /c} ,îïåðàöèé f (x̄) ∗ g (x̄) ;I ïðîâåðêè ðàâåíñòâà áóëåâûõ ôóíêöèéI ïîäñòàíîâêè êîíñòàíòI âû÷èñëåíèÿ áóëåâûõÏðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;2.

Äëÿ ROBDD èìåþòñÿ ýôôåêòèâíûå ïðîöåäóðûf (x̄) = g (x̄) ,f (x̄){xi /c} ,îïåðàöèé f (x̄) ∗ g (x̄) ;I ïðîâåðêè ðàâåíñòâà áóëåâûõ ôóíêöèéI ïîäñòàíîâêè êîíñòàíòI âû÷èñëåíèÿ áóëåâûõ3. Ìíîæåñòâî ñîñòîÿíèé S ìîäåëè Êðèïêå M = (S, S0, R, L)êîäèðóåòñÿ äâîè÷íûìè íàáîðàìè (σ1, σ2, . .

. , σn ) ;Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;2. Äëÿ ROBDD èìåþòñÿ ýôôåêòèâíûå ïðîöåäóðûf (x̄) = g (x̄) ,f (x̄){xi /c} ,îïåðàöèé f (x̄) ∗ g (x̄) ;I ïðîâåðêè ðàâåíñòâà áóëåâûõ ôóíêöèéI ïîäñòàíîâêè êîíñòàíòI âû÷èñëåíèÿ áóëåâûõ3. Ìíîæåñòâî ñîñòîÿíèé S ìîäåëè Êðèïêå M = (S, S0, R, L)êîäèðóåòñÿ äâîè÷íûìè íàáîðàìè (σ1, σ2, . . .

, σn ) ;4. Îòíîøåíèå ïåðåõîäîâ R ìîäåëè Êðèïêå M = (S, S0, R, L)ðàññìàòðèâàåòñÿ êàê áóëåâà ôóíêöèÿ R(x̄, x̄ 0) , êîòîðàÿçàâèñèò îò ïåðåìåííûõ, ïðåäñòàâëÿþùèõ ñîñòîÿíèÿìîäåëè;Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;2. Äëÿ ROBDD èìåþòñÿ ýôôåêòèâíûå ïðîöåäóðûf (x̄) = g (x̄) ,f (x̄){xi /c} ,îïåðàöèé f (x̄) ∗ g (x̄) ;I ïðîâåðêè ðàâåíñòâà áóëåâûõ ôóíêöèéI ïîäñòàíîâêè êîíñòàíòI âû÷èñëåíèÿ áóëåâûõ3. Ìíîæåñòâî ñîñòîÿíèé S ìîäåëè Êðèïêå M = (S, S0, R, L)êîäèðóåòñÿ äâîè÷íûìè íàáîðàìè (σ1, σ2, .

. . , σn ) ;4. Îòíîøåíèå ïåðåõîäîâ R ìîäåëè Êðèïêå M = (S, S0, R, L)ðàññìàòðèâàåòñÿ êàê áóëåâà ôóíêöèÿ R(x̄, x̄ 0) , êîòîðàÿçàâèñèò îò ïåðåìåííûõ, ïðåäñòàâëÿþùèõ ñîñòîÿíèÿìîäåëè;5. Ôóíêöèÿ ðàçìåòêè L ìîäåëè Êðèïêå M = (S, S0, R, L)ðàññìàòðèâàåòñÿ êàê íàáîð áóëåâûõ ôóíêöèéLp (x̄), p ∈ AP , âûäåëÿþùèõ òå ñîñòîÿíèÿ, íà êîòîðûõâûïîëíèìû àòîìàðíûå ôîðìóëû.Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèèÎïåðàöèè íàä ìíîæåñòâàìè è îòíîøåíèÿìè ìîäåëèðóþòñÿîïåðàöèÿìè íàä áóëåâûìè ôóíêöèÿìè:I ïåðåñå÷åíèå: A ∩ B = C =⇒ fC = fA ∧ fB ,I îáúåäèíåíèå: A ∪ B = C =⇒ fC = fA ∨ fB ,I äîïîëíåíèå: S \ A = C =⇒ fC = ¬fA ,I îáðàç: R(A) = C =⇒ fC = ∃x̄(fA (x̄) ∧ R(x̄, ȳ )) ,I ïðîîáðàç: R −1 (A) = C =⇒ fC = ∃ȳ (fA (ȳ ) ∧ R(x̄, ȳ )) .Çäåñü ∃y h(x, y ) = h(x, 0) ∨ h(x, 1) .Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèèÀëãîðèòìû àíàëèçà ìîäåëåé, èñïîëüçóþùèå èõ ïðåäñòàâëåíèÿâ âèäå OBDD, íàçûâàþòñÿ ñèìâîëüíûì èëè íåÿâíûìè ,ïîñêîëüêó îí îïåðèðóåò íå ñ ñàìèìè ìíîæåñòâàìè, ýëåìåíòûêîòîðûõ ÿâíî ïåðå÷èñëåíû, à ñ ñèìâîëüíûìè îïèñàíèÿìè(ïðåäñòàâëåíèÿìè) ìíîæåñòâ.Êîãäà ìîäåëü èìååò áîëüøîé ðàçìåð (≥ 232 ), ïðèõîäèòñÿîïåðèðîâàòü ñ öåëûìè ìíîæåñòâàìè, à íå ñ îòäåëüíûìèñîñòîÿíèÿìè è ïåðåõîäàìè.

Òàáëè÷íûå àëãîðèòìû modelchecking äëÿ ýòîé öåëè íåïðèãîäíû. Íóæíû èòåðàòèâíûåàëãîðèòìû, ðàáîòàþùèå ñ îïèñàíèÿìè ìíîæåñòâ.Äëÿ ýòîãî âîñïîëüçóåìñÿ îïðåäåëåíèåì îïåðàòîðîâòåìïîðàëüíîé ëîãèêè â òåðìèíàõ íåïîäâèæíîé òî÷êè .Ïîêàæåì, êàê îïèñàòü ìíîæåñòâî ñîñòîÿíèé, óäîâëåòâîðÿþùèõíåêîòîðîé CTL-ôîðìóëå, ïðè ïîìîùè íàèìåíüøåé èëèíàèáîëüøåé íåïîäâèæíîé òî÷êè ïîäõîäÿùåé ôóíêöèè.Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÏóñòü çàäàíà ïðîèçâîëüíàÿ ìîäåëü Êðèïêå M = (S, S0, R, L) ñêîíå÷íûì ìíîæåñòâîì ñîñòîÿíèé.Ñîâîêóïíîñòü ℘(S) âñåõ ïîäìíîæåñòâ ìíîæåñòâà S îáðàçóåòðåøåòêó ïî îòíîøåíèþ âêëþ÷åíèÿ ⊆ :I òî÷íàÿ âåðõíÿÿ ãðàíü sup(S1 , S2 ) = S1 ∪ S2 ,I òî÷íàÿ íèæíÿÿ ãðàíü inf (S1 , S2 ) = S1 ∩ S2 ,Âñÿêèé ýëåìåíò S 0 ðåøåòêè (℘(S), ⊆) ìîæåò ðàññìàòðèâàòüñÿêàê ïðåäèêàò (îòíîøåíèå) íà S , ïðèíèìàþùèé çíà÷åíèå true âòî÷íîñòè íà âñåõ ñîñòîÿíèÿõ èç S 0 .Íàèìåíüøèì ýëåìåíòîì ðåøåòêè ÿâëÿåòñÿ ïóñòîå ìíîæåñòâî,êîòîðîå áóäåò îáîçíà÷àòüñÿ False , à íàèáîëüøèì ýëåìåíòîìðåøåòêè ñëóæèò ñàìî ìíîæåñòâî S , êîòîðîå ìû áóäåìîáîçíà÷àòü True .Ôóíêöèþ, îòîáðàæàþùóþ ℘(S) â ℘(S) , áóäåì íàçûâàòüïðåîáðàçîâàòåëåì ïðåäèêàòîâ .Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÏóñòü τ : ℘(S) → ℘(S) îäèí èç òàêèõ ïðåîáðàçîâàòåëåéïðåäèêàòîâ.

Òîãäà1) Ôóíêöèÿ τ ñ÷èòàåòñÿ ìîíîòîííîé , åñëè èç âêëþ÷åíèÿP ⊆ Q ñëåäóåò τ (P) ⊆ τ (Q) ;2) Ôóíêöèÿ τ ñ÷èòàåòñÿ ∪-íåïðåðûâíîé , åñëè äëÿ âñÿêîéìîíîòîííî íåóáûâàþùåé ïîñëåäîâàòåëüíîñòèïðåäèêàòîâ∞∞SSτ (Pi ) ;P1 ⊆ P2 ⊆ . . . âåðíî ðàâåíñòâî τ ( Pi ) =i=1i=13) Ôóíêöèÿ τ ñ÷èòàåòñÿ ∩-íåïðåðûâíîé , åñëè äëÿ âñÿêîéìîíîòîííî íåâîçðàñòàþùåé ïîñëåäîâàòåëüíîñòè∞∞ïðåäèêàòîâ P1 ⊇ P2 ⊇ .

. . âåðíî τ ( T Pi ) = T τ (Pi )i=1i=1Ïðåäèêàò P íàçûâàåòñÿ íåïîäâèæíîé òî÷êîé ïðåîáðàçîâàòåëÿτ , åñëè èìååò ìåñòî ðàâåíñòâî τ (P) = P .Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÓ ìîíîòîííîãî ïðåîáðàçîâàòåëÿ τ íà ℘(S) âñåãäà åñòüíàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà µZ . τ (Z ) èíàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà νZ . τ (Z )Íàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà èìååò âèäµZ . τ (Z ) = ∩{Z | τ (Z ) ⊆ Z }äëÿ ìîíîòîííîãîτ , è ïðè ýòîì∞Sτ i (False),µZ .

τ (Z ) =i=1åñëè ïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∪ -íåïðåðûâíûì.Àíàëîãè÷íî, íàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà èìååò âèäνZ . τ (Z ) = ∪{Z | τ (Z ) ⊇ Z }τ∞TµZ . τ (Z ) =τ i (True)äëÿ ìîíîòîííîãî , è ïðè ýòîì,i=1åñëè ïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∩ -íåïðåðûâíûì.Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÓ ìîíîòîííîãî ïðåîáðàçîâàòåëÿ τ íà ℘(S) âñåãäà åñòüíàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà µZ . τ (Z ) èíàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà νZ . τ (Z )Íàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà èìååò âèäµZ . τ (Z ) = ∩{Z | τ (Z ) ⊆ Z }äëÿ ìîíîòîííîãîτ , è ïðè ýòîì∞Sτ i (False),µZ .

τ (Z ) =i=1åñëè ïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∪ -íåïðåðûâíûì.Àíàëîãè÷íî, íàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà èìååò âèäνZ . τ (Z ) = ∪{Z | τ (Z ) ⊇ Z }τ∞TµZ . τ (Z ) =τ i (True)äëÿ ìîíîòîííîãî , è ïðè ýòîì,i=1åñëè ïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∩ -íåïðåðûâíûì.Ïîïðîáóéòå äîêàçàòü ñàìîñòîÿòåëüíî. Ýòî íåñëîæíûéìàòåìàòè÷åñêèé ýòþä èç òåîðèè ìíîæåñòâ.Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . .

.ïîäìíîæåñòâ ìíîæåñòâà S .Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . . .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 .

Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 .00Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ .

. .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 . Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 . Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) .0000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . .

.ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 . Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 . Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) . Ñ äðóãîéñòîðîíû, â ñèëó ìîíîòîííîñòè τ ìû èìååì0000τ (P1 ) ⊆ τ (P2 ) ⊆ . . .Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . . .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 .

Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 . Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) . Ñ äðóãîéñòîðîíû, â ñèëó ìîíîòîííîñòè τ ìû èìååìτ (P1 ) ⊆ τ (P2 ) ⊆ . . . Ïîýòîìó τ (Pj ) ⊆ τ (Pj ) äëÿ êàæäîãîj < j0 , è τ (Pj ) = τ (Pj ) äëÿ êàæäîãî j > j0 .000000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1.

Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . . .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 . Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 . Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) .

Ñ äðóãîéñòîðîíû, â ñèëó ìîíîòîííîñòè τ ìû èìååìτ (P1 ) ⊆ τ (P2 ) ⊆ . . . Ïîýòîìó τ (Pj ) ⊆ τ (Pj ) äëÿ êàæäîãîj < j0 , è τ (Pj ) = τ (Pj ) äëÿ êàæäîãî j > j0 .  ðåçóëüòàòåïîëó÷àåì ñîîòíîøåíèå ∪i τ (Pi ) = τ (Pj ) , à ýòî îçíà÷àåò, ÷òîïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∪ -íåïðåðûâíûì.0000000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1.

Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . . .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 . Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 .