Decorated Trace Semantics over BPA have no Finite Equational Axiomatization

Fokkink and Zantema 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 based on decorated traces can be finitely axiomatized. This we achieve by exhibiting a family of (in)equivalences that holds in ready trace 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 based on decorated ..