We present a symbolic transition system for the fusion calculus together with alternative characterizations of strong and weak hyperequivalence, without universal quantification over substitutions. We show that this symbolic bisimulation equivalence coincides with the standard hyperequivalence. Based on the symbolic semantics we present an algorithm for deciding the hyperequivalences and its implementation in the Mobility Workbench.
The space requirements are significantly reduced compared to earlier work, making it reasonable to use a normal workstation for verification even of large examples.
Technical report DoCS 98/96: December 1998 (Postscript, compressed)
See also these related papers:
Last modified: Tue, 19-Jan-1999 11:26 MET