Process Algebra, some rules

by Theo Verelst (of course feel free to comment / correct, pref. with id)

The Process Algebra page gives an idea of that concept, but lacking in it was some indication of the algebraic manipulation that is of interest, and that, of course, is a major reason for the algebraic angle.

Distributiveness, associativeness, substitution of the parallel and serial composition and the restriction operator.

escargo 27 Apr 2003 - I see interesting strings of characters here, but I can't tell what the notation is supposed to denote. I can't tell if ^= is supposed to be not equals, equals (under some special assumptions), equivalence, or implies. Wait! Now I see that it means is defined as (which got added since the last time I looked). Maybe all these notations could be collected and defined in the beginning. TV Agreed, this page stated as sort of a scratch to recollect this stuff. I'm in the library now, I'll see if I can find some nice existing frame with some history, before thinking it all up myself again.

TV (29 apr 03) I though I'd take some remarks up, so let's first do a process algebra definitions and notation page


Let's see (sort of like typing while my memory and imagination are working, I should do my library work first, in fact), starting with parallel composition of agents capable of communication with a certain message set and a certain set of state progression orders:

 (A | B) | C  ^= A | (B | C) ^= A | B | C

  A | B  ^=  B ^| A 

TV, nope, I think I must have (or should have) typed:

  A | B  ^=  B | A  

Parallel composition simply doesn't depend on the algebraic ordering of the defining composition. A | B means the same as B | A: processes A and B are put together in a composition and may communicate with each other. The ^= I made stand for is defined as

Serial composition:

 A ; B  !=  B ; A

 ( A ; B ) ; C ==> ( A ; C ) &&  ( B ; C )

Combined:

 ( A | B ) ; C ==>

Oh boy, still thinking, don't take this for granted, it's been years....