Лекция 8. Отношения бисимуляционной эквивалентности, страница 3

. . , Dk } îòíîñèòåëüíîáëîêà E íàçûâàåòñÿñåìåéñòâî áëîêîânSRef (Π|E ) =Ref (Di |E ) .i=1Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÓòî÷íåíèåì áëîêà D îòíîñèòåëüíî áëîêà E íàçûâàåòñÿñåìåéñòâî áëîêîâ Ref (D|E ) , ñîñòîÿùåå èçI ïàðû áëîêîâ D 0 , D 00 , ãäåD 0 = {s 0 : s 0 ∈ D, ({s 0 } × E ) ∩ R 6= ∅} ,D 00 = {s 00 : s 00 ∈ D, ({s 00 } × E ) ∩ R = ∅} ,åñëè áëîê E ðàçâåòâèòåëü áëîêà D ,I åäèíñòâåííîãî áëîêà D â ïðîòèâíîì ñëó÷àå.Óòî÷íåíèåì ñåìåéñòâà áëîêîâ Π = {D1, .

. . , Dk } îòíîñèòåëüíîáëîêà E íàçûâàåòñÿñåìåéñòâî áëîêîânSRef (Π|E ) =Ref (Di |E ) .i=1Óòî÷íåíèåì ðàçáèåíèÿ Π = {D1, . . . , Dk } íàçûâàåòñÿ ðàçáèåíèåRef (Π) = Ref (. . . Ref (Ref (Π|D1 )|D2 )| . . . |Dk ).Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÀëãîðèòì âû÷èñëåíèÿ ðàçáèåíèÿS/≈.1. Âû÷èñëåíèå íà÷àëüíîãî ðàçáèåíèÿ Π0 .Ââåäåì îòíîøåíèå ýêâèâàëåíòíîñòè RL íà ìíîæåñòâåñîñòîÿíèé S :(s 0 , s 00 ) ∈ RL ⇔ L(s 0 ) = L(s 00 ).è ïîëîæèì Π0 = S/R .LÂû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÀëãîðèòì âû÷èñëåíèÿ ðàçáèåíèÿS/≈.1. Âû÷èñëåíèå íà÷àëüíîãî ðàçáèåíèÿ Π0 .Ââåäåì îòíîøåíèå ýêâèâàëåíòíîñòè RL íà ìíîæåñòâåñîñòîÿíèé S :(s 0 , s 00 ) ∈ RL ⇔ L(s 0 ) = L(s 00 ).è ïîëîæèì Π0 = S/R .2.

Èòåðàòèâíîå âû÷èñëåíèå S/≈ .LdoΠi+1 := Ref (Πi )untilΠi = Πi+1Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÀëãîðèòì âû÷èñëåíèÿ ðàçáèåíèÿÏðèìåð.M{a} s0@@@?{a} s2∅?- s4 {a} - s1 @ @ R s3 @{a} ∅ ?s5S/≈.Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÀëãîðèòì âû÷èñëåíèÿ ðàçáèåíèÿÏðèìåð.M@@∅?- s4 D1@{a} s2.{a} Π0 = [{s0 , s1 , s2 , s3 }; {s4 , s5 }]- s1 {z} | {z }|{a} s0?S/≈@ @ R s3 @{a} ∅ ?s5D2Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÀëãîðèòì âû÷èñëåíèÿ ðàçáèåíèÿÏðèìåð.M@@∅?- s4 D1@{a} s2.{a} Π0 = [{s0 , s1 , s2 , s3 }; {s4 , s5 }]- s1 {z} | {z }|{a} s0?S/≈D2Π1 = Ref (Π0 ) =@ @ = Ref (Ref (Π0 |D1 )|D2 )R s3 @{a} = Ref ([{s0 , s1 , s3 }; {s2 }; {s4 , s5 }]|D2 )| {z } |{z} | {z }∅ ?s5D11D12D2= [{s0 , s1 }; {s3 }; {s2 }; {s4 , s5 }]| {z } |{z} |{z} | {z }D111D112D12D2Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÀëãîðèòì âû÷èñëåíèÿ ðàçáèåíèÿÏðèìåð.M@@@{a} s2∅?- s4 .{a} - s1 Π2 = Ref (Π1 ) ={a} s0?S/≈= [{s0 }; {s1 }; {s3 }; {s2 }; {s4 , s5 }]|{z} |{z} |{z} |{z} | {z }@ D1111 D1112 D112@ R s3 @{a} ∅ ?s5D12D2Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÀëãîðèòì âû÷èñëåíèÿ ðàçáèåíèÿÏðèìåð.M@@@{a} s2∅?- s4 .{a} - s1 Π2 = Ref (Π1 ) ={a} s0?S/≈= [{s0 }; {s1 }; {s3 }; {s2 }; {s4 , s5 }]|{z} |{z} |{z} |{z} | {z }@ D1111 D1112 D112 D12@ Π3 = Ref (Π2 ) = Π2R s3 @{a} Êîíåö âû÷èñëåíèÿì∅ ?s5D2Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÓòî÷íåíèåì îòíîøåíèÿ ýêâèâàëåíòíîñòè B íà ìíîæåñòâåñîñòîÿíèé S íàçîâåì òàêîå îòíîøåíèå ýêâèâàëåíòíîñòè Ref(B) ,êîòîðîå óäîâëåòâîðÿåò ðàâíåñòâó S/Ref (B) = Ref (S/B ) .Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÓòî÷íåíèåì îòíîøåíèÿ ýêâèâàëåíòíîñòè B íà ìíîæåñòâåñîñòîÿíèé S íàçîâåì òàêîå îòíîøåíèå ýêâèâàëåíòíîñòè Ref(B) ,êîòîðîå óäîâëåòâîðÿåò ðàâíåñòâó S/Ref (B) = Ref (S/B ) .Óòâåðæäåíèå 5.Îòíîøåíèå ýêâèâàëåíòíîñòè B íà ìíîæåñòâå ñîñòîÿíèé Sÿâëÿåòñÿ îòíîøåíèåì áèñèìóëÿöèè íà S òîãäà è òîëüêî òîãäà,êîãäà Ref (B) = B .Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÓòî÷íåíèåì îòíîøåíèÿ ýêâèâàëåíòíîñòè B íà ìíîæåñòâåñîñòîÿíèé S íàçîâåì òàêîå îòíîøåíèå ýêâèâàëåíòíîñòè Ref(B) ,êîòîðîå óäîâëåòâîðÿåò ðàâíåñòâó S/Ref (B) = Ref (S/B ) .Óòâåðæäåíèå 5.Îòíîøåíèå ýêâèâàëåíòíîñòè B íà ìíîæåñòâå ñîñòîÿíèé Sÿâëÿåòñÿ îòíîøåíèåì áèñèìóëÿöèè íà S òîãäà è òîëüêî òîãäà,êîãäà Ref (B) = B .Óòâåðæäåíèå 6.Äëÿ ëþáîãî îòíîøåíèÿ ýêâèâàëåíòíîñòè B íà ìíîæåñòâåñîñòîÿíèé S âåðíîI Ref (B) ⊆ B ,I≈⊆ B =⇒ ≈⊆ Ref (B)Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÒåîðåìà 2.Àëãîðèòì âû÷èñëåíèÿ áèñèìóëÿöèîííîé ýêâèâàëåíòíîñòè äëÿëþáîé ìîäåëè M1.

çàâåðøàåò âû÷èñëåíèå;2. âû÷èñëÿåò íàèáîëüøåå îòíîøåíèå áèñèìóëÿöèè ≈ íà S .Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÓïðàæíåíèå 4.Äîêàæèòå óòâåðæäåíèÿ 5 è 6.Óïðàæíåíèå 5.Êàêîâà ñëîæíîñòü ïðåäëîæåííîãî àëãîðèòìà âû÷èñëåíèÿáèñèìóëÿöèîííîé ýêâèâàëåíòíîñòè?Óïðàæíåíèå 6 [òðóäíîå].Ðàçðàáîòàéòå àëãîðèòì âû÷èñëåíèÿ áèñèìóëÿöèîííîéýêâèâàëåíòíîñòè, èìåþùèé ñëîæíîñòü O(|S||AP| + |R| log |S|) .Îòíîøåíèå ñèìóëÿöèèÈíîãäà áèñèìóëÿöèîííàÿ ýêâèâàëåíòíîñòü íå ïðèâîäèòçíà÷èòåëüíîìó ñîêðàùåíèþ ÷èñëà ñîñòîÿíèé. Îñëàáëÿÿòðåáîâàíèå òîãî, ÷òîáû íà ìîäåëÿõ âûïîëíÿëîñü îäíî è òî æåìíîæåñòâî ôîðìóë, ìîæíî äîáèòüñÿ áîëüøåãî ñîêðàùåíèÿ.Îïðåäåëåíèå ñèìóëÿöèèÅñëè äëÿ çàäàííûõ ìîäåëåé M è M 0 âûïîëíÿåòñÿ âêëþ÷åíèåAP ⊇ AP 0 , òî îòíîøåíèå H ⊆ S × S 0 íàçûâàåòñÿ îòíîøåíèåìñèìóëÿöèè ìåæäó M è M 0 â òîì è òîëüêî òîì ñëó÷àå, êîãäàI äëÿ âñÿêîãî íà÷àëüíîãî ñîñòîÿíèÿ s0 èç S0 â ìîäåëè Míàéäåòñÿ íà÷àëüíîå ñîñòîÿíèå s00 èç S00 â ìîäåëè M 0 , äëÿêîòîðîãî âûïîëíÿåòñÿ îòíîøåíèå H(s0, s00 ) ,I äëÿ ëþáîé ïàðû ñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ âîòíîøåíèè H(s, s 0) , âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:1)L(s) ∩ AP 0 = L0 (s 0 );2) äëÿ ëþáîãî ñîñòîÿíèÿ s1 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s, s1 ) , íàéäåòñÿ ñîñòîÿíèå s10 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿR 0 (s 0 , s10 )èH(s1 , s10 ).Îòíîøåíèÿ ñèìóëÿöèèÁóäåì ãîâîðèòü, ÷òî M 0 ñèìóëèðóåò M (îáîçíà÷èì ýòîîòíîøåíèå çàïèñüþ M M 0 ), åñëè ñóùåñòâóåò îòíîøåíèåñèìóëÿöèè ìåæäó M è M 0 .Îòíîøåíèÿ ñèìóëÿöèèÁóäåì ãîâîðèòü, ÷òî M 0 ñèìóëèðóåò M (îáîçíà÷èì ýòîîòíîøåíèå çàïèñüþ M M 0 ), åñëè ñóùåñòâóåò îòíîøåíèåñèìóëÿöèè ìåæäó M è M 0 .Ïðèìåðû ê îïðåäåëåíèþ áèñèìóëÿöèè@@R@Maba?bb??c d Ðèñ.: ÌîäåëüM0M0@@R@ d cñèìóëèðóåò ìîäåëüM:M M0Îòíîøåíèå ñèìóëÿöèèÓòâåðæäåíèå 7.Îòíîøåíèå ÿâëÿåòñÿ êâàçèïîðÿäêîì íà ìíîæåñòâå ìîäåëåé.Îòíîøåíèå ñèìóëÿöèèÓòâåðæäåíèå 7.Îòíîøåíèå ÿâëÿåòñÿ êâàçèïîðÿäêîì íà ìíîæåñòâå ìîäåëåé.Áóäåì ãîâîðèòü, ÷òî ïóòè π = s0s1, .

. . â ìîäåëè M èπ 0 = s00 s10 , . . . â ìîäåëè M 0 ñîîòâåòñòâóþò äðóã äðóãó , åñëè äëÿëþáîãî i , i ≥ 0 , âûïîëíÿåòñÿ îòíîøåíèå H(si , si0) .Óòâåðæäåíèå 8.Ïðåäïîëîæèì, ÷òî äëÿ ñîñòîÿíèé s è s 0 âûïîëíÿåòñÿîòíîøåíèå H(s, s 0) . Òîãäà äëÿ êàæäîãî ïóòè π , âûõîäÿùåãî èçs , èìååòñÿ ñîîòâåòñòâóþùèé åìó ïóòü π 0 , âûõîäÿùèé èç s 0 .Îòíîøåíèå ñèìóëÿöèèÔîðìóëà CTL â ïîçèòèâíîé íîðìàëüíîé, ñîäåðæàùàÿ òîëüêîòåìïîðàëüíûå îïåðàòîðû ñ êâàíòîðîì âñåîáùíîñòè, ò.å.îïåðàòîðû , , , , , íàçûâàåòñÿACTL-ôîðìóëîé.AX AF AG AU ARÒåîðåìà 3.Äîïóñòèì, ÷òî M M 0 . Òîãäà äëÿ âñÿêîé ACTL-ôîðìóëû ϕ (ñàòîìàðíûìè âûñêàçûâàíèÿìè èç AP 0 ) èç ñîîòíîøåíèÿ M 0 |= ϕñëåäóåò, ÷òî M |= ϕ .Èíäóêöèåé ïî ñòðóêòóðå ôîðìóëû ñïðèìåíåíèåì Óòâåðæäåíèÿ 8.ÄîêàçàòåëüñòâîÎòíîøåíèå ñèìóëÿöèè ÷åì ñîñòîèò ðàçëè÷èå ìåæäó ñèìóëÿöèåé è áèñèìóëÿöèåé?M0Ma@ 21@R@bba@ 43@R@bbAAAAAAU?U?cdccd d Ìîäåëè, ïðåäñòàâëåííûå íà ðèñóíêå, íå ÿâëÿþòñÿáèñèìóëÿöèîííî ýêâèâàëåíòíûìè, õîòÿ êàæäàÿ èç íèõñèìóëèðóåò äðóãóþ.Îòíîøåíèå ñèìóëÿöèèÁóäåì ãîâîðèòü, ÷òî ìîäåëè M 0 è M 00 ñèìóëÿöèîííîýêâèâàëåíòíû , åñëè M 0 M 00 è M 00 M 0 .Îòíîøåíèå ñèìóëÿöèèÁóäåì ãîâîðèòü, ÷òî ìîäåëè M 0 è M 00 ñèìóëÿöèîííîýêâèâàëåíòíû , åñëè M 0 M 00 è M 00 M 0 .Òåîðåìà 5.Åñëè ìîäåëè M 0 è M 00 ñèìóëÿöèîííî ýêâèâàëåíòíû, òî äëÿëþáîé ACTL ôîðìóëû ϕ ìû èìååìM 0 |= ϕ ⇔ M 00 |= ϕ.Îòíîøåíèå ñèìóëÿöèèÁóäåì ãîâîðèòü, ÷òî ìîäåëè M 0 è M 00 ñèìóëÿöèîííîýêâèâàëåíòíû , åñëè M 0 M 00 è M 00 M 0 .Òåîðåìà 5.Åñëè ìîäåëè M 0 è M 00 ñèìóëÿöèîííî ýêâèâàëåíòíû, òî äëÿëþáîé ACTL ôîðìóëû ϕ ìû èìååìM 0 |= ϕ ⇔ M 00 |= ϕ.Îáðàòíàÿ òåîðåìà òàêæå âåðíà.Åñëè äâå ìîäåëè óäîâëåòâîðÿþò îäíîìó è òîìó æå ìíîæåñòâóACTL-ôîðìóë, òî îíè ñèìóëÿöèîííî ýêâèâàëåíòíû.Îòíîøåíèå ñèìóëÿöèèÓïðàæíåíèå 7.

[òðóäíîå]Ðóêîâîäñòâóÿñü èäåÿìè, ïðåäëîæåííûìè ïðè ñîçäàíèèàëãîðèòìà âû÷èñëåíèÿ áèñèìóëÿöèîííîé ýêâèâàëåíòíîñòè,ðàçðàáîòàéòå àëãîðèòì âû÷èñëåíèÿ íàèáîëüøåãî îòíîøåíèÿñèìóëÿöèè ìåæäó ñîñòîÿíèÿìè çàäàííîé ìîäåëè.Àáñòðàêöèÿ ìîäåëåéÀáñòðàêöèÿ ýòî ñàìûé äåéñòâåííûé ìåòîä ðåøåíèÿïðîáëåìû ¾êîìáèíàòîðíîãî âçðûâà¿.

Ìû ðàññìîòðèì äâàðàçëè÷íûõ ìåòîäà àáñòðàêöèè: ðåäóêöèþ ïî êîíóñó âëèÿíèÿ èàáñòðàêöèþ äàííûõ .Îíè ïðèìåíÿþòñÿ ê îïèñàíèÿì ñèñòåìû íà âûñøåì óðîâíå,åùå äî òîãî êàê ïîñòðîåíà åå ìîäåëü, è ïîçâîëÿþò èçáåæàòüïîñòðîåíèÿ íåðåäóöèðîâàííîé ìîäåëè, êîòîðàÿ ìîæåòîêàçàòüñÿ ñëèøêîì áîëüøîé, ÷òîáû ïîìåñòèòüñÿ â ïàìÿòü.Àáñòðàêöèÿ ìîäåëåéñîñòîèò â òîì, ÷òîáûñîêðàòèòü ðàçìåð ãðàôà ïåðåõîäîâ, ðàññìàòðèâàÿ òîëüêî òåïåðåìåííûå ñèñòåìû, êîòîðûå çàäåéñòâîâàíû â ñïåöèôèêàöèè.Ñîêðàùåíèå äîñòèãàåòñÿ çà ñ÷åò óäàëåíèÿ ïåðåìåííûõ, êîòîðûåíå îêàçûâàþò íèêàêîãî âëèÿíèÿ íà ïåðåìåííûå, ôèãóðèðóþùèåâ ñïåöèôèêàöèè.Òàêèì îáðàçîì, ïðîâåðÿåìûå ñâîéñòâà ñîõðàíÿþòñÿ, íî ðàçìåðìîäåëè, êîòîðóþ íóæíî âåðèôèöèðîâàòü, ñòàíîâèòñÿ ìåíüøå.Ìåòîä ðåäóêöèè ïî êîíóñó âëèÿíèÿÀáñòðàêöèÿ ìîäåëåéñîñòîèò â òîì, ÷òîáûñîêðàòèòü ðàçìåð ãðàôà ïåðåõîäîâ, ðàññìàòðèâàÿ òîëüêî òåïåðåìåííûå ñèñòåìû, êîòîðûå çàäåéñòâîâàíû â ñïåöèôèêàöèè.Ñîêðàùåíèå äîñòèãàåòñÿ çà ñ÷åò óäàëåíèÿ ïåðåìåííûõ, êîòîðûåíå îêàçûâàþò íèêàêîãî âëèÿíèÿ íà ïåðåìåííûå, ôèãóðèðóþùèåâ ñïåöèôèêàöèè.Òàêèì îáðàçîì, ïðîâåðÿåìûå ñâîéñòâà ñîõðàíÿþòñÿ, íî ðàçìåðìîäåëè, êîòîðóþ íóæíî âåðèôèöèðîâàòü, ñòàíîâèòñÿ ìåíüøå.ïðåäóñìàòðèâàåò ïîèñê îòîáðàæåíèÿðåàëüíûõ çíà÷åíèé äàííûõ, èñïîëüçóåìûõ â ñèñòåìå, âíåáîëüøîå ìíîæåñòâî àáñòðàêòíûõ çíà÷åíèé äàííûõ.Ðàñïðîñòðàíèâ ýòî îòîáðàæåíèå íà ñîñòîÿíèÿ è ïåðåõîäû,ìîæíî ïîñòðîèòü àáñòðàêòíóþ ñèñòåìó, êîòîðàÿ ñèìóëèðóåòèñõîäíóþ, íî îáû÷íî èìååò ãîðàçäî ìåíüøèé ðàçìåð.Èç-çà òàêîãî ñîêðàùåíèÿ ðàçìåðà àáñòðàêòíóþ ñèñòåìó ïîä÷àñóäàåòñÿ âåðèôèöèðîâàòü ãîðàçäî ëåã÷å, íåæåëè èñõîäíóþ.Ìåòîä ðåäóêöèè ïî êîíóñó âëèÿíèÿÀáñòðàêöèÿ äàííûõÐåäóêöèÿ ïî êîíóñó âëèÿíèÿÏîñìîòðèì, êàê ðåäóêöèÿ ïî êîíóñó âëèÿíèÿ ìîæåò áûòüïðèìåíåíà ê ñèíõðîííûì ñõåìàì.Ïóñòü V ìíîæåñòâî ïåðåìåííûõ çàäàííîé ëîãè÷åñêîé ñõåìû.Ýòà ñõåìà ìîæåò áûòü îïèñàíà ñèñòåìîé óðàâíåíèé âèäàvi0 = fi (V )äëÿ êàæäîé ïåðåìåííîé vi ∈ V , ãäå fi áóëåâà ôîðìóëà.Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÏîñìîòðèì, êàê ðåäóêöèÿ ïî êîíóñó âëèÿíèÿ ìîæåò áûòüïðèìåíåíà ê ñèíõðîííûì ñõåìàì.Ïóñòü V ìíîæåñòâî ïåðåìåííûõ çàäàííîé ëîãè÷åñêîé ñõåìû.Ýòà ñõåìà ìîæåò áûòü îïèñàíà ñèñòåìîé óðàâíåíèé âèäàvi0 = fi (V )äëÿ êàæäîé ïåðåìåííîé vi ∈ V , ãäå fi áóëåâà ôîðìóëà.Ïðåäïîëîæèì, ÷òî çàäàíî ìíîæåñòâî ïåðåìåííûõ V 0 ⊆ V ,ïðåäñòàâëÿþùèõ èíòåðåñ â ñâåòå ïðåäúÿâëåííîé ñïåöèôèêàöèè.Íàì õîòåëîñü áû óïðîñòèòü îïèñàíèå ñèñòåìû, ñîõðàíèâ â íåìòîëüêî ýòè ïåðåìåííûå, íî îíè ìîãóò çàâèñåòü îò çíà÷åíèéïåðåìåííûõ, íå âõîäÿùèõ â V 0 .Ïîýòîìó ìû îïðåäåëÿåì êîíóñ âëèÿíèÿ C äëÿ V 0 è èñïîëüçóåìC äëÿ ñîêðàùåíèÿ îïèñàíèÿ ñèñòåìû.Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÎïðåäåëåíèå êîíóñà âëèÿíèÿÊîíóñîì âëèÿíèÿ C äëÿ ìíîæåñòâà ïåðåìåííûõ V 0 íàçîâåìòàêîå íàèìåíüøåå ìíîæåñòâî ïåðåìåííûõ, ÷òîI V0 ⊆ C ,I åñëè äëÿ íåêîòîðîé ïåðåìåííîé v` ∈ C åå ôóíêöèÿ f`çàâèñèò îò ïåðåìåííîé vj , òî vj ∈ C .×òîáû ïîñòðîèòü íîâóþ (óïðîùåííóþ) ñèñòåìó, íóæíî óäàëèòüâñå òå óðàâíåíèÿ, ó êîòîðûõ ïåðåìåííûå â ëåâîé ÷àñòè íåâõîäÿò â C .Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÏðèìåð êîíóñà âëèÿíèÿÎáðàòèìñÿ ê ïðèìåðó ñ÷åò÷èêà ïî ìîäóëþ 8.

Åãî ñèñòåìàóðàâíåíèé òàêîâà:v00 = ¬v0 ;v10 = v0 ⊕ v1 ;v20 = (v0 ∧ v1 ) ⊕ v2 .ßñíî, ÷òî åñëè V 0 = {v0} , òî C = {v0} , ïîñêîëüêó f0 íåçàâèñèò íè îò êàêîé äðóãîé ïåðåìåííîé, êðîìå v0 .Åñëè æå V 0 = {v1} , òî C = {v0, v1} , ïîñêîëüêó f1 çàâèñèò îòîáåèõ ïåðåìåííûõ, íî ïðè ýòîì v2 ∈/ C , èáî íèêàêàÿïåðåìåííàÿ èç C íå çàâèñèò îò v2 .È åñëè, íàêîíåö, V 0 = {v2} , òî C ýòî ìíîæåñòâî âñåõïåðåìåííûõ.Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿÏîêàæåì, ÷òî ðåäóêöèÿ ïî êîíóñó âëèÿíèÿ ñîõðàíÿåòêîððåêòíîñòü ñïåöèôèêàöèé â ëîãèêå CTL, åñëè îíèîïðåäåëåíû íàä ïåðåìåííûìè (àòîìàðíûìè âûñêàçûâàíèÿìè)èç C .Ðàññìîòðèì ìíîæåñòâî áóëåâûõ ïåðåìåííûõ V = {v1, .