A Menagerie of Non-Finitely Based Process Semantics over BPA*: From Ready Simulation Semantics to Completed Traces
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, 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 nite, complete equational axiomatizations over closed terms.
AMS Subject Classification (1991): 08A70, 03C05, 68Q10, 68Q40, 68Q45,
68Q55, 68Q68, 68Q70.
CR Subject Classification (1991): D.3.1, F.1.1, F.1.2, F.3.2, F.3.4, F.4.1.
Keywords and Phrases: Concurrency, process algebra, Basic Process Algebra
(BPA*), Kleene star, bisimulation, ready simulation, simulation, completed trace semantics,
ready trace semantics, failure trace semantics, readiness semantics, failures
semantics, trace semantics, equational logic, complete axiomatizations.
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.