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...). Notation
We can distinguish detailed models [ 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: [ math_71_Auto...Systems.html ] , Systems algebras: [ math_72_Systems_Algebra.html ] , and theories of programs: [ math_75_Programs.html ]
An informal introduction to Process Algebras can be found at [ Process_Algebra ] on the Wikipedia.
I've recently found [Fokkink07] , a text on a newer version of ACP + data abstraction -- μ_CRL.
Information on [ 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:
For P,Q,R,S:Process.
For a,b,c,d:Action.
For A,B:@Action.
Note. An expression like a;b;c;P has to be parsed as a;(b;(c;P))) because a;b is not an Action.
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! [click here if you can fill this hole]
Note. Again I don't know the Precedence of >> vs |...| or the associativity of |...|. [click here if you can fill this hole]
Note. in MATHS we write X:-Y, Z to mean X if Y and Z, as in Prolog.
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. [click here if you can fill this hole]
then we can show
. . . . . . . . . ( end of section example) <<Contents | End>>
More on LOTOS: [click here if you can fill this hole]
. . . . . . . . . ( end of section LOTOS in MATHS) <<Contents | End>>
μ[X:A](P(X)) ::Process= the X(α(X)=A and X=P(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.
The above is reminiscient of Gries's (later) notations: F(x:B. P. R) and Unity.
Can show that every well defined process is a fuction mapping a set of initally acceptable events into a set of future behaviors.
More "Real Soon Now"... [click here CSP if you can fill this hole]
. . . . . . . . . ( end of section Communicating Sequential Processes) <<Contents | End>>
. . . . . . . . . ( end of section Introduction) <<Contents | End>>
Choices:
Sequence:
Note: (;) has a higher priority than (|) in MATHS so we can omit parentheses
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'm not sure if the next property is very important. It seems intuitive but it is not usually stated in the literature.
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.
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.
BPA is used in DEADLOCK, BASIC_COMMUNICATION, COMMUNICATION, MERGE_AND_COMMUNICATION, ACP, SILENCE, ABSTRACTION, STANDARD_CONCURRENCY, BPA_EMPTY, below.
|-(CM1): For x,y, x<*>y::= x>*>y | y>*>x | x<&>y.
The full algebra allows us to take a whole slew of actions and hide or encapsulate them.
The operator δ[H] doesn't hide actions outside of H,
The operator δ[H] does hide actions in H,
Encapsulation preserves sequence and choice while hiding some actions:
Axioms from Milner's CCS.
A system is typically an expression of form <*>(x)=x1<*>x2<*>...<*>x[k] for some list of subsystems(expressions).
for n:1.., π[n]:: A->A.
for x,y, d(x,y) ::= 2^-n where n:=the least{n:Nat || π[n](x)<>π[n](y)}
if α(x)<&>(α(y)&H) ==>H then δ[H](x<*>y)=δ[H](x <*> δ[H](y)).
if α(x)<&>(α(y)&I) ={} then τ[I](x<*>y)=τ[I](x <*> τ[I](y)).
if α(x)&H ={} then δ[H](x)=x.
if α(x)&I ={} then τ[I](x)=x.
δ[H1|H2] = δ[H1] o δ[H2].
τ[I1|I2] = τ[I1] o τ[I2].
if H&I={} then τ[I] o δ[H] = δ[H] o τ[I].
Then
Compare with PAD1 above.
Here we can replace an action by either empty or deadlock to hide it.
Vranken hints at proofs by induction of the following theorems:
And so to th assoicativity of merge:
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:
More [click here if you can fill this hole]
Again <α> 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:
We can then provide a the Structured Operational Semantics as a set of derivation
rules like this:
In English the rule for shared actions is
Definition of equivalence/bisimulation/ etc. leading to an algebra.
. . . . . . . . . ( end of section Process Algebras) <<Contents | End>>
. . . . . . . . . ( end of section Process Algebras and Communicating Sequential Processes) <<Contents | End>>
Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.
The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.
For a complete listing of pages in this part of my site by topic see [ home.html ]
For a more rigorous description of the standard notations see