.Open Process Algebras and Communicating Sequential Processes .Open Introduction This set of notes is a work in progress. Slowly and steadily I'm placing the more on the web. The reader will almost certainly benefit from studying my sources. Meanwhile I am scattering a Hole link all over this page to invite you, the reader, to help me fill in the blanks. Process algebras are very high level models of complex systems or programs. Various actions can take place. The systems can perform (or suffer?) a sequence of actions (a;b;c;...). As a result they change. They can choose between alternative actions (x|y|z...). .Box Notation In the printed papers and books plus and minus are used, instead of '|' and ';', by the way. Systems can execute some actions in parallel and/or communicate. This I'll show as "<&>", however a vertical bar is used in the literature. The overall behavior is modelled by the idea that the different actions are interleaved or merged ("<*>"). .Close.Box We can distinguish detailed models .See http://www.csci.csusb.edu/dick/maths/math_76_Concurency.html like Petri Nets and Computation Graphs from the more abstract Process Algebras developed described below. Also see the following alternative models of complex dynamic systems: General Systems theory and automata: .See http://www/dick/maths/math_71_Auto...Systems.html , Systems algebras: .See http://www/dick/maths/math_72_Systems_Algebra.html , and theories of programs: .See http://www/dick/maths/math_75_Programs.html An informal introduction to Process Algebras can be found at .See http://en.wikipedia.org/wiki/Process_Algebra on the Wikipedia. I've recently found .See [Fokkink07] , a text on a newer version of $ACP + data abstraction -- \mu_CRL. . Current developments By adding probabillities to Process Algebras Jane Hilston has opened up a rich vein of research .See ../samples/PEPA.html into using Process Algebras to help predict performance. . Sources Process Algebras developed after Hoare's work on Communicating Sequential Processes ($CSP) .See [Hoare81] and Milner's Calculus of Communicating Systems (CCS) .See [Milner80] both of which are still worth studying. Information on .See Basic Process Algebras and $ACP (below) came from sources like: (BerKop90): JA Bergstra & J W Kop(pp1-22) in Baeton 90. J C M Baeton(ed) Applications of Process Algebra, Cambridge U. Press 1990. (Vran97): J L M Vrancken, The Algebra of Communicating Processes with empty process, Theor Comp Sci V177 pp287-328 1997. Probably the simplest of these schemes is LOTOS: LOTOS::=Language of Temporal Ordering Specifications. .See http://www.cs.stir.ac.uk/~kjt/research/well/ .See http://wwwtios.cs.utwente.nl/lotos/ .See http://lotos.csi.uottawa.ca/Links etc. LOTOS is an international standard ISO8807:1989: .See http://www.iso.org/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=16258 and so the following just gives a feeling for the system. Or else see .See LOTOS in MATHS below. .Open LOTOS in MATHS LOTOS_MATHS::=following .Net Process::Sets. Action::Sets. For P,Q,R,S:Process. For a,b,c,d:Action. For A,B:@Action. P-a->Q::@=P can be observed executing action a and then behaving like Q. Ready-signal->Process_signal. STOP::Process, takes part in no actions. |-(stop): for no a:Action, some P:Process( STOP-a->P). EXIT::Process, can only be seen to terminate. \delta::Action=observable termination of a Process THe EXIT Process can only terminate (\delta) and then STOP. |-(exit1): EXIT -\delta->STOP. |-(exit2): for no a:Action~\delta, some P:Process( EXIT-a->P). . Process Descriptions a;P ::Process= a prefix P. Ready = signal;Process_signal. Note. An expression like a;b;c;P has to be parsed as a;(b;(c;P))) because a;b is not an Action. P>>Q::Process=P disabled by Q. Note the standard notation is [> not >>. Working >> interupt; Handle_interupt. Normal >> exception; Catch_exception_and_continue. Note. I'm not sure of the associativity of >>: Is P>>Q>>R the same as P>>(Q>>R) or (P>>Q)>>R. I don't know whether the meaning is same either! .Hole P|A|Q::Process=P and Q synchonizing on A. User|{give_data, get_data}|System. Note. Again I don't know the Precedence of >> vs |...| or the associativity of |...|. .Hole . Structural Operational Semantics The semantics/meaning of LOTOS expressions can be given as rules describing the conditions for a transition P-a->Q to occur. Note. in MATHS we write X:-Y, Z to mean X if Y and Z, as in Prolog. |-(step): a;P-a->P. |-(nointerupt): P>>Q-a->R>>Q :- a<>\delta, P-a->R. Notice that Q can interupt P later... |-(termination): P>>Q-\delta->R :- P-\delta->R. |-(interupt): P>>Q-a->R :- Q-a->R. Notice how Q overides P. |-(alone1): P|A|Q-a->R|A|Q :- a not_in A| \delta, P-a->R. |-(alone2): P|A|Q-a->P|A|R :- a not_in A | \delta, Q-a->R |-(shared): P|A|Q-a->R|A|S :- a in A | \delta, a=b, P-a->R, Q-b->S. Note. I'm not sure about expressions like P|{a,b}|(Q|{a,c}|R) allow P, Q, and R all to evolve with an action a at the same time. .Hole .Open example .Net Proc::= Pdcc |ctrlc| Edcc. Pdcc::= Ping>>CtrlC. Ping::=ping; EXIT. CtrlC::=ctrlc; EXIT. Edcc::=EXIT>>CtrlC. then we can show ()|- Ping-ping->EXIT. ()|- Pdcc-ping->EXIT>>CtrlC ()|- Proc-ping->(EXIT>>CtrlC)[ctrlc]Edcc. .Close.Net .Close example More on LOTOS: .Hole . ACTONE LOTOS combined with Abstract data types. .Hole .Close.Net LOTOS_MATHS .Close LOTOS in MATHS .Open Communicating Sequential Processes CSP::=following, .Net Process::Finite_sets. For P,Q,R,X,Y:Process. Event::Finite_sets. For x,y,z:Event. For A,B,C:@Event. Each Process has a set of events assoicated with it. \alpha::Process->@Event. then::Event> Process. The above declaration does not capture one rule. We can only prefix a process with an event in that processes alphabet. a then P is only correct when a in \alpha(P). |-(fixed_alpha): \alpha(x then P) = \alpha(P). \leftarrow::=then. A left pointing arrow is the original notation. \mu[X:A](P(X)) ::Process= the X(\alpha(X)=A and X=P(X)). This is used to formulate (and clarify) recursive defininitions. Example: CLOCK = tick then CLOCK iff CLOCK = \mu[X:{tick}](tick then X). Mutual recursive definitions are allowed and have solutions as long as each LHS is defined once and only once. If there are choices($Choice next) then each alternative must have a defferent set of prefixes. . Choice The most general form is For B in @\alpha(P), (x:B then P(x))::Process, choose an x in B and then follow process R that depends n the choice of x in B. For x,y:Alpha(P), \alpha(P)=\alpha(Q), (x then P | y then Q)::Process = (z:{x,y} then if(z=x, P, Q)). |- \alpha(x then P | y then Q) = \alpha(P)=\alpha(Q). Extended to (x then P | y then Q | x then R | ...), STOP::=(x:{} then P), no choice leads anywhere. |-(singleton): (x:{e} then P(x)) = e then P(e). The above is reminiscient of Gries's (later) notations: F(x:B. P. R) and Unity. . Laws |-(id): ( (x:A then P(x)) = (y:B then Q(y) ) iff (A=B and for all x:A(P(x) iff Q(x))). (STOP, id)|-(STOPunique): STOP <> (d then P). (id)|- if c<>d then (c then P)<>(d then Q). ()|-(comm): (c then P | d then Q) = (d then Q|c then P). (id)|-(c then P)=(c then Q) iff )P iff Q). if F(X) is a properly guarded expression then (Y=F(Y)) iff (Y=\mu[X](F(X))).. |- \mu[X](F(X)) = F( \mu[X](F(X)) ). Can show that every well defined process is a fuction mapping a set of initally acceptable events into a set of future behaviors. . Traces More "Real Soon Now"... .Hole CSP .Close.Net CSP .Close Communicating Sequential Processes .Close Introduction .Open Process Algebras . Basic Process Algebras Basic_Process_Operators::=following, .Net Original notation used multiplication and addition. Actions::Sets. A::=Actions, -- local abbreviation. For x,y,z:$A, x,y,z are used for general actions. Choices: x | y ::$A= the process which choose to either do x or y. |- (A1_2): $abelian_semigroup($A,(|)). (-1)|- x|y = y|x. (-2)|- (x|y)|z = x|(y|z). Normally we omit parentheses. |- (A3): $idempotent(|). (-1)|- x|x = x. Sequence: x;y ::$A= the process that first does x and then does y. |- (A5): $semigroup($A,(;)). (-1)|- (x;y);z = x; (y;z). Normally we omit parentheses. Note: (;) has a higher priority than (|) in MATHS so we can omit parentheses (a;B) | C = a;B | C. However we do not assume that (;) distributes over (|)... until $BPA. Note. I could declare (|) and (;) to be serial operators which would allow actions like |[i:1..10] a(i) We usually have a set of atomic steps which are used to describe more complex actions. For example in modelling a vending machine an atomic step might be insert money and another give change. Atomic_steps::@$A. S::=$Atomic_steps. For a,b,c:$S, a,b,c are used for atomic steps. I'm not sure if the next property is very important. It seems intuitive but it is not usually stated in the literature. ATOMICITY::@=atoms can not be decomposed. |- ATOMICITY iff for no a:$S, some x,y:$A( a=x;y or a=x|y). .Close.Net BPA Operators used in $BPA,$SHARED_ACTIONS... below. BPA::=Basic_Process_Algebra. Basic_Process_Algebra::=$Basic_Process_Operators with following, .Net Making a choice and then acting is the same as choosing one of two sequences: |- (A4): for x,y,z:$A((y|z);z=(x;z)|(y;z)). $BPA does not specify full distributivity because (z;y)|(z;y) =z;(x|y) implies that a (z;y)|(z;y) can start to execute z;x and then change its mind and execute z;y instead. This is called backtracking. CTM::@=closed term model, |-$CTM iff $A is_finitely_generated_by_applying {(|),(;)} to$S. .Hole finitely_generated One of the key reasons for studying the CTM is that we can prove results by induction. If a result is true of all atomic steps and is preserved however we assemble the processes, then the result is true for all possible processes. As a result the result suggest possible assumptions to make when we don't know that the terms are constructed by a finite process for known atomic steps/pieces. They can also be taken as axioms when the CTM is not assumed. An alternative model is based on labelled graphs. .Close.Net $BPA is used in$DEADLOCK, $BASIC_COMMUNICATION,$COMMUNICATION, $MERGE_AND_COMMUNICATION,$ACP, $SILENCE,$ABSTRACTION, $STANDARD_CONCURRENCY,$BPA_EMPTY, below. . Special Processes and Combinations DEADLOCK::=Net{ |- $BPA. deadlock::$A. \delta::=$deadlock, standard notation use the Greek letter for "d". ATOMIC_DELTA::@=\delta in atomic_steps. |- (A6): for all x:$A( \delta|x=x), -- processes avoid deadlock if they have the choice. |- (A7): for all x:$A( \delta;x=\delta). --However precess can not proceed past a deadlock. }=::DEADLOCK. BASIC_COMMUNICATION::=Net{Original notation uses a vertical bar to show communication. |-$BPA. x <&> y ::$A=the process in which x communicates with y, The idea is that the two actions must occur quasi-simultaneaously. It is not necessary that information is actually transfered. Just that two things (x and y) happen at one time. |- (C1_2):$abelian_semigroup($A, <&>). HANDSHAKING::@=all communication occurs in pairs. |- HANDSHAKING = for all x,y,z ( x<&>y<&>z = \delta ). }=::BASIC_COMMUNICATION. COMMUNICATION::=Net{ |-$BPA. |- $DEADLOCK. |-$BASIC_COMMUNICATION. \gamma::S>S|{\delta}, defines those atomic steps that can occur at the same time. The function \gamma either gives the name of the pair. If the name is \delta then the system can not execute both actions at the same time without deadlock occurring. For all a,b:S, if \gamma(a,b)<>\delta then a and b are two parts of a single action \gamma(a,b) else a and b will deadlock the system. |- (C3): For a:S, \delta<&>a=\delta. }=::COMMUNICATION. MERGE::=Net{ Merging describes how a collection of parts evolve by interleaving different actions. |-$BASIC_COMMUNICATION. For x,y, x<*>y::$A=free merge of x with y, Original uses a double bar for <*> For x,y, x>*>y::A$=auxilary notation. Left merge. |-(CM1): For x,y, x<*>y::= x>*>y | y>*>x | x<&>y. Original notation used a double vertical bars with an underscore on the right "||_" |-(CM2): a>*>x=a;x. |-(CM3): a;x>*>y=a(x>*>y). |-(CM4): (x|y)>*>z=x>*>z | y>*>z }=::MERGE. MERGE_AND_COMMUNICATION::=Net{ |-$BPA. |-$COMMUNICATION. |-$MERGE. |-(CM5): (a;x)<&>b=(a<&>b);x. |-(CM6): a<&>(b;x)=(a<&>b);x. |-(CM7): (a;x)<&>(b;y)=(a<&>b);(x<&>y). |-(CM8_9): distribute (<&>) over (|). }=::MERGE_AND_COMMUNICATION. . Algebra of Communicating Processes The full algebra allows us to take a whole slew of actions and hide or encapsulate them. ACP::=$Algebra_of_Communicating_Processes. Algebra_of_Communicating_Processes::=Net{ Encapsulation removes (deadlocks) unwanted communication. |-$BPA. |-$DEADLOCK. |-$MERGE_AND_COMMUNICATION. For H:@A, \delta[H]::A->A~H. The operator \delta[H] doesn't hide actions outside of H, |-(D1): For a:A~H, \delta[H](a)=a. The operator \delta[H] does hide actions in H, |-(D2): For a:H, \delta[H](a)=\delta. Encapsulation preserves sequence and choice while hiding some actions: |-(D3_4): \delta[H] in ((;), (|)) A->(A~H). }=::Algebra_of_Communicating_Processes. SILENCE::= Net{ |-BPA. \tau::A=the silent step. ??{\tau in A~S}? Axioms from Milner's CCS. |-(T1): x;\tau=x. |-(T2): \tau;x=\tau;x|x |-(T3): a;(\tau;x|y)=a;(\tau;x|y)|a;x. |-$COMMUNICATION. |-(TM1): \tau>*>x=\tau;x. |-(TM2): \tau;x >*> y = \tau;(x <*> y). |-(TC1_2): \tau<&>x=x<&>\tau=\delta. |-(TC3): \tau;x <&> y = x <&>y. |-(TC4): x<&>(\tau;y)=x<&>y. }=::SILENCE. A system is typically an expression of form <*>(x)=x1<*>x2<*>...<*>x[k] for some list of subsystems(expressions). ABSTRACTION::=Net{ Abstraction is a matter of silencing actions(?atomic steps?). |-$BPA. |-$SILENCE. For I:@S, \tau[I]:: A->A~I, -- assuming I can only be atomic |-(AT1): \tau[I](\tau)=\tau. |-(AT2): For a:A~I, \tau[I](a)=a. |-(AT3): For a:I, \tau[I](a)=\tau. |-(AT4_5): \tau[I] in ((;), (|)) A->(A~I) }=::ABSTRACTION. ACP[\tau]::=$ACP with $ABSTRACTION and following, .Net (DT): \delta[H](\tau)=\tau. .Close.Net . Standard Concurrency Rules for ACP STANDARD_CONCURRENCY::=Net{$ACP. |- <&> and <*> in $associative(A) &$commutative(A). |- >*> in $associative(A). |- (x<&>(a;y))>*>z=x<&>((a;y)>*>z). }=::STANDARD_CONCURRENCY. . Expansion Theorem for ACP EXPANSION_THEOREM::=Net{ |-(H1):$ACP and $HANDSHAKING. (H1)|- For k:3..., x:A^k, <*>(x) = |[i:1..k](x[i]>*>(<*>((1..k)~i);x) | |[i,j:1..k]((x[i]<&>x[j])>*>(<*>((1..k)~{i,j});x). }=::EXPANSION_THEOREM. . Projection PROJECTION::=Net{ |-$ACP[\Tau]. for n:1.., \pi[n]:: A->A. |-(PR1): \pi[1](a;x)=a. |-(PR2): \pi[n+1](a;x)=a;\pi[n](x). |-(PR3): \pi[n](a)=a. |-(PR4): \pi[n](x|y)=\pi[n](x) | \pi[n](y). |-(PR5): \pi[n](\tau)=\tau. |- (PR6): \pi[n](\tau;x)=\tau.\pi[n](x). }=::PROJECTION. . A Topology TOPOLOGY_OF_PROCESSES::=Net{ |-$PROJECTION. for x,y, d(x,y) ::= 2^-n where n:=the least{n:Nat || \pi[n](x)<>\pi[n](y)} |-$METRIC_SPACES. |-d in ultra_metric(A). |-$completion. guarded recursion equations without abstraction guarded V=guard;...V....|.... \tau is never a guard \tau[I] is not used in the equations .Note Why_no_tau::=Net{ X=a;\tau[{a}](X)} has infinitely many solutions {a;q||for some q, \tau[a]q=q}. . Recursion definition principle |-(RDP): all guarded recursion equations without abstraction have a solution. . Recursion specification principle |-(RSP): all guarded recursion equations without abstraction have no more than one solution. . Approximation Induction Principle |-(AIP): A process is determined by its finite projections. For x,y, if for all n:1..(x (= mod \pi[n])y) then x=y. (Weak_AIP): all guarded recursion equations without abstraction have solutions determined by its finite projections }=::TOPOLOGY_OF_PROCESSES. . Alphabets ALPHABET_CALCULUS::=Net{ |-$APC[\tau]. \alpha::A->@S. |-(AC1): \alpha(\tau)=\alpha(\delta)={}. |-(AC2): \alpha(a)={a}. |-(AC3): \alpha(\tau;a)=\alpha(a). |-(AC4): \alpha(a;x)={a}|\alpha(x). |-(AC5): \alpha(x|y)=\alpha(x)|\alpha(y). |-(AC6): \alpha(x)=|[n:1..]\alpha(\pi[n](x)). |-(AC7): \alpha(\tau[I](x))=\alpha(x)~I. if \alpha(x)<&>(\alpha(y)&H) ==>H then \delta[H](x<*>y)=\delta[H](x <*> \delta[H](y)). if \alpha(x)<&>(\alpha(y)&I) ={} then \tau[I](x<*>y)=\tau[I](x <*> \tau[I](y)). if \alpha(x)&H ={} then \delta[H](x)=x. if \alpha(x)&I ={} then \tau[I](x)=x. \delta[H1|H2] = \delta[H1] o \delta[H2]. \tau[I1|I2] = \tau[I1] o \tau[I2]. if H&I={} then \tau[I] o \delta[H] = \delta[H] o \tau[I]. }=::ALPHABET_CALCULUS. . Koomen's Fair Abstraction Rule(KFAR) Gedanken experiment - someone flips a coin behind closed doors until a head occurs. Will they ever come out? .Example Vaandrager_s_room::=Net{ coin_tosser::= flip;( tail; coin_tosser | head). Room::=\tau[{flip,tail}](coin_tosser). if fair then Room = \tau;head else Room=\tau;head|\tau. }=::Vaandrager_s_room. FAIR_1::=Net{ |- APC[\tau]. I:@S. i:I |- (KFAR_1): if x=(i;x | y) then \tau[I](x)=\tau;\tau[I](y). }=::FAIR_1. LIVELOCK::=Net{ |- $APC[\tau] with$FAIR_1. livelock::=(;)[i:Nat](\tau). |- \tau[{i}](Solution{X=i;X}) = livelock ()|-(ld): if FAIR_1 then livelock=deadlock . Proof of ld .Let |- FAIR_1. ()|- \tau[{i}](Solution{X=i;X|\delta}) = livelock, (KFAR_1)|- livelock=\tau;\tau[I](\delta)=\tau;\delta. .Close.Let }=::LIVELOCK. FAIR_2::=Net{ |- $APC[\tau]. I:@S. i1,i2:I (KFAR_2): if x1=(i1;x2 | y1) and x2=i2;x1+y2 then \tau[I](x1)=\tau;\tau[I](y1|y2). }=::FAIR_2. FAIRNESS::=Net{ ... Cluster Fair Abstraction Rule. V:@variables, I:@S. E:@equations: cluster is C:@V such that each eqn in E has form for some C(X) : @C, X= |[c:C(X)] (i(c);X(c))) | |Y X~~>Y exits::=A~C conservative if all exits are reached from every C Then ()|- \tau[I](X)=\tau; |[Y:exits(C)]\tau[I](Y). }=::FAIRNESS. . Empty Processes The idea that it helps to include an empty process that does nothing much comes from Karst Koymans and is worked out in detail by J L M Vranken in the paper [$Vran97] published in Theoretical Computer Science in 1997. BPA_EMPTY::=Net{ |-$BPA. empty::A. \epsilon::=$empty, -- standard notation. |-(E1): $empty+$empty = $empty. |-(E2):$empty; x = x. |-(E3): x; $empty = x. }=::EMPTY. BPA_DELTA_EMPTY::=Net{ |-$BPA_EMPTY. |-$DEADLOCK. |-(DE1): \delta+$empty = $empty, given the choice of do nothing and deadlock, it avoids deadlock. (A7)|-(DE2): \delta;$empty = \delta. }=::BPA_DELTA_EMPTY. PA_DELTA_EMPTY::=Net{ Process algebra with deadlocks and empty processes. |- $BPA_DELTA_EMPTY. <*>::serial(A)=merge. >*>::serial(A)=left merge. |-(PAD1):x<*>y = x>*>y | y>*>x. |- empty >*> empty = empty. |- empty >*> \delta = \delta. |- empty>*>(a;x)=\delta. |-empty>*>(x | y) = (empty>*>x) | (empty>*>y). |- \delta >*> \delta. |- a;x >*> = a; ( x<*> y). |- (x|y)>*>z = x>*>y | y*>z. }=::PA_DELTA_EMPTY. ACP_EMPTY::=Net{ |-$BPA_DELTA_EMPTY <&>::serial(A)=communication. <*>::serial(A)=merge. >*>::serial(A)=left merge. \gamma:: S> S|\delta. |-(ACPDE1): x<*>y = x>*>y | y>*>x | x<&>y. |- empty >*> empty = empty. |- empty >*> \delta = \delta. |- empty>*>(a;x)=\delta. |-empty>*>(x | y) = (empty>*>x) | (empty>*>y). |- \delta >*> \delta. |- a;x >*> = a; ( x<*> y). |- (x|y)>*>z = x>*>y | y*>z. |- a<&>b = \gamma(a,b), much simpler the in $ACP. |- x<&>y = y<*>x. |- empty <&>x = \delta = \delta<&>x. |- a;x<*>y = (a<*>y)>*>x. |- (x|y)<&>z = x<&>z | x<&>z. Compare with$PAD1 above. |- empty >*> empty = empty. |- empty >*> \delta = \delta. |- empty>*>(a;x)=\delta. |-empty>*>(x + y) = (empty>*>x) + (empty>*>y). |- \delta >*> \delta. |- a;x >*> = a; ( x<*> y). |- (x+y)>*>z = x>*>y + y*>z. Here we can replace an action by either empty or deadlock to hide it. For H:@A, r:{\delta, \epsilon}, r[H](x) ::A. |- r[H](empty)=empty. |- r[H](\delta)=delta. |- for x:H~{empty,\delta}, r[H](x) = r. |- for x:A~H, r[H](x) = x. |- r[H](x;y) = r[H](x);r[H](y). |- r[H](x|y) = r[H](x)|r[H](y). Vranken hints at proofs by induction of the following theorems: ()|- if $CTM then x>*>empty = x. ()|- if$CTM then x<*>empty = x. ()|- if $CTM then empty>*>x = empty or \delta. ()|- if$CTM then (empty>*>x = empty iff x|empty=x). ()|- if $CTM then empty>*>(x>*>(y|z))= empty>*>(x>*>y)+empty>*>(x>*>z). ()|- if$CTM then empty>*>x;\delta = \delta. ()|- if $CTM then empty>*>(x|y)= \delta. ()|- if$CTM then (empty>*>(x>*>y)= empty iff(empty>*>x=empty and empty>*>y=empty)). ()|- if $CTM then empty>*>(x>*>y)= empty >*>(x<*>y). ()|- if$CTM then ((empty>*>)x>*>y= empty iff ( empty>*>x=empty and empty>*>y=empty)). ()|- if $CTM then x;\delta>*>y = (x>*>y);\delta. ()|- if$CTM then y>*>x;\delta = (y>*>x);\delta. ()|- if $CTM then x;\delta<&>y = (x<&>y);\delta. ()|- if$CTM then x;\delta<*>y = (x<*>y);\delta. ()|- if $CTM then (x>*>y)>*>z = x>*>(y<*>z). ()|- if$CTM then (x<&>y)>*>z = x<&>(y>*>z). And so to th assoicativity of merge: ()|- if $CTM then associative(A, (<*>)). STANDARD_CONCURRENCY_WITH_EMPTY::=Net{ Replace$STANDARD_CONCURENCY above in $ACP. ()|- if$CTM then all following, .Set (x>*>y)>*>z = x>*>(y<*>z). (y>*>x)>*>z = (x>*>y)>*>z). (x<&>y)>*>z = x<&>(y>*>z). z>*>(x<&>y)=(z>*>y)>*>x. (x>*>y)<&>z = x<*>(z>*>y). (y>*>x)<&>z = (y<&>z)>*>x. (x<&>y)<&>z = x<&>(y<&>z). .Close.Set }=::STANDARD_CONCURRENCY_WITH_EMPTY. ()|- $EXPANSION_THEOREM. Vranken also developes projection and priority operations. In place of Koman's Fair Abstraction Rule$KFAR_1 and $KFAR_2 we have the Epsilon Abstraction Rule: EAR::@. EAR iff for all n( x[n]=a[n]x[n+1]+y[n]) then empty[|a](x[0]) = |[n]empty[|a](y[n]). More .Hole }=::ACP_EMPTY. . Shared Actions SHARED_ACTIONS::=$Basic_Proces_Operators with following, .Net For \alpha:@$Atomic_steps, x<\alpha>y::$Action, Defines a system of processes x and y that share the actions in \alpha. |- (S1): For all \alpha, SEMIGROUP($Action, <\alpha> ). |- (S2): x<\alpha>y<\alpha>z =x<\alpha> ( y <\alpha> z ). x <*> y ::= x <{}> y, parallel composition. Again <\alpha> could be declared to be serial. Semantics. To capture the semantics we need a relation expressing a single step of the evolution in a process: x -a-> y ::= in one step a action x can evolve into y. We can then provide a the Structured Operational Semantics as a set of derivation rules like this: |-(S3): a;x -a-> x. |-(S3):If x -a-> y then (x+z) -a-> (y+z). |-(S4):If x -a-> y then (z+x) -a-> (z+y). In English the rule for shared actions is If x evolves thru a to x' and y thru a to y' then .( x<\alpha>y can evolve to x'<\alpha>y iff a not in \alpha and x<\alpha>y can evolve to x<\alpha>y' iff a not in \alpha and x<\alpha>y can evolve to x'<\alpha>y' iff a \in \alpha .) If x -a-> x' and y-a-> y' then .( x<\alpha>y -a-> x'<\alpha>y iff a not_in \alpha and x<\alpha>y -a-> x<\alpha>y' iff a not_in \alpha and x<\alpha>y -a-> x'<\alpha>y' iff a \in \alpha .) Definition of equivalence/bisimulation/ etc. leading to an algebra. .Close.Net . See Also abelian_semigroup::=http://www/dick/maths/math_31.html#abelian_semigroup. commutative::=http://www/dick/maths/math_31.html#commutative. completion::=$METRIC_SPACES. idempotent::=http://www/dick/maths/math_11_STANDARD.html#idempotent. METRIC_SPACES::=http://www/dick/maths/math_92_Metric_Spaces.html. semigroup::=http://www/dick/maths/math_31.html#semigroup. .Close Process Algebras .Close Process Algebras and Communicating Sequential Processes