### A Menagerie of Non-Finitely Based Process Semantics over BPA*: From Ready Simulation Semantics to Completed Traces

#### 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, 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.

#### Full Text:

PDFDOI: http://dx.doi.org/10.7146/brics.v3i23.20003

ISSN: 0909-0878

Hosted by the Royal Danish Library and Aarhus University Library