dfweak: find a weak HML formula distinguishing two agents
dfweak(A,B);
Notes
Produces a weak HML formula which distinguishes between the two
agents if they are not weakly bisimilar. The formula is true of the
first agent and false of the second.
See also
dfstrong
dftrace
Edinburgh Concurrency Workbench (v7.1).
Page generated: Sun Jul 18 11:46:51 BST 1999