diveq: are two agents divergence equivalent?
diveq(A,B);
Notes
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