dfstrong: find a strong HML formula distinguishing two agents

dfstrong(A,B);

Notes

Produces a strong HML formula which distinguishes between the two agents if they are not strongly bisimilar. The formula is true of the first agent and false of the second.

Synonyms

df

See also

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