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

Âåðèôèêàöèÿìîäåëåé ïðîãðàììËÅÊÒÎÐ:Âëàäèìèð Àíàòîëüåâè÷ ÇàõàðîâÂëàäèñëàâ Âàñèëüåâè÷ Ïîäûìîâzakh@cs.msu.suËåêöèÿ 8.Áèñèìóëÿöèÿ, ñèìóëÿöèÿ èàáñòðàêöèÿ ìîäåëåé1.Îòíîøåíèå áèñèìóëÿöèè è åãîñâîéñòâà2.Âû÷èñëåíèå áèñèìóëÿöèîííîéýêâèâàëåíòíîñòè3.Îòíîøåíèÿ ñèìóëÿöèè4.Àáñòðàêöèÿ ìîäåëåé5.Ðåäóêöèÿ ïî êîíóñó âëèÿíèÿ6.Àáñòðàêöèÿ äàííûõÌîäåëè ïðîñòûå è ñëîæíûåÌîäåëè èíôîðìàöèîííûõ ñèñòåì áûâàþò ðàçíûå.Áûâàþò ìîäåëè ïðîñòûå:Ìîäåëè ïðîñòûå è ñëîæíûåÌîäåëè èíôîðìàöèîííûõ ñèñòåì áûâàþò ðàçíûå.È áûâàþò ñëîæíûå:Ìîäåëè ïðîñòûå è ñëîæíûåÑëîæíûå ìîäåëè ïîçâîëÿþòI íàèáîëåå òî÷íî îïèñûâàòü óñòðîéñòâî è ïîâåäåíèåìîäåëèðóåìîãî îáúåêòà,I íàèáîëåå ïîäðîáíî âîñïðîèçâîäèòü äåòàëè ïîâåäåíèÿ(¾ìåëêî ãðàíóëèðîâàííûå ìîäåëè¿),íî òðåáóþò çíà÷èòåëüíûõ âû÷èñëèòåëüíûõ ðåñóðñîâ äëÿ èõïîñòðîåíèÿ è àíàëèçà .Ìîäåëè ïðîñòûå è ñëîæíûåÑëîæíûå ìîäåëè ïîçâîëÿþòI íàèáîëåå òî÷íî îïèñûâàòü óñòðîéñòâî è ïîâåäåíèåìîäåëèðóåìîãî îáúåêòà,I íàèáîëåå ïîäðîáíî âîñïðîèçâîäèòü äåòàëè ïîâåäåíèÿ(¾ìåëêî ãðàíóëèðîâàííûå ìîäåëè¿),íî òðåáóþò çíà÷èòåëüíûõ âû÷èñëèòåëüíûõ ðåñóðñîâ äëÿ èõïîñòðîåíèÿ è àíàëèçà .Ïðîcòûå ìîäåëè íå äàþò âîçìîæíîñòè óâèäåòü ïîäðîáíîñòèóñòðîéñòâà ìîäåëèðóåìîãî îáúåêòà è/èëè ìîãóò ëèøü âåñüìàãðóáî (ñ íåáîëüøîé òî÷íîñòüþ) îïèñûâàòü åãî ïîâåäåíèå, íîçàòî ïðîñòûå ìîäåëèI ëåãêî ñòðîèòü èI ëåãêî àíàëèçèðîâàòü .Ìîäåëè ïðîñòûå è ñëîæíûåÑëîæíûå ìîäåëè ïîçâîëÿþòI íàèáîëåå òî÷íî îïèñûâàòü óñòðîéñòâî è ïîâåäåíèåìîäåëèðóåìîãî îáúåêòà,I íàèáîëåå ïîäðîáíî âîñïðîèçâîäèòü äåòàëè ïîâåäåíèÿ(¾ìåëêî ãðàíóëèðîâàííûå ìîäåëè¿),íî òðåáóþò çíà÷èòåëüíûõ âû÷èñëèòåëüíûõ ðåñóðñîâ äëÿ èõïîñòðîåíèÿ è àíàëèçà .Ïðîcòûå ìîäåëè íå äàþò âîçìîæíîñòè óâèäåòü ïîäðîáíîñòèóñòðîéñòâà ìîäåëèðóåìîãî îáúåêòà è/èëè ìîãóò ëèøü âåñüìàãðóáî (ñ íåáîëüøîé òî÷íîñòüþ) îïèñûâàòü åãî ïîâåäåíèå, íîçàòî ïðîñòûå ìîäåëèI ëåãêî ñòðîèòü èI ëåãêî àíàëèçèðîâàòü .À íåëüçÿ ëè âîñïîëüçîâàòüñÿ äîñòîèíñòâàìè ïðîñòûõ ìîäåëåéäëÿ ïîñòðîåíèÿ è àíàëèçà ñëîæíûõ ìîäåëåé?Ìîäåëè ïðîñòûå è ñëîæíûåÑÖÅÍÀÐÈÉ 1Ìîäåëü M áûëà ïîñòðîåíà, è áûëî ïðîâåðåíî, ÷òî îíàóäîâëåòâîðÿåò ìíîæåñòâó ñïåöèôèêàöèé {ϕ1, .

. . , ϕN } .Îäíàêî ïîçäíåå çà ñ÷åò óëó÷øåíèé, âíåäðåíèÿ íîâûõ èäåé,èçìåíåíèé ìîäåëü M áûëà ïðåîáðàçîâàíà â ìîäåëü M 0 .Ìîäåëè ïðîñòûå è ñëîæíûåÑÖÅÍÀÐÈÉ 1Ìîäåëü M áûëà ïîñòðîåíà, è áûëî ïðîâåðåíî, ÷òî îíàóäîâëåòâîðÿåò ìíîæåñòâó ñïåöèôèêàöèé {ϕ1, . . .

, ϕN } .Îäíàêî ïîçäíåå çà ñ÷åò óëó÷øåíèé, âíåäðåíèÿ íîâûõ èäåé,èçìåíåíèé ìîäåëü M áûëà ïðåîáðàçîâàíà â ìîäåëü M 0 .Ìîæíî ëè, ñðàâíèâ ìîäåëè M è M 0 , óáåäèòüñÿ â òîì, ÷òî âìîäåëè M 0 òàêæå âûïîëíÿåòñÿ ìíîæåñòâî ñïåöèôèêàöèé{ϕ1 , . . . , ϕN } ?Ìîäåëè ïðîñòûå è ñëîæíûåÑÖÅÍÀÐÈÉ 1Ìîäåëü M áûëà ïîñòðîåíà, è áûëî ïðîâåðåíî, ÷òî îíàóäîâëåòâîðÿåò ìíîæåñòâó ñïåöèôèêàöèé {ϕ1, . . . , ϕN } .Îäíàêî ïîçäíåå çà ñ÷åò óëó÷øåíèé, âíåäðåíèÿ íîâûõ èäåé,èçìåíåíèé ìîäåëü M áûëà ïðåîáðàçîâàíà â ìîäåëü M 0 .Ìîæíî ëè, ñðàâíèâ ìîäåëè M è M 0 , óáåäèòüñÿ â òîì, ÷òî âìîäåëè M 0 òàêæå âûïîëíÿåòñÿ ìíîæåñòâî ñïåöèôèêàöèé{ϕ1 , . . . , ϕN } ?Äà, åñëè óäàñòñÿ îáíàðóæèòü òàêîå îòíîøåíèå ∼ (îòíîøåíèåáèñèìóëÿöèè), äëÿ êîòîðîãî âåðíî ñîîòíîøåíèåM ∼ M 0 =⇒ ∀ ϕ (M |= ϕ ⇔ M 0 |= ϕ).Ìîäåëè ïðîñòûå è ñëîæíûåÑÖÅÍÀÐÈÉ 2Ñëîæíàÿ èíôîðìàöèîííàÿ ñèñòåìà ñòðîèòñÿ èíêðåìåíòàëüíî:íà êàæäîì i -îì ýòàïå ïîñòðîåíèÿ áîëåå ïðîñòàÿ ìîäåëü Mi çàñ÷åò óòî÷íåíèÿ íåêîòîðûõ åå êîìïîíåíòîâ ïðåîáðàçóåòñÿ âáîëåå ñëîæíóþ ìîäåëü Mi+1 .×òîáû ïðîâåðÿòü êîððåêòíîñòü óòî÷íåíèé, íà êàæäîì ýòàïåïðîâåðÿþòñÿ íåêîòîðûå òðåáîâàíèÿ ê ïðîåêòèðóåìîé ñèñòåìå.Ìîäåëè ïðîñòûå è ñëîæíûåÑÖÅÍÀÐÈÉ 2Ñëîæíàÿ èíôîðìàöèîííàÿ ñèñòåìà ñòðîèòñÿ èíêðåìåíòàëüíî:íà êàæäîì i -îì ýòàïå ïîñòðîåíèÿ áîëåå ïðîñòàÿ ìîäåëü Mi çàñ÷åò óòî÷íåíèÿ íåêîòîðûõ åå êîìïîíåíòîâ ïðåîáðàçóåòñÿ âáîëåå ñëîæíóþ ìîäåëü Mi+1 .×òîáû ïðîâåðÿòü êîððåêòíîñòü óòî÷íåíèé, íà êàæäîì ýòàïåïðîâåðÿþòñÿ íåêîòîðûå òðåáîâàíèÿ ê ïðîåêòèðóåìîé ñèñòåìå.Ìîæíî ëè, ñðàâíèâ ìîäåëè Mi è Mi+1 , óáåäèòüñÿ â òîì, ÷òîìîäåëü Mi+1 óäîâëåòâîðÿåò âñåì òåì òðåáîâàíèÿì, êîòîðûåáûëè ïðîâåðåíû äëÿ ìîäåëåé M1, M2, .

. . , Mi ?Ìîäåëè ïðîñòûå è ñëîæíûåÑÖÅÍÀÐÈÉ 2Ñëîæíàÿ èíôîðìàöèîííàÿ ñèñòåìà ñòðîèòñÿ èíêðåìåíòàëüíî:íà êàæäîì i -îì ýòàïå ïîñòðîåíèÿ áîëåå ïðîñòàÿ ìîäåëü Mi çàñ÷åò óòî÷íåíèÿ íåêîòîðûõ åå êîìïîíåíòîâ ïðåîáðàçóåòñÿ âáîëåå ñëîæíóþ ìîäåëü Mi+1 .×òîáû ïðîâåðÿòü êîððåêòíîñòü óòî÷íåíèé, íà êàæäîì ýòàïåïðîâåðÿþòñÿ íåêîòîðûå òðåáîâàíèÿ ê ïðîåêòèðóåìîé ñèñòåìå.Ìîæíî ëè, ñðàâíèâ ìîäåëè Mi è Mi+1 , óáåäèòüñÿ â òîì, ÷òîìîäåëü Mi+1 óäîâëåòâîðÿåò âñåì òåì òðåáîâàíèÿì, êîòîðûåáûëè ïðîâåðåíû äëÿ ìîäåëåé M1, M2, . . . , Mi ?Äà, åñëè óäàñòñÿ îáíàðóæèòü òàêîå îòíîøåíèå ≺ (îòíîøåíèåñèìóëÿöèè), äëÿ êîòîðîãî âåðíî ñîîòíîøåíèåM ≺ M 0 =⇒ ∀ ϕ (M |= ϕ ⇒ M 0 |= ϕ).Ìîäåëè ïðîñòûå è ñëîæíûåÑÖÅÍÀÐÈÉ 3Èç-çà íåäîñòàòêà âû÷èñëèòåëüíûõ ðåñóðñîâ íåâîçìîæíîïðîâåðèòü âûïîëíèìîñòü ñïåöèôèêàöèè ϕ äëÿ ñëîæíîé ìîäåëèM .Ìîäåëè ïðîñòûå è ñëîæíûåÑÖÅÍÀÐÈÉ 3Èç-çà íåäîñòàòêà âû÷èñëèòåëüíûõ ðåñóðñîâ íåâîçìîæíîïðîâåðèòü âûïîëíèìîñòü ñïåöèôèêàöèè ϕ äëÿ ñëîæíîé ìîäåëèM .Ìîæíî ëè äëÿ çàäàííîé ìîäåëè M è ñïåöèôèêàöèè ϕïîñòðîèòü òàêóþ ìîäåëü M 0 (àáñòðàêöèþ ìîäåëè M ), äëÿêîòîðîéI ãîðàçäî ïðîùå ðåøàòü çàäà÷ó âåðèôèêàöèè ìîäåëåéïðîãðàìì, èI âåðíî ñîîòíîøåíèå M 0 |= ϕ =⇒ M |= ϕ.Ìîäåëè ïðîñòûå è ñëîæíûåÊàê èçâåñòíî, äëÿ ëþáîé LTL ôîðìóëû ϕ è äëÿ ëþáîé ìîäåëèMM |= ϕ ⇔ ∀tr ∈ Trace(M) tr |= ϕ.Ïî÷åìó áû òîãäà íå ñðàâíèâàòü ìîäåëè M1 è M2 , ñîïîñòàâëÿÿìíîæåñòâà èõ òðàññ Trace(M1) è Trace(M2) ?Íàïðèìåð, îáúÿâëÿÿ M1 ≈ M2 òîãäà è òîëüêî òîãäà, êîãäàTrace(M1 ) = Trace(M2 ) ?Ìîäåëè ïðîñòûå è ñëîæíûåÊàê èçâåñòíî, äëÿ ëþáîé LTL ôîðìóëû ϕ è äëÿ ëþáîé ìîäåëèMM |= ϕ ⇔ ∀tr ∈ Trace(M) tr |= ϕ.Ïî÷åìó áû òîãäà íå ñðàâíèâàòü ìîäåëè M1 è M2 , ñîïîñòàâëÿÿìíîæåñòâà èõ òðàññ Trace(M1) è Trace(M2) ?Íàïðèìåð, îáúÿâëÿÿ M1 ≈ M2 òîãäà è òîëüêî òîãäà, êîãäàTrace(M1 ) = Trace(M2 ) ?Ýòî íåöåëåñîîáðàçíî ïî äâóì ïðè÷èíàì:Ìîäåëè ïðîñòûå è ñëîæíûåÊàê èçâåñòíî, äëÿ ëþáîé LTL ôîðìóëû ϕ è äëÿ ëþáîé ìîäåëèMM |= ϕ ⇔ ∀tr ∈ Trace(M) tr |= ϕ.Ïî÷åìó áû òîãäà íå ñðàâíèâàòü ìîäåëè M1 è M2 , ñîïîñòàâëÿÿìíîæåñòâà èõ òðàññ Trace(M1) è Trace(M2) ?Íàïðèìåð, îáúÿâëÿÿ M1 ≈ M2 òîãäà è òîëüêî òîãäà, êîãäàTrace(M1 ) = Trace(M2 ) ?Ýòî íåöåëåñîîáðàçíî ïî äâóì ïðè÷èíàì:1.

Ðàâåíñòâî ìíîæåñòâà òðàññ íå ïîääåðæèâàåòðàâíîâûïîëíèìîñòü ôîðìóë äðóãèõ ëîãèê, íàïðèìåð, CTL.Ìîäåëè ïðîñòûå è ñëîæíûåÊàê èçâåñòíî, äëÿ ëþáîé LTL ôîðìóëû ϕ è äëÿ ëþáîé ìîäåëèMM |= ϕ ⇔ ∀tr ∈ Trace(M) tr |= ϕ.Ïî÷åìó áû òîãäà íå ñðàâíèâàòü ìîäåëè M1 è M2 , ñîïîñòàâëÿÿìíîæåñòâà èõ òðàññ Trace(M1) è Trace(M2) ?Íàïðèìåð, îáúÿâëÿÿ M1 ≈ M2 òîãäà è òîëüêî òîãäà, êîãäàTrace(M1 ) = Trace(M2 ) ?Ýòî íåöåëåñîîáðàçíî ïî äâóì ïðè÷èíàì:1. Ðàâåíñòâî ìíîæåñòâà òðàññ íå ïîääåðæèâàåòðàâíîâûïîëíèìîñòü ôîðìóë äðóãèõ ëîãèê, íàïðèìåð, CTL.2. Ïðîâåðêà îòíîøåíèÿ ðàâåíñòâà ìíîæåñòâ òðàññ êîíå÷íûõìîäåëåé ýòî âû÷èñëèòåëüíî ñëîæíàÿ (PSPACE-ïîëíàÿ)çàäà÷à.Ïîýòîìó íóæíû äðóãèå, áîëåå ¾ïðîñòûå¿ îòíîøåíèÿ ñðàâíåíèÿìîäåëåé.Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÁóäåì çàíèìàòüñÿ ñðàâíåíèåì ìîäåëåé èíôîðìàöèîííûõñèñòåì, çàäàííûõ â âèäå ìîäåëåé Êðèïêå (ðàçìå÷åííûõ ñèñòåìïåðåõîäîâ, LTS) M = (AP, S, R, S0, L) , ãäåI AP ìíîæåñòâî àòîìàðíûõ âûñêàçûâàíèé;I S ìíîæåñòâî ñîñòîÿíèé ìîäåëè;I R, R ⊆ S × S òîòàëüíîå îòíîøåíèå ïåðåõîäîâ;I S0 , S0 ⊆ S ìíîæåñòâî íà÷àëüíûõ ñîñòîÿíèé;I L : S → 2AP ôóíêöèÿ ðàçìåòêè.Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèè ìîäåëåéÏóñòü çàäàíû äâå ìîäåëè (LTS) ñ îäíèì è òåì æå ìíîæåñòâîìàòîìàðíûõ âûñêàçûâàíèé AP :M = (AP, S, R, S0 , L) è M 0 = (AP, S 0 , R 0 , S00 , L0 )Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèè ìîäåëåéÏóñòü çàäàíû äâå ìîäåëè (LTS) ñ îäíèì è òåì æå ìíîæåñòâîìàòîìàðíûõ âûñêàçûâàíèé AP :M = (AP, S, R, S0 , L) è M 0 = (AP, S 0 , R 0 , S00 , L0 )Îòíîøåíèå B ⊆ S × S 0 íàçûâàåòñÿìåæäó M è M 0 , åñëè äëÿ ëþáîé ïàðûñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ â îòíîøåíèè B(s, s 0) ,âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:îòíîøåíèåìáèñèìóëÿöèèÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèè ìîäåëåéÏóñòü çàäàíû äâå ìîäåëè (LTS) ñ îäíèì è òåì æå ìíîæåñòâîìàòîìàðíûõ âûñêàçûâàíèé AP :M = (AP, S, R, S0 , L) è M 0 = (AP, S 0 , R 0 , S00 , L0 )Îòíîøåíèå B ⊆ S × S 0 íàçûâàåòñÿìåæäó M è M 0 , åñëè äëÿ ëþáîé ïàðûñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ â îòíîøåíèè B(s, s 0) ,âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:1) L(s) = L0(s 0) ;îòíîøåíèåìáèñèìóëÿöèèÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèè ìîäåëåéÏóñòü çàäàíû äâå ìîäåëè (LTS) ñ îäíèì è òåì æå ìíîæåñòâîìàòîìàðíûõ âûñêàçûâàíèé AP :M = (AP, S, R, S0 , L) è M 0 = (AP, S 0 , R 0 , S00 , L0 )Îòíîøåíèå B ⊆ S × S 0 íàçûâàåòñÿìåæäó M è M 0 , åñëè äëÿ ëþáîé ïàðûñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ â îòíîøåíèè B(s, s 0) ,âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:1) L(s) = L0(s 0) ;2) Äëÿ ëþáîãî ñîñòîÿíèÿ s1 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s, s1) , íàéäåòñÿ ñîñòîÿíèå s10 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿ R 0(s 0, s10 ) è B(s1, s10 ) ;îòíîøåíèåìáèñèìóëÿöèèÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèè ìîäåëåéÏóñòü çàäàíû äâå ìîäåëè (LTS) ñ îäíèì è òåì æå ìíîæåñòâîìàòîìàðíûõ âûñêàçûâàíèé AP :M = (AP, S, R, S0 , L) è M 0 = (AP, S 0 , R 0 , S00 , L0 )Îòíîøåíèå B ⊆ S × S 0 íàçûâàåòñÿìåæäó M è M 0 , åñëè äëÿ ëþáîé ïàðûñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ â îòíîøåíèè B(s, s 0) ,âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:1) L(s) = L0(s 0) ;2) Äëÿ ëþáîãî ñîñòîÿíèÿ s1 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s, s1) , íàéäåòñÿ ñîñòîÿíèå s10 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿ R 0(s 0, s10 ) è B(s1, s10 ) ;3) Äëÿ ëþáîãî ñîñòîÿíèÿ s10 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s 0, s10 ) , íàéäåòñÿ ñîñòîÿíèå s1 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿ R(s, s1) è B(s1, s10 ) .îòíîøåíèåìáèñèìóëÿöèèÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÈëëþñòðàöèÿ îïðåäåëåíèÿ áèñèìóëÿöèèÄëÿ ëþáîé ïàðû ñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ â îòíîøåíèèB(s, s 0 ) , âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:'M$'$ds 0s d&M0B&%%Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÈëëþñòðàöèÿ îïðåäåëåíèÿ áèñèìóëÿöèèÄëÿ ëþáîé ïàðû ñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ â îòíîøåíèèB(s, s 0 ) , âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:2) Äëÿ ëþáîãî ñîñòîÿíèÿ s1 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s, s1) ,'$'Ms1 dM0$Rds 0s d&B&%%Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÈëëþñòðàöèÿ îïðåäåëåíèÿ áèñèìóëÿöèèÄëÿ ëþáîé ïàðû ñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ â îòíîøåíèèB(s, s 0 ) , âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:2) Äëÿ ëþáîãî ñîñòîÿíèÿ s1 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s, s1) , íàéäåòñÿ ñîñòîÿíèå s10 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿ R 0(s 0, s10 )'$'MRs1 d0ds1@I@s d&B&%M0$0@R@ ds 0%Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÈëëþñòðàöèÿ îïðåäåëåíèÿ áèñèìóëÿöèèÄëÿ ëþáîé ïàðû ñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ â îòíîøåíèèB(s, s 0 ) , âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:2) Äëÿ ëþáîãî ñîñòîÿíèÿ s1 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s, s1) , íàéäåòñÿ ñîñòîÿíèå s10 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿ R 0(s 0, s10 ) è B(s1, s10 ) ;'$'MRB@I@s d&M00ds1s1 dB&%$0@R@ ds 0%Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÈëëþñòðàöèÿ îïðåäåëåíèÿ áèñèìóëÿöèèÄëÿ ëþáîé ïàðû ñîñòîÿíèé s è s 0 , íàõîäÿùèõñÿ â îòíîøåíèèB(s, s 0 ) , âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:2) Äëÿ ëþáîãî ñîñòîÿíèÿ s1 , äëÿ êîòîðîãî âûïîëíÿåòñÿîòíîøåíèå R(s, s1) , íàéäåòñÿ ñîñòîÿíèå s10 , äëÿ êîòîðîãîâûïîëíÿþòñÿ îòíîøåíèÿ R 0(s 0, s10 ) è B(s1, s10 ) ;'$'MRB@I@s d&M00ds1s1 d$0@R@ ds 0B&%È ÍÀÎÁÎÐÎÒ%Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÎïðåäåëåíèå áèñèìóëÿöèèÌîäåëè M è M 0 ñ÷èòàþòñÿ áèñèìóëÿöèîííî ýêâèâàëåíòíûìè(îáîçíà÷àåòñÿ M ∼ M 0 ), åñëè ñóùåñòâóåò òàêîå îòíîøåíèåáèñèìóëÿöèè B , ÷òîI äëÿ âñÿêîãî íà÷àëüíîãî ñîñòîÿíèÿ s0 èç S0 â ìîäåëè Míàéäåòñÿ íà÷àëüíîå ñîñòîÿíèå s00 èç S00 â ìîäåëè M 0 , äëÿêîòîðîãî âûïîëíÿåòñÿ îòíîøåíèå B(s0, s00 ) ,I è äëÿ âñÿêîãî íà÷àëüíîãî ñîñòîÿíèÿ s 0 èç S 0 â ìîäåëè M 000íàéäåòñÿ íà÷àëüíîå ñîñòîÿíèå s0 èç S0 â ìîäåëè M , äëÿêîòîðîãî âûïîëíÿåòñÿ îòíîøåíèå B(s0, s00 ) .Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÏðèìåðû ê îïðåäåëåíèþ áèñèìóëÿöèèbjYab*HHHjHaaYHHH HbÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÏðèìåðû ê îïðåäåëåíèþ áèñèìóëÿöèèbjYab*HHHjHaaYHHH HbÐèñ.: Ðàçâåðòêà ñîõðàíÿåò áèñèìóëÿöèþÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÏðèìåðû ê îïðåäåëåíèþ áèñèìóëÿöèè@@R@@@R@abbabbAAAAAAU??U cccddd Ðèñ.: Äóáëèðîâàíèå ñîõðàíÿåò áèñèìóëÿöèþÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÏðèìåðû ê îïðåäåëåíèþ áèñèìóëÿöèè@@R@abb??c d a?b@@R@ d cÐèñ.: Äâå áèñèìóëÿöèîííî íåýêâèâàëåíòíûå ìîäåëèÎòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÓòâåðæäåíèå 1.Îòíîøåíèå áèñèìóëÿöèè ∼ ýòî îòíîøåíèå ýêâèâàëåíòíîñòè.Îòíîøåíèå áèñèìóëÿöèè è åãî ñâîéñòâàÓòâåðæäåíèå 1.Îòíîøåíèå áèñèìóëÿöèè ∼ ýòî îòíîøåíèå ýêâèâàëåíòíîñòè.Áóäåì ãîâîðèòü, ÷òî äâà ïóòè π = s0, s1, .