Symbolic Characterizations and Algorithms for Hyperequivalence
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:
[an error occurred while processing this directive]
-
The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes,
by Joachim Parrow and Björn Victor, LICS'98.
[an error occurred while processing this directive]
-
Concurrent Constraints in the Fusion Calculus,
by Björn Victor and Joachim Parrow, ICALP'98.
[an error occurred while processing this directive]
-
The Tau-Laws of Fusion,
by Joachim Parrow and Björn Victor, CONCUR'98.
[an error occurred while processing this directive]
-
The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes,
PhD thesis by Björn Victor.
[an error occurred while processing this directive]
-
Symbolic Characterizations and Algorithms for Hyperequivalence,
by Björn Victor, technical report DoCS 98/96.
[an error occurred while processing this directive]
-
Solos in Concert,
by Cosimo Laneve and Björn Victor, ICALP'99 / MSCS 13(5) 2003.
[an error occurred while processing this directive]
-
Solo Diagrams,
by Cosimo Laneve, Joachim Parrow and Björn Victor, TACS2001.
and Lucian Wischik's excellent overview of fusion research.
Björn Victor
Last modified: Tue, 19-Jan-1999 11:26 MET