8 Отношения бисимуляционной эквивалентности (бисимуляции) и симуляционного квазипорядка (симуляции) на моделях Крипке, страница 2

. . â ìîäåëè M èπ 0 = s00 , s10 , . . . â ìîäåëè M 0 ñîîòâåòñòâóþò äðóã äðóãó , åñëè äëÿëþáîãî i, i ≥ 0 , ñïðàâåäëèâî îòíîøåíèå B(si , si0) .Óòâåðæäåíèå 2.Ïóñòü s è s 0 äâà ñîñòîÿíèÿ, äëÿ êîòîðûõ âûïîëíÿåòñÿB(s, s 0 ) . Òîãäà äëÿ âñÿêîãî ïóòè, íà÷èíàþùåãîñÿ èç s ,íàéäåòñÿ ñîîòâåòñòâóþùèé åìó ïóòü, íà÷èíàþùèéñÿ èç s 0 , èíàîáîðîò, äëÿ âñÿêîãî ïóòè, íà÷èíàþùåãîñÿ èç s 0 , íàéäåòñÿñîîòâåòñòâóþùèé åìó ïóòü, íà÷èíàþùèéñÿ èç s .Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÈëëþñòðàöèÿ ê Óòâåðæäåíèþ 2.Äëÿ ëþáîãî ïóòè â îäíîé ìîäåëè$'M'$M06yy6yy&%&%Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÈëëþñòðàöèÿ ê Óòâåðæäåíèþ 2.Äëÿ ëþáîãî ïóòè â îäíîé ìîäåëè ñóùåñòâóåò ïóòü â äðóãîéìîäåëè,$'M'66yyM0I@y@ y66yyI@y&$@ y%&%Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÈëëþñòðàöèÿ ê Óòâåðæäåíèþ 2.Äëÿ ëþáîãî ïóòè â îäíîé ìîäåëè ñóùåñòâóåò ïóòü â äðóãîéìîäåëè, êîòîðûé ñîîòâåòñòâóåò ïåðâîìó ïóòè.$'M'66yyB@ yB6yyI@By&M0I@y6$@ yB%&%Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÓòâåðæäåíèå 3.Ïóñòü ϕ ýòî ëèáî ôîðìóëà ïóòè, ëèáî ôîðìóëà ñîñòîÿíèÿëîãèêè CTL∗.Ïðåäïîëîæèì, ÷òî ìîäåëè M è M 0 áèñèìóëÿöèîííîýêâèâàëåíòíû, ñîñòîÿíèÿ s è s 0 òàêîâû, ÷òî (s, s 0) ∈ B , à ïóòèπ è π 0 ñîîòâåòñòâóþò äðóã äðóãó.ÒîãäàI åñëè ϕ ýòî ôîðìóëà ñîñòîÿíèÿ, òîM, s |= ϕ ⇔ M 0 , s 0 |= ϕ ;I åñëè ϕ ýòî ôîðìóëà ïóòè, òî M, π |= ϕ ⇔ M 0 , π 0 |= ϕ .Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÓòâåðæäåíèå 3.Ïóñòü ϕ ýòî ëèáî ôîðìóëà ïóòè, ëèáî ôîðìóëà ñîñòîÿíèÿëîãèêè CTL∗.Ïðåäïîëîæèì, ÷òî ìîäåëè M è M 0 áèñèìóëÿöèîííîýêâèâàëåíòíû, ñîñòîÿíèÿ s è s 0 òàêîâû, ÷òî (s, s 0) ∈ B , à ïóòèπ è π 0 ñîîòâåòñòâóþò äðóã äðóãó.ÒîãäàI åñëè ϕ ýòî ôîðìóëà ñîñòîÿíèÿ, òîM, s |= ϕ ⇔ M 0 , s 0 |= ϕ ;I åñëè ϕ ýòî ôîðìóëà ïóòè, òî M, π |= ϕ ⇔ M 0 , π 0 |= ϕ .Äîêàçàòåëüñòâî.Èíäóêöèåé ïî ñòðóêòóðå ôîðìóëû.Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÒåîðåìà 1.Åñëè âûïîëíÿåòñÿ îòíîøåíèå M ∼ M 0 , òî äëÿ ëþáîé CTL∗ôîðìóëû ϕ ìû èìååìM |= ϕ ⇔ M 0 |= ϕ.Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÒåîðåìà 1.Åñëè âûïîëíÿåòñÿ îòíîøåíèå M ∼ M 0 , òî äëÿ ëþáîé CTL∗ôîðìóëû ϕ ìû èìååìM |= ϕ ⇔ M 0 |= ϕ.Îáðàòíàÿ òåîðåìà òàêæå âåðíà.Åñëè äâå ìîäåëè óäîâëåòâîðÿþò îäíîìó è òîìó æå ìíîæåñòâóCTL∗-ôîðìóë, òî îíè áèñèìóëÿöèîííî ýêâèâàëåíòíû.Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÒåîðåìà 1.Åñëè âûïîëíÿåòñÿ îòíîøåíèå M ∼ M 0 , òî äëÿ ëþáîé CTL∗ôîðìóëû ϕ ìû èìååìM |= ϕ ⇔ M 0 |= ϕ.Îáðàòíàÿ òåîðåìà òàêæå âåðíà.Åñëè äâå ìîäåëè óäîâëåòâîðÿþò îäíîìó è òîìó æå ìíîæåñòâóCTL∗-ôîðìóë, òî îíè áèñèìóëÿöèîííî ýêâèâàëåíòíû.Òàêèì îáðàçîì, åñëè ìîäåëü M 0 , îáðàçîâàëàñü â ðåçóëüòàòåïðåîáðàçîâàíèÿ ìîäåëè M , óäîâëåòâîðÿþùåé çàäàííûìCTL∗-ñïåöèôèêàöèÿì, òî äëÿ âåðèôèêàöèè ìîäåëè M 0äîñòàòî÷íî ïðîâåðèòü áèñèìóëÿöèîííóþ ýêâèâàëåíòíîñòüM0 ∼ M .Êàê ýòî ñäåëàòü?Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèè ñîñòîÿíèéÏóñòü çàäàíà ìîäåëü M = (AP, S, R, S0, L)Îòíîøåíèå B ⊆ S × S íàçûâàåòñÿíà ìîäåëè M , åñëè äëÿ ëþáîé ïàðû ñîñòîÿíèé s1 è s2 ,íàõîäÿùèõñÿ â îòíîøåíèè B(s1, s2) , âûïîëíÿþòñÿ ñëåäóþùèåóñëîâèÿ:îòíîøåíèåì áèñèìóëÿöèèÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèè ñîñòîÿíèéÏóñòü çàäàíà ìîäåëü M = (AP, S, R, S0, L)Îòíîøåíèå B ⊆ S × S íàçûâàåòñÿíà ìîäåëè M , åñëè äëÿ ëþáîé ïàðû ñîñòîÿíèé s1 è s2 ,íàõîäÿùèõñÿ â îòíîøåíèè B(s1, s2) , âûïîëíÿþòñÿ ñëåäóþùèåóñëîâèÿ:1) L(s1) = L(s2) ;îòíîøåíèåì áèñèìóëÿöèèÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèè ñîñòîÿíèéÏóñòü çàäàíà ìîäåëü M = (AP, S, R, S0, L)Îòíîøåíèå B ⊆ S × S íàçûâàåòñÿíà ìîäåëè M , åñëè äëÿ ëþáîé ïàðû ñîñòîÿíèé s1 è s2 ,íàõîäÿùèõñÿ â îòíîøåíèè B(s1, s2) , âûïîëíÿþòñÿ ñëåäóþùèåóñëîâèÿ:1) L(s1) = L(s2) ;2) Äëÿ ëþáîãî ñîñòîÿíèÿ t1 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s1, t1) , íàéäåòñÿ ñîñòîÿíèå t2 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿ R(s2, t2) è B(t1, t2) ;îòíîøåíèåì áèñèìóëÿöèèÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèè ñîñòîÿíèéÏóñòü çàäàíà ìîäåëü M = (AP, S, R, S0, L)Îòíîøåíèå B ⊆ S × S íàçûâàåòñÿíà ìîäåëè M , åñëè äëÿ ëþáîé ïàðû ñîñòîÿíèé s1 è s2 ,íàõîäÿùèõñÿ â îòíîøåíèè B(s1, s2) , âûïîëíÿþòñÿ ñëåäóþùèåóñëîâèÿ:1) L(s1) = L(s2) ;2) Äëÿ ëþáîãî ñîñòîÿíèÿ t1 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s1, t1) , íàéäåòñÿ ñîñòîÿíèå t2 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿ R(s2, t2) è B(t1, t2) ;3) Äëÿ ëþáîãî ñîñòîÿíèÿ t2 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s2, t2) , íàéäåòñÿ ñîñòîÿíèå t1 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿ R(s1, t1) è B(t1, t2) .îòíîøåíèåì áèñèìóëÿöèèÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèîííîé ýêâèâàëåíòíîñòèñîñòîÿíèéÄâà ñîñòîÿíèÿ s1 è s2 ìîäåëè M = (AP, S, R, S0, L) íàçûâàþòñÿáèñèìóëÿöèîííî ýêâèâàëåíòíûìè (îáîçíà÷àåòñÿ s1 ≈ s2 ), åñëèñóùåñòâóåò òàêîå îòíîøåíèå áèñèìóëÿöèè B íà ìîäåëè M , äëÿêîòîðîãî âûïîëíÿåòñÿ ñîîòíîøåíèå B(s1, s2) .Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèîííîé ýêâèâàëåíòíîñòèñîñòîÿíèéÄâà ñîñòîÿíèÿ s1 è s2 ìîäåëè M = (AP, S, R, S0, L) íàçûâàþòñÿáèñèìóëÿöèîííî ýêâèâàëåíòíûìè (îáîçíà÷àåòñÿ s1 ≈ s2 ), åñëèñóùåñòâóåò òàêîå îòíîøåíèå áèñèìóëÿöèè B íà ìîäåëè M , äëÿêîòîðîãî âûïîëíÿåòñÿ ñîîòíîøåíèå B(s1, s2) .Óòâåðæäåíèå 4.Îòíîøåíèå áèñèìóëÿöèîííîé ýêâèâàëåíòíîñòè ≈ ñîñòîÿíèéìîäåëè M = (AP, S, R, S0, L) ÿâëÿåòñÿI îòíîøåíèåì ýêâèâàëåíòíîñòè,I îòíîøåíèåì áèñèìóëÿöèè íà ìîäåëè M ,I íàèáîëüøèì îòíîøåíèåì áèñèìóëÿöèè íà ìîäåëè MÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå ôàêòîð-ìîäåëèÔàêòîð-ìîäåëüþ ìîäåëè M = (AP, S, R, S0, L) íàçûâàåòñÿìîäåëü M/≈ = (AP, S/≈, R/≈, S0/≈, L/≈) äëÿ êîòîðîéI S/≈ = {[s]≈ : s ∈ S} ìíîæåñòâî êëàññîâáèñèìóëÿöèîííîé ýêâèâàëåíòíîñòè ñîñòîÿíèé;I R/≈ = {([s 0 ]≈ , [s 00 ]≈ ) : s 0 , s 00 ∈ S, (s 0 , s 00 ) ∈ R} ;I S0 /≈ = {[s]≈ : s ∈ S0 } ;I L/≈ ([s]≈ ) = L(s) .Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÓïðàæíåíèå 1.Äîêàæèòå, ÷òî äëÿ ëþáîé ìîäåëè M âåðíî ñîîòíîøåíèåM ∼ M/≈Óïðàæíåíèå 2.Êàêîâà âçàèìîñâÿçü îòíîøåíèÿ áèñèìóëÿöèîííîéýêâèâàëåíòíîñòè ìîäåëåé ∼ è îòíîøåíèÿ áèñèìóëÿöèîííîéýêâèâàëåíòîñòè ñîñòîÿíèé ìîäåëè ≈ ?Óïðàæíåíèå 3.

[òðóäíîå]Äîêàæèòå, ÷òî äëÿ ëþáîé ìîäåëè M åñëè B1 è B2 îòíîøåíèÿ áèñèìóëÿöèè ñîñòîÿíèé ìîäåëè M , òî è îòíîøåíèåB1 ∪ B2 òàêæå ÿâëÿåòñÿ îòíîøåíèåì áèñèìóëÿöèè ñîñòîÿíèéìîäåëè M .Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÌîäåëü èíôîðìàöèîííîé ñèñòåìû èç 3-õ ïðèíòåðîâ.MÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÈ åå ôàêòîð-ìîäåëü.M/≈Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÀëãîðèòì âû÷èñëåíèÿ áèñèìóëÿöèîííîé ýêâèâàëåíòíîñòèñîñòîÿíèé ≈ äëÿ êîíå÷íûõ ìîäåëåé Êðèïêå ïîõîæ íà àëãîðèòììèíèìèçàöèè äåòåðìèíèðîâàííûõ êîíå÷íûõ àâòîìàòîâ.Äëÿ êàæäîé ìîäåëè M = (AP, S, R, S0, L) îí âû÷èñëÿåòìíîæåñòâî S≈ è, òàêèì îáðàçîì, ìîæåò áûòü èñïîëüçîâàí äëÿïîñòðîåíèÿ ôàêòîð-ìîäåëè M/≈ .Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÀëãîðèòì âû÷èñëåíèÿ áèñèìóëÿöèîííîé ýêâèâàëåíòíîñòèñîñòîÿíèé ≈ äëÿ êîíå÷íûõ ìîäåëåé Êðèïêå ïîõîæ íà àëãîðèòììèíèìèçàöèè äåòåðìèíèðîâàííûõ êîíå÷íûõ àâòîìàòîâ.Äëÿ êàæäîé ìîäåëè M = (AP, S, R, S0, L) îí âû÷èñëÿåòìíîæåñòâî S≈ è, òàêèì îáðàçîì, ìîæåò áûòü èñïîëüçîâàí äëÿïîñòðîåíèÿ ôàêòîð-ìîäåëè M/≈ .Îñíîâíîé ïðèíöèï àëãîðèòìà ïðèáëèæåíèå ñâåðõóìíîæåñòâà S/≈ , ïðåäñòàâëÿþùåãî ñîáîé ðàçáèåíèåïðîñòðàíñòâà ñîñòîÿíèé S ïî îòíîøåíèþ áèñèìóëÿöèîííîéýêâèàâëåíòíîñòè ≈ .Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÏóñòü çàäàíà ìîäåëü Êðèïêå ìîäåëè M = (AP, S, R, S0, L) .Áëîêîì íàçûâàåòñÿ âñÿêîå íåïóñòîå ïîäìíîæåñòâî ñîñòîÿíèéD, D ⊆ S .Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÏóñòü çàäàíà ìîäåëü Êðèïêå ìîäåëè M = (AP, S, R, S0, L) .Áëîêîì íàçûâàåòñÿ âñÿêîå íåïóñòîå ïîäìíîæåñòâî ñîñòîÿíèéD, D ⊆ S .Ðàçáèåíèåì ìíîæåñòâà ñîñòîÿíèé S íàçûâàåòñÿ âñÿêîå òàêîåêîíå÷íîå ñåìåéñòâî Π = {D1, .

. . , Dk } ïîïàðíîíåïåðåñåêàþùèõñÿ áëîêîâ, êîòîðîå óäîâëåòâîðÿåò ðàâåíñòâókSS=Di .i=1Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÏóñòü çàäàíà ìîäåëü Êðèïêå ìîäåëè M = (AP, S, R, S0, L) .Áëîêîì íàçûâàåòñÿ âñÿêîå íåïóñòîå ïîäìíîæåñòâî ñîñòîÿíèéD, D ⊆ S .Ðàçáèåíèåì ìíîæåñòâà ñîñòîÿíèé S íàçûâàåòñÿ âñÿêîå òàêîåêîíå÷íîå ñåìåéñòâî Π = {D1, .

. . , Dk } ïîïàðíîíåïåðåñåêàþùèõñÿ áëîêîâ, êîòîðîå óäîâëåòâîðÿåò ðàâåíñòâókSS=Di .i=1Áëîê E íàçûâàåòñÿ ðàçâåòâèòåëåì áëîêà D , åñëè ñóùåñòâóåòòàêàÿ ïàðà ñîñòîÿíèé s 0, s 00 ∈ D , äëÿ êîòîðîé âåðíûñîîòíîøåíèÿ({s 0 } × E ) ∩ R 6= ∅è({s 00 } × E ) ∩ R = ∅,Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèò.å. èç îäíèõ ñîñòîÿíèé áëîêà D åñòü ïåðåõîäû â ñîñòîÿíèÿáëîêà E ,'$'D&$E%&%Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèò.å.

èç îäíèõ ñîñòîÿíèé áëîêà D åñòü ïåðåõîäû â ñîñòîÿíèÿáëîêà E ,'$D&%'$- E-&%Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèò.å. èç îäíèõ ñîñòîÿíèé áëîêà D åñòü ïåðåõîäû â ñîñòîÿíèÿáëîêà E , à èç äðóãèõ íåò.'$D&%'$- E-&%Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèò.å. èç îäíèõ ñîñòîÿíèé áëîêà D åñòü ïåðåõîäû â ñîñòîÿíèÿáëîêà E , à èç äðóãèõ íåò.'$D@ @@@@@@@&%@@ @@@R@@R@RR@@'$- E-&%Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÓòî÷íåíèåì áëîêà 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 â ïðîòèâíîì ñëó÷àå.Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòèÓòî÷íåíèåì áëîêà 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, .