Ready To Preorder: Get Your BCCSP Axiomatization for Free!
Luca Aceto
February 2007 |
Abstract:
This paper contributes to the study of the equational theory of
the semantics in van Glabbeek's linear time - branching time spectrum over
the language BCCSP, a basic process algebra for the description of finite
synchronization trees. It offers an algorithm for producing a complete
(respectively, ground-complete) equational axiomatization of a behavioral
congruence lying between ready simulation equivalence and partial traces
equivalence from a complete (respectively, ground-complete) inequational
axiomatization of its underlying precongruence--that is, of the
precongruence whose kernel is the equivalence. The algorithm preserves
finiteness of the axiomatization when the set of actions is finite. It
follows that each equivalence in the spectrum whose discriminating power lies
in between that of ready simulation and partial traces equivalence is
finitely axiomatizable over the language BCCSP if so is its defining
preorder
Available as PostScript, PDF. |