CompSys705

Bisimulation. Whenever one process does an action, the other process must also be able to take the same action and both processes must reach the same state.

Partition refinement: separating a set into mutually exclusive sets. Greatest fixed point: start with the largest set and apply a transformation function such that the next set settles down to itself. Least fixed point: start with the smallest set and apply a function such that it continues to grow until it reaches saturation.

Going through the bisinulation algorithm which is quite a complex ball of steps. matchP is a set where the elements belongs to the partition such that the transitions on an action is not null or itself.

Weak bisimulation is observational equivalence.

Composed and transmitted from my iPod Touch