diveq: are two agents divergence equivalent?



This is observational equivalence which respects divergence. A state is divergent in this sense if it can perform an infinite sequence of unobservable actions (tau for CCS or 1 for SCCS), or if it can reach an unguarded occurrence of the divergent agent, @, through some sequence of unobservable actions.

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