Лекция 8. Отношения бисимуляционной эквивалентности, страница 4
Описание файла
PDF-файл из архива "Лекция 8. Отношения бисимуляционной эквивалентности", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 4 страницы из PDF
. . , vn } èìîäåëü ñèíõðîííîé ñõåìû M = (S, R, S0, L) íàä ìíîæåñòâîìïåðåìåííûõ V , ãäåI S = {0, 1}n ìíîæåñòâî âñåõ âîçìîæíûõ çíà÷åíèéïåðåìåííûõèç V ;Vn0I R =i=1 [vi = fi (V )] ;I L(s) = {vi | s(vi ) = 1, 1 ≤ i ≤ n} ;I S0 ⊆ S .Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÏðåäïîëîæèì, ÷òî ìû ðåäóöèðóåì ñõåìó îòíîñèòåëüíî êîíóñàâëèÿíèÿ C = {v1, . . . , vk } äëÿ íåêîòîðîãî k ≤ n .Óïðîùåííàÿ ìîäåëü èìååò âèä red(M, C ) = (S 0, R 0, S00 , L0) , ãäåI S 0 = {0, 1}k ìíîæåñòâî âñåõ âîçìîæíûõ çíà÷åíèéïåðåìåííûõèç C ;Vk00I R =i=1 [vi = fi (V )] ;I L0 (s 0 ) = {vi | s 0 (vi ) = 1, 1 ≤ i ≤ k} ;I S 0 = {(d 0 , .
. . , d 0 ) | ñóùåñòâóþò òàêèå áèòû (dk+1 , . . . , dn ) ,01k÷òî (d10 , . . . , dk0 , dk+1, . . . , dn ) ∈ S0} .Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÎáîçíà÷èì çàïèñüþ M|C ïðîåêöèþ ìîäåëè M íà êîíóñâëèÿíèÿ C , ò.å. M|C = (S, R, S0, L|C ) , ãäå L|C (s) = L(s) ∩ Cäëÿ ëþáîãî ñîñòîÿíèÿ s, s ∈ S .Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÎáîçíà÷èì çàïèñüþ M|C ïðîåêöèþ ìîäåëè M íà êîíóñâëèÿíèÿ C , ò.å. M|C = (S, R, S0, L|C ) , ãäå L|C (s) = L(s) ∩ Cäëÿ ëþáîãî ñîñòîÿíèÿ s, s ∈ S .Óòâåðæäåíèå 9.Äëÿ ëþáîé CTL∗-ôîðìóëû ϕ , çàâèñÿùåé òîëüêî îò àòîìàðíûõâûñêàçûâàíèé èç ìíîæåñòâà C , âåðíî ñîîòíîøåíèåM |= ϕ ⇐⇒ M|C |= ϕ.Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÎáîçíà÷èì çàïèñüþ M|C ïðîåêöèþ ìîäåëè M íà êîíóñâëèÿíèÿ C , ò.å.
M|C = (S, R, S0, L|C ) , ãäå L|C (s) = L(s) ∩ Cäëÿ ëþáîãî ñîñòîÿíèÿ s, s ∈ S .Óòâåðæäåíèå 9.Äëÿ ëþáîé CTL∗-ôîðìóëû ϕ , çàâèñÿùåé òîëüêî îò àòîìàðíûõâûñêàçûâàíèé èç ìíîæåñòâà C , âåðíî ñîîòíîøåíèåM |= ϕ ⇐⇒ M|C |= ϕ.Óòâåðæäåíèå 10.Ìîäåëè M|C è red(M, C ) áèñèìóëÿöèîííî ýêâèâàëåíòíû.Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÎáîçíà÷èì çàïèñüþ M|C ïðîåêöèþ ìîäåëè M íà êîíóñâëèÿíèÿ C , ò.å. M|C = (S, R, S0, L|C ) , ãäå L|C (s) = L(s) ∩ Cäëÿ ëþáîãî ñîñòîÿíèÿ s, s ∈ S .Óòâåðæäåíèå 9.Äëÿ ëþáîé CTL∗-ôîðìóëû ϕ , çàâèñÿùåé òîëüêî îò àòîìàðíûõâûñêàçûâàíèé èç ìíîæåñòâà C , âåðíî ñîîòíîøåíèåM |= ϕ ⇐⇒ M|C |= ϕ.Óòâåðæäåíèå 10.Ìîäåëè M|C è red(M, C ) áèñèìóëÿöèîííî ýêâèâàëåíòíû.Ïîêàæèòå, ÷òî îòíîøåíèå B ⊆ S × S 0 , òàêîå÷òî ((d1, .
. . , dn ), (d10 , . . . , dk0 )) ∈ B ⇐⇒ d1 = d10 , . . . , dk = dk0 .ÿâëÿåòñÿ îòíîøåíèåì áèñèìóëÿöèè ìåæäó M|C è red(M, C ) .Äîêàçàòåëüñòâî.Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÒåîðåìà 6.Äëÿ ëþáîé ìîäåëè M , êîíóñà âëèÿíèÿ C è ïðîèçâîëüíîéCTL∗-ôîðìóëû ϕ , çàâèñÿùåé òîëüêî îò àòîìàðíûõâûñêàçûâàíèé èç ìíîæåñòâà C , âåðíî ñîîòíîøåíèåM |= ϕ ⇐⇒ red(M, C ) |= ϕ.Àáñòðàêöèÿ äàííûõÀáñòðàêöèÿ äàííûõ îïðåäåëÿåòñÿ îòîáðàæåíèåì ôàêòè÷åñêèõçíà÷åíèé äàííûõ ñèñòåìû â íåáîëüøîå ìíîæåñòâî àáñòðàêòíûõçíà÷åíèé äàííûõ.
Ðàñïðîñòðàíèâ ýòî îòîáðàæåíèå íà ñîñòîÿíèÿè ïåðåõîäû, ìîæíî ïîñòðîèòü àáñòðàêòíûé âàðèàíòàíàëèçèðóåìîé ñèñòåìû.Àáñòðàêòíàÿ ñèñòåìà îêàçûâàåòñÿ ãîðàçäî ìåíüøå ðåàëüíîéñèñòåìû, è ïîýòîìó íà àáñòðàêòíîì óðîâíå ïðîâåðÿòü ñâîéñòâàïîâåäåíèÿ ìîäåëè çíà÷èòåëüíî ïðîùå. Êîððåêòíîñòü ïðîâåðêèîáåñïå÷èâàåò îòíîøåíèå ñèìóëÿöèè, ïîääåðæèâàåìîå ìåæäóèñõîäíîé ìîäåëüþ è åå àáñòðàêöèåé.Àáñòðàêöèÿ äàííûõÏóñòü çàäàíà íåêîòîðàÿ ìîäåëü M = (AP, S, R, S0, L) èðàçáèåíèå H = (D1, D2, . .
. , Dk ) ïðîñòðàíñòâà åå ñîñòîÿíèé S ,ñîãëàñîâàííîå ñ ôóíêöèåé ðàçìåòêè L , ò.å. óäîâëåòâîðÿþùååóñëîâèþ ðàâåíñòâà L(s 0) = L(s 00) äëÿ ëþáîé ïàðû ñîñòîÿíèés 0 , s 00 èç ëþáîãî áëîêà Bj , 1 ≤ j ≤ k .Àáñòðàêöèÿ äàííûõÏóñòü çàäàíà íåêîòîðàÿ ìîäåëü M = (AP, S, R, S0, L) èðàçáèåíèå H = (D1, D2, . . . , Dk ) ïðîñòðàíñòâà åå ñîñòîÿíèé S ,ñîãëàñîâàííîå ñ ôóíêöèåé ðàçìåòêè L , ò.å. óäîâëåòâîðÿþùååóñëîâèþ ðàâåíñòâà L(s 0) = L(s 00) äëÿ ëþáîé ïàðû ñîñòîÿíèés 0 , s 00 èç ëþáîãî áëîêà Bj , 1 ≤ j ≤ k .Àáñòðàêöèÿ, ïîðîæäåííàÿ ðàçáèåíèåìÀáñòðàêöèåé ìîäåëè M , ïîðîæäåííîé ðàçáèåíèåì Híàçûâàåòñÿ ìîäåëü abstr (M, H) = (AP, S 0, R 0, S00 , L0) , â êîòîðîéI S =H ,I R 0 = {(Di , Dj ) : (si , sj ) ∈ R äëÿ íåêîòîðîé ïàðû ñîñòîÿíèési ∈ Di , sj ∈ Dj } ,I S 0 = {Di : Di ∩ S0 6= ∅} ,0I L0 (Di ) = L(si ) , ãäå si ïðîèçâîëüíîå ñîñòîÿíèå èç áëîêàDi .Àáñòðàêöèÿ äàííûõÏðèìåð àáñòðàêöèè, ïîðîæäåííîé ðàçáèåíèåìMr r r - −3 - −2 - −1 - 0- 1- 2- r r r {p}{p}{p}∅{q}{q}Àáñòðàêöèÿ äàííûõÏðèìåð àáñòðàêöèè, ïîðîæäåííîé ðàçáèåíèåìMr r r - −3 - −2 - −1 - 0- 1- 2- r r r {p}Ðàçáèåíèå{p}H{p}∅{q}{q}: D1 = {.
. . , −3, −2, −1}, D2 = {0}, D3 = {1, 2, . . . }Àáñòðàêöèÿ äàííûõÏðèìåð àáñòðàêöèè, ïîðîæäåííîé ðàçáèåíèåìMr r r - −3 - −2 - −1 - 0- 1- 2- r r r {p}Ðàçáèåíèå{p}H{p}∅{q}{q}: D1 = {. . . , −3, −2, −1}, D2 = {0}, D3 = {1, 2, . . . }abstr (M, H) - D1{p}- D2∅ - D3 {q}Àáñòðàêöèÿ äàííûõÓòâåðæäåíèå 11.Äëÿ ëþáîé ìîäåëè M è ðàçáèåíèÿ H ïðîñòðàíñòâà ååñîñòîÿíèé, ñîãëàñîâàííîãî ñ åå ôóíêöèåé ðàçìåòêè,âûïîëíÿåòñÿ îòíîøåíèå M abstr (M, H) .Àáñòðàêöèÿ äàííûõÓòâåðæäåíèå 11.Äëÿ ëþáîé ìîäåëè M è ðàçáèåíèÿ H ïðîñòðàíñòâà ååñîñòîÿíèé, ñîãëàñîâàííîãî ñ åå ôóíêöèåé ðàçìåòêè,âûïîëíÿåòñÿ îòíîøåíèå M abstr (M, H) .Òåîðåìà 7.Äëÿ ëþáîé ìîäåëè M , ðàçáèåíèÿ H ïðîñòðàíñòâà ååñîñòîÿíèé, ñîãëàñîâàííîãî ñ åå ôóíêöèåé ðàçìåòêè, èïðîèçâîëüíîé ACTL-ôîðìóëû ϕ âåðíî ñîîòíîøåíèåabstr (M, H) |= ϕ =⇒ M |= ϕ.ÊÎÍÅÖ ËÅÊÖÈÈ 8..
