8 Отношения бисимуляционной эквивалентности (бисимуляции) и симуляционного квазипорядка (симуляции) на моделях Крипке (1185960)
Текст из файла
Âåðèôèêàöèÿìîäåëåé ïðîãðàììËÅÊÒÎÐ:Âëàäèìèð Àíàòîëüåâè÷ ÇàõàðîâÂëàäèñëàâ Âàñèëüåâè÷ Ïîäûìîâ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, .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
