9. Особенности мобильной связи. π-исчисление мобильных процессов. Синтаксис π-исчисления. Операционная семантика π-исчисления (1265180)
Текст из файла
Ìîäåëèïîñëåäîâàòåëüíûõèïàðàëëåëüíûõâû÷èñëåíèéÂ.À. ÇàõàðîâËåêöèÿ 9.1. Îñîáåííîñòè ìîáèëüíîé ñâÿçè2. π-èñ÷èñëåíèå ïðîöåññîâ3. Îïåðàöèîííàÿ ñåìàíòèêàπ -èñ÷èñëåíèÿ4. Êðèïòîãðàôè÷åñêèå ïðîòîêîëû5. spi-èñ÷èñëåíèå: ñèíòàêñèñ è ñåìàíòèêà6. Ïðèìåíåíèå spi-èñ÷èñëåíèÿ âêðèïòîàíàëèçåÎñîáåííîñòè ìîáèëüíîé ñâÿçèÀëãåáðû ïðîöåññîâ ýòî ïðîñòîå è âûðàçèòåëüíîå ñðåäñòâîîïèñàíèÿ ñèñòåì âçàèìîäåéñòâóþùèõ ïðîöåññîâ.
Íî èíîãäàâîçìîæíîñòåé ýòîé àëãåáðû íåäîñòàòî÷íî äëÿ ïîñòðîåíèÿàäåêâàòíîé ìàòåìàòè÷åñêîé ìîäåëè èíôîðìàöèîííîé ñèñòåìû.1. Ïðåäïîëîæèì, ÷òî Àëèñà ïîëó÷àåò ñîîáùåíèå îò Áîáà:¾Ïîçâîíè ïî íîìåðó 123 45 67 è ïîïðîñè àáîíåíòà îòïðàâèòüïîäòâåðæäåíèå ïî àäðåñó abc.def.com¿.Êàê äîëæíà äîëæíà ðåàãèðîâàòü íà ýòî ñîîáùåíèå "Àëèñà" ,êàêèå äåéñòâèÿ îíà äîëæíà ïðåäïðèíÿòü?Îñîáåííîñòü ñîîáùåíèÿ ñîñòîèò â òîì, ÷òî ïåðåñûëàåìûå âíåì äàííûå ýòî èìåíà êàíàëîâ ñâÿçè äëÿ ïîñëåäóþùåéêîììóíèêàöèè, êîòîðûå íåèçâåñòíû çàðàíåå ïðîöåññó "Àëèñà"è ïîýòîìó îòñóòñòâóþò â ÿâíîì âèäå â åãî ïðîãðàììå.Çíà÷èò, âçàèìîäåéñòâóþùèì ïðîöåññàì íóæíû ñðåäñòâààâòîìàòè÷åñêîé íàñòðîéêè êàíàëîâ ñâÿçè íà ¾ïðàâèëüíóþ÷àñòîòó¿.Îñîáåííîñòè ìîáèëüíîé ñâÿçè2.
Ïðåäïîëîæèì äàëåå, ÷òî Àëèñà ïðè îáðàùåíèè ñ äðóãèìïðîöåññîì (íàïðèìåð, ñ ïîèñêîâîé ìàøèíîé) îòêðûâàåò îäèíçà äðóãèì íåñêîëüêî ñåàíñîâ ñ ðàçíûìè çàïðîñàìè.Êàê Àëèñå îòêðûòü ñêîëü óãîäíî ìíîãî ñåàíñîâ ñâÿçè ñ îäíè èòåì æå àáîíåíòîì?Îñîáåííîñòü òàêîãî âçàèìîäåéñòâèÿ ñîñòîèò â òîì, ÷òî Àëèñàäîëæíà èìåòü âîçìîæíîñòü èñïîëüçîâàòü ñêîëü óãîäíî ìíîãîðàçíûõ (âèðòóàëüíûõ) êàíàëîâ ñâÿçè, èìåíà êîòîðûõíåèçâåñòíû çàðàíåå ïðîöåññó "Àëèñà" è ïîýòîìó îòñóòñòâóþò âÿâíîì âèäå â åãî ïðîãðàììå.Çíà÷èò, âçàèìîäåéñòâóþùèì ïðîöåññàì íóæíû ñðåäñòâàïîðîæäåíèÿ íîâûõ èìåí.Îñîáåííîñòè ìîáèëüíîé ñâÿçèÝòè è äðóãèå ïîäîáíîãî ðîäà âîïðîñû âîçíèêàþò â òåõ ñëó÷àÿõ,êîãäà òîïîëîãèÿ êîììóíèêàöèîííîé ñðåäû èçìåíÿåòñÿ ñàìîéðàñïðåäåëåííîé ïðîãðàììîé ïî õîäó åå ðàáîòû.Äëÿ èõ ðåøåíèÿ Ðîáèí Ìèëíåð, Õîàêèí Ïàððîó è ÄåâèäÓîëêåð ïðèäóìàëèèñ÷èñëåíèå ìîáèëüíûõ âçàèìîäåéñòâóþùèõ ïðîöåññîâèëè, êîðîòêî, π-èñ÷èñëåíèå. ýòîé ìîäåëè âû÷èñëåíèé áûëè ïðåäëîæåíû íîâûåìàòåìàòè÷åñêèå ñðåäñòâà îïèñàíèÿ âçàèìîñâÿçè ìåæäóïðîöåññàìè:1.
àïïàðàò ñâîáîäíûõ è ñâÿçíûõ èìåí, äàþùèé âîçìîæíîñòüîáðàçîâûâàòü íåîãðàíè÷åííî áîëüøîå êîëè÷åñòâî êàíàëîâñâÿçè;2. àïïàðàò ïåðåäà÷è è ïðèåìà èìåí, ïîçâîëÿþùèé ñäåëàòüêîììóíèêàöèþ ìîáèëüíîé.π -èñ÷èñëåíèåïðîöåññîâ: ñèíòàêñèñÏóñòü çàäàíî ìíîæåñòâî èìåí Names = {x, y , z, .
. . } .Äåéñòâèåì â π-èñ÷èñëåíèè íàçûâàåòñÿ âñÿêîå âûðàæåíèåîäíîãî èç ñëåäóþùèõ âèäîâ:1. τ íåâèäèìîå äåéñòâèå, ðåçóëüòàò âûïîëíåíèÿ êîòîðîãîíåäîñòóïåí äëÿ íàáëþäåíèÿ èçâíå (ñêðûòíîå äåéñòâèå);2. x̄hy i , ãäå x, y ∈ Names äåéñòâèå îòïðàâëåíèÿ ñîîáùåíèÿ(ïî êàíàëó ñ èìåíåì x îòïðàâèòü ñîîáùåíèå ïî èìåíè y );3. x[y ] , ãäå x, y ∈ Names äåéñòâèå ïðèåìà ñîîáùåíèÿ (ïîêàíàëó x ïîëó÷èòü ñîîáùåíèå è ñäåëàòü åãî çíà÷åíèåìèìåíè y );4.
νx äåéñòâèå ñîçäàíèÿ íîâîãî èìåíè x .Ìíîæåñòâî âñåõ äåéñòâèé îáîçíà÷èì çàïèñüþ Actπ .π -èñ÷èñëåíèå ïðîöåññîâ: ñèíòàêñèñÏóñòü çàäàíî ìíîæåñòâî èìåí Names = {x, y , z, . . . } .Ïðîöåññîì π-èñ÷èñëåíèÿ íàçûâàåòñÿ âñÿêîå âûðàæåíèå,êîòîðîå ìîæåò áûòü ïîñòðîåíî ïî ñëåäóþùèì ïðàâèëàì:1. nil ýòî ïðîöåññ;2. åñëè p ýòî ïðîöåññ, à a ýòî äåéñòâèå, òî ïðîöåññîìÿâëÿåòñÿ âûðàæåíèå a.p (âûïîëíèòü äåéñòâèå a è äàëååâûïîëíÿòü ïðîöåññ p );3. åñëè p1 è p2 ýòî ïðîöåññû, òî ïðîöåññàìè ÿâëÿþòñÿòàêæå âûðàæåíèÿ(p1 p2 ) âíà÷àëå âûïîëíèòü ïðîöåññ p1 , à çàòåìâûïîëíèòü ïðîöåññ p2 ;(p1 + p2 ) âûáðàòü è âûïîëíèòü îäèí èç äâóõ ïðîöåññîâp1 èëè p2 ;(p1 k p2 ) âûïîëíÿòü ïàðàëëåëüíî ïðîöåññû p1 è p2 ;(!p1 ) âûïîëíÿòü ïàðàëëåëüíî íåñêîëüêî êîïèé ïðîöåññàp1 .Ìíîæåñòâî âñåõ ïðîöåññîâ îáîçíà÷èì çàïèñüþ Procπ ..π -èñ÷èñëåíèåïðîöåññîâ: ñèíòàêñèñÏðèìåðû ïðîöåññîâ.TrentAlice:Bob::athteli.
athe-maili.e-mail[S]. nilkat[X ]. at[Y ]. X hY i.nilktel[Z ]. ν secret. Z hsecretei. nilTrent ïðè ïîìîùè Alice óñòàíàâëèâàåò íàäåæíûéêàíàë ñâÿçè ñ ïðîöåññîì Bob è ïîëó÷åò îò íåãîñåêðåòíûå ñâåäåíèÿ.π -èñ÷èñëåíèåïðîöåññîâ: ñèíòàêñèñÏðèìåðû ïðîöåññîâ.:!(ν req. ν new . chhreqi. chhnew i. new [X ]. nil)Alice:Bobk!(ch[X ]. ch[Y ]. Proc(X , resp). Y hrespi. nil)Alice ïîñòîÿííî îïðàøèâàåò ïðîöåññ Bob, ïîëó÷àÿíà êàæäûé çàïðîñ îòäåëüíûé îòâåò.π -èñ÷èñëåíèå ïðîöåññîâ: ñèíòàêñèñ ïðîöåññàõ π-èñ÷èñëåíèÿ âñå âõîæäåíèÿ èìåí ðàçäåëÿþòñÿ íàñâîáîäíûå è ñâÿçàííûå .Ñâîáîäíûå èìåíà ýòî ãëîáàëüíûå ïàðàìåòðû ïðîöåññà,¾îòêðûòûå¿ äëÿ âíåøíåé ñðåäû.
Ñâÿçíûå èìåíà ýòîëîêàëüíûå îáúåêòû, íåäîñòóïíûå äëÿ âîçäåéñòâèÿ èçâíå.Ñ êàæäûì ïðîöåññîì P àññîöèèðîâàíî ìíîæåñòâî ñâîáîäíûõèìåí fn(P) è ìíîæåñòâî ñâÿçíûõ èìåí bn(P) , êîòîðûåôîðìèðóþòñÿ íà îñíîâàíèè ñëåäóþùèõ ïðàâèë:1) fn(nil) = bn(0) = ∅ ,2) åñëè P = x̄hy i. p , òî fn(P) = fn(p)∪{x, y }, bn(P) = bn(p), ,à ñâîáîäíûìè âõîæäåíèÿìè èìåí â ïðîöåññ P ñ÷èòàþòñÿâñå ñâîáîäíûå âõîæäåíèÿ èìåí èç ìíîæåñòâà fn(P) âïðîöåññ p , à òàêæå âõîæäåíèÿ èìåí x è y â òåðì x̄hy i ;3) åñëè P = x[y ]. p , òî fn(P) = fn(p)∪{x}, bn(P) = bn(p)∪{y },à ñâîáîäíûìè âõîæäåíèÿìè èìåí â ïðîöåññ P ñ÷èòàþòñÿâñå ñâîáîäíûå âõîæäåíèÿ èìåí èç ìíîæåñòâà fn(P) âïðîöåññ p , à òàêæå âõîæäåíèå èìåíè x â òåðì x[y ] ;π -èñ÷èñëåíèåïðîöåññîâ: ñèíòàêñèñ4) åñëè P = ν x.
p , òî fn(P) = fn(p) \ {x}, bn(P) = bn(p)∪{x},à ñâîáîäíûìè âõîæäåíèÿìè èìåí â ïðîöåññ P ÿâëÿþòñÿâñå ñâî- áîäíûå âõîæäåíèÿ èìåí èç ìíîæåñòâà fn(P) âïðîöåññ p ;5) åñëè P = p. q , èëè P = p + q , èëè P = p k q , òîfn(P) = fn(p)∪ fn(q), bn(P) = bn(p)∪bn(q) , à ñâîáîäíûìèâõîæäåíèÿìè èìåí â ïðîöåññ P ñ÷èòàþòñÿ âñå ñâîáîäíûåâõîæäåíèÿ èìåí èç ìíîæåñòâà fn(P) â ïðîöåññû p è q ;6) åñëè P =!p , òî fn(P) = fn(p), bn(P) = bn(p) , à ñâîáîäíûìèâõîæäåíèÿìè èìåí â ïðîöåññ P ñ÷èòàþòñÿ âñå ñâîáîäíûåâõîæäåíèÿ èìåí èç ìíîæåñòâà fn(P) â ïðîöåññ p .Ñâÿçàííûìè âõîæäåíèÿìè èìåí â ïðîöåññ îáúÿâëÿþòñÿ âñåâõîæäåíèÿ èìåí, íå ÿâëÿþùèåñÿ ñâîáîäíûìè âõîæäåíèÿìè.π -èñ÷èñëåíèåïðîöåññîâ: ñèíòàêñèñÏðèìåð.xhy i. ν x.
x[z]. nil k x[x]. xhzi. nilπ -èñ÷èñëåíèåïðîöåññîâ: ñèíòàêñèñÏðèìåð.xhy i. ν x. x[z]. nil k x[x]. xhzi. nil6 6666ñâÿçíûå âõîæäåíèÿπ -èñ÷èñëåíèåïðîöåññîâ: ñèíòàêñèñÏðèìåð.xhy i. ν x. x[z]. nil k x[x]. xhzi. nil6 66ñâîáîäíûå âõîæäåíèÿ6π -èñ÷èñëåíèåïðîöåññîâ: ñèíòàêñèñÏðèìåð.xhy i. ν x. x[z]. nil k x[x]. xhzi. nilπ -èñ÷èñëåíèåïðîöåññîâ: ñåìàíòèêàÍà ìíîæåñòâå ïðîöåññîâ Procπ îïðåäåëèì ïðè ïîìîùèòîæäåñòâ îòíîøåíèå ñòðóêòóðíîé ýêâèâàëåíòíîñòè ≡ , ïîäîáíîòîìó, êàê ýòî áûëî ñäåëàíî â àëãåáðå ïðîöåññîâ.Íîâûå òîæäåñòâàRen1 :νx.p ≡ νy .p{x/y },åñëè y ∈/ names(p)Ren2 :n[x].p ≡ n[y ].p{x/y },Com ν :ν x. ν y . p ≡ ν y .
ν. x. p,Zero ν :ν x. nil ≡ nil,Ext :(νx. p) k q ≡ νx. (p k q)åñëè y ∈/ names(p)åñëè x ∈/ fn(q).π -èñ÷èñëåíèåïðîöåññîâ: ñåìàíòèêàÎòíîøåíèå ïåðåõîäîâ →⊆ Procπ × Acts × Procπ îïðåäåëÿåòñÿêàê íàèìåíüøåå îòíîøåíèå óêàçàííîãî òèïà, êîòîðîåóäîâëåòâîðÿåò ñëåäóþùèì òðåáîâàíèÿì:RA : τ. p −→τpαR≡:p 0 ≡ p, p −→ q, q ≡ q 0αp 0 −→ q 0R.:p −→ qαp.r −→ q.rR+:p −→ qx(r + p) −→ qαxπ -èñ÷èñëåíèåRν :RCν x.
p −→ p:Rk:ïðîöåññîâ: ñåìàíòèêàx̄hy ix̄hy i. p k x[z]. q −→ p k q{z/y }αïðè óñëîâèè y ∈/ bn(q)ãäå α = x̄hy i èëè α = τ .p −→ p 0αp k q −→ p 0 k qÂû÷èñëåíèå ïðîöåññà p ýòî ïîñëåäîâàòåëüíîñòü ïåðåõîäîâααα123p −→p1 −→p2 −→···π -èñ÷èñëåíèåïðîöåññîâ: ñåìàíòèêàÏðèìåðû âû÷èñëåíèÿ ïðîöåññîâ.Trent::athteli.
ν e-mail. ath:i.e-mailat[X ]. at[Y ]. X hY i.nilAliceBobe-mailkktel[Z ]. ν secret. Z hsecretei. nilathteli ↓ RC , R k, Com k, Assoc kν e-mail. athe-maili.e-mail[S]. nilkat[Y ]. telhY i.nilktel[Z ]. ν secret. Z hsecretei. nil[S]. nilπ -èñ÷èñëåíèåïðîöåññîâ: ñåìàíòèêàν e-mail. athe-maili.e-mail[S]. nilkat[Y ].
telhY i.nilktel[Z ]. ν secret. Z hsecretei. nil≡ Ext, Ren1ν U.athUi. U [S]. nilkat[Y ]. telhY i.nilktel[Z ]. ν secret. Z hsecretei. nilπ -èñ÷èñëåíèåν U.ïðîöåññîâ: ñåìàíòèêàathUi. U [S]. nilkat[Y ]. telhY i.nilktel[Z ]. ν secret. Z hsecretei. nil↓ RνathUi. U [S]. nilkat[Y ]. telhY i.nilktel[Z ]. ν secret. Z hsecretei. nilπ -èñ÷èñëåíèåïðîöåññîâ: ñåìàíòèêàathUi.
U [S]. nilkat[Y ]. telhY i.nilktel[Z ]. ν secret. Z hsecretei. nilathUi ↓ RC , R k, Com k, Assoc kU [S]. nilktelhUi.nilktel[Z ]. ν secret. Z hsecretei. nilU [S]. nil k telhUi.nil k tel[Z ]. ν secret. Z hsecretei. niltelhUi ↓ RC , R k, Com k, Assoc kU [S]. nil k nil k ν secret. Uhsecretei. nil≡ Ext, Ren1, Zeroν V . U [S].
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.