A Menagerie of Non-Finitely Based Process Semantics over BPA tex2html_wrap_inline25 : From Ready Simulation Semantics to Completed Tracs

Luca Aceto
Wan J. Fokkink
Anna Ingólfsdóttir

July 1996


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 tex2html_wrap_inline25 ). In light of this positive result on the mathematical tractability of bisimulation equivalence over BPA tex2html_wrap_inline25 , 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 tex2html_wrap_inline25 . 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 tex2html_wrap_inline25 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 tex2html_wrap_inline25 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 tex2html_wrap_inline25 . 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 tex2html_wrap_inline25 , 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.


Last modified: 2003-06-08 by webmaster.