Reading material

Pages 12-15 and 26-29 of Process Algebra1
Pages 1-13 of A Calculus of Mobile Processes, Part I2

1

2

Additional material

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