dfweak: find a weak HML formula distinguishing two agents
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.
Edinburgh Concurrency Workbench (v7.1).
Page generated: Sun Jul 18 11:46:51 BST 1999