- Propositions:
- ~~ is the largest bisimulation.
- ~~ is an equivalence relation.
- $P$ ~~
`tau`.$P$

- ~~ is
*not*yet equality:- ~~ not preserved by summation.
- $a.0\; +\; b.0$ ~~ $a.0+$
`tau`.$b.0$ does*not*hold! - Proof: if ($P$,$Q$) were in a bisimulation $S$, then, since $Q$
->$$
`tau`$b.0$, we need ($P\text{'}$, $b.0$) in $S$ with $P$ =>$$`epsilon`$Q\text{'}$. But the only $P\text{'}$ is $P$ itself but $(P,b.0)$ can be not in $S$, since $P$ ->$$a$$ 0, while $b.0$ has no $a$-descendant.

- Relations:
- $P$~$Q$ implies $P$=$Q$ implies $P$~~$Q$

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: ccs2.tex,v 1.1 1996/06/12 15:55:52 schreine Exp schreine $$