process algebra definitions and notation

by Theo Verelst

To take most recent book I read years ago on the subject, I'll summarize some parts of [koomen]'s notation (see below).

• An agent is an entity able to communicate over a port
• communication happens when a port has a label and another port has the complementary label
• When agent A and B have ports x and x_ (complementary) they communicate by def. which is called internal action, and the event is denoted by tau.
• a behaviour equation (E1,E2,..) algebraically defines a part of the behaviour of an agent (A,B..).

See also process algebra

References:

C.A.R. Hoare Communicating Sequential Processes Pren.H. '85.

Robin Milner A Calculus of Communicating Systems Lecture notes in computer science 92, Springer Verlag '80.

C.J. Koomen, The Design of Communicating Systems A System Engineering Approach, Kluwer Ac. Pr. '91.

Does anyone know of a logical reasoning in tcl package, I guess like prolog does, so a proof mechanism, and maybe a exploration mechanism ?

It's been a long time after I scored my 'formal logic' advanced university course after 3 attempts, and I was fed up with trying, but it was kind of fun to play formal sherlock holmes on the computer...