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



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