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