Axiomatisations of Weak Equivalences for De Simone Languages

Irek Ulidowski^{⋆}

Research Institute for Mathematical Sciences, Kyoto University, Japan.

               Email: irek@kurims.kyoto-u.ac.jp.

Abstract. Aceto, Bloom and Vaandrager proposed in [ABV92] a procedure for generating a complete axiomatisation of strong bisimulation for process languages in the GSOS format. However, the choice operator +, which the procedure uses, as well as other auxiliary GSOS operators, which it introduces to obtain a finite axiomatisation, do not preserve many of weak equivalences. We propose a modification of this procedure, which works for a subclass of process languages in the De Simone format with a special treatment of silent actions. A choice of such a subclass of process languages guarantees that all the considered and auxiliary operators preserve many of weak equivalences. Our procedure generates a complete axiomatisation of refusal simulation preorder and it can be easily adapted to coarser preorders. The completeness result depends on the completeness result for the basic process language, which we prove. This language does not use prefixing with τ and the choice operator +. Instead, we employ the CSP external and internal choice operators as well as the third choice operator.

1 Introduction

In recent years there has been a considerable interest in structural operational semantics (SOS) as a mechanism to give operational meaning to classes of process languages. Main ingredients of such a semantics are SOS rules, which describe how the behaviour of a composite process depends on the behaviour of its component processes. Many general formats for SOS rules have been proposed (e.g. [dS85, BIM88, GV92, Gro90]), and a number of important results for process languages defined in these formats have been established. For example, various behavioural equivalences on processes were shown to be preserved by all process operators definable in these formats [dS85, BIM88, GV92, Gro90, Vaa91, Uli92, vG93, Blo95a] and (completed) trace congruences with respect to these formats where discovered [BIM88, GV92, Gro90, Vaa91, Uli92, vG93]. In [ABV92, Ace94] Aceto, Bloom and Vaandrager showed how axiomatic characterisations can be derived for equivalences on processes. More recently, SOS was used as a specification language in [Blo95b] and denotational models for classes of languages defined by certain formats were developed in [AI95].

⋆ On leave from the School of Computing, University of North London, London N7 8DB.

Among the general research on formats of rules, there is a number of contributions concerning formats with a special treatment of silent actions [Blo90, Vaa91, Uli92, Blo95a, Uli94]. In these formats, the traditional meaning of silent actions, as independent from the environment, invisible and spontaneous actions, is guaranteed by imposing certain restrictions on the form rules can take. In this paper, we are interested in process languages in such formats of rules.

We aim to build upon the work started by Aceto, Bloom and Vaandrager in [ABV92]. They proposed two procedures for generating finite complete axiomatisations, possibly with one infinitary induction rule, for any process language defined by rules in the GSOS format [BIM88]. Their procedures introduce auxiliary operators as they are needed. For example, for the axiomatisation of the parallel operator of ACP [BK84], the left-merge and communication merge operators are automatically introduced.

In this paper, our interest is in weak equivalences, where silent actions are treated as invisible, with divergence. Examples of these are weak bisimulation and refusal simulation equivalences [Uli92, Uli94]. The last has a natural characterisation in terms of local tests consisting of trace, refusal and copy tests [Uli92, Uli94]. Our aim is to adapt the procedure from [ABV92] to generate axiomatisations for refusal simulation equivalence and other coarser (weak) equivalences. However, it is well known that + and some other GSOS process operators, left-merge and communication merge among them, do not preserve these and many other weak equivalences. This is due to their interaction with silent actions. For example, consider the left-merge operator defined by the following single rule, where α is any (visible or silent) action:

{X →^{α} X′ \atop X Y →^{α} X ∥ Y′.}

Although the processes a0 and τa0 are weakly trace equivalent, but a0 b0 and τa0 b0 are not: the second process can perform a sequence of action τba which cannot be matched by any equivalent trace of the first process. The implication is that the above mentioned operators and many other auxiliary operators, which are introduced by the procedure from [ABV92], cannot be easily used in verifications with respect to many weak equivalences. This problem is addressed in [vGV93], where it is postulated to use module logic instead of standard equational logic in reasoning about weak equivalences in the presence of operators like + and . Another solution is given by Bloom in [Blo95a]. Instead of weak bisimulation, he considers a number of versions of rooted weak bisimulation and rooted branching bisimulation since they are preserved by operators like + and . Several classes of process languages, all subclasses of GSOS languages, are proposed such that they preserve the relevant versions of rooted bisimulations. The author describes how to adapt the methods of [ABV92] to produce sound axiomatisations of some of the rooted versions of bisimulations for the relevant process languages.

We propose an alternative solution to the above problem, together with a new procedure to derive complete axiom systems for refusal simulation preorder.

The results are as follows. Firstly, we limit our attention to a subformat of the GSOS format which preserves weak bisimulation, refusal simulation and many other weak equivalences. This format is the De Simone format [dS85] with a special treatment of silent actions as described in [Uli92, Uli94]. We call this format the τDeS format. Secondly, instead of using + and prefixing with silent action τ we use the CSP external and internal choice operators ⊞ and ⊕ respectively [BHR84, Hoa85]. These operators were used, instead of + and τ, in CCS [NH87, Hen88] and in ACP [Ace91]. We also use the third choice operator ⊳, called mixed choice in [Uli94], which together with the null process, prefixing and the other two choice operators is needed to represent finite processes up to refusal simulation equivalence. We give a complete axiomatisation for refusal simulation preorder for the basic language augmented with the explicit divergent process. Thirdly, we present a new procedure, based on the procedure from [ABV92], for generating complete axiomatisations of refusal simulation preorder for well-founded τDeS languages. Our procedure introduces auxiliary operators too, as they are needed. However, all our auxiliary operators are τDeS, hence they preserve refusal simulation.

The paper is organised as follows. We define, in Sect. 2, τDeS process languages and refusal simulation preorder. In Sect. 3, we introduce our basic process language and give a complete characterisation of refusal simulation preorder for this language. In Sect. 4, we present a procedure for generating a sound axiomatisation for an arbitrary τDeS language. The completeness results for well-founded and for finitely branching τDeS languages are given in Sect. 5. The last section suggests a number of improvements to our procedure and outlines future work.

Due to the lack of space the proofs of our results are not included in this paper. These proofs as well as examples illustrating the applications of our axiomatisation procedure can be found in the full version of the paper [Uli95].

2 Preliminaries

This section defines notions of τDeS process languages, labelled transition systems with divergence and refusal simulation preorder. We assume a knowledge of basic ideas, definitions and results for process algebras as, for example, in [BHR84, Mil89, Hen88, BW90, BIM88, GV92].

Let Var be a countable set of variables ranged by X, X_{i}, Y, Y_{i}, . . .. A signature Σ is a set process operators which are pairs (f, n), where f ∉ Var and n ∈ ℕ is an arity of f. Often, when the arity of the operator is clear from the context, the operator is simply abbreviated by its name, for example f. The set of open terms over Σ with variables in Var, denoted by 𝕋(Σ), is ranged by P, Q, . . .. The set of closed terms, written as T(Σ), is ranged by p, q, . . .. var(T) denotes a set of variables appearing in a term T. Σ context with n holes C[X_{1}, …, X_{n}] is a member of T(Σ, {X_{1}, …, X_{n}}) in which X_{i}, 1 ≤ i ≤ n, occurs only once. If t_{1}, …, t_{n} are Σ terms then C[t_{1}, …, t_{n}] is a term obtained by substituting X_{i} by t_{i}, 1 ≤ i ≤ n. A preorder ⊑ on T(Σ) is a precongruence ( or substitutive) if for all Σ contexts C[X] we have t ⊑ t′ implies C[t] ⊑ C[t′]. A (closed) substitution ρ is a mapping from Var to (T(Σ)) 𝕋(Σ). The substitution ρ extends to a mapping 𝕋(Σ) → 𝕋(Σ) in a standard way. We will write P [P_{1}/X_{1}, …, P_{n}/X_{n}] to denote the substitution which assigns each X_{i} to P_{i}. Act = Vis∪{τ}, ranged by α, …, is a countably infinite set of actions, where Vis is the set of visible actions, ranged by a, b, …, and τ is a silent, internal action not in Vis.

Definition 1. A De Simone rule for (f, n) has the following form:

{\{ X_{i} →^{a_{i}} X′_{i} \}_{i∈I} \atop f(X_{1}, …, X_{n}) →^{α} C[Y ],}  (1)

where X_{i}, X′_{i} are all different variables and I ⊆ {1, …, n}. C[Y ] contains at most the variables Y_{1}, …, Y_{n}, where Y_{i} = X′_{i} if i ∈ I and Y_{i} = X_{i} otherwise. We say that (f, n) tests its m-th argument and the m-th argument for (f, n) is active if there is a De Simone rule for (f, n) with m ∈ I. The notions of the operator of the rule, the action, trigger, antecedents and consequent are as usual.

A τ-rule for the above rule is any of the following rules for i ∈ I:

{X_{i} →^{τ} X′_{i} \atop f(X_{1}, …, X_{i}, …, X_{n}) →^{τ} f(X_{1}, …, X′_{i}, …, X_{n}).}

A set of all τ-rules for the operator f is called its set of associated τ-rules. A set of rules is in the De Simone format (τDeS) if it consists of De Simone rules and their associated τ-rules. A process operator is τDeS if the set of its defining rules is in τDeS. A τDeS process language is a triple (Σ, A ∪ {τ}, R), where Σ is a finite set of operators, A ⊂_{fin} Vis and R is a finite set of τDeS rules defining the operational meaning of the operators in Σ.

Most of the operators in process algebras are τDeS except, for example, for the CCS and ACP + and the ACP left-merge operators, which do not have the associated τ-rules. De Simone rules were introduced, in a slightly more general form (with no distinction between silent and visible actions), in [dS85]. The notion of τ-rules was introduced by Bloom in [Blo90] and it was used in [Vaa91] and [Uli92] in connection with the De Simone^{2} and the ISOS formats respectively.

In order to represent divergent and underspecified processes in τDeS languages we will employ the operator (Ω, 0), which we will simply write as Ω.

Definition 2. Let G = (Σ_{G}, A ∪ {τ}, R_{G}) be a τDeS language. A labelled transition system with divergence is a structure (T(Σ_{G}), A ∪ {τ}, →_{G}, ↑_{G}), where T(Σ_{G}) is a set of process terms or processes, →_{G}⊆ T(Σ_{G})×A∪{τ}×(T(Σ_{G}) is the unique transition relation generated by G^{3} and ↑_{G}⊆ T(Σ_{G}) is the (postfix) divergence predicate. ↑_{G} is defined as the least relation satisfying Ω↑_{G} if Ω ∈ Σ_{G}, and f(p)↑_{G}, for any f ∈ Σ_{G}, if p_{i}↑_{G} for some active i-th argument of f.

2 Our τDeS languages are somewhat different from De Simone languages in [Vaa91]. Vaandrager allows silent actions in the antecedents of De Simone rules, provides an extra “idling” axiom and, separately, provides recursion.

3 Full details of the construction of transition relation from the language definition in a general format of rules can be found in, for example, [BIM88, GV92].

We will often call this transition system the basic transition system for G, and omit the subscript G when it is clear from the context. We will use some standard notation: for (p, a, q) ∈→ we write p →^{a} q and interpret it as process p performs a and in doing so becomes q. The convergence predicate is defined as p↓_{G} ≡ ¬ p↑_{G}, and read as ‘p converges’. The abbreviations we will use are: p →^{a} for

∃q ∈ T(Σ). p →^{a} q and p ↛^{a} for ¬∃q ∈ T(Σ). p →^{a} q.

We are interested in weak equivalences which are usually defined over some form of a derived transition system. In the derived transition system, which we consider, we hide silent actions and internalise refusals of actions (ã, for all a ∈ A). Thus, we label the derived transition relation with both actions and refusals of actions—the two basic elements of observable process behaviour.

Definition 3. [Uli94] Let (T(Σ), A∪{τ}, →, ↑) be the basic transition system for a τDeS language G. A structure (T(Σ), A∪Ã∪{ε}, ⇒, ⇑) is a derived transition system with divergence, where p⇑ ≡ (∃q. p →^{τ^{∗}} q & q↑) ∨ p →^{τ^{ω}} and ⇒⊆ T(Σ) × A ∪ Ã ∪ {ε} × T(Σ) is a derived transition relation defined as follows:

\begin{aligned}p ⇒^{a} q & ≡ & p →^{τ^{∗}}→^{a} q, \\ p ⇒^{ã} q & ≡ & p →^{τ^{∗}} q ↛^{τ} & q↓ & q ↛^{a}, \\ p ⇒^{ε} q & ≡ & p →^{τ^{∗}} q. \end{aligned}

For simplicity we will call this transition system the derived transition system. Finally, we introduce refusal simulation preorder [Uli92, Uli94].

Definition 4. Let (T(Σ), Λ, ⇒, ⇑) be the derived transition system for a τDeS language G, where Λ = A ∪ Ã ∪ {ε}. Relations R and S : T(Σ) × T(Σ) are L-simulation and U-simulation relations respectively if for all p, q

pRq implies ∀μ ∈ Λ, ∀p′. p ⇒^{μ} p′ implies ∃q′. q ⇒^{μ} q′ & p′Rq′,
pSq implies ∀μ ∈ Λ.  p⇓ implies

q⇓ & (∀q′. q ⇒^{μ} q′ implies ∃p′. p ⇒^{μ} p′ & p′Sq′).

We define ⊏_{∼}_{L}, ⊏_{∼}_{U} and refusal simulation relation, ⊏_{∼}_{RS}, as a binary relation over T(Σ) as follows:

p ⊏_{∼}_{L} q ≡ ∃R. R is an L-simulation and pRq,
p ⊏_{∼}_{U} q ≡ ∃S. S is a U-simulation and pSq,
p ⊏_{∼}_{RS} q ≡ p ⊏_{∼}_{L} q & p ⊏_{∼}_{U} q.

It can be demonstrated that ⊏_{∼}_{L}, ⊏_{∼}_{U} and ⊏_{∼}_{RS} are preorders. Refusal simulation equivalence, ≈_{RS}, is defined in a following way: p≈_{RS}q ≡ p ⊏_{∼}_{RS} q & q ⊏_{∼}_{RS} p. Moreover, ⊏_{∼}_{RS} and weak bisimulation preorder (a version which takes divergence into account [Uli94]) are precongruences for all τDeS process languages.

Lemma 5. [Uli92, Uli94] ⊏_{∼}_{RS} is a precongruence for all τDeS process languages.

Definition 6. [ABV92] A τDeS language H is a disjoint extension of a τDeS language G, written as G ≤ H, if the signature and rules of H include those of G, and H introduces no new rule for the operators in G.

Following the notational agreements in [ABV92, Ace94], for a given τDeS language G we will use RSim(G) to denote the quotient algebra of elements of T(Σ) factored by ⊏_{∼}_{RS}. That is RSim(G) ⊨ P ⊑ Q iff ρ(P) ⊏_{∼}_{RS} ρ(Q), for all P, Q ∈ 𝕋(Σ_{G}) and all closed Σ_{G} substitutions ρ. Moreover, since we will consider axioms which are preserved by taking disjoint extensions of τDeS languages we will need RSIM(G), a class of all algebras RSim(G′) where G′ is a disjoint extension of G. We have, for P, Q ∈ 𝕋(Σ_{G}),

RSIM(G) ⊨ P ⊑ Q iff (∀G′.G ≤ G′ implies RSim(G′) ⊨ P ⊑ Q).

3 Basic Language

The basic language, as we mentioned in the introduction, contains the external, internal and mixed choice operators instead of + and the prefixing with τ. The main reason for not using + is that it does not preserve many of weak equivalences. This is due to its interaction with τ. Another criticism of + is that it represents a mixture of different types of nondeterministic choice. Consider the following three terms:

ap + bq, τap + τbq and ap + τbq.

The first term represents the external choice between ap and bq, the (external) user can choose to synchronise on either a or b. The second term represents the internal choice between ap and bq. The choice is made internally by the process (represented the two τ actions), and the user has no control over which of a and b is offered for synchronisation. The third term represent a mixture of both the external and internal choice. Here, the user is guaranteed to synchronise on b if she/he chooses to, but not on a—the process may internally evolve to bq, thus disabling a. Such choice can be interpreted as offering a synchronisation on a and b but with a preference to the one on b. These different types of nondeterministic choice between ap and bq are represented in our language as follows:

ap ⊞ bq, ap ⊕ bq and ap ⊳ bq.

When a = b then the user has no control over which of the actions a is offered. Since we are considering weak equivalences, which are defined in terms of the observable behaviour of processes, we find prefixing with τ counterintuitive. We think that silent actions should be a result of interactions between process operators, like between the prefixing and parallel composition operators in CCS and ACP, prefixing and hiding operators in CSP, rather than an explicit method of process creation. Hence, in this paper we do not use prefixing with τ.

3.1 Operational Semantics

Our basic language is a finite version of the ISOS process language introduced in [Uli94] with an extra constant Ω to represent totally divergent processes.

Table 1. The operational semantics for B.

prefixing  aX →^{a} X
external choice {X →^{a} X′ \atop X ⊞ Y →^{a} X′}  {Y →^{a} Y′ \atop X ⊞ Y →^{a} Y′}

{X →^{τ} X′ \atop X ⊞ Y →^{τ} X′ ⊞ Y}  {Y →^{τ} Y′ \atop X ⊞ Y →^{τ} X ⊞ Y′}
internal choice X ⊕ Y →^{τ} X  X ⊕ Y →^{τ} Y
mixed choice {X →^{a} X′ \atop X ⊳ Y →^{a} X′}  {X →^{τ} X′ \atop X ⊳ Y →^{τ} X′ ⊳ Y}  X ⊳ Y →^{τ} Y

Definition 7. The basic language, denoted by B, is a τDeS process language (Σ, A ∪ {τ}, R), where Σ = Σ_{0} ∪ Σ_{1} ∪ Σ_{2} is defined below, A ⊂_{fin} Vis and R is a set of τDeS rules in Table 1.

\begin{aligned}Σ_{0} & = & \{(0, 0), (Ω, 0)\} \\ Σ_{1} & = & \{(a, 1) | a ∈ A\} \\ Σ_{2} & = & \{(⊞, 2), (⊕, 2), (⊳, 2)\}. \end{aligned}

The precedence of operators is given by a > ⊞ > ⊕ > ⊳.

B generates the basic transition system B = (T(Σ), A ∪ {τ}, →, ↑) as in Definition 2. Note that all processes in T(Σ) are finite. Given B the derived transition system (T(Σ), A∪Ã∪{τ}, ⇒, ⇑) is defined as in Definition 3. One can check that divergence predicate ⇑ is the least relation satisfying the following: Ω⇑ and if p⇑ then (p ⊞ q)⇑, (q ⊞ p)⇑, (p ⊕ q)⇑, (q ⊕ p)⇑, (p ⊳ q)⇑ and (q ⊳ p)⇑. Refusal simulation preorder, ⊏_{∼}_{RS}, on D is defined as in Definition 4.

Example 1. We show why the operator ⊳ is needed in B. The operators ⊞ and ⊕ are the only choice operators used in the language TCCS [NH87]. This is because they are sufficiently expressive for testing equivalence, but they are not for refusal simulation equivalence: testing equivalent processes (a ⊞ b) ⊕ b and a⊳b are not refusal simulation equivalent: (a⊞b)⊕b ⇒^{c̃} a⊞b ⇒^{a} but a⊳b ⇒^{c̃} b ⇏^{a}.

3.2 Axiom System

In this section, we give a complete axiom system RS for ⊏_{∼}_{RS} on processes in the basic language B. The system RS consists of equations and inequations given in Table 2 as well as the usual properties of precongruences (e.g. substitutivity: if p ⊑ q then f(p) ⊑ f(q)), as in [Hen88]. The inequations in Table 2 are new, but the equations are taken from the axiomatisation of copy+refusal preorder in [Uli94], where they are motivated and discussed. At this point, we only comment on E2, which does not hold without the side condition. A counterexample is

Table 2. Axioms for refusal simulation preorder.

E1  X ⊞ 0 = X
E2 X ⊞ X = X if X ↛^{τ}
E3  X ⊞ Y = Y ⊞ X
E4  X ⊞ (Y ⊞ Z) = (X ⊞ Y) ⊞ Z
I2  X ⊕ X = X
I3  X ⊕ Y = Y ⊕ X
I4  X ⊕ (Y ⊕ Z) = (X ⊕ Y) ⊕ Z
M1  0 ⊳ X = X
M2  X ⊳ X = X
M4  X ⊳ (Y ⊳ Z) = (X ⊳ Y) ⊳ Z
D1  X ⊞ (Y ⊕ Z) = (X ⊞ Y) ⊕ (X ⊞ Z)
D2  X ⊞ (Y ⊳ Z) = Y ⊳ (X ⊞ Z)
D3  X ⊕ (Y ⊳ Z) = Y ⊳ (X ⊕ Z)
D4  (X ⊳ Y) ⊳ Z = (X ⊞ Y) ⊳ Z
D5  (X ⊕ Y) ⊳ Z = (X ⊞ Y) ⊳ Z
C1  aX ⊞ aY = aX ⊞ aY ⊕ aX
C2  a(X ⊞ Y ⊳ V ⊕ Z) = a(X ⊞ Y ⊳ V ⊕ Z) ⊞ a(X ⊳ V)
Ω1  Ω ⊑ X
Ω2  X ⊞ Ω ⊑ X ⊳ Ω
Ω3  Ω ⊳ X ⊑ Ω ⊕ X

(a ⊕ b) ⊞ (a ⊕ b) / ⊏_{∼}_{RS} (a ⊕ b): the left process can become stable and then do a and b, which cannot be matched by the right process. This property of ⊞ will force us to use similar side conditions in the laws concerning ⊞ in Sect. 4. Note that E2 can be replaced by a family of axioms aX ⊞ aX = aX, one for each a.

We will use the summation notation ∑_{i∈I} X_{i} and ⨁_{j∈J} Y_{j}, for J ≠ ∅, since ⊞ and ⊕ are associative. We will write T ⊢ p ⊑ q, (p = q) to mean that p ⊑ q, (p = q) can be derived from the axiomatic theory T.

Theorem 8. RS ⊢ p ⊑ q if and only if RSim(B) ⊨ p ⊑ q.

The completeness part is proved, as usual, by extracting normal and head normal forms. Their definitions and the details of the proof can be found in [Uli95].

4 Deriving Sound Axioms for τ -DeS Process Languages

In this section, we give a procedure for deriving sound axiomatisations of refusal simulation preorder for arbitrary τDeS process languages. The derived axiomatisations are head normalising, but they are infinite and conditional. We illustrate the application of our procedure by deriving axioms for the CSP hiding and the ACP merge operators.

We begin by noting that all τDeS operators are smooth, as in [ABV92]. We will need to distinguish two subclasses of τDeS operators, namely distinctive, after [ABV92], and τ-introducing operators.

Definition 9. A τ-DeS operator (f, n) is distinctive if for each argument i either all rules for f, which are not τ-rules, test i or none of them does, and also for each pair of different non-τ-rules for f there is an argument for which both rules have the same antecedents, but with a different action. A non-τ-rule is τ-introducing if it has action τ in the consequent. A τDeS operator (f, n) is τ-introducing if one of its rules is τ-introducing.

The following three lemmas introduce the action and inaction laws, adapted from [ABV92], and the new divergence laws.

Lemma 10. (Action Laws). Let (f, n) be a distinctive operator of a τDeS language G, a disjoint extension of B, with a rule of the form (1). Let P_{i} ≡ a_{i}X′_{i} for i ∈ I and P_{i} ≡ X_{i} otherwise. If α ∈ Vis then, for an appropriate P′, we have

RSIM(G) ⊨ f(P) = αC[P′]  (2)

else, for some P′, we have

RSIM(G) ⊨ f(P) = C[P′].  (3)

Lemma 11. (Inaction Laws). Let (f, n) be an operator of a τDeS language G, a disjoint extension of B. Suppose that for each rule for f of the form (1) there is an index i ∈ I such that either P_{i} ≡ 0 or P_{i} ≡ aX′_{i}, for some a ≠ a_{i}. Then

RSIM(G) ⊨ f(P) = 0.  (4)

Lemma 12. (Divergence Laws). Let (f, n) be an operator of a τDeS language G, a disjoint extension of B. Suppose that there is a rule for f of the form (1) such that for some i ∈ I we have P_{i} ≡ Ω, and, for all other rules for f of the form

{\{ X_{i} →^{a_{i}} X′_{i} \}_{i∈I′} \atop f(X_{1}, …, X_{n}) →^{α} C′[Y ],}

there is an index i ∈ I′ such that P_{i} ≡ 0, P_{i} ≡ Ω or P_{i} ≡ aX′_{i}, for some a ≠ a_{i}. Then

RSIM(G) ⊨ f(P) ⊑ Ω.  (5)

Next, we present the distributivity laws, which together with the above laws are needed to transform terms to head normal form. We will need two predicates over process terms to describe their structural properties. The first predicate sum(f, p) is true if all elements of p, which are active for f, have the form ∑_{I} a_{i}p_{i} or ∑_{I} a_{i}p_{i} ⊞ Ω, where I ⊂_{fin} ℕ. The second predicate tau(f(p)) is true if f(p) can perform τ as a result of applying a τ-introducing rule, possibly after a number of actions τ due to the application of τ-rules.

Lemma 13. Let (f, n) be an operator of a τDeS language G, the disjoint extension of B, and suppose that i is an argument of f such that each rule for f has an antecedent for i. (Distributivity over ⊞ laws). Let X_{i} ≡ X ⊞ Y. If f is non-τ-introducing then

RSIM(G) ⊨ f(X) = f(X)[X/X_{i}] ⊞ f(X)[Y/X_{i}] if sum(f, X)), (6)

else (f is τ-introducing) the following laws are valid in RSIM(G):

f(X) = f(X)[X/X_{i}] ⊞ f(X)[Y/X_{i}]
if sum(f, X)) & ¬tau(f(X)[X/X_{i}]) & ¬tau(f(X)[Y/X_{i}]) (7)
f(X) = f(X)[X/X_{i}] ⊳ f(X)[Y/X_{i}]
if sum(f, X)) & ¬tau(f(X)[X/X_{i}]) & tau(f(X)[Y/X_{i}]) (8)
f(X) = f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}]
if sum(f, X)) & tau(f(X)[X/X_{i}]) & tau(f(X)[Y/X_{i}]).  (9)

(Distributivity over ⊳ laws). Let X_{i} ≡ X ⊳ Y. If f is non-τ-introducing then

RSIM(G) ⊨ f(X) = f(X)[X/X_{i}] ⊳ f(X)[Y/X_{i}],  (10)

else (f is τ-introducing) the following laws are valid in RSIM(G):

f(X) = f(X)[X/X_{i}] ⊳ f(X)[Y/X_{i}]  if ¬tau(f(X)[X/X_{i}]) (11)
f(X) = f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}]  if tau(f(X)[X/X_{i}])  (12)

(Distributivity over ⊕ laws). Let X_{i} ≡ X ⊕ Y. Then

RSIM(G) ⊨ f(X) = f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}].  (13)

The presence of sum and tau predicates in the conditions of the above laws makes the resulting axiomatisations infinite. It is not clear whether or not there are finite axiomatisations of ≈_{RS} for arbitrary τDeS languages (disjoint extensions of B). In practice tau predicates can be removed from the conditions: this is briefly described in the last section. However, we see no way to replace sum predicates: giving more structure to the subterms and using extra τDeS operators does not seem to remove the infinitary character of axiomatisations.

Theorem 14. Let G be a τDeS language such that B ≤ G. Let Σ ⊆ Σ_{G} \ Σ_{B} be a set of distinctive operators. Suppose that T is an equational theory that extends RS with the following (conditional) equations (inequations) for each f in Σ: an action law (2) or (3) for each rule for f; all the inaction laws (4); all the divergence laws (5); for each active argument of f the distributivity over the three choice operators laws. Then RSIM(G) ⊨ T and T is head normalising.

Next, consider the CSP hiding operator \a defined by the following rules:

{X →^{a} X′ \atop X \a →^{τ} X′\a}  X →^{b} X′ ; b ≠ a ; X \a →^{b} X′\a  {X →^{τ} X′ \atop X \a →^{τ} X′\a.}

Below, we present a set of conditional axioms for \a as an example of the application of Theorem 14. In the following sum(·) denotes sum(⊞, X, Y).

(X ⊞ Y)\a = X \a ⊞ Y \a  if sum(·), ¬tau(X \a), ¬tau(Y \a) (14)
(X ⊞ Y)\a = X \a ⊳ Y \a  if sum(·), ¬tau(X \a), tau(Y \a) (15)
(X ⊞ Y)\a = X \a ⊕ Y \a  if sum(·), tau(X \a), tau(Y \a) (16)
(X ⊳ Y)\a = X \a ⊳ Y \a  if ¬tau(X \a)  (17)
(X ⊳ Y)\a = X \A ⊕ Y \a  if tau(X \a)  (18)
(X ⊕ Y)\a = X \a ⊕ Y \a
(bX)\a = a(X \a)  if b ≠ a
(aX)\a = X \a
0\a = 0
Ω\a ⊑ Ω

Note that due to the presence of sum and tau this axiomatisation is infinite. The next two lemmas show how to axiomatise non-distinctive operators.

Lemma 15. Let (f, n) be a non-distinctive non-τ-introducing operator of a τDeS language G, the disjoint extension of B. Then there exists a disjoint extension G′ of G with n-ary distinctive operators f_{1}, …, f_{k} such that G′ is a τDeS language and the following (conditional) equations hold in RSIM(G):

f(X) = f_{1}(X) ⊞ … ⊞ f_{k}(X) if sum(f, X)),  (19)

for each active argument i of f and for X_{i} ≡ X ⊳ Y

f(X) = f_{1}(X) ⊞ … ⊞ f_{k}(X) ⊳ f(X)[Y/X_{i}],  (20)

for each active argument i of f and for X_{i} ≡ X ⊕ Y

f(X) = f_{1}(X) ⊞ … ⊞ f_{k}(X) ⊳ f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}]. (21)

Lemma 16. Let (f, n) be a non-distinctive τ-introducing operator of a τDeS language G, the disjoint extension of B. Then there exists a disjoint extension G′ of G with n-ary distinctive non-τ-introducing operators f_{k}, k ∈ K ⊂_{fin} ℕ, and n-ary distinctive τ-introducing operators g_{l}, l ∈ L ⊂_{fin} ℕ, such that G′ is a τDeS language and the following (conditional) equations hold in RSIM(G):

f(X) = ∑_{K} f_{k}(X) ⊞ ∑_{L} g_{l}(X)
if sum(f, X)) & ∀l. ¬tau(g_{l}(X)),  (22)

f(X) = ∑_{K} f_{k}(X) ⊞ ∑_{m∈L\N} g_{m}(X) ⊳ ⨁_{N≠∅} g_{n}(X)
& if sum(f, X)) & ∀m. ¬tau(g_{m}(X)) & ∀n. tau(g_{n}(X)), (23)

for each active argument i of f and for X_{i} ≡ X ⊳ Y

f(X) = ∑_{K} f_{k}(X) ⊞ ∑_{L} g_{l}(X)[X/X_{i}] ⊳ f(X)[Y/X_{i}]
if ∀l. ¬tau(g_{l}(X)[X/X_{i}]),  (24)
f(X) = ∑_{K} f_{k}(X) ⊞ ∑_{m∈L\N} g_{m}(X)[X/X_{i}] ⊳ ⨁_{N≠∅} g_{n}(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}]
if ∀m. ¬tau(g_{m}(X)[X/X_{i}]) & ∀n. tau(g_{n}(X)[X/X_{i}]),  (25)

for each active argument i of f and for X_{i} ≡ X ⊕ Y

f(X) = ∑_{K} f_{k}(X) ⊞ ∑_{L} g_{l}(X) ⊳ f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}].  (26)

Below, we give algorithm A, based on the algorithm form [ABV92], for generating a sound and head normalising axiom system for ⊏_{∼}_{RS} for any τDeS language.

1. If G is not a disjoint extension of B then add to G a disjoint copy of B. Call the resulting language G′′′.

2. For each non-distinctive and non-τ-introducing operator f ∉ Σ_{B} in G′′′ apply the construction of Lemma 15 in order to obtain distinctive non-τ-introducing operators f_{1}, …, f_{k}. Call the resulting language G′′. Add to RS all the resulting instances of axioms (19)–(21) and call the resulting system T′′.

3. For each non-distinctive τ-introducing operator f ∉ Σ_{B} in G′′ apply the construction of Lemma 16 in order to obtain distinctive non-τ-introducing operators f_{1}, …, f_{k} and distinctive τ-introducing operators g_{1}, …, g_{l}. Call the resulting language G′. Add to T′′ all the resulting instances of axioms (22)–(26) and call thus obtained system T′.

4. Add to T′ the axioms produced by applying Theorem 14 to all distinctive operators in Σ_{G′} \ Σ_{B}. Call the resulting system T.

Theorem 17. Let G be a τDeS process language and G′ be a disjoint extension of G produced by algorithm A. Moreover, let T be the axiom system produced by algorithm A. Then RSIM(G) ⊨ T and T is head normalising.

As an example of the application of Theorem 17, we present below a set of conditional axioms for the merge operator ∥ [BW90], which is defined by the following rules:

{X →^{α} X′ \atop X ∥ Y →^{α} X′ ∥ Y}  {Y →^{α} Y′ \atop X ∥ Y →^{α} X ∥ Y′.}

The axiomatisation uses the auxiliary operators left-merge , defined in the introduction, and the right-merge which, due to the lack of space, is replaced below by . For the precedence of ∥ and we assume a > ∥ > > ⊞.

X ∥ Y = X Y ⊞ Y X  if sum(∥, X, Y)
X ∥ (Y ⊕ Z) = X (Y ⊕ Z) ⊞ (Y ⊕ Z) X ⊳ X ∥ Y ⊕ X ∥ Z
(Y ⊕ Z) ∥ X = Y ⊕ Z) X ⊞ X (Y ⊕ Z) ⊳ Y ∥ X ⊕ Z ∥ X
X ∥ (Y ⊳ Z) = X (Y ⊳ Z) ⊞ (Y ⊳ Z) X ⊳ X ∥ Z
(Y ⊳ Z) ∥ X = (Y ⊳ Z) X ⊞ X (Y ⊳ Z) ⊳ Z ∥ X
(X ⊞ Y) Z = X Z ⊞ Y Z  if sum( , X, Y)
(X ⊕ Y) Z = X Z ⊕ Y Z
(X ⊳ Y) Z = X Z ⊳ Y Z
aX Y = a(X ∥ Y)
0 X = 0
Ω X ⊑ Ω

5 Completeness

Algorithm A produces, for any τDeS process language G, a disjoint extension G′ with the axiom system T, which allows conversion of process terms into head normal form. If G is well-founded (defined below) then we can eliminate all the operators not in B from any term over G. It is done by applying the reduction to head normal form a finite number of times. In all such languages, those with a finite alphabet and no recursion, the problem of the completeness of their axiom systems reduces to the problem of head normalisation in the basic language B, which we addressed in Sect. 3.2. The following definition is from [ABV92]:

Definition 18. Let G be a τDeS process language. A term p ∈ T(Σ_{G}) is wellfounded iff there exists no infinite sequence p_{0}, a_{0}, p_{1}, a_{1}, … with p ≡ p_{0} and p_{i} →^{a_{i}} p_{i+1} for all i ≥ 1. G is well-founded iff all terms in T(Σ_{G}) are well-founded.

It is easy to show that, given any well-founded τDeS process language G with B ≤ G, the disjoint extension G′ produced by algorithm A is also well-founded. Thus, similarly as in [ABV92], we obtain the completeness result.

Theorem 19. Let G be a well-founded τDeS process language such that B ≤ G. Let G′ and T denote the disjoint extension and the axiom system produced by algorithm A respectively. Then for all p, q ∈ T(Σ_{G′}) if RSim(G′) ⊨ p ⊑ q then T ⊢ p ⊑ q.

The second completeness result is for τDeS languages which generate finitely branching derived transition systems. The axiom system is augmented with the following rule, based on AIP^{−} [BW90] and similar to the rule in [ABV92],

X/b^{n}Ω ⊑ Y/b^{n}Ω (for all n)
X ⊑ Y,

together with the axioms for the extra operator ·/·, which is defined in [ABV92]. The details concerning this completeness result can be found in [Uli95].

6 Conclusion

We have described how to derive complete axiomatisations of refusal simulation preorder for well-founded and for finitely branching τDeS languages. Our procedure can be easily adapted to coarser preorders such as refusal preorder [Phi87] or testing preorder [Hen88]. As our axioms are valid for any such preorder, we only need to augment the axioms for B with the extra axioms for that preorder.

For many τ-introducing operators, it is possible to remove tau conditions in favour of using extra operators and more structure in the subterms. Consider / ↓ A, the ‘initial’ restriction of actions in A operator, from [ABV92]. Axioms (14)-(16) can be rewritten, with a changed but obvious meaning of sum, as follows:

(X/ ↓ {a} ⊞ Y/ ↓ {a})\a = X/ ↓ {a}\a ⊞ Y/ ↓ {a}\a  if sum(X, Y) (27)
(X/ ↓ {a} ⊞ aY ⊞ Z)\a = X/ ↓ {a}\a ⊳ (aY ⊞ Z)\a if sum(X, Z) (28)
(aX ⊞ aY ⊞ Z)\a = aX \a ⊕ (aY ⊞ Z)\a.  if sum(Z) (29)

The axioms (17) and (18) can be similarly rewritten. However, for the operators like the CCS parallel the above trick will work provided that extra conditions concerning the initial actions of the subterms are used.

Finally, it would be interesting to find out if there are finite axiomatisations of ≈_{RS} for arbitrary τDeS languages (possibly with auxiliary τDeS operators).

Acknowledgements

I would like to thank the referees for their comments and suggestions. Thanks are also due to Paul Taylor for his Proof Trees macros.

References

[ABV92] L. Aceto, B. Bloom, and F.W. Vaandrager. Turning SOS rules into equations. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, 1992. IEEE Computer Science Press.

[Ace91] L. Aceto. A theory of testing for ACP. In Proceedings of 2nd International Conference CONCUR’91, Amsterdam, The Netherlands, 1991. LNCS 527.

[Ace94] L. Aceto. Deriving complete inference systems for a class of GSOS languages generating regular behaviours. In Proceedings of the 5th International Conference CONCUR’94, Uppsala, Sweden, 1994. Springer-Verlag. LNCS 789.

[AI95] L. Aceto and A. Ingólfsdóttir. CPO models for a class of GSOS languages. In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, Proceedings of TAPSOFT’95. Springer, 1995. LNCS 915.

[BHR84] S.D. Brookes, C.A.R. Hoare, and W. Roscoe. A theory of communicating sequential processes. Journal of ACM, 31:560–599, 1984.

[BIM88] B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can’t be traced: preliminary report. In Conference Record of the 15th ACM Symposium on Principles of Programming Languages, San Diego, California, 1988.

[BK84] J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Computation, 60:109–137, 1984.

[Blo90] B. Bloom. Strong process equivalence in the presence of hidden moves. Preliminary report, MIT, 1990.

[Blo95a] B. Bloom. Structural operational semantics for weak bisimulations. Theoretical Computer Science, 146:27–68, 1995. Also appeared as Technical Report TR 93-1373, Cornell, 1993.

[Blo95b] B. Bloom. Stuctured operational semantics as a specification language. In Conference Record of the 22nd ACM Symposium on Principles of Programming Languages, San Francisco, California, 1995.

[BW90] J.C.M Baeten and W.P Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science, volume 18. Cambridge University Press, 1990.

[dS85] R. de Simone. Higher-level synchronising devices in MEIJE-SCCS. Theoretical Computer Science, 37:245–267, 1985.

[Gro90] J.F. Groote. Transition system specifications with negative premises. In J.C.M. Baeten and J.W. Klop, editors, Proceedings of CONCUR’90, Amsterdam, 1990. Springer-Verlag. LNCS 458.

[GV92] J.F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100:202–260, 1992.

[Hen88] M. Hennessy. An Algebraic Theory of Processes. The MIT Press, 1988.

[Hoa85] C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

[Mil89] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[NH87] R. De Nicola and M. Hennessy. CCS without τ’s. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proceedings of TAPSOFT’87, Berlin, 1987. Springer-Verlag. LNCS 250.

[Phi87] I.C.C. Phillips. Refusal testing. Theoretical Computer Science, 50:241–284, 1987.

[Uli92] I. Ulidowski. Equivalences on observable processes. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, 1992. IEEE Computer Science Press.

[Uli94] I. Ulidowski. Local Testing and Implementable Concurrent Processes. PhD thesis, Imperial College, University of London, 1994.

[Uli95] I. Ulidowski. Axiomatisations of weak equivalences for De Simone languages. Technical report, RIMS, Kyoto University, 1995.

[Vaa91] F.W. Vaandrager. On the relationship between process algebra and input/output automata. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, 1991. IEEE Computer Science Press.

[vG93] R.J. van Glabbeek. Full abstraction in structured operational semantics. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Proceedings of the 3rd AMAST Conference. Workshops in Computing, Springer-Verlag, 1993.

[vGV93] R.J. van Glabbeek and F. Vaandrager. Modular specifications of process algebras. Theoretical Computer Science, 113:293–348, 1993.