6 Представления неподвижной точки в CTL. Алгоритм символьной верификации моделей в CTL, страница 2
Описание файла
PDF-файл из архива "6 Представления неподвижной точки в CTL. Алгоритм символьной верификации моделей в CTL", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 11 семестр (3 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) . Ñ äðóãîéñòîðîíû, â ñèëó ìîíîòîííîñòè τ ìû èìååìτ (P1 ) ⊆ τ (P2 ) ⊆ . . . Ïîýòîìó τ (Pj ) ⊆ τ (Pj ) äëÿ êàæäîãîj < j0 , è τ (Pj ) = τ (Pj ) äëÿ êàæäîãî j > j0 .  ðåçóëüòàòåïîëó÷àåì ñîîòíîøåíèå ∪i τ (Pi ) = τ (Pj ) , à ýòî îçíà÷àåò, ÷òîïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∪ -íåïðåðûâíûì.
Îáîñíîâàíèå ∩-íåïðåðûâíîñòè ïðåîáðàçîâàòåëÿ τ ïðîâîäèòñÿ àíàëîãè÷íî.0000000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÇàïèñü τ i (Z ) áóäåò îáîçíà÷àòü i -êðàòíîå ïðèìåíåíèå τ ê Z .Áîëåå ñòðîãî τ i (Z ) îïðåäåëÿåòñÿ ðåêóðñèâíî ñîîòíîøåíèÿìèτ 0 (Z ) = Z è τ i+1 (Z ) = τ (τ i (Z )) .Ëåììà 2. Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, òî äëÿëþáîãî íàòóðàëüíîãî ÷èñëà i èìåþò ìåñòî âêëþ÷åíèÿτ i (False) ⊆ τ i+1 (False) è τ i (True) ⊇ τ i+1 (True).Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÇàïèñü τ i (Z ) áóäåò îáîçíà÷àòü i -êðàòíîå ïðèìåíåíèå τ ê Z .Áîëåå ñòðîãî τ i (Z ) îïðåäåëÿåòñÿ ðåêóðñèâíî ñîîòíîøåíèÿìèτ 0 (Z ) = Z è τ i+1 (Z ) = τ (τ i (Z )) .Ëåììà 2. Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, òî äëÿëþáîãî íàòóðàëüíîãî ÷èñëà i èìåþò ìåñòî âêëþ÷åíèÿτ i (False) ⊆ τ i+1 (False) è τ i (True) ⊇ τ i+1 (True).Ëåììà 3.
Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, à S êîíå÷íîå ìíîæåñòâî, òî ñóùåñòâóþò òàêèå íàòóðàëüíûå ÷èñëài0 è j0 , ÷òî äëÿ ëþáîãî i > i0 âåðíî ðàâåíñòâîτ i (False) = τ i (False) , è äëÿ ëþáîãî j > j0 âåðíî ðàâåíñòâîτ j (True) = τ j (True) .00Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÇàïèñü τ i (Z ) áóäåò îáîçíà÷àòü i -êðàòíîå ïðèìåíåíèå τ ê Z .Áîëåå ñòðîãî τ i (Z ) îïðåäåëÿåòñÿ ðåêóðñèâíî ñîîòíîøåíèÿìèτ 0 (Z ) = Z è τ i+1 (Z ) = τ (τ i (Z )) .Ëåììà 2. Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, òî äëÿëþáîãî íàòóðàëüíîãî ÷èñëà i èìåþò ìåñòî âêëþ÷åíèÿτ i (False) ⊆ τ i+1 (False) è τ i (True) ⊇ τ i+1 (True).Ëåììà 3.
Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, à S êîíå÷íîå ìíîæåñòâî, òî ñóùåñòâóþò òàêèå íàòóðàëüíûå ÷èñëài0 è j0 , ÷òî äëÿ ëþáîãî i > i0 âåðíî ðàâåíñòâîτ i (False) = τ i (False) , è äëÿ ëþáîãî j > j0 âåðíî ðàâåíñòâîτ j (True) = τ j (True) .Ëåììà 4.
Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, à S êîíå÷íîå ìíîæåñòâî, òî ñóùåñòâóþò òàêèå íàòóðàëüíûå ÷èñëài0 è j0 , ÷òîµZ . τ (Z ) = τ i (False) è νZ . τ (Z ) = τ j (True)0000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÍà îñíîâàíèè ïðèâåäåííûõ ëåìì äëÿ âû÷èñëåíèÿ íàèìåíüøåéíåïîäâèæíîé òî÷êè ìîíîòîííîãî ïðåîáðàçîâàòåëÿ τ ìîæíîâîñïîëüçîâàòüñÿ ïðîãðàììîéfunctionLfp(Tau : PredicateTransformer ) : PredicateQ := False Q 0 := Tau(Q)0 dowhile Q 6= Q0Q := Q Q 0 := Tau(Q 0 )(;(Q )end whilereturnend function;);;;Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÈíâàðèàíò öèêëàâ òåëå ïðîöåäóðû çàäàåòñÿ îòíîøåíèåì(Q 0 = τ (Q)) ∧ (Q 0 ⊆ µZ . τ (Z )) .Íåòðóäíî çàìåòèòü, ÷òî â íà÷àëå i -é èòåðàöèè öèêëàâûïîëíÿåòñÿ Q ⊆ τ i−1(False) è Q 0 ⊆ τ i (False) .whileÏðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÈíâàðèàíò öèêëàâ òåëå ïðîöåäóðû çàäàåòñÿ îòíîøåíèåì(Q 0 = τ (Q)) ∧ (Q 0 ⊆ µZ .
τ (Z )) .Íåòðóäíî çàìåòèòü, ÷òî â íà÷àëå i -é èòåðàöèè öèêëàâûïîëíÿåòñÿ Q ⊆ τ i−1(False) è Q 0 ⊆ τ i (False) .Èç ëåììû 4 âûòåêàåò False ⊆ τ (False) ⊆ τ 2(False) ⊆ . . .Ïîýòîìó ìàêñèìàëüíîå ÷èñëî èòåðàöèé îïåðàòîðà öèêëàîãðàíè÷åíî êîëè÷åñòâîì ýëåìåíòîâ â S . Ïðè âûõîäå èç öèêëà,Q = τ (Q) è Q ⊆ µZ . τ (Z ) . Òàê êàê Q ÿâëÿåòñÿ íåïîäâèæíîéòî÷êîé, µZ . τ (Z ) ⊆ Q , è ïîýòîìó Q = µZ . τ (Z ) .
Òåì ñàìûìïîêàçàíî, ÷òî çíà÷åíèå, êîòîðîå âîçâðàùàåò ïðîöåäóðà, ýòîäåéñòâèòåëüíî íàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà.whileÏðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÍàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà âû÷èñëÿåòñÿ ïîäîáíûì æåîáðàçîì ïðè ïîìîùè äðóãîé ïðîãðàììû. Ïðèìåíÿÿ ïî ñóòèäåëà òó æå ñàìóþ àðãóìåíòàöèþ, ìîæíî ïîêàçàòü, ÷òî è ýòàïðîöåäóðà âñåãäà çàâåðøàåò ñâîè âû÷èñëåíèÿ è âîçâðàùàåò âêà÷åñòâå çíà÷åíèÿ νZ .
τ (Z ) .functionGfp(Tau : PredicateTransformer ) : PredicateQ := True Q 0 := Tau(Q)0 dowhile Q 6= Q0Q := Q Q 0 := Tau(Q 0 )(;(Q )end whilereturnend function;);;;Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûÅñëè ñîïîñòàâèòü êàæäîé ôîðìóëå f ïðåäèêàò {s | M, s |= f }íà ℘(S) , òî êàæäûé òåìïîðàëüíûé îïåðàòîð CTL ìîæíîîïèñàòü â òåðìèíàõ íàèìåíüøåé èëè íàèáîëüøåé íåïîäâèæíîéòî÷êè ïîäõîäÿùåãî ïðåîáðàçîâàòåëÿ ïðåäèêàòîâ. Ìû îáîñíóåìîïèñàíèÿ â òåðìèíàõ íåïîäâèæíûõ òî÷åê òîëüêî äëÿ è .If1 = νZ . f1 ∧Z,I[f1 f2 ] = µZ . f2 ∨ (f1 ∧Z) ,Èíòóèòèâíî ïîíÿòíî, ÷òî íàèìåíüøèå íåïîäâèæíûå òî÷êèñîîòâåòñòâóþò ñâîéñòâàì, êîòîðûå äîëæíû âûïîëíÿòüñÿêîãäà-íèáóäü, à íàèáîëüøèå íåïîäâèæíûå òî÷êè ñîîòâåòñòâóþòñâîéñòâàì, êîòîðûå äîëæíû âûïîëíÿòüñÿ âñåãäà. Ïîýòîìóf1 õàðàêòåðèçóåòñÿ ïðè ïîìîùè íàèìåíüøåé íåïîäâèæíîéòî÷êè, à f1 èìååò îïèñàíèå â òåðìèíàõ íàèáîëüøåéíåïîäâèæíîé òî÷êè.EGEGEEXUAFEGEXEUÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5.
Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧EXZìîíîòîííûé.Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5. Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧Äîê-âî. Ïðåäïîëîæèì, ÷òî P1 ⊆ P2 .EXZìîíîòîííûé.Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5. Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧ Z ìîíîòîííûé.Äîê-âî. Ïðåäïîëîæèì, ÷òî P1 ⊆ P2 . ×òîáû ïðîâåðèòüâêëþ÷åíèå τ (P1) ⊆ τ (P2) , âîçüìåì ïðîèçâîëüíîå ñîñòîÿíèås ∈ τ (P1 ) . Òîãäà s |= f1 è ñóùåñòâóåò òàêîå ñîñòîÿíèå s 0 , ÷òî(s, s 0 ) ∈ R è s 0 ∈ P1 .EXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5. Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧ Z ìîíîòîííûé.Äîê-âî. Ïðåäïîëîæèì, ÷òî P1 ⊆ P2 . ×òîáû ïðîâåðèòüâêëþ÷åíèå τ (P1) ⊆ τ (P2) , âîçüìåì ïðîèçâîëüíîå ñîñòîÿíèås ∈ τ (P1 ) .
Òîãäà s |= f1 è ñóùåñòâóåò òàêîå ñîñòîÿíèå s 0 , ÷òî(s, s 0 ) ∈ R è s 0 ∈ P1 . Íî ââèäó òîãî ÷òî P1 ⊆ P2 , âåðíî òàêæå èâêëþ÷åíèå s 0 ∈ P2 .EXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5. Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧ Z ìîíîòîííûé.Äîê-âî. Ïðåäïîëîæèì, ÷òî P1 ⊆ P2 . ×òîáû ïðîâåðèòüâêëþ÷åíèå τ (P1) ⊆ τ (P2) , âîçüìåì ïðîèçâîëüíîå ñîñòîÿíèås ∈ τ (P1 ) . Òîãäà s |= f1 è ñóùåñòâóåò òàêîå ñîñòîÿíèå s 0 , ÷òî(s, s 0 ) ∈ R è s 0 ∈ P1 .
Íî ââèäó òîãî ÷òî P1 ⊆ P2 , âåðíî òàêæå èâêëþ÷åíèå s 0 ∈ P2 . Çíà÷èò, s ∈ τ (P2) .EXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 6. Ïóñòü τ (Z ) = f1 ∧ Z . Îáîçíà÷èì ÷åðåç τ i (True)ïðåäåë ïîñëåäîâàòåëüíîñòè True ⊇ τ (True) ⊇ . . . Òîãäà äëÿëþáîãî ñîñòîÿíèÿ s èç τ i (True) ìû èìååì s |= f1 è, êðîìåòîãî, íàéäåòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî (s, s 0) ∈ R ès 0 ∈ τ i (True) .EX000Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 6. Ïóñòü τ (Z ) = f1 ∧ Z . Îáîçíà÷èì ÷åðåç τ i (True)ïðåäåë ïîñëåäîâàòåëüíîñòè True ⊇ τ (True) ⊇ . . . Òîãäà äëÿëþáîãî ñîñòîÿíèÿ s èç τ i (True) ìû èìååì s |= f1 è, êðîìåòîãî, íàéäåòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî (s, s 0) ∈ R ès 0 ∈ τ i (True) .Äîê-âî. Ïðåäïîëîæèì, ÷òî s ∈ τ i (True) . Ïîñêîëüêó ïðåäèêàòτ i (True) ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîé τ , èìååò ìåñòîðàâåíñòâî τ i (True) = τ (τ i (True)) .0EX000000Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 6. Ïóñòü τ (Z ) = f1 ∧ Z .
Îáîçíà÷èì ÷åðåç τ i (True)ïðåäåë ïîñëåäîâàòåëüíîñòè True ⊇ τ (True) ⊇ . . . Òîãäà äëÿëþáîãî ñîñòîÿíèÿ s èç τ i (True) ìû èìååì s |= f1 è, êðîìåòîãî, íàéäåòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî (s, s 0) ∈ R ès 0 ∈ τ i (True) .Äîê-âî. Ïðåäïîëîæèì, ÷òî s ∈ τ i (True) . Ïîñêîëüêó ïðåäèêàòτ i (True) ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîé τ , èìååò ìåñòîðàâåíñòâî τ i (True) = τ (τ i (True)) . Òàêèì îáðàçîì,s ∈ τ (τ i (True)) .0EX0000000Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 6. Ïóñòü τ (Z ) = f1 ∧ Z . Îáîçíà÷èì ÷åðåç τ i (True)ïðåäåë ïîñëåäîâàòåëüíîñòè True ⊇ τ (True) ⊇ . .
. Òîãäà äëÿëþáîãî ñîñòîÿíèÿ s èç τ i (True) ìû èìååì s |= f1 è, êðîìåòîãî, íàéäåòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî (s, s 0) ∈ R ès 0 ∈ τ i (True) .Äîê-âî. Ïðåäïîëîæèì, ÷òî s ∈ τ i (True) . Ïîñêîëüêó ïðåäèêàòτ i (True) ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîé τ , èìååò ìåñòîðàâåíñòâî τ i (True) = τ (τ i (True)) .
Òàêèì îáðàçîì,s ∈ τ (τ i (True)) . Ïî îïðåäåëåíèþ ïðåîáðàçîâàòåëÿ τ ïîëó÷àåì,÷òî s |= f1 è, êðîìå òîãî, èìååòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî(s, s 0 ) ∈ R è s 0 ∈ τ i (True) .0EX00000000Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .EGEXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî. Ïðåäïîëîæèì, ÷òî s0 |= f1 .EGEXEGÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî. Ïðåäïîëîæèì, ÷òî s0 |= f1 .
Òîãäà ïî îïðåäåëåíèþîòíîøåíèÿ âûïîëíèìîñòè |= ñóùåñòâóåò òàêîé ïóòü s0, s1, . . . âM , ÷òî äëÿ âñÿêîãî k èìååò ìåñòî ñîîòíîøåíèå sk |= f1 .EGEXEGÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî. Ïðåäïîëîæèì, ÷òî s0 |= f1 . Òîãäà ïî îïðåäåëåíèþîòíîøåíèÿ âûïîëíèìîñòè |= ñóùåñòâóåò òàêîé ïóòü s0, s1, .
. . âM , ÷òî äëÿ âñÿêîãî k èìååò ìåñòî ñîîòíîøåíèå sk |= f1 .Îòñþäà ñëåäóåò, ÷òî s0 |= f1 è s1 |= f1 . Èíûìè ñëîâàìè,s0 |= f1 è s0 |=f1 .EGEXEGEGEX EGÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî. Ïðåäïîëîæèì, ÷òî s0 |= f1 . Òîãäà ïî îïðåäåëåíèþîòíîøåíèÿ âûïîëíèìîñòè |= ñóùåñòâóåò òàêîé ïóòü s0, s1, . . .
âM , ÷òî äëÿ âñÿêîãî k èìååò ìåñòî ñîîòíîøåíèå sk |= f1 .Îòñþäà ñëåäóåò, ÷òî s0 |= f1 è s1 |= f1 . Èíûìè ñëîâàìè,f1 ⊆ f1 ∧f1 .s0 |= f1 è s0 |=f1 . ÏîýòîìóEGEXEGEGEX EGEGEX EGÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî. Ïðåäïîëîæèì, ÷òî s0 |= f1 . Òîãäà ïî îïðåäåëåíèþîòíîøåíèÿ âûïîëíèìîñòè |= ñóùåñòâóåò òàêîé ïóòü s0, s1, . . . âM , ÷òî äëÿ âñÿêîãî k èìååò ìåñòî ñîîòíîøåíèå sk |= f1 .Îòñþäà ñëåäóåò, ÷òî s0 |= f1 è s1 |= f1 .
