Symbolic Characterizations and Algorithms for Hyperequivalence

Björn Victor

Abstract:

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:

and Lucian Wischik's excellent overview of fusion research.
Björn Victor

Last modified: Tue, 19-Jan-1999 11:26 MET