A format for semantic equivalence comparison
V.C. Galpin
Abstract
This paper presents a new format for process algebras, the extended
tyft/tyxt format which generalises the tyft/tyxt format
of Groote and Vaandrager. The format differs from most previous
formats in that the labels on transitions are treated as many-sorted
terms. Bisimulation is a congruence for all operators defined in this
format.
When one extended transition system specification is summed with
another,
the resulting bisimulation can either identify more terms (an
abstracting
extension up to bisimulation) or fewer terms (a refining extension
up to bisimulation) than the original bisimulation on the individual
system. The notions of abstracting extension and refining extension are
defined, and two theorems are presented giving conditions required for
achieving each type of extension. These results provide a way to compare
different semantic equivalences defined for different process algebras.
Finally, an application of this theory to semantic equivalence
comparison
is given for a new result relating Castellani's pomset equivalence and
Krishnan's multiprocessor equivalence.
Preprint (final version) - PDF
doi:10.1016/S0304-3975(03)00129-4
Back to Publications page