February 25, 2000

Rance Cleaveland and Scott A. Smolka. Process Algebra. In J.G. Webster, editor, Encyclopedia of Electrical Engineering. John Wiley & Sons, 1999.

Robin Milner, Joachim Parrow and David Walker. A Calculus of Mobile Processes, Part I. Report ECS-LFCS-89-85, University of Edinburgh. 1989.

The Concurrency Workbench of the New Century has been installed at CAT. To start the system, type

/cs/fac/src/cwb-nc/bin/cwb-nc ccs

To check that the processes a.b.nil + a.c.nil and a.(b.nil + c.nil) are trace equivalent, type

eq -S trace "a.b.nil + a.c.nil" "a.(b.nil + c.nil)"

To check that they are bisimilar, type

eq -S bisim "a.b.nil + a.c.nil" "a.(b.nil + c.nil)"

To check that the processes defined by the equations C1 = a.C1 and C2 = a.C2 + a.nil are trace equivalent, use the file simple.ccs and type

load simple.ccs
eq -S trace C1 C2

To check that the processes are bisimilar, type

eq -S bisim C1 C2