8. Алгебраические модели систем взаимодействующих процессов. Алгебра процессов - синтаксис. Алгебра процессов - операционная семантика (Лекция)

Ìîäåëèïîñëåäîâàòåëüíûõèïàðàëëåëüíûõâû÷èñëåíèéÂ.À. ÇàõàðîâËåêöèÿ 8.1. Àëãåáðàè÷åñêèå ìîäåëè ñèñòåìâçàèìîäåéñòâóþùèõ ïðîöåññîâ2. Àëãåáðà ïðîöåññîâ: ñèíòàêñèñ3. Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêà4. Ïðîöåññíûå ãðàôû è òåìïîðàëüíûåëîãèêè5. Îòíîøåíèå áèñèìóëÿöèè6. Ðåêóðñèÿ è àáñòðàêöèÿ7. Âåòâÿùàÿñÿ áèñèìóëÿöèÿ8. Ïðèìåíåíèå àëãåáðû ïðîöåññîâ âçàäà÷àõ âåðèôèêàöèè ðàñïðåäåëåííûõñèñòåìÀëãåáðàè÷åñêèå ìîäåëè ñèñòåìâçàèìîäåéñòâóþùèõ ïðîöåññîâÌîäåëè âû÷èñëåíèé, êîòîðûå ðàññìàòðèâàëèñü ðàíåå, âåäóòñâîå ïðîèñõîæäåíèå èëè ÿâëÿþòñÿ áëèçêèìè ðîäñòâåííèêàìèêîíå÷íûõ àâòîìàòîâ.Èõ óñòðîéñòâî è ïîâåäåíèå îïèñûâàåòñÿ ïðè ïîìîùè òàêèõïîíÿòèé êàê ¾ñîñòîÿíèå¿, ¾êîíôèãóðàöèÿ¿, ¾ïåðåõîä¿.Îäíàêî èçâåñòíî, ÷òî ïîâåäåíèå êîíå÷íûõ àâòîìàòîâ, êîòîðîåïðîÿâëÿåòñÿ â ðàñïîçíàâàíèè îïðåäåëåííûõ ÿçûêîâ, ìîæåòáûòü îïèñàíî è àëãåáðàè÷åñêèìè ñðåäñòâàìè ïðè ïîìîùèîïåðàöèé êîíêàòåíàöèè, ñëîæåíèÿ, èòåðàöèè, èç êîòîðûõñòðîÿòñÿ ðåãóëÿðíûå âûðàæåíèÿ.Åñëè àâòîìàòû ïðèìóòñÿ ¾îáùàòüñÿ¿ äðóã ñ äðóãîì,îáìåíèâàÿñü ñîîáùåíèÿìè, òî ìû ïîëó÷èì ñèñòåìóïàðàëëåëüíûõ âçàèìîäåéñòâóþùèõ ïðîöåññîâ.Åñòü ëè ïîäõîäÿùèå àëãåáðàè÷åñêèå ñðåäñòâà äëÿ îïèñàíèÿâû÷èñëåíèé òàêèõ ñèñòåì?Àëãåáðàè÷åñêèå ìîäåëè ñèñòåìÂû÷èñëåíèå ñèñòåìû âçàèìîäåéñòâóþùèõ ïðîöåññîâïðîÿâëÿåòñÿ â âûïîëíåíèè äåéñòâèé .Íåêîòîðûå äåéñòâèÿ çàòðàãèâàþò òîëüêî òîò ïðîöåññ, âêîòîðîì îíè âûïîëíÿþòñÿ.

Òàêèå äåéñòâèÿ íàçûâàþòñÿâíóòðåííèìè . Ïðèìåð âíóòðåííåãî äåéñòâèÿ îïåðàòîðïðèñâàèâàíèÿ.Äðóãèå äåéñòâèÿ ìîãóò âûïîëíÿòüñÿ òîëüêî ñèíõðîííî â ïàðå ñäðóãèìè äåéñòâèÿìè. Ñ ïîìîùüþ òàêèõ ñîãëàñîâàííûõ ïàðäåéñòâèé ïðîöåññû âñòóïàþò âî âçàèìîäåéñòâèå. Ïðèìåðñîãëàñîâàííîé ïàðû äåéñòâèé îïåðàöèè îòïðàâëåíèÿïðèåìàñîîáùåíèé.Âûïîëíåíèå íåêîòîðûå äåéñòâèÿ ìîæåò áûòü çàðåãèñòðèðîâàíîñòîðîííèì íàáëþäàòåëåì, òîãäà êàê äðóãèå äåéñòâèÿ îñòàþòñÿíåäîñòóïíûìè äëÿ íàáëþäåíèÿ. Ïîýòîìó äåéñòâèÿ ñèñòåìûìîæíî ðàçäåëèòü òàêæå íà âèäèìûå è ñêðûòíûå .Àëãåáðàè÷åñêèå ìîäåëè ñèñòåìÄëÿ îáîçíà÷åíèÿ àòîìàðíûõ äåéñòâèé ïðîöåññîâââåäåì ìíîæåñòâî èìåíNames = E ∪ A ∪ {τ },êîòîðîå âêëþ÷àåò â ñåáÿïîìíîæåñòâî E èìåí âèäèìûõ âíóòðåííèõäåéñòâèé ïðîöåññîâ,ïîìíîæåñòâî A èìåí âçàèìîäåéñòâèéïðîöåññîâ,èìÿ τ äëÿ ñêðûòíûõ (íåâèäèìûõ) âíóòðåííèõäåéñòâèé ïðîöåññîâ.Êàæäîå âçàèìîäåéñòâèå ñ èìåíåì a ðåàëèçóåòñÿïàðîé êîìïëèìåíòàðíûõ äåéñòâèé a è a .IIIÀëãåáðàè÷åñêèå ìîäåëè ñèñòåìÏðîöåññû ôîðìèðóþòñÿ èç äåéñòâèé ïðè ïîìîùè îïåðàöèéêîìïîçèöèè, òàêèõ êàêIïîñëåäîâàòåëüíàÿ êîìïîçèöèÿ .

:âûðàæåíèå p1 .p2 îáîçíà÷àåò ïðîöåññ, âñÿêîå âû÷èñëåíèåêîòîðîãî íà÷èíàåòñÿ âû÷èñëåíèåì ïðîöåññà p1 , è ïîçàâåðøåíèè åãî ïðîäîëæàåòñÿ âû÷èñëåíèåì ïðîöåññà p2 ;Iàëüòåðíàòèâíàÿ êîìïîçèöèÿ + :âûðàæåíèå p1 +p2 îáîçíà÷àåò ïðîöåññ, âñÿêîå âû÷èñëåíèåêîòîðîãî ëèáî ÿâëÿåòñÿ âû÷èñëåíèåì ïðîöåññà p1 , ëèáîâû÷èñëåíèåì ïðîöåññà p2 ;Iïàðàëëåëüíàÿ êîìïîçèöèÿ k :âûðàæåíèå p1 kp2 îáîçíà÷àåò ïðîöåññ, âñÿêîå âû÷èñëåíèåêîòîðîãî ïðåäñòàâëÿåò ñîáîé ÷åðåäîâàíèå âû÷èñëåíèéïðîöåññîâ p1 è p2 , ñîïðîâîæäàåìîå âûïîëíåíèåìâçàèìîäåéñòâèÿ.Àëãåáðà ïðîöåññîâ: ñèíòàêñèñÏðîöåññîì íàä ìíîæåñòâîì èìåí Names íàçûâàåòñÿ âñÿêîåâûðàæåíèå (òåðì), êîòîðîå ìîæåò áûòü ïîñòðîåíî ïîñëåäóþùèì ïðàâèëàì:1.

nil ýòî ïðîöåññ;2. åñëè p ýòî ïðîöåññ, à n ýòî èìÿ, òî (n.p) ýòîïðîöåññ;3. åñëè p1 , p2 ýòî ïðîöåññû, òî (p1 .p2 ) , (p1 + p2 ) , (p1 k p2 ) ýòî ïðîöåññû;4. è íèêàêèõ äðóãèõ ïðîöåññîâ íå áûâàåò.Ìíîæåñòâî âñåõ ïðîöåññîâ îáîçíà÷èì çàïèñüþ Proc .Ïðîöåññàìè ÿâëÿþòñÿ ñëåäóþùèå òåðìû:Inil ∈ Proc ,Ia.nil ∈ Proc , ā.nil ∈ Proc , τ.nil ∈ Proc ,I(a.nil) k (ā.nil) ∈ Proc ,I(τ.nil) + ((a.nil) k (ā.nil)) ∈ Proc .Àëãåáðà ïðîöåññîâ: ñèíòàêñèñÏîïðîáóåì ïîñòðîèòü ñèñòåìó âçàèìîäåéñòâóþùèõ ïðîöåññîâ,ñîñòîÿùóþ èçÊîôåéíîãî àïïàðàòà×åëîâåêà-ïîëüçîâàòåëÿCòàêàíàÀëãåáðà ïðîöåññîâ: ñèíòàêñèñÑöåíàðèé ðàáîòû ýòîé ñèñòåìû òàêîâ:Àëãåáðà ïðîöåññîâ: ñèíòàêñèñÑöåíàðèé ðàáîòû ýòîé ñèñòåìû òàêîâ:1) Ïîëüçîâàòåëü îïóñêàåò ìîíåòó â àâòîìàò,2) âûáèðàåò æåëàåìûé âèä êîôå,3) íàæèìàåò íà êíîïêó,4) çàáèðàåò ñòàêàí ñ íàïèòêîì.1) Àâòîìàò ïðîâåðÿåò ìîíåòó,2) ïðèíèìàåò çàêàç íà êîôå,3) ãîòîâèò êîôå,4) íàëèâàåò êîôå â ñòàêàí.1) Ñòàêàí ïðèíèìàåò â ñåáÿ êîôå,2) îòäàåòñÿ â ðóêè ïîëüçîâàòåëÿ.Àëãåáðà ïðîöåññîâ: ñèíòàêñèñSystem:UserChoiceMachineSelectProceedGlassUser k Machine= coin.Choice.button.wait.bring .nil= (espresso.nil) + (americano.nil)====coin.Select.button.Proceed.nil(espresso.nil) + (americano.nil)(make.fill.nil) k Glassfill.bring .nilÀëãåáðà ïðîöåññîâ: ñèíòàêñèñÏðîãðàììà íà ÿçûêå ïðîãðàììèðîâàíèÿ OccamPROCEDURE MachinePROCEDURE Proceed(x,y)SEQPARcoin ? xSEQselect(y)make_coffee(x,y,w)button ? zfill ! wproceed(x,y)GlassPROCEDURE select(x) PROCEDURE GlassALTSEQespresso ? ufill ? vy:=1bring ! vespresso ? uy:=2Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêàÀ êàê îïðåäåëèòü âû÷èñëåíèå ïðîöåññîâ? àëãåáðå ðàçíûå âûðàæåíèÿ ìîãóò èìåòü îäíî è òî æåçíà÷åíèå, ò.å.

áûòü òîæäåñòâåííî ðàâíûìè.Òîæäåñòâåííî ðàâíûå ïðîöåññû èìåþò îäèíàêîâîå ïîâåäåíèå.Ïîýòîìó ñåìàíòèêó âûðàæåíèé â àëãåáðå ïðîöåññîâ îïðåäåëèìïðè ïîìîùè äâóõ îòíîøåíèé:Iîòíîøåíèÿ òîæäåñòâåííîãî ðàâåíñòâà ïðîöåññîâ,ïðè ïîìîùè êîòîðîãî âûäåëÿþòñÿ êëàññû ïðîöåññîâ ñíåîòëè÷èìûì ïîâåäåíèåì, èIîòíîøåíèÿ ïåðåõîäîâ ïðîöåññîâ,ïðè ïîìîùè êîòîðîãî ñîáñòâåííî îïðåäåëÿþòñÿâû÷èñëåíèÿ ïðîöåññîâ.Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêàÎòíîøåíèå òîæäåñòâåííîãî ðàâåíñòâà ïðîöåññîâ ≡ ýòîíàèìåíüøåå îòíîøåíèå êîíãðóåíòíîñòè (îòíîøåíèåýêâèâàëåíòíîñòè, ñîõðàíÿþùååñÿ ïðè ïîäñòàíîâêå) íàìíîæåñòâå Proc , êîòîðîå óäîâëåòâîðÿåò ñëåäóþùèìñîîòíîøåíèÿì:Com+ :p + q ≡ q + p,Assoc+ : p + (q + r ) ≡ (p + q) + r ,Com k:p k q ≡ q k p,Assoc k:p k (q k r ) ≡ (p k q) k r ,Zero :p ≡ nil.p ≡ nil + p ≡ nil k p.Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêàÒàêèì îáðàçîì,≡≡≡≡(nil.nil) k (p k (nil + nil))nil k (p k (nil + nil))nil k (p k nil)nil k ppÄàëåå ìû íå áóäåì ïðîâîäèòü ðàçëè÷èå ìåæäóýêâèâàëåíòíûìè ïðîöåññàìè.Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêàÂâåäåì ôóíêöèþ âçàèìîäåéñòâèÿ ϕ : A → E ,êîòîðàÿ ñîïîñòàâëÿåò êàæäîìó òèïóâçàèìîäåéñòâèÿ a íåêîòîðîå âíóòðåííååàòîìàðíîå äåéñòâèå e = ϕ(a) .Âçàèìîäåéñòâèå äâóõ ïàðàëëåëüíî ðàáîòàþùèõïðîöåññîâ îñóùåñòâëÿåòñÿ çà ñ÷åò ñèíõðîííîãîâûïîëíåíèÿ ïàðû âçàèìîäåéñòâèé ā è a .Íî äëÿ ñòîðîííåãî íàáëþäàòåëÿ è äëÿ òîéñèñòåìû, êîòîðàÿ âêëþ÷àåò â ñåáÿ ýòè ïðîöåññû,èõ âçàèìîäåéñòâèå áóäåò âûãëÿäåòü êàêâûïîëíåíèå ñèñòåìîé âíóòðåííîãî äåéñòâèÿ ϕ(a) .Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêàÎòíîøåíèå ïåðåõîäîâ →⊆ Proc × Names × Proc (åãî òàêæåíàçûâàþò îòíîøåíèåì ñðàáàòûâàíèÿ ïðîöåññîâ)îïðåäåëÿåòñÿ êàê íàèìåíüøåå îòíîøåíèå óêàçàííîãî òèïà,êîòîðîå óäîâëåòâîðÿåò ñëåäóþùèì òðåáîâàíèÿì:äëÿ ëþáûõ x ∈ E ∪ {τ }, p ∈ Proc ;RA :xx.p −→ pxR≡:p 0 ≡ p, p −→ q, q ≡ q 0xp 0 −→ q 0R.

:p −→ qxp.r −→ q.rR+ :p −→ qx(r + p) −→ qxxäëÿ ëþáîãî x ∈ Names ;Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêàR1 k :ϕ(a)äëÿ ëþáîãî âçàèìîäåéñòâèÿ a ∈ A ;a.p k ā.q −→ p k qR2 k :xp −→ qx(r k p) −→ (r k q)äëÿ ëþáîãî âíóòðåííåãî äåéñòâèÿx ∈ E ∪ {τ }Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêàÏðèìåðÏðåäïîëîæèì, ÷òî ϕ(a) = c .

Òîãäàc(b̄.nil + nil.a.nil) k τ.nil k (b.nil + ā.nil) −→ τ.nil,ïîñêîëüêóa.nil k ā.nilnil.a.nilnil.a.nil k ā.nil(b̄.nil + nil.a.nil) k ā.nil(b̄.nil + nil.a.nil k (b.nil + ā.nil)(b̄.nil + nil.a.nil) k (b.nil + ā.nil) k τ.nilnil k τ.nil(b̄.nil + nil.a.nil) k (b.nil + ā.nil) k τ.nilc−→≡c−→c−→c−→c−→≡c−→nil k nila.nilnilnilnilnil k τ.nilτ.nilτ.nilR1 k0R≡R1+R2+R2 k0, Com kR≡Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêàÂû÷èñëåíèå ñèñòåìû âçàèìîäåéñòâóþùèõïðîöåññîâ, çàäàííîé ïðîöåññíûì âûðàæåãèåì t0 ýòî ìàêñèìàëüíàÿ ïîñëåäîâàòåëüíîñòü ïðîöåññîâxxxxxi+1123it0 −→t1 −→t2 −→· −→xi −→ · · · ,ñâÿçàííûõ ìåæäó ñîáîé îòíîøåíèåì ïåðåõîäîâ.Àëãåáðà ïðîöåññîâ: îïåðàöèîííàÿñåìàíòèêàÏðîöåññ ìîæåò èìåòü íåñêîëüêî ðàçëè÷íûõ âû÷èñëåíèéb̄.e1 .nil k b.e2 .nil k b̄.e3 .nilce1 .nil k e2 .nil k b̄.e3 .nile1HHHHcHjHb̄.e1 .nil k e2 .nil k e3 .nile3?e2 .nil k b̄.e3 .nile2?b̄.e1 .nil k e2 .nile2??b̄.e3 .nilb̄.e1 .nilÂñå âû÷èñëåíèÿ ñèñòåìû ðàçóìíî îáúåäèíèòü â îäíîéñòðóêòóðå ïðîöåññíîì ãðàôå .Ïðîöåññíûå ãðàôûÏóñòü èìååòñÿ ïðîöåññ p, p ∈ Proc .Îáîçíà÷èì çàïèñüþ −→∗ ðåôëåêñèâíî-òðàíçèòèâíîåçàìûêàíèå îòíîøåíèÿ ïåðåõîäîâ, è âûäåëèì ìíîæåñòâîïðîöåññîâ p ↓= {p 0 : p −→∗ p 0 } äîñòèæèìûõ èç ïðîöåññà p ïîîòíîøåíèþ ïåðåõîäîâ.Ïðîöåññíûì ãðàôîì , ïîðîæäåííûì ïðîöåññîì p , íàçûâàåòñÿîðèåíòèðîâàííûé ðàçìå÷åííûé ãðàô Γ(p) = ([p ↓]≡ , −→) , âêîòîðîìIìíîæåñòâî âåðøèí [p ↓]≡ ýòî ôàêòîð-ìíîæåñòâîïðîöåññîâ, äîñòèæèìûõ èç ïðîöåññà p , ïî îòíîøåíèþòîæäåñòâåííîñòè ïðîöåññîâ ≡ ;Ièç âåðøèíû [q]≡ â âåðøèíó [r ]≡ âåäåò äóãà, ïîìå÷åííàÿèìåíåì x â òîì è òîëüêî òîì ñëó÷àå, åñëè äîïóñòèìxïåðåõîä q −→ r .Ïðîöåññíûå ãðàôûÏðèìåð ïðîöåññíîãî ãðàôà(a.nil + e1 .nil) k (ā.nil + e2 .nil)e1c@HHHe2 @e1@e2 .nile2 - nil? e1?e1 .nilR@ā.nilHe2HHHHja.nilÏðîöåññíûå ãðàôûÏðîöåññíûé ãðàô Γ(p) = ([p ↓]≡ , −→) ýòî ñèñòåìà ïåðåõîäîâ,äóãè êîòîðîé ðàçìå÷åíû èìåíàìè áàçîâûõ äåéñòâèé.Èìåíà áàçîâûõ äåéñòâèé ìîæíî ðàññìàòðèâàòü êàêýëåìåíòàðíûå (àòîìàðíûå) ëîãè÷åñêèé óñëîâèÿ èíäèêàòîðûâûïîëíåíèÿ ýòèõ äåéñòâèé.Ïðîöåññíûå ãðàôûÏðîöåññíûé ãðàô Γ(p) = ([p ↓]≡ , −→) ýòî ñèñòåìà ïåðåõîäîâ,äóãè êîòîðîé ðàçìå÷åíû èìåíàìè áàçîâûõ äåéñòâèé.Èìåíà áàçîâûõ äåéñòâèé ìîæíî ðàññìàòðèâàòü êàêýëåìåíòàðíûå (àòîìàðíûå) ëîãè÷åñêèé óñëîâèÿ èíäèêàòîðûâûïîëíåíèÿ ýòèõ äåéñòâèé.(a.nil + e1 .nil) k (ā.nil + e2 .nil)e1c@HHe2 @e1@e2 .nile2 - nil? e1?e1 .nilR@HHe2Hā.nilHHjHa.nilÈ òîãäà äëÿ îïèñàíèÿ ñâîéñòâ âû÷èñëåíèé âçàèìîäåéñòâóþùèõïðîöåññîâ ìîæíî èñïîëüçîâàòü òåìïîðàëüíûå ëîãèêè CTL,LTL, CTL∗ , ñåìàíòèêà êîòîðûõ çàäàåòñÿ ïðè ïîìîùèðàçìå÷åííûõ ñèñòåì ïåðåõîäîâ (ìîäåëåé Êðèïêå).Ïðîöåññíûå ãðàôûÏðîöåññíûé ãðàô Γ(p) = ([p ↓]≡ , −→) ýòî ñèñòåìà ïåðåõîäîâ,äóãè êîòîðîé ðàçìå÷åíû èìåíàìè áàçîâûõ äåéñòâèé.Èìåíà áàçîâûõ äåéñòâèé ìîæíî ðàññìàòðèâàòü êàêýëåìåíòàðíûå (àòîìàðíûå) ëîãè÷åñêèé óñëîâèÿ èíäèêàòîðûâûïîëíåíèÿ ýòèõ äåéñòâèé.deadlock: ∂ ye1e2y@ e@2R y@e1y@- y∂ deadlockce2@@Ry@?e1nilÈ òîãäà äëÿ îïèñàíèÿ ñâîéñòâ âû÷èñëåíèé âçàèìîäåéñòâóþùèõïðîöåññîâ ìîæíî èñïîëüçîâàòü òåìïîðàëüíûå ëîãèêè CTL,LTL, CTL∗ , ñåìàíòèêà êîòîðûõ çàäàåòñÿ ïðè ïîìîùèðàçìå÷åííûõ ñèñòåì ïåðåõîäîâ (ìîäåëåé Êðèïêå).Ïðîöåññíûå ãðàôûdeadlock: ∂ ye1e2y@ e@2R y@e1y@- y∂ deadlockce2@@R?@ynile1Íàïðèìåð, èíòåðåñ ïðåäñòàâëÿþò òàêèå ñâîéñòâà âû÷èñëåíèé:I AF nilÏðàâäà ëè, ÷òî êàæäîå âû÷èñëåíèå çàâåðøàåòñÿ óñïåøíî ?(Îòâåò: ÍÅÒ)I EG EF nilÏðàâäà ëè, ÷òî íåêîòîðîå âû÷èñëåíèå ìîæíî âñåãäàíàïðàâèòü ê óñïåøíîìó çàâåðøåíèþ ? (Îòâåò: ÄÀ)I A (c R ¬e1 )Ïðàâäà ëè, ÷òî äåéñòâèå e1 âûïîëíÿåòñÿ íå ðàíüøå, ÷åìäåéñòâèå c ? (Îòâåò: ÍÅÒ)Îòíîøåíèå áèñèìóëÿöèèÏðîöåññíûå ãðàôû ìîæíî ñðàâíèâàòü ìåæäóñîáîé ïî îòíîøåíèþ âçàèìíîãî ìîäåëèðîâàíèÿ(áèñèìóëÿöèè).Îòíîøåíèå áèñèìóëÿöèè íà ìíîæåñòâå ïðîöåññîâProc ýòî òàêîå ñèììåòðè÷íîå ðåôëåêñèâíîåáèíàðíîå îòíîøåíèå R, R ⊆ Proc × Proc ,êîòîðîå óäîâëåòâîðÿåò ñëåäóþùèì òðåáîâàíèÿì:1.

nil R p ⇒ px≡ nil ,x2. p R p0 ∧ p −→ q ⇒ ∃q0 : p0 −→q0 ∧ q R q0 .Äâà ïðîöåññà p è q ñ÷èòàþòñÿ áèñèìóëÿöèîííîýêâèâàëåíòíûìè (p ∼ q ), åñëè ñóùåñòâóåò òàêîåîòíîøåíèå áèñèìóëÿöèè R , äëÿ êîòîðîãîâûïîëíÿåòñÿ pRq .Îòíîøåíèå áèñèìóëÿöèèÏðîöåññû e1 .nil k e2 .nil è e1 .e2 .nil + e2 .e1 .nil áèñèìóëÿöèîííîýêâèâàëåíòíû èõ ïðîöåññíûå ãðàôû èçîìîðôíû.Ïðîöåññû e0 .(e1 .nil + e2 .nil) è e0 .e1 .nil + e0 .e2 .niláèñèìóëÿöèîííî ýêâèâàëåíòíûìè.e0 .e1 .nil + e0 .e2 .nile0 .(e1 .nil + e2 .nil)e0?e1- nil &@e0e1 .nil + e2 .nilíå ÿâëÿþòñÿe1 .nile2%@@e1@R@@ e0@R@e2 .nile2nilÎòíîøåíèå áèñèìóëÿöèèÎêàçûâàåòñÿ, ÷òî îòíîøåíèå áèñèìóëÿöèèïðîöåññîâ ñîõðàíÿåò âûïîëíèìîñòü ôîðìóëòåìïîðàëüíûõ ëîãèê íà ïðîöåññíûõ ãðàôàõ.Òåîðåìà 1.Äâà ïðîöåññà p è q áèñèìóëÿöèîííîýêâèâàëåíòíû â òîì è òîëüêî òîì ñëó÷àå, åñëèäëÿ ëþáîé ôîðìóëû ϕ òåìïîðàëüíîé ëîãèêè CTL∗ñïðàâåäëèâî ñîîòíîøåíèåΓ(p) |= ϕ ⇔ Γ(q) |= ϕ.Îòíîøåíèå áèñèìóëÿöèè1.