## contraction: are agents related by the contraction pre-order?

`contraction(A,B);`

### Notes

Returns true iff A and B are related by some contraction.
C is a contraction iff PCQ implies
whenever P -a-> P' there exists Q' s.t. Q =^a=> Q' and P' C Q' and

whenever Q -a-> Q' there exists P' s.t. (P -a-> P' or P -^a-> P') and
P' C Q'

(P and Q are weakly bisimilar, and P need never do more tau moves than Q)

See Milner "Contractions", RM 13, Handwritten notes, dated 23 March 1990.

Edinburgh Concurrency Workbench (v7.1).
Page generated: Sun Jul 18 11:46:51 BST 1999