Finite Axiom Systems for Testing Preorder and De Simone Process Languages

Irek Ulidowski

Research Institute for Mathematical Sciences, Kyoto University, Japan Email: irek@kurims.kyoto-u.ac.jp, tel:+ 8175-753-7238

Abstract

We prove that testing preorder of De Nicola and Hennessy is preserved by all De Simone process operators. Based on this result we propose an algorithm for generating axiomatisations of testing preorder for arbitrary De Simone process languages. The axiom systems produced by our algorithm are finite and complete for processes with finite behaviour. In order to achieve completeness for a subclass of processes with infinite behaviour we use one infinitary induction rule. The usefulness of our results is illustrated in specification and verification of small concurrent systems, where suspension, resumption and alternation of execution of component systems occur. We argue that better specifications can be more easily written in custom-made De Simone process languages which contain both the standard operators as well as new, specially tailored for the task in hand De Simone operators. Moreover, the automatically generated axiom systems for such specification languages make the verification straightforward.

1 Introduction

Process languages, for example CCS of Milner and CSP of Hoare, together with their semantic theories are reasonably successful in specification and verification of small concurrent systems. Both specifications, of varying level of abstractness, and the implementation of a given system are represented by processes—the terms in a process language. The task of proving that a more concrete specification refines an abstract one, and that the implementation meets some specification is then performed. There is a number of different proof methods which can be employed. One can define a denotational meaning of processes and then argue that the abstract specifications, concrete specifications and the implementation have increasingly better (in some sense) denotations. Alternatively, an operational preorder may be defined which relates the abstract with concrete specifications and the concrete specifications with the implementation. The third method, which is solely based on the syntax of processes, uses equational reasoning within some axiom system.

The major process languages (algebras) and their theories were developed in [Hoa85, Mil89a, Hen88, BW90] where, among others, the above described approach to specification and verification of concurrent systems was originally presented. More recently, due to Plotkin style structured operational semantics (SOS), these particular process languages and their numerous extensions were generalized to whole classes of process languages. Moreover, the theories for these languages and specification and verification techniques were extended to apply to such classes of languages. For example, a number of important preorders and equivalences on processes were shown to be congruences for certain classes of process languages [BIM88, BIM95, GV90, Gro90, Vaa91, Uli92, Blo95a, Uli94]. Axiomatic systems and denotational models for these classes of process languages were proposed in [ABV92, ABV94, Ace94, Uli95] and [AI95] respectively. Also, two classes of languages were used in [Blo95b] as general specification languages.

This paper continues the research related to general process languages. We consider a class of process languages generated by the De Simone format of rules with a special treatment of silent actions. This class, denoted by τDeS, was defined in [Uli95]. Out of many preorders (equivalences) proposed in the concurrency literature we consider testing preorder of De Nicola and Hennessy [NH84, Nic87, Hen88], which is based on an intuitive notion of comparing responses of processes to tests.

The first contribution of this paper is the proof that testing preorder is a precongruence for all τDeS languages. This result is the foundation on which our axiomatisation algorithm is based. It guarantees compositionality of specification and verification when working with τDeS process languages. For example, it allows to split the verification of a complex system into the verifications of its components. In this paper we employ equational reasoning as the method of proof for verification.

Since arbitrary τDeS operators are to be used in our specifications we require a general algorithm for deriving axiomatisations for these operators. Our second contribution is such an algorithm. It produces sound and complete axiomatisations of testing preorder for of τDeS languages generating well-founded processes. In contrast to axiomatisations of refusal simulation preorder for well-founded τDeS languages [Uli95] the axiomatisations of testing preorder for the same class of process languages are finite. Our algorithm is a modification of the original axiomatisation algorithm developed by Aceto, Bloom and Vaandrager [ABV92, ABV94] for strong bisimulation and GSOS process languages.

We support the argument of Bloom in [Blo95b] that classes of process languages, where one can use any operators within the class, are more superior for specification purposes than the standard languages like CCS and CSP. This is because simpler and easier to understand specifications can be written using both newly invented, specially tailored operators and the standard operators. As our third contribution we present examples of systems, where suspension and resumption of execution is important. Such systems usually do not have simple specifications in standard languages, although the addition of extra features like prioritized actions [CH90] may help. However, clear and intuitive specifications of such systems can be written using new, invented for that purpose operators. We give both abstract and concrete specifications. Equational reasoning, based on axiomatisation generated by our procedure, is then used to show that the specifications are equivalent.

The paper is organized as follows. We recall, in Section 2, the definitions of τDeS process languages, labelled transition systems and testing preorder. In Section 3 we show that (a characterisation of) testing preorder is a precongruence for any τDeS language. We begin Section 4 by restating a completeness result for a simple τDeS language and testing preorder. Then, we present an algorithm for generating sound axiomatisations for arbitrary τDeS languages. These axiomatisations are proved to be finite and head normalising for certain classes of τDeS languages. The section finishes with a completeness result. In Section 5 we present two examples illustrating the application of our results. The last section contains a conclusion and a discussion of related work. A number of proofs concerning soundness, head normalisation and completeness of axiom systems produced by our algorithm appears in Appendices A and B.

2 Basic Concepts

In this section we repeat the definitions of τDeS process languages, labelled transition systems and testing preorder. We also define a number of other notions in order to make the paper selfcontained. Full definitions and the results concerning the above can be found, for example, in [NH84, Hen88, BIM95, GV90, Uli95, Uli92].

Let Var be a countable set of variables ranged by X, Y, . . .. A signature Σ is a set process operators (f, n), where f ∉ Var and n ∈ is the arity of the operator. Often, when the operator’s arity 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 V is denoted by (Σ, V). (Σ, Var), abbreviated by (Σ), is ranged by P, Q, . . .. The set of closed terms T(Σ) is ranged by p, q, t, . . .. A Σ context with n holes C[X_{1}, …, X_{n}], n ∈ , is a member of (Σ, {X_{1}, …, X_{n}}) in which each X_{i} occurs at most once. If t_{1}, …, t_{n} are Σ terms then C[t_{1}, …, t_{n}] is a term obtained by replacing each X_{i} with t_{i}, 1 ≤ i ≤ n. We will often denote a sequence of process terms P_{1}, …, P_{n} as P. We will also write P RQ, for some relation R, to mean P_{1}RQ_{1}, …, P_{n}RQ_{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 from (Σ) to (Σ) in a standard way. We will write Q[P_{1}/X_{1}, …, P_{n}/X_{n}] to denote the substitution which assigns each X_{i} to P_{i}. Act ∪ {τ}, ranged by α, …, is a finite set of actions, where Act consists of visible actions a, b, …, and τ ∉ Act is the silent action.

2.1 τDeS Process Languages

We define τDeS format of SOS rules and τDeS process languages both of which are based on the structured transition rules originally proposed by De Simone [dS85].

Definition 2.1 [Uli95] A De Simone (structured transition) 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.

A τ-rule for the above De Simone rule is any of the rules with the following form, where i ∈ I:

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

The set of all τ-rules for rule (1) is called the set of associated τ-rules. A set of rules is in the De Simone format, written as τDeS, if it consists of De Simone rules, their associated τ-rules and no other rules. A process operator is τDeS if the set of its defining rules is in τDeS. The set of associated τ-rules for a τDeS operator consists of all τ-rules associated with all De Simone rules defining the operator. A De Simone process language, or simply τDeS language, is a triple (Σ, A ∪ {τ}, R), where Σ is a finite set of τDeS operators, A ⊆ Act and R is a finite set of rules defining the operators in Σ.

Most of the operators in process algebras are τDeS except, for example, the CCS and ACP choice operator + and the ACP left-merge and communication merge operators: their sets of defining rules do not contain the required τ-rules. τDeS is a subformat of the GSOS format [BIM88, BIM95, Blo90a] and thus it enjoys all the properties of the GSOS format. In particular, τDeS operators preserve (strong) bisimulation [BIM88, BIM95]. Moreover, τDeS is a subformat of the ISOS format [Uli92, Uli94] which itself is a minor restriction of the GSOS format with a natural treatment of silent actions. Since a version of weak bisimulation, sometimes called delay bisimulation, is preserved by ISOS operators [Uli94] it is also preserved by τDeS operators.

Below, we define a number of notions related to De Simone rules.

Definition 2.2 Let (Σ, Act ∪ {τ}, R) be τDeS language and r ∈ R has the form (1). Then, {X_{i} →^{a_{i}} X′_{i}}_{i∈I} is the set of antecedents of r, written as ante(r), and f(X_{1}, …, X_{n}) →^{α} C[Y ] is the consequent, written as cons(r). In general, expressions T →^{α} T′ with T, T′ ∈ (Σ) and α ∈ Act ∪ {τ} are called transitions. T is the source and T′ is the target of T →^{α} T′. f is the operator of r and α is the action. The trigger of r is an n-tuple (λ_{1}, …, λ_{n}), where λ_{i} = a_{i}, if i ∈ I, and λ_{i} = ∗ otherwise. The α trigger for f is a trigger of one of De Simone rules for f with the action α. We will use trig_{α}(f) for the set of all α triggers for f. We say that i-th argument of f is active if there is a De Simone rule for f with the antecedent X_{i} →^{a_{i}} X′_{i}, for some a_{i}. active(f) denotes the set of all i such that the ith argument of f is active.

2.2 Labelled Transition Systems

Next, we define labelled transition systems for τDeS languages. We will use a special nullary operator Ω with no defining rules to represent divergence of processes due to underspecification (lack of information about behaviour). Later, we will also discuss another form of divergence, namely the ability to perform an infinite sequence of silent actions.

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

The above defined transition system will be often called the basic transition system for G, and the subscript G will be omitted when it is obvious from the context. We will use the following abbreviations: p →^{a} q denotes (p, a, q) ∈→; p →^{a} is equivalent to ∃q ∈ T(Σ). p →^{a} q; and p →^{t} stands for p →^{a_{1}} … →^{a_{n}}, where t = a_{1} … a_{n} ∈ Act^{∗}. ε is the empty sequence in Act^{∗} and s ≤ t, for s, t ∈ Act^{∗}, means that s is an initial subsequence of t. With the notation as in the previous definition, we say that transition t →^{α} t′, for t, t′ ∈ T(Σ_{G}), is valid (holds) in →_{G} if (t, α, t′) ∈→_{G}.

Since the τDeS format is a subformat of the GSOS format the finite branching property of (basic) transition systems generated by the GSOS languages [BIM88, BIM95] also holds for basic transition systems of τDeS languages. Namely, {q | p →^{α} q, any α ∈ Act ∪ {τ}} is finite, for each process p in a given τDeS language.

The derived transition system, which abstracts away the silent actions and captures divergence due to infinite sequences of silent actions, is defined below.

1Full details of the construction of transition relation for a process language defined by a general format of rules can be found in, for example, [BIM88, BIM95, GV90].

Definition 2.4 Given the basic transition system (T(Σ), Act∪{τ}, →, ↑) for a τDeS language a structure (T(Σ), Act ∪ {ε}, ⇒, ⇑) is the derived transition system with divergence. The transition relation ⇒⊆ T(Σ)×Act∪{ε}×T(Σ) and the divergence predicate ⇑ ⊆ T(Σ)×Act^{∗} are defined as follows, where →^{τ^{∗}} is the reflexive and transitive closure of →^{τ}:

\begin{matrix}p ⇒^{ε} q ≡ p →^{τ^{∗}} q, & p ⇒^{a} q ≡ p →^{τ^{∗}}→^{a}→^{τ^{∗}} q, \\ p⇑ε ≡ ∃q.(p →^{τ^{∗}} q ∧ q↑) ∨ p →^{τ^{ω}}, & p⇑as ≡ p⇑ε ∨ ∃q.(p ⇒^{a} q ∧ q⇑s). \end{matrix}

We say ‘p converges on s’, written as p⇓s, if ¬ p⇑s. Expressions p ⇒^{a} and p ⇒^{t} are defined correspondingly as p →^{a} and p →^{t}. Expression p ⇒ q means p ⇒^{α} q, for some α ∈ Act ∪ {ε}. The language of p, written as L(p), is {s | p ⇒^{s}}. The set of initial visible actions a process can perform S(p) is {a | p ⇒^{a}}. The set of t descendants of process p is defined as D(p, t) ≡

{p′ | p ⇒^{t} p′}.

We distinguish the following classes of processes and τDeS languages according to the properties of transition systems they are related to.

Definition 2.5 Assume the basic and derived transition systems for an arbitrary τDeS process language.

(a) A process p is well-founded if and only if there exists no infinite sequence p_{0}, α_{0}, p_{1}, α_{1}, … with p ≡ p_{0} and p_{i} →^{α_{i}} p_{i+1} for all i ≥ 1. A τDeS language is well-founded if and only if all its processes are.

(b) A process p is finite branching if and only if {q | p′ ⇒ q} is finite, for every t ∈ Act^{∗} and p′ in D(p, t).

(c) A process p is τ-divergent if and only if q →^{τ}^{ω}, for some t ∈ Act^{∗} and q in D(p, t). A process p is initially τ-divergent if and only if p →^{τ}^{ω}. A process is τ-convergent (initially τ-convergent) if and only if it is not τ-divergent (not initially τ-divergent). A τDeS language is τ-convergent if and only if all its processes are τ-convergent.

Example 2.6 Not all τDeS process languages are finite branching. Consider a τDeS language with prefixing with a, the deadlocked process 0 and the operators g and f defined by

g →^{a} g  {X →^{a} X′ \atop f(X, Y) →^{τ} f(X′, a.Y)}  f(X, Y) →^{τ} Y.

Consider term f(g, 0). We have f(g, 0) →^{τ} f(g, a.0) →^{τ} … →^{τ} f(g, a^{n}.0) →^{τ} and f(g, a^{n}.0) →^{τ} a^{n}.0, for all n. Process f(g, 0) is not finite branching since f(g, 0) ⇒^{ε} a^{n}.0, for all n.

Finally, we define disjoint extensions of τDeS languages.

Definition 2.7 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 of G.

2.3 Basic τDeS Language B

Throughout this work we will consider a simple τDeS language B which is essentially a finite version of the language considered in [NH87, Hen88]. It has the two CSP choice operators and ⊕, the external and internal choice operators respectively, instead of the CCS choice operator + and prefixing with τ. B is a τDeS process language (Σ, Act ∪ {τ}, R), where Σ = {(0, 0), (Ω, 0)} ∪{(a, 1) | a ∈ Act} ∪ {( , 2), (⊕, 2)} and R is given below. Operators (0, 0) and (Ω, 0) are abbreviated by 0 and Ω; they do not have the defining rules. The precedence of operators is given by a > > ⊕.

prefixing  a.X →^{a} X,  a ∈ Act
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

We will call B the basic τDeS process language. Sometime it will be convenient to consider sub-languages of B which only have some of the prefixing operators of B. We will write B(A) for a language which contains prefixing operators a for all a ∈ A, the two choice operators as well as 0 and Ω. Clearly B(Act) = B.

B generates the basic transition system B = (T(Σ), Act ∪ {τ}, →, ↑). Note that all processes in T(Σ) are well-founded and τ-convergent. We have Ω↑. Also, if p↑ then (p q) ↑ and (q p) ↑. But, for example, p↑ does not imply (p ⊕ q)↑. Given B we can define (T(Σ), Act ∪ {ε}, ⇒, ⇑) in a straightforward way. One can check that the divergence predicate ⇑ is the least relation satisfying the following: Ω⇑ and if p⇑ then (p q) ⇑, (q p) ⇑, (p ⊕ q)⇑ and (q ⊕ p)⇑.

2.4 Testing Preorder

Testing was introduced by De Nicola and Hennessy in [NH84, Nic87, Hen88]. The preorder based on testing, testing preorder, is defined in terms of the responses of processes to tests, which themselves are special processes with a set of actions containing a success action w. The responses of a process to a test are determined by observing the computations of a system consisting of the test ‘applied’ to the process.

This paper concerns itself with testing in τDeS process languages. For technical reasons we will limit our attention to a certain subclass of τDeS process languages which we describe below. First, we define an auxiliary notion.

Definition 2.8 A τDeS process language G with the set of visible actions A is called selfencoding if B(A) ≤ G.

Given any τDeS language G let G_{T} denote a disjoint extension of G with an extra prefixing operator (w, 1) not in Σ_{G} and the test application operator (|, 2) defined by the τDeS rules below.

{X →^{a} X′ Y →^{a} Y′ \atop X |Y →^{τ} X′ |Y′}  {X →^{τ} X′ \atop X |Y →^{τ} X′ |Y}  {Y →^{τ} Y′ \atop X |Y →^{τ} X |Y′}

In what follows we will consider testing in τDeS languages G with the set of actions A ∪ {τ} only if B(A)_{T} ≤ G. In other words, only if G is self-encoding and it contains the operators (w, 1) and (|, 2) described above. We will give such τDeS languages a special name.

Definition 2.9 A τDeS process language G is called self-testing if B_{T} (A) ≤ G.

When we consider testing we assume that the processes are those terms over G which do not involve prefixing with w and the tests (varied by t, t′, …) are the terms which contain w. The operator | is used to express the application of a test t to a process p, written as p | t. Sequence p_{0} | t_{0} →^{τ} p_{1} | t_{1} … →^{τ} p_{k} | t_{k} … is called a computation if it is maximal, i.e. it is infinite or it is finite with the last element p_{k} |t_{k} such that p_{k} |t_{k} →^{τ} p′ |t′ for no pair p′, t′.

Next, we restate the definitions of relations ‘may satisfy’ and ‘must satisfy’ between processes and tests, and of testing preorders _{∼}may, _{∼}must and _{∼} as in [NH84, Nic87, Hen88].

Definition 2.10 Let G be a self-testing τDeS process language. Given a process p and a test t over G

1. p may t if p|t →^{τ^{∗}} p′ |t′ and t′ →^{w},

2. p must t if whenever (p|t =)p_{0} |t_{0} →^{τ} p_{1} |t_{1} →^{τ} … is a computation then (a) ∃n ≥ 0 such that t_{n} →^{w}, and (b) if (p_{k} |t_{k})↑ then t_{k′} →^{w}, for some k′ ≤ k.

Definition 2.11 For processes p, q over the language G as in the previous definition we have

p _{∼}may q ≡ ∀ tests t. p may t implies q may t,
p _{∼}must q ≡ ∀ tests t. p must t implies q must t,
p _{∼} q  ≡ p _{∼}may q ∧ p _{∼}must q.

It is easily checked that _{∼}may, _{∼}must and _{∼} are preorders. Testing equivalence, written as ≈, is defined by p ≈ q ≡ p _{∼} q ∧ q _{∼} p. The equivalences arising from _{∼}may and _{∼}must, denoted by ≈may and ≈must, are defined correspondingly.

Instead of working directly with _{∼}may, _{∼}must and _{∼}, we will employ their alternative characterisations as described in [NH84, Hen88].

Definition 2.12 With the notation as in the previous definition

p ≪may q ≡ L(p) ⊆ L(q),
p ≪must q ≡ ∀s ∈ Act^{∗}. p⇓s implies

(a) q⇓s ∧

(b) ∀q′. q ⇒^{s} q′ implies ∃p′. p ⇒^{s} p′ ∧ S(p′) ⊆ S(q′),

p ≪ q  ≡ p ≪may q ∧ p ≪must q.

Note that our definition of ≪ is almost the same as the corresponding Definition 4.4.5 in [Hen88]. The only difference is that instead of condition (b) the condition A(q, s) ⊂⊂ A(p, s) is used in [Hen88]. We remind that A(q, s) is {S(p′) | p ⇒^{s} p′} and A ⊂⊂ B if for every A ∈ A there is some B ∈ B such that B ⊆ A. It is easily checked that condition (b) and A(q, s) ⊂⊂ A(p, s) are logically equivalent.

The equivalences based on ≪may, ≪must and ≪, denoted by ≃may, ≃must and ≃, are defined correspondingly as ≈may, ≈must and ≈.

Finally, we have our version of a characterisation result.

Theorem 2.13 p _{∼} q if and only if p ≪ q, for all processes p and q over any self-testing τDeS process language.

The proof of this theorem follows similar lines as the proofs of characterisation results proposed by the De Nicola and Hennessy, in particular the proofs in [Hen88] of Lemma 4.4.9, which corresponds to the ‘only if’ part of Theorem 2.13, and Lemma 4.4.13, which corresponds to the ‘if’ part of Theorem 2.13. A careful examination of the proof of Lemma 4.4.9 will show that it does not depend on the process language considered. Hence, the proof can be easily adapted for any τDeS language. The same is true of Lemma 4.4.13 provided that the following two conditions are satisfied by the considered process language. Firstly, the language has to have appropriate operators to encode the essential tests. This condition is trivially satisfied by self-testing τDeS languages. Secondly, a certain finite branching condition needs to be satisfied by the derived transition system of the considered τDeS language. As we have seen in Example 2.6 not all τDeS processes are finite branching. But, the proof of Lemma 4.4.13 (in particular, the proof of auxiliary Lemma 4.4.12) only requires τ-convergent processes to be finite branching. More precisely, the following property must hold: for all processes p in the considered language, if p⇓t and s ≤ t then {q | p′ ⇒ q} is finite, for all p′ ∈ D(p, s). Since for any τDeS language its basic transition system is finite branching it is easy to show that the above property is indeed valid. Hence, ≪ can be used instead of _{∼} in every self-testing τDeS process language.

In the rest of the paper we will need the following notational agreements. We will use Test(G) to denote the quotient algebra of elements of (Σ_{G}) factored by ≪ and write Test(G) P ⊑ Q to mean ρ(P) ≪ ρ(Q), for all P and Q and all ground substitutions ρ over G. Since we will talk about axioms which are preserved by taking disjoint extensions of τDeS languages we will need TEST(G): a class of all algebras Test(G′), where G′ is a disjoint extension of G. For P, Q ∈ (Σ_{G}) we have

TEST(G) P ⊑ Q iff (∀G′.G ≤ G′ implies Test(G′) P ⊑ Q).

3 Congruence Theorem

In this section we prove the congruence theorem which is the foundation of our axiomatisation algorithm. Then, we briefly comment on congruence results for other formats with a special treatment of silent actions.

Theorem 3.1 (Congruence) ≪ is a precongruence for all τDeS languages.

Its proof, like the proofs of congruence theorems for other weak equivalences and classes of process languages [Blo95a, Uli94], is rather long, technical and relies on checking many cases. Before we present the details of the proof we will show that ≪ is not in general preserved by non-τDeS operators. We consider only two classes of such operators: the operators defined by rules with ‘copying’ and the operators defined by rules with negative premises.

Example 3.2 Consider the operator θ_{b>a} which gives a priority to action b over action a. The defining rules, which clearly are not τDeS, are as follows:

X →^{b} X′ ; b ≠ a ; θ_{b>a}(X) →^{b} θ_{b>a}(X′)  {X →^{a} X′ X ^{b} \atop θ_{b>a}(X) →^{a} θ_{b>a}(X′)}

Let p = a(b aΩ) aa and q = a(b aΩ) a(a aΩ). Clearly p ≃ q but not θ_{b>a}(p) ≃ θ_{b>a}(q).

For θ_{b>a}(p)⇓aa, but θ_{b>a}(q)⇑aa since θ_{b>a}(q) ^{aa} Ω.

Example 3.3 Consider operators f and f′ defined by the following rules.

X →^{a} X′ ; b ≠ a ; f(X) →^{τ} f′(X′, X′)  {X →^{b} X′ Y →^{c} Y′ \atop f′(X, Y) →^{c} 0}

Let p = ab ac and q = a(b ⊕ c). Clearly p ≃ q but not f(p) ≃ f(q): f(q) ⇒^{c} but f(X) ^{c} .

Now, we turn the attention to the proof of Theorem 3.1. We will introduce a number of helpful notions. In order to improve the analysis of the behavior of processes in arbitrary contexts we will employ ruloids and Ruloid Theorem for τDeS languages—these are based on Bloom’s work on ruloids for GSOS languages [Blo90a, Blo95a].

Ruloids are like τDeS rules except that the consequent has the form C[X] →^{α} C′[Y ], where both C[X] and C′[Y ] are contexts and the elements of Y are defined as in Definition 2.1. For example, the following is a ruloid for the context (X b.Y)\a, where \a is the usual CSP hiding operator (it will be formally defined in Section 4.1), and action b not equal to a

{X →^{b} X′ \atop (X b.Y)\a →^{b} X′\a}  (2)

Given a τDeS language G, Ruloid Theorem says that given a term C[p] and an action α ∈ Act ∪ {τ} it is possible to construct a set ruloids which describe all the circumstances when C[p] performs α.

Theorem 3.4 Let G be a τDeS language, C[X] a context over Σ and α an action in Act∪{τ}. Then, there exists a finite set R of ruloids for C[X] and α such that

1. the consequent of each r ∈ R has the form C[X] →^{α} D[Y ], for some context D[Y ] with Y as in Definition 2.1,

2. R explains all α moves of all instances of C[X]. Namely, if ρ(C[X] →^{α} D[Y ]) is valid, for some Σ ground substitution ρ, then (a) there exists r ∈ R such that ρ(cons(r)) = ρ(C[X] →^{α} D[Y ]) and (b) ρ(ante(r)) is valid.

3. all ruloids in R are valid. Namely, for any r ∈ R and Σ ground substitution ρ, if ρ(ante(r)) is valid then ρ(cons(r)) is valid.

For example, the set of ruloids for (X b.Y)\a and action b as above consists of the ruloid (2) and the ruloid (X b.Y)\a →^{b} Y \a. In general, there are also τ-ruloids, the notion corresponding to τ-rules. In our example, there is only one τ-ruloid since only the argument X is active (active arguments of ruloids are defined in the same way as for rules):

{X →^{τ} X′ \atop (X b.Y)\a →^{τ} (X′ b.Y)\a}

Also it will be beneficial to use a certain notation for ruloids similar to ruloids in ϵ-presentation [Blo95a], which are described first. A ruloid for C[X] is ϵ-presented if it has one antecedent X_{i} →^{μ} X′_{i} for each variable in X, where μ ∈ A ∪ {τ} ∪ {ϵ} and ϵ ∉ Act. An ordinary ruloid for C[X] and α, call it r, can be made into a corresponding ϵ-presented ruloid by adding to antecedents the transition X_{i} →^{ϵ} X′_{i} for each variable X_{i} of X which does not appear in the antecedents of r. The antecedent X_{i} →^{ϵ} X′_{i} represents a null transition: when a ruloid with such an antecedent is used then X_{i} and X′_{i} are bound to the same term. For example, the following is the set of ϵ-presented ruloids for (X b.Y)\a and b, where because of the form of antecedents the second ruloid could be called ‘axiom’ ruloid.

{X →^{b} X′ Y →^{ϵ} Y′ \atop (X b.Y)\a →^{b} X′\a}  {X →^{ϵ} X′ Y →^{ϵ} Y′ \atop (X b.Y)\a →^{b} Y′\a}

The first of the above ϵ-presented ruloids and the ruloid for X\a and action c not equal to a can be written using the following abstract notation

{X →^{b} X′ Y →^{ϵ} Y′ \atop C[X, Y] →^{b} C′[X′, Y′]}  {X →^{c} X′ Y →^{ϵ} Y′ \atop C′[X, Y] →^{c} C′[X′, Y′]}

where C[X, Y] and C′[X, Y] stand for the contexts (X b.Y)\a and X\a respectively. Note that the second ruloid has antecedents for both X and Y although C′[X, Y] actually stands for X\a in which Y does not appear. Note that since no process variable can be copied in De Simone rules or ruloids, i.e. used more than once in the target of the consequent, it is correct to use the same number of process variables in both the source and target of the consequent. This abstract notation for ϵ-presented ruloids will be extensively used in the proof of the congruence theorem. Proof of Theorem 3.1. Let G = (Σ, Act ∪ {τ}, R) be a τDeS process language. Assume p ≪ q, where p and q are vectors of closed Σ terms. We need to prove C[p] ≪ C[q], for any n-ary Σ context C[X]. The last can be subdivided, by Definition 2.12, into three parts:

1. L(C[p]) ⊆ L(C[q]),
2. ∀s ∈ Act^{∗}. C[p]⇓s implies C[q]⇓s,
3. ∀s ∈ Act^{∗}. C[p]⇓s implies (∀D[X], q′. C[q] ⇒^{s} D[q′] implies

∃p′.(C[p] ⇒^{s} D[p′] ∧ S(D[p′]) ⊆ S(D[q′]))).

Part 1. Let α_{1} … α_{k} ∈ (Act ∪ {τ})^{∗} be such that after removing actions τ we obtain s ∈ Act^{∗}. We will show that C[p] ⇒^{s} implies C[q] ⇒^{s}. C[p] →^{α_{1}} … →^{α_{k}} can be represented as C[p] ≡ C_{0}[p_{0}] →^{α_{1}} … →^{α_{k}} C_{k}[p_{k}], for some n-ary contexts C_{j}[X] and n-ary vectors p_{j}. Note that some contexts C_{j}[X] may in fact stand for open terms where not all elements of X appear. For each 0 ≤ j < k, C_{j}[p_{j}] ⟶^{α_{j+1}} C_{j+1}[p_{j+1}] gives rise, by Ruloid Theorem and the above discussion on the notation for ϵ-presented ruloids, to the following:

p_{1j} ⟶^{μ_{1j+1}} p_{1j+1}, …, p_{nj} ⟶^{μ_{nj+1}} p_{nj+1},  (3)

where each μ_{ij+1} ∈ Act ∪ {τ} ∪ {ϵ}. Sequence (3) specifies the behavior of the components p_{ij} of p_{j}, where 1 ≤ i ≤ n, which produces C_{j}[p_{j}] ⟶^{α_{j+1}} C_{j+1}[p_{j+1}].

Sequence (3) can be abbreviated by p_{j} →^{A_{j+1}} p_{j+1}, where A_{j+1} is the column vector of μ_{ij+1}’s. We can say more about the chemistry of vectors A_{l}. When A_{l} contains no visible action then it consists either of a single τ and n − 1 labels ϵ or it consists of n labels ϵ. These vectors arise when applying ϵ-presented τ-ruloids and ‘axiom’ ruloids respectively. The first of these vectors is called a τ-column. Putting the individual transitions of all p_{j} together we obtain p_{0} →^{A_{1}} … →^{A_{k}} p_{k}, or abbreviating even further p_{0} \underrightarrow{A} p_{k}, where A is a vector of column vectors A_{j}. In other words, A is an n × k + 1 matrix. Note that the ith row of A is μ_{i1} … μ_{ik} and it represents the behavior the ith component p_{i0} of p_{0}. Let s_{i} be μ_{i1} … μ_{ik} with all labels τ and ϵ removed, thus p_{i0} ⇒^{s_{i}}. Performing the same for other components of p_{0} we obtain p_{0} \underrightarrow{s}, where s is the column vector s_{1}, …, s_{n}. Since p ≪ q and p ≡ p_{0} we have q(≡ q_{0}) \underrightarrow{s}.

If we could repeat the above argument in reverse for q_{0}, that is from q_{0} \underrightarrow{s} deduce q_{0} \underrightarrow{A},

then we would derive C[q_{0}] ⇒^{s} as required. However, q_{0} \underrightarrow{A} is not valid in general since the components of q_{0} and p_{0} may vary in the number of actions τ they can perform and the places of their occurrence. But, it can be easily shown that given q_{0} \underrightarrow{s} (and keeping A in mind) we can construct an n × l + 1 matrix B such that it only differs from A in the number and positions of τ-columns. Having this we can deduce C[q_{0}] →^{ν_{1}} … →^{ν_{l}}, where the sequence ν_{1} … ν_{l} differs from μ_{1} … μ_{k} in the number and places of occurrences of actions τ. Hence,

(C[q] ≡)C[q_{0}] ⇒^{s} follows.

Part 2. We will show that for every s ∈ Act^{∗} if C[q]⇑s then C[p]⇑s. Assume C[q]⇑s, for some s. This means that for some minimal t ≤ s, C′[X] and q′ such that C[q] ⇒^{t} C′[q′] we either have C′[q′]↑ or C′[q′] →^{τ^{ω}}. (The minimality of t means that for all proper subsequences t′ of t we have C[q]⇓t′). We only consider the first case C′[q′]↑, the proof of the second is similar. C′[q′]↑ implies there is a ruloid for C′[X] and some α which has the antecedent X_{i} →^{μ} X′_{i} with μ ≠ ϵ such that q′_{i}↑. From C[q] ⇒^{t} C′[q′] we obtain, using Ruloid Theorem, q_{i} ⇒^{t_{i}} q′_{i} for some t_{i} ∈ Act^{∗} and thus q_{i}⇑t_{i}. Since p ≪ q we easily obtain p_{i}⇑t_{i}. Thus, there

exist p′_{i} and t′_{i} ≤ t_{i}, such that p_{i} ⇒^{t′_{i}} p′_{i} and p′_{i}↑ or p′_{i} →^{τ^{ω}}. Using Ruloid Theorem for C[X] and the other contexts involved in C[q] → … → C′[q′] we obtain: (a) C[p] ⇒^{t′} C^{∗}[p′], where C^{∗}[X] is some context which appears in C[q] → … → C′[q′], (b) the ith argument of C^{∗}[X] is active and the ith component of p′ is p′_{i} and (c) t′ ≤ t. Thus, C^{∗}[p′]↑ or C^{∗}[p′] →^{τ^{ω}}. This implies C[p]⇑t′ and so C[p]⇑s.

Part 3. Assume C[p]⇓s and C[q] ⇒^{s} D[q′], for some s ∈ Act^{∗}, q′ and D[X]. We need to show that (a) there exists p′ such that C[p] ⇒^{s} D[p′] and (b) S(D[p′]) ⊆ S(D[q′]). Using Ruloid Theorem and the technique from Part 1 we establish the behavior of q which gives rise to C[q] ⇒^{s} D[q′]. We write it as q \underrightarrow{s} q′, where s is a vector of s_{i} ∈ Act^{∗}. By Part 2 we obtain C[q]⇓s and thus, overloading the notation, q⇓s. C[p]⇓s means that for all t ≤ s if

C[p] ⇒^{t} then, by Ruloid Theorem, p \underrightarrow{t} and p⇓t. Clearly t ≤ s, i.e. t_{i} ≤ s_{i} for all i. We wish to prove that p \underrightarrow{s}. Assume the opposite: p_{i} ⇒^{t_{i}} for all t_{i} ≤ s_{i} described above and p_{i} ^{s_{i}}. The last gives p_{i}⇓s_{i} which, together with p_{i} ≪ q_{i} and q_{i} ⇒^{s_{i}}, produces p_{i} ⇒^{s_{i}}: a contradiction. Thus, for all i and p′_{i} we get p_{i} ⇒^{s_{i}} p′_{i}. Hence, p \underrightarrow{s} p′. Similarly as in Part 1, we deduce C[p] ⇒^{s} D[p′] which is the required part (a). Since for each i we have S(p′_{i}) ⊆ S(q′_{i}) and since the behavior of D[p′] and D[q′] depends on the actions of p′ and q′ we deduce that if D[p′] ⇒^{a}, for some a, then D[q′] ⇒^{a}. Thus, S(D[p′]) ⊆ S(D[q′]) as required.

As an immediate consequence we have

Corollary 3.5 _{∼} is a precongruence in all self-testing τDeS languages.

Concluding this section we wish to underline how simple and intuitive τDeS operators are. They preserve testing preorder as well as many other weak equivalences and preorders. Since

Figure 1: Axiomatization of Testing Preorder.

E1 X 0 = X
E2 X X = X  I2 X ⊕ X = X
E3 X Y = Y X  I3 X ⊕ Y = Y ⊕ X
E4 X (Y Z) = (X Y) Z  I4 X ⊕ (Y ⊕ Z) = (X ⊕ Y) ⊕ Z
C1 a.X a.Y = a.X ⊕ a.Y
C2 a.X a.Y = a.(X ⊕ Y)  C3 X ⊕ Y ⊑ X Y
D1 X (Y ⊕ Z) = (X Y) ⊕ (X Z)  Ω1 Ω ⊑ X
D2 X ⊕ (Y Z) = (X ⊕ Y) (X ⊕ Z)  Ω2 X Ω ⊑ X ⊕ Ω

the τDeS format is a subformat of the ISOS format τDeS operators preserve refusal simulation preorder [Uli92, Uli94] and delay bisimulation [Uli94]. It is thus somewhat surprising that such well behaved operators do not preserve the standard version of weak bisimulation as defined, for example, in [Mil89a]. It was argued in [vG90] that useful operators such as action refinement operators do not preserve weak bisimulation. In [PU96] a simple τDeS version of action refinement operator is defined which does not preserve weak bisimulation. However, there is a format (similar in the expressive power to the ISOS format) proposed by Bloom [Blo95a] which preserves weak bisimulation, but in our opinion it suffers from a complicated definition. Bloom [Blo95a] also proposes formats of rules for branching bisimulation and the ‘rooted’ versions of both weak and branching bisimulations.

4 Finite Axiom Systems for τDeS Languages

In this section we show how to generate an axiomatisation of an arbitrary τDeS language. The strategy is as follows. Given a τDeS language G we disjointly extend it with the basic process language B to obtain G′. We propose sound laws (axiom schemas) for all G′ operators which are not in B. The axiom system for G (in fact for G′) consists of the instances of these laws together with the axiom system for B. If G is well-founded then the proposed axiom system is sufficient to rewrite arbitrary process terms over G into equivalent terms over B. This is possible because well-founded terms over G can be put into head normal form by using the axiom system. Hence, the problem of completeness for well-founded processes over G is reduced to the already solved completeness problem for B. In order to achieve completeness for a certain subclass of not well-founded processes it is enough to extend the axiom system with one infinitary induction rule.

We start by recalling the axiom system TB for ≪ over the language B. TB consists of equations and inequations given in Figure 1 as well as the usual properties of precongruences: reflexivity, transitivity, substitutivity (if p ⊑ q then f(p) ⊑ f(q)), instantiation and inequations as, for example, in Figure 1.2 in [Hen88]. We will write T ⊢ P ⊑ Q, (P = Q) to mean that P ⊑ Q, (P = Q) can be derived from the axiomatic system T.

Lemma 4.1 [Hen88] TB ⊢ P ⊑ Q if and only if Test(B) P ⊑ Q.

Since and ⊕ are associative the summation notations ∑_{i∈I} X_{i} and ⨁_{j∈J≠∅} Y_{j} are justified.

Finally, we remind the definitions of head normal forms, hnf for short, from [NH84, Hen88].

Definition 4.2 Let A be a finite non-empty set of subsets of Act. We say that A is saturated if and only if (a) A, B ∈ A implies A ∪ B ∈ A and (b) A, B ∈ A, A ⊆ C ⊆ B implies C ∈ A. Head normal forms are defined as follows: 0 is in hnf; if A is saturated and A ≠ {∅} then ⨁_{A∈A} ∑_{a∈A} aP_{a} is in hnf; if A is a subset of Act then ∑_{a∈A} aP_{a} Ω is in hnf.

Hence, Ω, (ap bq) ⊕ cr and ap Ω are in hnf but (ap Ω) ⊕ cr and ap aq are not. An important property of terms in hnf is that they have unique a descendants. For example, (ap + bq) ⊕ ar is in hnf if and only if p ≡ r. This property is vital for obtaining finite axiomatisations of ≪. Terms can be put in hnf using system TB and the following derived axioms.

Der1  X ⊕ Ω = X Ω
Der2  X ⊕ (Y Ω) = X Y Ω
Der3  X ⊕ Y = X ⊕ Y ⊕ (X Y)
Der4  X ⊕ (X Y Z) = X ⊕ (X Y) ⊕ (X Y Z)
Der5  (aX Z) ⊕ (aY V) = (a(X ⊕ Y) Z) ⊕ (a(X ⊕ Y) V)

4.1 Axiomatisation Algorithm

This subsection introduces a number of laws or axiom schemas which allow rewriting process terms into hnf. We define an algorithm which uses these laws to generate sound axiomatisations of arbitrary τDeS languages. The usefulness of our algorithm is illustrated by generating axiomatisations of the language B extended with the CSP hiding operator and the CCS parallel composition operator.

We will need to distinguish two subclasses of τDeS operators, namely distinctive [ABV92] and τ-introducing operators [Uli95]. 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 τDeS operator (f, n) is τ-introducing if τ is the action of one of its De Simone rules.

Lemma 4.3 [Uli95] (Action Laws). Let G be a self-encoding τDeS process language. Let (f, n) be a distinctive operator of G with a rule of the form (1). Also assume P_{i} ≡ a_{i}.X′_{i} for i ∈ I and P_{i} ≡ X_{i} otherwise. If α ∈ Act then, for an appropriate P′, we have

TEST(G) f(P) = α.C[P′]  (4)

else (i.e. f is τ-introducing), for some P′, we have

TEST(G) f(P) = C[P′].  (5)

(Inaction Laws). Let (f, n) be an operator of G such 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} ≡ a.X′_{i}, for some a ≠ a_{i}. Then

TEST(G) f(P) = 0.  (6)

(Divergence Laws). Let (f, n) be an operator of G. 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} ≡ a.X′_{i}, for some a ≠ a_{i}. Then

TEST(G) f(P) ⊑ Ω.  (7)

Since we also have Ω ⊑ X (axiom Ω1), for all X, we could substitute (7) by f(P) = Ω.

Proof. The above laws are sound with respect to refusal simulation preorder [Uli95] and since refusal simulation preorder refines ≪ we obtain that the laws are also sound for ≪.

Next, we define the distributivity over ⊕ and laws.

Lemma 4.4 (Distributivity over ⊕ laws). Let G be a self-encoding τDeS process language. Let (f, n) be an operator of G such that its ith argument is active. If X_{i} ≡ X ⊕ Y then

TEST(G) f(X) = f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}].  (8)

It is important to note that ⊕ laws hold, unlike the corresponding laws in [Uli95] and the distributivity over + laws in [ABV92], without the requirement that each rule for f has an antecedent for the ith argument. The proof of Lemma 4.4 can be found in Appendix A.

Notice that by left-to-right application of the derived axiom X Ω = X ⊕ Ω and the instances of distributivity over ⊕ laws a process f(p) with active arguments in hnf can be rewritten as ⨁_{I} f(p_{i}), where all active components of each p_{i} are either Ω or of the form ∑_{A} a.p_{a}, where A ⊆ Act. This suggests that the distributivity over laws need only be given for f(X) with all active arguments of the form ∑_{A} a.X_{a} or Ω. This is, as will be explained later, one of the two reasons why our axiomatisations are finite.

We will use the following notation to express the form of active arguments. Let A be an n-ary vector whose i-th element A_{i} is ∗ if i ∉ active(f) and it is ∗ or A_{i} ⊆ Act otherwise. Then, AX (as in f(AX) below) denotes an n-ary vector of open terms such that its i-th element, written as A_{i}X_{i}, is any term if i ∉ active(f). Otherwise A_{i}X_{i} is Ω if A_{i} = ∗ and ∑_{a_{j}∈A_{i}} a_{j}.X_{ij} if A_{i} ⊆ Act. In the last two cases we will write (A_{i}X_{i})_{j} to denote Ω if A_{i} = ∗ and a_{j}.X_{ij} otherwise. Moreover, given trigger χ we say that χ fires from A (or χ ∈ A) if whenever χ_{i}, the ith element of χ, is not ∗ then A_{i} ≠ ∗ and χ_{i} ∈ A_{i}. Also, let Ω(f(AX)) be true if one of the active arguments of f(AX) is Ω.

Lemma 4.5 (Distributivity over laws) Let (f, n) be an operator of a self-encoding τDeS process language G. Suppose that i is such that each rule for f has an antecedent for X_{i}. Then the following laws are valid in TEST(G):

f(AX) = ∑_{j} f(AX)[(A_{i}X_{i})_{j}/A_{i}X_{i}]
if Ω(f(AX)) ∨
¬Ω(f(AX)) ∧ ∀χ ∈ trig_{τ} (f). χ ∉ A  (9)
f(AX) = ∑_{A_{i}} f(AX)[a_{j}.X_{ij}/A_{i}X_{i}] ⊕ ⨁_{C_{i}⊆A_{i}} f(AX)[c_{j}.X_{ij}/A_{i}X_{i}]
if ¬Ω(f(AX)) ∧ trig_{τ} (f) ≠ ∅ ∧
∃minimal C_{i}, ∀χ ∈ trig_{τ} (f). if χ ∈ A then χ ∈ A[C_{i}/A_{i}]  (10)

Next, we briefly explain the syntactic conditions of the laws. The condition for law (9) says that either one of the active arguments (not necessarily the jth) is Ω or none of the active

Figure 2: Axioms for hiding.

(X ⊕ Y)\a = X \a ⊕ Y \a
(∑_{b∈B} b.X_{b})\a = ∑_{b∈B}(b.X_{b})\a  if a ∉ B
(∑_{b∈B} b.X_{b} a.X)\a = (∑_{b∈B}(b.X_{b})\a (a.X)\a) ⊕ (a.X)\a  if a ∉ B
(b.X)\a = b.(X \a)  if b ≠ a
(a.X)\a = X \a
0\a = 0
Ω\a ⊑ Ω

arguments is Ω and no τ triggers for f can fire from A. The right conjunct of the condition for law (10) says that f is τ-introducing and there exists the minimal (non-empty) C_{i} ⊆ A_{i} such that whenever any τ trigger for f can fire from A then it can fire from A[C_{i}/A_{i}].

The proof of Lemma 4.5 can be found in Appendix A.

Next, consider the extension of B with 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.}

Since \a is distinctive it clearly satisfies the condition in Lemma 4.5. The axioms obtained by Lemmas (4.3)–(4.5) are given in Figure 2. Note that the second axiom does not hold without the side condition. Each of the first two equations is an axiom schema but, as Act is finite, it represents a finite set of axioms—one for each subset B of Act. Hence, the axiomatisation is finite. Similarly, the axiomatisations of other distinctive operators, for example the restriction or renaming of CCS, will also be finite.

The following lemma show how non-distinctive operators can be axiomatised with the help of certain auxiliary distinctive operators.

Lemma 4.6 (Non-distinctive operator laws) Let a non-distinctive (f, n) be an operator of a self-encoding τDeS process language G. Then there is a disjoint extension G′ of G with (possibly zero) n-ary distinctive non-τ-introducing operators f_{k}, where k ∈ K ⊂_{fin} , and (possibly zero) n-ary distinctive τ-introducing operators f^{l}, l ∈ L ⊂_{fin} , such that G′ is a τDeS language and the following laws hold in TEST(G′):

f(AX) = ∑_{K} f_{k}(AX) ∑_{L} f^{l}(AX)
if Ω(f(AX)) ∨
¬Ω(f(AX)) ∧ ∀χ ∈ trig_{τ} (f). χ ∉ A  (11)
f(AX) = (∑_{K} f_{k}(AX) ∑_{L} f^{l}(AX)) ⊕ ⨁_{N} f^{n}(AX)
if ¬Ω(f(AX)) ∧ trig_{τ} (f) ≠ ∅ ∧ ∃N ⊆ L, ∀χ ∈ trig_{τ} (f).
if χ ∈ A then ∃n ∈ N.χ ∈ trig_{τ} (f^{n})  (12)

The condition of (11) is the same as the one for (9). The condition of (12) says that none of the active arguments of f(AX) is Ω, f is τ-introducing and there exists a (non-empty since f is τ-introducing) subset N of L such that whenever a τ trigger for f fires from A then this trigger is a τ trigger for some f^{n}, n ∈ N.

The sketch of proof of Lemma 4.6 can be found in Appendix A.

As an example of axiomatisation of a non-distinctive and τ-introducing operator we consider B extended with the CCS parallel composition operator ∥. Assume that for each a ∈ Act we have ā ∈ Act and ¯ ā = a. By Lemma 4.6, the ∥ operator is axiomatised in terms of three auxiliary operators. These operators might be called the left-merge, written , the rightmerge, written , and the communication merge, written |, since they are very similar to the same named original operators discussed in [BK84, BK85, BW90, ABV92]. They are defined by the following De Simone rules together with the associated τ-rules which are not shown. Note that, unlike their original versions, these operators are τDeS.

{X →^{a} X′ \atop X Y →^{a} X′ ∥ Y}  {Y →^{a} Y′ \atop X Y →^{a} X ∥ Y′}  {X →^{a} X′ Y →^{ā} Y′ \atop X |Y →^{τ} X′ ∥ Y′}

As before AX and BY stand for ∑_{a∈A} aX_{a} and ∑_{b∈B} bX_{b} respectively, where A, B ≠ ∅. The axioms for ∥ and the auxiliary operators obtained by applying Lemmas (4.3)–(4.6) are given in Figure 4. For the same reason as with hiding the axiomatisation of the CCS parallel is finite.

We can remove some redundancy among the axioms in Figure 4 by adding, for example, valid and derivable (from the axioms generated by our method) reflexivity axioms for ∥ and | and for closed terms. Such an addition would make the second, the fourth and five other easily identifiable axioms redundant. However, it can be shown employing a similar argument as in [ABV94] that the reflexivity axioms for ∥ and | and for open terms are not in general derivable from the axioms generated by our method.

Next, in Figure 3 we present algorithm A which generates a sound axiom system for ≪ and an arbitrary τDeS process language. Moreover, the axiom system generated by A is head normalising for initially τ-convergent processes in the considered language.

Theorem 4.7 (Soundness) 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 TEST(G′) T.

Proof. TEST(G′) T follows from Lemmas (4.3)–(4.6).

4.2 Finiteness and Head Normalisation

In this subsection we argue that the axiomatisations produced by algorithm A are finite. Moreover, they are head normalising for initially τ-convergent processes.

Theorem 4.8 (Finiteness) Axiom systems produced by A are finite.

Proof. Given a τDeS process language G with the set of visible actions A the following are true about the resulting language G′ and the axiomatisation T produced by algorithm A.

1. Since G has finitely many operators there are only finitely many instances of law (8) in T.

Input: τDeS language G with the set of visible actions A.

1. If G is not self-encoding then add disjointly to G a copy of B(A). Call the result G′′.

2. For each operator f ∉ Σ_{B(A)} in G′′ add to T_{B(A)} all the instances of the distributivity over ⊕ laws (8) and call the resulting system T′′.

3. For each non-distinctive operator f ∉ Σ_{B(A)} in G′′ apply the construction of Lemma 4.6 to obtain the language G′. Add to T′′ all the resulting instances of axioms (11)–(12) and call the resulting system T′.

4. For each distinctive operator f ∉ Σ_{B(A)} in G′ add to T′ the following axioms: an action law (4) or (5) for each rule for f; all the inaction laws (6); all the divergence laws (7); for each active argument of f the distributivity over laws (9)–(10). Call the resulting system T.

Output: τDeS language G′ such that G < G′ and the axiom system T such that TEST(G′) T.

Figure 3: Axiomatisation algorithm A.

2. G can only have finitely many non-distinctive operators. Since each τDeS operator has only finitely many defining rules there will only be finitely many auxiliary distinctive operators required by Lemma 4.6. Thus, G′ has a finite number of distinctive operators.

3. It is clear, from the remarks in point 2 above, that laws (4)–(7) give rise to finitely many instances for each distinctive operator in G′.

4. There are only finitely many different instances of laws (9) and (10) in T, up to a change of variable names. This is because there is only a finite number of different A we can use in f(AX): for A_{i} is either ∗ or Ω or one of the finitely many subsets of finite A.

5. For the same reason as for laws (9) and (10), each of laws (11) and (12) contributes a finite set of instances to T.

Since T consists of a finite T_{B(A)} and the sets of all instances of laws (4)–(12), each of them finite, we conclude that T is finite.

In the next subsection we will argue that the axiomatisations produced by algorithm A are not only finite but also complete for well-founded τDeS languages. Since B_{∥}, the basic language B extended with the CCS parallel composition operator, is well-founded the axiomatisation of testing preorder over B_{∥} is both finite and complete, and so is the axiomatisation of B extended with the hiding operator.

The next theorem is essential in proving completeness of the generated axiomatisations.

Theorem 4.9 (Head Normalisation) 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 T is head normalising for all initially τ-convergent processes in T(Σ_{G′}).

Proof. We will prove by induction the following property denoted by (⋆):

if p ∈ T(Σ_{G′}) and p is initially τ-convergent then there exists q ∈ T(Σ_{G′}) such that q is in hnf and T ⊢ p = q.

The induction is on d_{ε}(p) which is defined as follows. Firstly, we define a function d : T(Σ) → which specifies the depth of operator names in ground terms over some signature Σ. Function d is defined inductively as follows: d(t) = 0 if t is a constant, and d(g(t_{1}, …, t_{r})) = 1 + max{d(t_{i}) | 1 ≤ i ≤ r}. Function d_{ε} is defined only for initially τ-convergent processes. It specifies the maximal operator depth of ε-descendants of processes: for τ-convergent p we define d_{ε}(p) as max{d(p′) | p ⇒^{ε} p′}.

In the base case and the inductive step we will demonstrate how to rewrite initially τconvergent process terms into terms with a certain form by using laws (4)–(12) and some of the axioms and derived axioms for B. The mentioned form is called sum of prefixed terms form, sptf for short, and it is defined inductively as follows. A term p is in sptf if

• p ≡ 0, p ≡ Ω or p ≡ a.r, for some action a and term r,

• p ≡ p′ p′′ or p ≡ p′ ⊕ p′′, for p′ and p′′ in sptf.

It is routine to prove, using the rewriting techniques developed in [NH84, Hen88], that terms in sptf can be transformed into terms in hnf.

We begin with the base case. Assume that p is initially τ-convergent Σ_{G′} process and d_{ε}(p) = 0. This means that p is a constant and for each p′ such that p ⇒^{ε} p′ p′ is a constant too. We transform p into sptf by repeatedly performing the following steps:

1. If p is distinctive, which means that there is at most one defining rule for p, then p can be rewritten using action or inaction laws.

2. If p is not distinctive then it can be rewritten using law (11) or law (12). The resulting term will contain only distinctive constants and each of them will be rewritten using action and inaction laws if required.

It may happen that after performing steps 1 and 2 the resulting term t is in sptf, then we are finished. If t is not in sptf (this will happen when p is τ-introducing) we rewrite each of the constants in t, which is not prefixed by an action and it is neither 0 nor Ω, according to steps 1 and 2 above. We continue the transformation of the resulting term as long as it contains other than 0 and Ω constants which are not prefixed with actions. In the transformation we use the above steps 1 and 2. Notice that each τ transition of a constant corresponds to the rewriting by action law (5) or by law (12) together with (5). Since p is initially τ-convergent the transformation will eventually terminate with the resulting process term in sptf. Finally, the axioms and the derived axioms for B can be used to rewrite it into hnf.

Next, we assume that the property (⋆) holds for all q such that d_{ε}(q) ≤ n and show that it also holds for any p with d_{ε}(p) = n + 1. As in the base case it is enough to show how to rewrite p into sptf. Since p is not necessarily a constant the steps corresponding to 1 and 2 above are more complicated. They are as follows:

1′. If the operator of p is distinctive and moreover p is a constant then rewrite it using action and inaction laws if required. However, if p ≡ f(p) then since d_{ε}(p_{i}) ≤ n, for each p_{i} of p, the term p_{i} can be put into hnf p′_{i} by inductive hypothesis. Thus, we continue with f(p′).

(a) If any active argument of f(p′) has the form r Ω, for r other than 0, then each such argument is rewritten as r ⊕ Ω by the derived axiom Der1. As the result we obtain f(p′′), where each active argument p′′_{i} has one of the following forms: Ω, 0, ⨁_{K≠∅} p′′_{ik} or p′′_{ik} ⊕ Ω, where p′′_{ik} is an external choice of terms prefixed with actions. If p′′_{i} is not active then it equals p′_{i}.

(b) If any of the active arguments of f(p′′) have the form of an internal sum then we repeatedly use law (8) from left to right to rewrite f(p′′). As the result we obtain ⨁_{M} f(p′′_{m}), where each active argument of each f(p′′_{m}) has one of the forms Ω, 0 or ∑_{I≠∅} a_{i}.r_{i}, for some actions a_{i} and terms r_{i}. Remark. Note that Lemmas (4.5)–(4.6) give the distributivity laws for terms f(AX) with active arguments of the form: Ω, 0 or ∑_{I≠∅} a_{i}.r_{i}.

(c) If any of the active arguments of any f(p′′_{m}) have the form of an external sum then use the distributivity over laws for such arguments of all such f(p′′_{m}). The resulting term will be a sum (external and/or internal) of terms f(p′′′_{n}), where each active argument is either Ω, 0 or a_{ni}.r_{ni}, for some a_{ni} and r_{ni}. Finally, rewrite each of the subterms f(p′′′_{n}) using action, inaction and divergence laws as appropriate.

2′. If the operator of p is not distinctive then p can be rewritten using law (11) or law (12). The resulting term will be a sum (external and/or internal) of terms with outermost operators being distinctive. Each of these terms will be rewritten as in step 1′.

At this stage the resulting term is almost in sptf—it is a sum (external and/or internal) of terms of the following form: Ω, 0, a_{ni}.r_{ni} or g(r), where g is neither the action prefixing operator, the internal choice nor the external choice. The last form of term appears when f is τ-introducing and there is a De Simone rule for f with the consequent f(X) →^{τ} g(Y ) and a ground substitution ρ such that ρ(f(X) →^{τ} g(Y )) ≡ f(p) →^{τ} g(r). Since d_{ε}(g(r)) can be n + 1 we cannot use the inductive hypothesis to rewrite it to hnf.

If after rewriting p according to steps 1′ and 2′ the resulting term is not in sptf yet then we continue to apply steps 1′ and 2′ to all subterms g(r) (as described in the previous paragraph) and all the resulting from them similar subterms. Since p is initially τ-convergent the rewriting of p will eventually terminate with the resulting process term in sptf. As in the base case, the axioms and the derived axioms for B can be used to rewrite it into hnf.

4.3 Completeness

Given any τDeS process language G with the set of visible actions A algorithm A produces axiom system T which allows conversion of initially τ-convergent processes into head normal form. For well-founded processes this implies completeness of T: it is possible to rewrite arbitrary process terms over G into terms over B(A) by applying the reduction to head normal form a finite number of times. However, in order to obtain completeness for (some) process terms representing infinite behaviours we need to augment T with some (infinitary) induction rule. These two ways of achieving completeness are described below.

We start with the completeness result for well-founded processes. Its proof together with a number of auxiliary results appears in Appendix B.

Theorem 4.10 Let G be a well-founded self-encoding τDeS process language. Let G′ and T denote the disjoint extension and the axiom system produced by the algorithm in Figure 3 respectively. Then for all p, q ∈ T(Σ_{G′}) if Test(G′) p ⊑ q then T ⊢ p ⊑ q.

Although well-foundedness of τDeS process languages has been defined semantically (Definition 2.5) it can also be characterised in a syntactical manner. We follow the approach developed in [ABV94]. There, syntactical well-foundedness of GSOS languages is introduced (Definition 6.6) in terms of a certain weight function, if it exists. The authors prove that syntactically well-founded and linear GSOS languages are well-founded. Also, they argue that although (semantic) well-foundedness is not in general decidable syntactic well-foundedness is. Since τDeS languages are a subclass of linear GSOS languages every syntactically wellfounded τDeS language is well-founded. However, as noticed in [ABV94], not all well-founded GSOS (and thus τDeS) languages are syntactically well-founded.

Axiomatisations of process languages with terms representing non-finite behaviour require some form of induction rule in order to obtain completeness. For example, a version of AIP is used in [ABV92, ABV94] to achieve completeness for arbitrary GSOS languages. A version of ω-Induction is suggested in [Uli95] as the induction rule needed for completeness of axiomatisations of refusal simulation preorder and τDeS process languages. A similar from of ω-Induction rule is employed here. Our rule is based on the ω-Induction rule as discussed in [NH84, Hen88]. It represents a principle that if two processes are testing related at all finite depths then they are testing related.

X/b^{n}Ω ⊑ Y all n

(ω-Induction)

X ⊑ Y

The notation b^{n}Ω denotes b … b.Ω, where b appears n times. A binary infix operator /, taken from [ABV92, ABV94], is defined by the following rule

{X →^{a} X′ Y →^{b} Y′ \atop X/Y →^{a} X/Y′}

together with the associated τ-rules. Since / is defined by a single De Simone rule it is distinctive. Moreover, it is not τ-introducing. Hence, using our axiomatisation method we obtain the following intuitive axioms for /, where AX and BY stand for ∑_{A} a.X_{a} and ∑_{B} b.Y_{b} respectively with A, B ≠ ∅.

\begin{aligned}(X ⊕ Y)/Z & = & X/Z ⊕ Y/Z \\ X/(Y ⊕ Z) & = & X/Y ⊕ X/Z \\ (∑_{A} a.X_{a})/BY & = & ∑_{A}(a.X_{a}/BY) \\ AX/(∑_{B} b.Y_{b}) & = & ∑_{B}(AX/b.Y_{b}) \\ a.X/b.Y & = & a.(X/Y) \\ 0/X & = & 0 \\ X/0 & = & 0 \\ Ω/X & ⊑ & Ω \\ X/Ω & ⊑ & Ω \end{aligned}

We let G_{/} denote the disjoint extension of a τDeS language G with the operator /. The soundness of ω-Induction and some useful properties of / are proved in Appendix B.

Finally, we have the soundness and completeness result for τ-convergent but not necessarily well-founded τDeS processes.

Theorem 4.11 Given τDeS language G let G′ and T denote the disjoint extension of G_{/} and the axiom system respectively produced by the algorithm in Figure 3. Then, for all τ-convergent p, q ∈ T(Σ_{G′}), Test(G′) p ⊑ q if and only if T, ω-Induction ⊢ p ⊑ q.

The proof for Theorem 4.11 can be found in Appendix B.

Our ω-Induction rule is very strong and in many cases (for example, the systems to be discussed in the next section) a weaker rule would be sufficient, for example the Recursive Specification Principle (RSP) defined in [BK88, BW90] and used in [Mil84, Mil89b, vG93, Ace94].

It is expected that for a suitably defined class of regular τDeS languages the techniques described in [Mil84, Mil89b, Ace94], which do not rely on infinitary rules, would be applicable. Moreover, weaker but effective induction rules, for example Scott Induction as discussed in [Hen88], may be sufficient for some interesting subclasses of τDeS languages. This will be considered elsewhere.

5 Applications

We argue that τDeS languages and their automatically generated axiomatisations can make the task of specification and verification of concurrent systems easier and more intuitive. Freedom to use arbitrary τDeS operators allows one to write intuitive and clear specifications without worrying about the implementation. It is advisable, in the specification process, to write a series of specifications of increasing concreteness. Ideally, the most concrete specification would suggest a good method of implementation. We prove that the more concrete specifications refine the less concrete ones. The proofs are done within the axiom systems as introduced in the last section.

The common theme in our examples is the control and scheduling of the execution of several systems acting in parallel. The situations we describe are:

• interruption or abortion, suspension and resumption of a system by its own or other system’s actions;

• alternate execution of two systems, where the control of execution is passed between the systems by ‘seizing’ and ‘releasing’ actions.

Example 5.1 Consider a system which repeatedly performs a until action s takes place, after which it performs repeatedly b until the next occurrence of s, after which the system behaves as originally. The abstract way to specify this system is by listing its states and describing the transitions between them. The system has two states which we represent by nullary τDeS operators S_{1} and S′_{1}. The operational meaning of S_{1} and S′_{1} is defined by the following rules:

S_{1} →^{a} S_{1}  S_{1} →^{s} S′_{1}  S′_{1} →^{b} S′_{1}  S′_{1} →^{s} S_{1}

Note that S_{1} (and S′_{1}) is non-distinctive: it fails the second part of the distinctiveness definition because it has two rules with the same (i.e. none) antecedents. The axiomatisation for S_{1} and S′_{1} produced by A gives a more familiar description of S_{1} and S′_{1}:

S_{1} = a.S_{1} s.S′_{1}  and  S′_{1} = b.S′_{1} s.S_{1}

How can this system be constructed? One way is to take two subsystems specified by P and Q, with P = a.P s.P and Q = b.Q s.Q, and combine them by means of the operator ≫ defined as follows, where α ∈ {a, b, τ}:

{X →^{α} X′ \atop X ≫ Y →^{α} X′ ≫ Y}  {Y →^{s} Y′ \atop X ≫ Y →^{s} Y′ ≫ X}  {Y →^{τ} Y′ \atop X ≫ Y →^{τ} X ≫ Y′}

Note that the process P in P ≫ Q executes freely until it is suspended by Q, then the process Q in Q ≫ P proceeds freely until P restarts itself (or suspends Q).

It is easy to derive axioms for ≫ and prove that P ≫ Q = a.(P ≫ Q) s.(Q ≫ P) and Q ≫ P = b.(Q ≫ P) s.(P ≫ Q). Thus, by ω-Induction, we obtain S_{1} = P ≫ Q and S′_{1} = Q ≫ P. Thus, we conclude that P ≫ Q is a more concrete version of S_{1}.

Example 5.2 Imagine a multi-media player which offers an interactive video performance. The viewer can start the performance, view the offered items, suspend and resume the performance by using the pause function and choose one of two alternatives. The viewer controls the player by a remote control, which has the buttons start (to start or restart the performance), pause, and the buttons 1 and 2 for making a choice. As in the previous example, we could represent the states of the system by the nullary operators, define the transitions between these states by certain rules and then derive the equation(s) describing their specification. But, we omit the details and just give the specifications. Let M and RC represent the multi-media player and the remote control systems respectively. M and RC are such that

M = s.M′
M′ = c_{1}.(c_{2}.M′′ M) M
M′′ = choice.(one.m_{1} two.m_{2} M) M
RC = start.s.r.RC pause.pause.RC
1.one.r.RC 2.two.r.RC

where s is the signal RC sends to M to start the performance afresh; c_{1}, c_{2} and m_{1}, m_{2} are commercials and movies respectively; one and two are the signals by which RC instructs M of the viewers’ choice and r is the actions by which RC returns the control to M.

M and RC make up the subsystem P with the intended behavior described as follows:

P = start.s.r.P′ pause.pause.P
P′ = c_{1}.(c_{2}.P′′ P) P
P′′ = choice.(1.one.r.m_{1} 2.two.r.m_{2} P) P

The whole system S consists of the viewer V together with M and RC . The concrete specification of the system is V ∥_{D}op(M, RC ), where D consists of start, c_{1}, c_{2}, choice, 1, 2, pause, m_{1}, m_{2} and ∥_{D} is a CSP-like parallel composition operator with synchronisation on all action in D. Instead of defining the specific op we will use a general operator A⟩B⟩C called the controlled parallel composition, which has three parameters A, B, C ⊂ Act such that (A ∪ C) ∩ B = ∅. The defining rules for the operator are given below. It binds weaker than the prefixing. but stronger than the choice operators.

\begin{matrix}X →^{a} X′ ; a ∉ A ; X A⟩B⟩C Y →^{a} X′ A⟩B⟩C Y & X →^{a} X′ ; a ∈ A ; X A⟩B⟩C Y →^{a} Y A⟩B⟩C X′ \\ X →^{b} X′ Y →^{b} Y′ ; b ∈ B ; X A⟩B⟩C Y →^{b} X′ A⟩B⟩C Y′ & Y →^{c} Y′ ; c ∈ C ; X A⟩B⟩C Y →^{c} Y′ A⟩B⟩C X \\ {X →^{τ} X′ \atop X A⟩B⟩C Y →^{τ} X′ A⟩B⟩C Y} & {Y →^{τ} Y′ \atop X A⟩B⟩C Y →^{τ} X A⟩B⟩C Y′} \end{matrix}

Next, we briefly explain these rules. In P A⟩B⟩C Q the control of execution is with the first argument: see the first rule. The parameter A contains the actions by which the first argument transfers the control to the second argument: the second rule. The parameter B contains the actions on which both the arguments must synchronize: the third rule. The parameter C consists of all actions by which the second argument takes over the control from the first one: the fourth rule. Finally, the last two rules are the associated τ-rules.

The set of axioms for A⟩B⟩Ccan be easily derived using algorithm A. Similarly as for the CCS parallel operator the axiomatisation of A⟩B⟩C uses three auxiliary operators. Using the derived axioms it is routine to show the following, for A = {choice, pause, r}, B = {s, one, two} and C = {start, pause, r}.

M A⟩B⟩C RC = start.s.r.(M′ A⟩B⟩C RC ) pause.pause.(M A⟩B⟩C RC )
M′ A⟩B⟩C RC = c_{1}.(c_{2}.(M′′ A⟩B⟩C RC ) M A⟩B⟩C RC ) M A⟩B⟩C RC
M′′ A⟩B⟩C RC = choice.(1.one.r.m_{1} 2.two.r.m_{2} M A⟩B⟩C RC ) M A⟩B⟩C RC

Finally, applying ω-Induction rule we prove P = M A⟩B⟩C RC .

6 Conclusions and Related Work

The De Simone format was introduced in [dS85] as a format which preserves strong bisimulation. However, when weak equivalences are considered the generality of the original De Simone rules permits to define some undesirable operators, namely those which do not preserve the considered equivalences. In order to correct this, one usually imposes various restrictions on the form of De Simone rules and uses τ-rules as, for example, in [Blo90b, Vaa91, Uli92, Blo95a, Uli94]. The τDeS format is a subformat of the ISOS format [Uli92, Uli94]. The ISOS rules may have negative antecedents and copying in the target of the consequent.

Regarding the congruence theorem, most of our proofs are based on the proofs in [Hen88] although neither De Simone nor other generally defined classes of process languages are considered there. The only directly related result is due to Vaandrager who argues in [Vaa91] that testing preorder, in the setting without divergence, is a precongruence for any language in a class of languages similar to τDeS^{2}.

The idea of generating axiomatisations of arbitrary process languages from their operational specifications (given by SOS rules) is due to Aceto, Bloom and Vaandrager [ABV92, ABV94]. They defined two procedures for obtaining axiomatisations of strong bisimulation for arbitrary GSOS languages. Such axiomatisations are finite for well-founded languages. The finiteness is achieved by extending the considered language with useful, and indeed required [Mol90], auxiliary operators. This approach is a generalisation of the method originally used by Bergstra and Klop in [BK84, BK85], where interleaving parallel composition (no communication) operator is finitely axiomatised with the help of auxiliary left-merge operator. Aceto [Ace94] proposed an extension of the algorithm from [ABV92] which generates finite axiomatisations of strong bisimulation for regular GSOS languages, i.e. languages in which certain infinite behaviours can be represented. However, if one tries to adapt the procedures from [ABV92, ABV94] to any of weak equivalences one finds that the introduced auxiliary operators do not preserve many of weak equivalences. In [Blo95a] this difficulty is overcome by considering rooted versions of weak equivalences and further restricting the (GSOS) format of rules. An alternative approach is presented in [Uli95], where a general procedure is defined for deriving axiomatisations of refusal simulation preorder and coarser (weak) preorders. The auxiliary operators introduced by the procedure in [Uli95] preserve the considered weak preorders and equivalences.

2Vaandrager allows silent actions in the antecedents of De Simone rules, provides an extra “idling” axiom and, separately, provides recursion.

The procedure from [Uli95] can be adjusted, by adding a number of extra axioms, to produce axiomatisations of testing preorder. But, the procedure presented in this paper has two important advantages over the adjusted procedure:

• it uses only nine laws instead of twenty of the adjusted procedure,

• it always gives finite axiomatisations for well-founded processes.

One of the motivations for theories concerning classes of process languages, which are defined by formats of SOS rules, is to facilitate the task of specification. However, except for some simple examples where new operators were used to make the specification easier [BIM88, BIM95, GV90, Gro90, Uli94] this theme has not been studied in detail. A recent exception is the work by Bloom [Blo95b], where the author gives several specifications of the job protecting an arbitrary server by a checkpoint/backup scheme. As for the verification method both the equational reasoning and process equivalence techniques are used.

Acknowledgements

The pioneering work of Luca Aceto, Bard Bloom and Frits Vaandrager [ABV92, ABV94] was the inspiration for the present (and the previous [Uli95]) work on axiom generation for weak process preorders, for which I am greatly indebted to them. I would like to thank the referees and the participants of AMAST ’96 for their helpful comments and suggestions. Thanks are also due to Paul Taylor for his LaTEX macros.

A Soundness of Head Normalising Laws

This appendix contains soundness proofs of the distributivity over and ⊕ laws and the non-distinctive operator laws.

Proof of Lemma 4.4. Let X_{i} ≡ X ⊕ Y. We need to show ρ(f(X) ≃ ρ(f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}]), for any closed substitution ρ over G′ with G ≤ G′. We will only show ρ(f(X) ≪ ρ(f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}]) as the converse is proved similarly. By Theorem 2.13 it is enough to prove

ρ(f(X)) ≪may ρ(f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}])

and

ρ(f(X)) ≪must ρ(f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}]).

For ≪may case let ρ(f(X) ⇒^{s}, where s is a non-empty sequence of visible actions over G′, and assume that s is the sequence α_{1} … α_{n} with all τ removed. Thus,

(ρ(f(X) ≡)ρ(C_{0}[X_{0}]) →^{α_{1}} ρ(C_{1}[X_{1}]) … →^{α_{n}} ρ(C_{n}[X_{n}])

for some n-ary contexts C_{i}[X_{i}]. We need to consider two cases depending on whether or not the computation of the above sequence depends on the value of the i-th argument. If it does not then it is clear that ρ(f(X)[X/X_{i}]) ⇒^{s} as well as ρ(f(X)[Y/X_{i}]) ⇒^{s}, and we are finished. Otherwise, let 1 ≤ k ≤ n be the smallest k such that ρ(C_{k}[X_{k}]) →^{α_{k+1}} ρ(C_{k+1}[X_{k+1}]) depends on the behaviour of ρ(X_{i}). Since ρ(X_{i}) is ρ(X)⊕ρ(Y) we deduce, by the Ruloid Theorem, that in fact α_{k+1} = τ and ρ(C_{k+1}[X_{k+1}]) equals ρ(C_{k}[X][X/X_{i}]) or ρ(C_{k}[X][Y/X_{i}]). Depending on which of the last two terms it is, we obtain either ρ(f(X)[X/X_{i}]) ⇒^{s} or ρ(f(X)[Y/X_{i}]) ⇒^{s} as required.

For ≪must case assume ρ(f(X)) ⇒^{s}, for s as above, and ρ(f(X))⇓s. We need to show (a) (ρ(f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}])⇓s and (b) for any open term T if (ρ(f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}]) ⇒^{s} T then ρ(f(X)) ⇒^{s} T′ and S(T′) ⊆ S(T), for some open term T′. As X_{i} ≡ X ⊕ Y we obtain, by the definition of the convergence predicate, ρ(f(X)) ⇒^{ε} ρ(f(X)[X/X_{i}]) and ρ(f(X)[X/X_{i}])⇓s. Similarly, we get ρ(f(X)[Y/X_{i}])⇓s. Hence, putting these together we obtain (ρ(f(X)[X/X_{i}] ⊕ f(X)[Y/X_{i}])⇓s as required. For part (b) we show, using a similar argument as for ≪may part of this proof, that for each T we have T ≡ T′ and thus S(T′) ⊆ S(T).

In the proof of Lemma 4.5 and Lemma 4.6 the following result, based on Lemma 4.1.3 in [NH84], will be helpful.

Result A.1 If D(p, μ) = D(q, μ), for every μ ∈ Act∪{ε}, then p ≃may q. If D(p, μ) = D(p, μ), for every μ ∈ Act ∪ {ε}, and p↓ if and only if q↓ then p ≃ q.

Proof of law (9) of Lemma 4.5. We need to show

ρ(f(AX)) ≃ ρ(∑_{j} f(AX)[(A_{i}X_{i})_{j}/A_{i}X_{i}])

provided that the condition of law (9) holds for any closed substitution ρ over any disjoint extension of G. The condition requires us to check two cases. In what follows we will use lhs and rhs to stand for the left and the right hand sides of the above expression respectively.

Firstly, we assume that the second disjunct of the condition holds: no active argument of f(AX) is Ω and ρ(f(AX)) ^{τ} , for all ρ. Thus, (A_{i}X_{i})_{j} ≡ ∑_{A_{i}} a_{j}X_{ij}. Clearly, by Definition 2.3, lhs↓ and rhs↓. Thus, by Result A.1, we only need to show D(lhs, μ) = D(rhs, μ). We notice that f(AX) cannot perform τ because f is not τ-producing and no τ-rule can be applied (due to the structure of the active arguments). We will show that lhs →^{a} t if and only if rhs →^{a} t, for all closed terms t and visible actions a. Assume ρ(f(AX)) →^{a} t. This means that there is a De Simone rule r

{\{ X_{k} →^{a_{k}} X′_{k} \}_{k∈K} \atop f(X) →^{a} C[Y ],}

where Y_{k} = X′_{k} if k ∈ K and Y_{k} = X_{k} otherwise, such that ρ(C[Y ]) = t and ρ(X_{k}) →^{a_{k}} ρ(X′_{k}) are valid transitions, for all k. Note that since each rule for f has an antecedent for i we have i ∈ K. Hence, ρ(A_{i}X_{i}) →^{a_{i}} ρ(X′_{i}), so a_{i} ∈ A_{i} and ρ(a_{i}.X_{ij}) →^{a_{i}} ρ(X_{ij}). This implies that the ith component of Y is X′_{i} = X_{ij}. Next, we notice that rule r can be applied to derive

ρ(f(AX)[a_{i}.X_{ij}/A_{i}X_{i}]) →^{a} ρ(C[Y′]). Moreover, Y′ = Y . Thus, ρ(f(AX)[a_{i}.X_{ij}/A_{i}X_{i}]) →^{a} t

and so rhs →^{a} t. The converse, rhs →^{a} t implies lhs →^{a} t follows similarly.

Secondly, assume that the other half of the condition holds, namely Ω(f(AX)). We deduce, by Definition 2.3, lhs↑ and rhs↑. This implies lhs ≃must rhs and we only need to show lhs ≃may rhs, i.e. L(lhs) = L(rhs). By the same argument as above we can show that lhs →^{a} t implies rhs →^{a} t, for all closed terms t and visible actions a. So, if we could prove that for every t such that lhs →^{τ} t there is t′ such that rhs →^{τ} t′ and L(t) ⊆ L(t′) then we would have proved a part of our goal: L(lhs) ⊆ L(rhs).

Let lhs →^{τ} t. Since every rule for f has an antecedent for X_{i} we can assume that the antecedent used to derive lhs →^{τ} t is X_{i} →^{a_{i}} X′_{i}. Because rhs is an external sum (choice) of terms the silent move of one the summands will not resolve the choice. We easily see that rhs →^{τ} t ρ(∑_{A_{i}\{a_{i}}} f(AX)[a_{j}.X_{ij}/A_{i}X_{i}]). By denoting the target of the last transition as t′ we deduce that L(t) ⊆ L(t′) as required.

Finally, in order to obtain L(rhs) ⊆ L(lhs) it is enough to prove

L(ρ(f(AX)[a_{j}.X_{ij}/A_{i}X_{i}])) ⊆ L(ρ(f(AX))

for each a_{j} ∈ A_{i}. This follows using a similar argument as in the first case.

Proof of law (10) of Lemma 4.5. Let ¬Ω(f(AX)) and let f be τ-introducing. Assume there exists the minimal (non-empty) C_{i} ⊆ A_{i} such that whenever any τ trigger for f can fire from A then it can fire from A[C_{i}/A_{i}]. We need to show

ρ(f(AX)) ≃ ρ(∑_{A_{i}} f(AX)[a_{j}.X_{ij}/A_{i}X_{i}] ⊕ ⨁_{C_{i}⊆A_{i}} f(AX)[c_{j}.X_{ij}/A_{i}X_{i}])

for any closed substitution ρ over any disjoint extension of G. As before we will use lhs and rhs to abbreviate the left and the right hand sides of the above expression.

We can prove, using a similar argument as for law (9), D(lhs, a) = D(rhs, a) for all relevant visible actions a. Thus, L(lhs) = L(rhs) and so lhs ≃may rhs. Next, we prove lhs ≪must rhs. The converse follows similarly. Assume lhs⇓s, for some sequence s. If s = ε then t⇓s for every t such that lhs →^{τ} t. Also, notice that {t′ | ρ(∑_{A_{i}} f(AX)[a_{j}.X_{ij}/A_{i}X_{i}]) →^{τ} t′} is a subset of {t | lhs →^{τ} t}. Moreover, every t′ such that ρ(f(AX)[c_{j}.X_{ij}/A_{i}X_{i}]) →^{τ} t′ is also a member of {t | lhs →^{τ} t}. Thus, rhs⇓ε. If s ≠ ε then we deduce rhs⇓s from D(lhs, a) = D(rhs, a), for all a, and lhs⇓s.

Next, assume also rhs ⇒^{s} q. If s ≠ ε then, by the above remarks about transitions of lhs and rhs, we obtain lhs ⇒^{s} p, p ≡ q and so S(p) ⊆ S(q). If s = ε then we have a number of cases:

1. q ≡ ρ(∑_{A_{i}} f(AX)[a_{j}.X_{ij}/A_{i}X_{i}]),

2. ρ(∑_{A_{i}} f(AX)[a_{j}.X_{ij}/A_{i}X_{i}]) →^{τ} q′ ⇒^{ε} q, for some q′,

3. q ≡ ρ(⨁_{C_{i}⊆A_{i}} f(AX)[c_{j}.X_{ij}/A_{i}X_{i}]),

4. ρ(⨁_{C_{i}⊆A_{i}} f(AX)[c_{j}.X_{ij}/A_{i}X_{i}]) →^{τ} q′ ⇒^{ε} q, for some q′.

In case (1) we have lhs ⇒^{ε} lhs and S(lhs) ⊆ S(q). In case (2) we notice that, because silent moves do not resolve external choice, q is like ρ(∑_{A_{i}} f(AX)[a_{j}.X_{ij}/A_{i}X_{i}]) except that at least one of its summands is replaced by a term to which it (the summand) evolves by performing at least one action τ. Let q^{∗} be such that ρ(f(AX)[a_{k}.X_{ik}/A_{i}X_{i}]) →^{τ} q^{∗}, for some a_{k} ∈ A_{i}. Since lhs →^{τ} q^{∗} we have S(lhs) ⊆ S(q). In case (3) we consider any p such that lhs →^{τ} p. Since q →^{τ}→^{τ} p we have S(p) ⊆ S(q). In the last case let a_{k} be such that f(AX)[c_{k}.X_{ik}/A_{i}X_{i}]) →^{τ} q′. Hence, lhs →^{τ} q′ and so there exists p(≡ q) such that lhs ⇒^{ε} p and S(p) ⊆ S(q).

Now, we are only left with a sketch of proof of Lemma 4.6.

Proof of Lemma 4.6. Firstly, we show how to construct the disjoint extension G′ of G required by the lemma. After removing all τ-rules from R, the set of rules for G, we divide the resulting set into R_{a}, the set of all non-τ-introducing rules, and R_{τ}, the set of all τ-introducing rules. Next, we split R_{a} and R_{τ} into R_{a1}, …, R_{an} and R_{τ1}, …, R_{τm} respectively in such a way that for any two rules r and r′ in R_{a} (R_{τ}) we have r, r′ ∈ R_{ai} (R_{τj}) whenever r and r′ have the same active arguments. Each of the resulting sets contains rules which, together with the associated τ-rules, define an operator which satisfies the first requirement of the distinctiveness (for each active argument either all or none of the rules test it). However, it may happen that in some set there are different rules but with the same trigger. Hence, we split further each of R_{ai} and R_{τj} into R_{ai1}, …, R_{ain(i)} and R_{τj1}, …, R_{τjm(j)} respectively in a way that none of the created sets has such rules. Now, it is clear that each of the new sets, together with the associated τ-rules, defines a distinctive operator. Next, we change the name of the operator in each of the rules in the sets R_{a11}, …, R_{a1n(1)}, …, R_{an1}, …, R_{ann(n)} to f_{1}, …, f_{k} respectively, for some k ∈ . It is easily checked that each f_{i} is distinctive and non-τ-introducing. We also change the name of operator in each of the rules in R_{τ11}, …, R_{τ1m(1)}, …, R_{τm1}, …, R_{τmm(m)} to g_{1}, …, g_{l} respectively, for some l ∈ . It can be shown that each g_{l} is distinctive and τintroducing. The signature of G′ is defined by Σ_{G′} = Σ_{G} ∪{(f_{i}, n) | i ∈ K}∪{(g_{j}, n) | j ∈ L}, where K = {1, …, k} and J = {1, …, l}. The set of rules for G′ is obtained by extending the set of rule for G with R_{ai1}, …, R_{ain(i)}, for all appropriate i, then with R_{τj1}, …, R_{τjm(j)}, for all appropriate j, and finally with all the τ-rules associated with the operators in Σ_{G′}. We easily check that G′ is a disjoint extension of G.

Finally, laws (11) and (12) are proved sound in a similar fashion as laws (9) and (10) respectively by a case analysis based on the conditions of the laws. This is possible since the conditions of the corresponding laws are identical or very similar.

B Completeness Proofs

Lemma B.1 Well-founded τDeS process languages are finitely branching.

Proof. Well-foundedness of a τDeS language and the fact that the basic transition system generated by the language is finitely branching [BIM88, BIM95] imply that the relevant derived transition system, and thus the language itself, is also finitely branching.

We will show that, given any well-founded self-encoding τDeS process language G, the disjoint extension G′ of G produced by the algorithm in Figure 3 is also well-founded. The following lemma will be useful.

Lemma B.2 Let G be a τDeS language with the set of visible actions A such that B(A) ≤ G. Assume that T, a theory that extends the axiom system for B(A), is head normalising and that Test(G) T. Then, for each well-founded Σ_{G} term p there exists a Σ_{B(A)} term q such that T ⊢ p = q.

Proof. We use induction on the action depth of process terms: this is well defined since well-founded τDeS process terms are finitely branching. Since T is head normalising we have T ⊢ p = ⨁_{B∈A} ∑_{a∈B} a.p_{a} or T ⊢ p = ∑_{a∈B} a.p_{a} Ω, for some B ⊆ A. One can easily show that ≃ preserves the action depth of well-founded process terms. Thus, as the action depth of each p_{a} is smaller than that of p we obtain, by inductive hypothesis, a Σ_{B(A)} term q_{a} such that T ⊢ p_{a} = q_{a}. We let q ≡ ⨁_{B∈A} ∑_{a∈B} a.q_{a} or q ≡ ∑_{a∈B} a.q_{a} Ω depending on the form of p. By the substitutivity of prefixing and the choice operators it is clear that T ⊢ p = q.

Lemma B.3 Suppose G is a well-founded self-encoding τDeS process language. Then the disjoint extension G′ of G produced by algorithm A is also well-founded.

Proof. Let G and G′ be τDeS languages as in the lemma with the set of actions A. We will show by structural induction that every Σ_{G′} term is well-founded. Assume p ≡ h(p). There are two cases depending on the origin of h.

1. h ∈ Σ_{G}. By the inductive hypothesis, all p_{j} of p are well-founded, thus finitely branching. By Lemma B.2 and the soundness theorem we deduce that for each p_{j} there exists a Σ_{B(A)} term q_{j} such that p_{j} ≃ q_{j}. Since ≃ is a congruence for all τDeS languages we get h(p) ≃ h(q). Moreover, h(q) is a Σ_{G} term so it is well-founded. But, as ≃ preserves well-foundedness we deduce that h(p) is also well-founded.

2. h ∈ Σ_{G′} \ Σ_{G}, so h results from applying Lemma 4.6. Let q be a α-descendant of h(p) obtained by applying some De Simone rule, say r, after possibly a number of applications of τ-rules for h. Thus, h(p) ⇒^{ε} h(p′) →^{α} q. Hence, there is a ground Σ_{G′} substitution ρ such that ρ(cons(r)) ≡ ρ(h(X) →^{α} C[Y′]) ≡ h(p′) →^{α} C[q] with C[q] ≡ q. This implies that ante(r) is valid, i.e. ρ(X_{i} →^{a_{i}} X′_{i}) ≡ p′_{i} →^{a_{i}} q_{i}, for all active i, so q_{i} ≡ p′_{i} for non-active i. Note that, by the construction of the rules for h (as described in the proof of Lemma 4.6), C[Y′] is some Σ_{G} context. Using the inductive hypothesis we find that all p_{i}, and thus all q_{i}, are well-founded. Next, by a similar argument as in case 1, there are Σ_{B(A)} terms u_{i} such that u_{i} ≃ q_{i}. Since ≃ is a congruence for the language G′ we get q ≡ C[q] ≃ C[u]. But, C[u] is a Σ_{G} term, so it is well-founded. Since ≃ preserves well-foundedness we deduce that q is also well-founded. As the above result is for any α-descendant of h(p), it follows that h(p) itself is well-founded.

This completes the proof. Proof of Theorem 4.10. Let A be the set of visible actions of G′. Assume that for any Σ_{G′} terms p and q we have Test(G′) p ⊑ q. By Lemma refw-f-dis-ext p and q are well-founded, hence initially τ-convergent. Thus, T is head normalising for p and q. Hence, using Lemma B.2, we find Σ_{B(A)} terms p′ and q′ such that T ⊢ p = p′ and T ⊢ q = q′ respectively. The soundness theorem gives Test(G′) p = p′ and Test(G′) q = q′. Thus, Test(G′) p′ ⊑ q′. Finally, by completeness of the axiom system for the language B(A), we obtain T ⊢ p′ ⊑ q′, and thus T ⊢ p ⊑ q as required.

The following lemma describes some of the properties of the operator /.

Lemma B.4 Given a process p, a well-founded process q over G′ such that G_{/} ≤ G′ and the action prefixing with b ∈ Σ_{G′} we have

• p/b^{n}Ω ≪ p,

• if q ≪ p then q ≪ p/b^{n}Ω, for some n ∈ .

We show that ω-Induction is sound for all τDeS process languages.

Theorem B.5 Suppose that G is a τDeS language. Then, TEST(G_{/}) ω-Induction.

Proof. Let G′ be τDeS language such that G_{/} ≤ G′. Let P, Q be open terms over Σ_{G′} and let ρ be a Σ_{G′} ground substitution. Assume ρ(P/b^{n}Ω) ≪ ρ(Q) for all n ∈ and some action b. We need to prove ρ(P) ≪ ρ(Q). We only show ρ(P) ≪must ρ(Q), the may part follows similarly. Let s be a sequence of visible actions over G′. Also, let ρ(P)⇓s. Clearly ρ(P/b^{m}Ω)⇓s, where m is greater than the length of s. By the assumption above (ρ(P/b^{n}Ω) ≪ ρ(Q)) we obtain ρ(Q)⇓s. Next, assume ρ(P)⇓s and ρ(Q) ⇒^{s} q′, where q′ = ρ(Q′) for some open term Q′ over Σ_{G′}. Again using the above assumption we deduce ρ(P/b^{m}Ω) ⇒^{s} p′, where m is greater than the length of s, and S(p′) ⊆ S(q′). Moreover, the term p′ has the form ρ(P′/b^{k}Ω) for some k > 0. Thus, ρ(P) ⇒^{s} ρ(P′). Since ρ(P′) and ρ(P′/b^{k}Ω) have the same initial actions we obtain S(ρ(P′)) ⊆ S(q′) as required. Proof of Theorem 4.11. The soundness part follows immediately from Theorems 4.7 and B.5. For the completeness part, assume that p and q are τ-convergent Σ_{G′} closed terms and Test(G′) p ⊑ q. The last means p ≪ q. Also, let A be the set of visible actions of G′. By Lemma B.4 we have p/b^{m}Ω ≪ q, for all m ∈ . Since p is τ-convergent p/b^{m}Ω is well-founded. Thus, by Lemma B.2 there exists, for each m, a Σ_{B(A)} term p_{m} such that T ⊢ p_{m} = p/b^{m}Ω. By soundness we obtain p_{m} ≃ p/b^{m}Ω, hence p_{m} ≪ q. Since p_{m} is wellfounded there is, by Lemma B.4, k ∈ such that p_{m} ≪ q/b^{k}Ω. Since q is τ-convergent q/b^{k}Ω is well-founded, so by Lemma B.4 we can construct, for each k, a Σ_{B(A)} term q_{k} such that T ⊢ q_{k} = q/b^{k}Ω. By soundness we obtain q_{k} ≃ q/b^{k}Ω, hence p_{m} ≪ q_{k}. But, both p_{m} and q_{k} are ΣB terms, so by the completeness result for B we have T ⊢ p_{m} ⊑ q_{k}, Thus, T ⊢ p/b^{m}Ω ⊑ q/b^{k}Ω. Since T ⊢ q/b^{k}Ω ⊑ q we get T ⊢ p/b^{m}Ω ⊑ q. Finally, using ω-Induction rule we obtain T, ω-Induction ⊢ p ⊑ q.

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.

[ABV94] L. Aceto, B. Bloom, and F.W. Vaandrager. Turning SOS rules into equations. Information and Computation, 111:1–52, 1994.

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

[AI95] L. Aceto and A. Ingólfdó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-Verlag, 1995. LNCS 915.

[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.

[BIM95] B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can’t be traced. Journal of ACM, 42(1), 1995. Also appeared as Technical Report TR 90-1150, Cornell, 1990.

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

[BK85] J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37, 1985.

[BK88] J.A. Bergstra and J.W. Klop. A complete inference system for regular processes with silent moves. In F.R. Drake and J.K. Truss, editors, Logic Colloquium ’86, pages 21–81. North-Holland, 1988. First appeared as Report CS-R8420, CWI, 1984.

[Blo90a] B. Bloom. Ready simulation, bisimulation, and the semantics of CCS-like languages. PhD thesis, MIT, 1990.

[Blo90b] 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, 1990.

[CH90] R. Cleaveland and M. Hennessy. Priorities in process algebra. Information and Computation, 87:58–77, 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.

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

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

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

[Mil84] R. Milner. A complete inference system for a class of regular behaviours. Journal of Computer System Sciences, 28:439–466, 1984.

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

[Mil89b] R. Milner. A complete axiomatisation for observational congruence of finite-state behaviours. Information and Computation, 81:227–247, 1989.

[Mol90] F. Moller. The importance of the left merge operator in process algebras. In M. Paterson, editor, Proceedings of 17th ICALP, Warwick. Springer-Verlag, 1990. LNCS 443.

[NH84] R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.

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

[Nic87] R. De Nicola. Extensional equivalences for transition systems. Acta Informatica, 24:212–237, 1987.

[PU96] I.C.C. Phillips and I. Ulidowski. Ordered SOS rules and weak bisimulation. In A. Adalat, S. Jourdan, and G. McCusker, editors, Theory and Formal Methods 1996, London, 1996. Imperial College Press.

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

[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. In I. Lee and S.A. Smolka, editors, Proceedings of the 6th International Conference on Concurrency Theory CONCUR’95, Philadelphia, 1995. Springer-Verlag. LNCS 962.

[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.

[vG90] R.J. van Glabbeek. Comparative Concurrency Semantics and Refinement of Actions. PhD thesis, CWI, 1990.

[vG93] R.J. van Glabbeek. A complete axiomatisation for branching bisimulation congruence of finite-state behaviours. In A.M. Borzyszkowski and S. Sokołowski, editors, Proceedings of MFCS 1993. Springer-Verlag, 1993. LNCS 711.

Figure 4: Axioms for CCS parallel composition.

(X ⊕ Y) ∥ Z = X ∥ Z ⊕ Y ∥ Z

X ∥ (Y ⊕ Z) = X ∥ Y ⊕ X ∥ Z

AX ∥ Ω = AX Ω Ω AX AX |Ω

Ω ∥ AX = Ω AX AX Ω Ω|AX

AX ∥ BY = AX BY BY AX AX |BY  if A ∩ B̄ = ∅
AX ∥ BY = AX BY BY AX ⊕ AX |BY  if A ∩ B̄ ≠ ∅

(X ⊕ Y) Z = X Z ⊕ Y Z

(∑_{A} a.X_{a}) Y = ∑_{A}(a.X_{a} Y)

a.X _{A}Y = a.(X ∥ Y)

0 X = 0

Ω X ⊑ Ω

(X ⊕ Y)|Z = X |Z ⊕ Y |Z

X |(Y ⊕ Z) = X |Y ⊕ X |Z

(∑_{A} a.X_{a})|BY = ∑_{A}(a.X_{a} |BY)  if A ∩ B̄ ≠ ∅
AX |(∑_{B} bY_{b}) = ∑_{B}(AX |bY_{b})  if A ∩ B̄ ≠ ∅
(∑_{A} a.X_{a})|BY = ∑_{A\C}(a.X_{a} |BY) ⊕ ⨁_{C}(c.X_{c} |BY) if A ∩ B̄ = C ≠ ∅
AX |(∑_{B} bY_{b}) = ∑_{B\C}(AX |bY_{b}) ⊕ ⨁_{C}(AX |cX_{c})  if Ā ∩ B = C ≠ ∅

a.X |ā.Y = X ∥ Y

a.X |b.Y = 0  if a ≠ b̄

0|X = 0

X |0 = 0

Ω|X ⊑ Ω

X |Ω ⊑ Ω