Abstract:
Fokkink and Zantema ((1994) Computer Journal
37:259-267) have shown that bisimulation equivalence has a finite
equational axiomatization over the language of Basic Process Algebra with the
binary Kleene star operation (BPA  ). In light of this positive result on
the mathematical tractability of bisimulation equivalence over BPA , a
natural question to ask is whether any other (pre)congruence relation in van
Glabbeek's linear time/branching time spectrum is finitely (in)equationally
axiomatizable over it. In this paper, we prove that, unlike bisimulation
equivalence, none of the preorders and equivalences in van Glabbeek's linear
time/branching time spectrum, whose discriminating power lies in between that
of ready simulation and that of completed traces, has a finite equational
axiomatization. This we achieve by exhibiting a family of (in)equivalences
that holds in ready simulation semantics, the finest semantics that we
consider, whose instances cannot all be proven by means of any finite set of
(in)equations that is sound in completed trace semantics, which is the
coarsest semantics that is appropriate for the language BPA . To this end,
for every finite collection of (in)equations that are sound in completed
trace semantics, we build a model in which some of the (in)equivalences of
the family under consideration fail. The construction of the model mimics the
one used by Conway ((1971) Regular Algebra and Finite Machines, page
105) in his proof of a result, originally due to Redko, to the effect that
infinitely many equations are needed to axiomatize equality of regular
expressions. Our non-finite axiomatizability results apply to the
language BPA over an arbitrary non-empty set of actions. In particular, when the set of actions is a singleton, our proof of the fact we show that
completed trace equivalence is not finitely based over BPA even when the
set of actions is a singleton. Our proof of this result may be easily adapted
to the standard language of regular expressions to yield a solution to an
open problem posed by Salomaa ((1969) Theory of Automata, page
143). Another semantics that is usually considered in process theory
is trace semantics. Trace semantics is, in general, not preserved by
sequential composition, and is therefore inappropriate for the language
BPA . We show that, if the set of actions is a singleton, trace
equivalence and preorder are preserved by all the operators in the signature
of BPA , and coincide with simulation equivalence and preorder,
respectively. In that case, unlike all the other semantics considered in this
paper, trace semantics have finite, complete equational axiomatizations over
closed terms.
Available as PostScript, PDF,
DVI.
|