Theo Verelst

Process Algebra refers to mathematical formulation and reasoning rules for defining processes, made up of events where we focus on communication events which occur between processes.

A process can be represented by an identifier, and is seen as something which can somehow decide to engage in a communication with another process, or maybe with itself, and we take it that we can have n processes which can communicate between 2 at one instance in time.

Because we do not explicitly discern what goes on in a process (sometimes the word 'agent' is preferable', though a more than loose coupling with the unix idea of a process is not so bad as thought frame), the only thing we can be sure of is when a communication takes place, which can be given a notation such as 

 com(Pa,Pb)

or 

 com(Pa, Pb, Mi)

where P is a process and M is a message, or the communication content. The former is a more general formulation which leaves room for more reasoning.

We can assume a process changes state after a communication of a certain kind with a certain other process took place, and we could make a list of all possible sequences of communication a set of processes or agents can take part in, possibly in an inductive way.

For instance:


 com(Pa,Pb,M1)   or:          com(Pa,Pb,M1)
 com(Pa,Pc,M2)                com(Pb,Pc,M2)
 com(Pb,Pc,m3)                com(Pb,Pa,m3)

We could take it that the first two arguments of the com operator are order insensitive.

A general way of speaking about processes somehow relevant to a problem is 'composition' which means they are being enabled to communicate. Also we could serialize them, a get a certain sequence.

 Pa | Pb    composition
 pa ; Pb    sequence

A limit operator can be used to 'rule out' a certain communication from the set of possible communications between certain composed processes:

 (Pa | Pc) \{M3}

would indicate the parallel composition of two processes restricting the allowed communications.

'''Strong and weak Bisimulation'''

''Traces''

''Links with real word programming''