mustpre: are two agents related by the must preorder?



Returns true iff for every s in the language of B (including the empty s) if A converges at s (i.e. you can't get to a divergent state by following observable path s) then B converges at s and every acceptance set of B after s contains some acceptance set of A after s.

(Here "divergence" includes performing an infinite sequence of tau moves, as well as @.)

See Hennessy: Algebraic Theory of Processes, MIT Press.

See also

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