.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
~~