On Cool Congruence Formats for Weak Bisimulations^{∗}

R.J. van Glabbeek

National ICT Australia and School of Computer Science and Engineering The University of New South Wales

                                        rvg@cs.stanford.edu

In TCS 146, Bard Bloom presented rule formats for four main notions of bisimulation with silent moves. He proved that weak bisimulation equivalence is a congruence for any process algebra defined by WB cool rules, and established similar results for rooted weak bisimulation (Milner’s “observational congruence”), branching bisimulation and rooted branching bisimulation. This study reformulates Bloom’s results in a more accessible form and contributes analogues for (rooted) η-bisimulation and (rooted) delay bisimulation. Moreover, finite equational axiomatisations of rooted weak bisimulation equivalence are provided that are sound and complete for finite processes in any RWB cool process algebra. These require the introduction of auxiliary operators with lookahead, and an extension of Bloom’s formats for this type of operator with lookahead. Finally, a challenge is presented for which Bloom’s formats fall short and further improvement is called for.

1 Introduction

Structural Operational Semantics [13, 16] is one of the main methods for defining the meaning of operators in system description languages like CCS [13]. A system behaviour, or process, is represented by a closed term built from a collection of operators, and the behaviour of a process is given by its collection of (outgoing) transitions, each specifying the action the process performs by taking this transition, and the process that results after doing so. For each n-ary operator f in the language, a number of transition rules are specified that generate the transitions of a term f(p_{1}, …, p_{n}) from the transitions (or the absence thereof) of its arguments p_{1}, …, p_{n}.

For purposes of representation and verification, several behavioural equivalence relations have been defined on processes, of which the most well-known is strong bisimulation equivalence [13], and its variants weak and branching bisimulation equivalence [13, 12], that feature abstraction from internal actions. In order to allow compositional system verification, such equivalence relations need to be congruences for the operators under consideration, meaning that the equivalence class of an n-ary operator f applied to arguments p_{1}, …, p_{n} is completely determined by the equivalence classes of these arguments. Although strong bisimulation equivalence is a congruence for the operators of CCS and many other languages found in the literature, weak bisimulation equivalence fails to be a congruence for the choice or alternative composition operator + of CCS. To bypass this problem one uses the coarsest congruence relation for + that is finer than weak bisimulation equivalence, characterised as rooted weak bisimulation equivalence [13, 4, 11], which turns out to be a minor variation of weak bisimulation equivalence, and a congruence for all of CCS and many other languages. Analogously, rooted branching bisimulation is the coarsest congruence for CCS and many other languages that is finer than branching bisimulation equivalence [12].

∗An extended abstract of this paper appeared in: D.V. Hung & M. Wirsing, editors: Proceedings International Colloquium on Theoretical Aspects of Computing, ICTAC’05, Hanoi, LNCS 3722, Springer, 2005, pp. 318-333.

In order to streamline the process of proving that a certain equivalence is a congruence for certain operators, and to guide sensible language definitions, syntactic criteria (rule formats) for the transition rules in structural operational semantics have been developed, ensuring that the equivalence is a congruence for any operator specified by rules that meet these criteria. One of these is the GSOS format of Bloom, Istrail & Meyer [6], generalising an earlier format by De Simone [17]. When adhering to this format, all processes are computably finitely branching, and strong bisimulation equivalence is a congruence [6]. Bloom [5] defines congruence formats for (rooted) weak and branching bisimulation equivalence by imposing additional restrictions on the GSOS format. As is customary in this field, finer equivalences have wider formats, so Bloom’s BB cool GSOS format, which guarantees that branching bisimulation equivalence is a congruence, is more general than his WB cool GSOS format, which suits weak bisimulation equivalence; also his RWB cool GSOS format, suiting rooted weak bisimulation, is more general than the WB cool GSOS format, and his RBB cool GSOS format, guaranteeing that rooted branching bisimulation equivalence is a congruence, is the most general of all. The prime motivating example for these formats is the structural operational semantics of CCS [13]. All CCS operators are RWB cool, and the CCS operators other than the + are even WB cool.

Bloom’s formats involve a fast bookkeeping effort of names of variables, used to precisely formulate the bifurcation rules that his formats require. To make his work more accessible, Bloom also presents simpler but less general versions of his formats, obtained by imposing an additional syntactic restriction. This restriction makes it possible to simplify the bifurcation rules to patience rules, which do not require such an extensive bookkeeping. Fokkink [8] generalises Bloom’s simply RBB cool format to a format he calls RBB safe, and writes “The definition of bifurcation rules is deplorably complicated, and we do not know of any examples from the literature that are RBB cool but not simply RBB cool. Therefore, we refrain from this generalisation here.” Ulidowski [18, 19, 20] studies congruence formats for variations of the semantic equivalences mentioned above with a different treatment of divergence. Ulidowski’s formats form the counterparts of Bloom’s simply cool formats only.

The main aim of the present study is to simplify and further clarify Bloom’s work, so as to make it more accessible for the development of applications, variations and extensions. In passing, analogous results are obtained for two equivalences, and their rooted variants, that bridge the gap between weak and branching bisimulation. Moreover, the method of Aceto, Bloom & Vaandrager [1] to extract from any GSOS language a finite equational axiomatisation that is sound and complete for strong bisimulation equivalence on finite processes, is adapted to rooted weak bisimulation equivalence. In the construction fresh function symbols may need to be added whose transition rules have lookahead and thereby fall outside the GSOS format. To this end, I extend the RWB cool format with a form of lookahead.

One of the simplifications of Bloom’s formats presented here stems from the observation that the operators in any of the cool formats can be partitioned in principal operators and abbreviations, such that the abbreviations can be regarded as syntactic sugar, adding nothing that could not be expressed with principal operators. For any abbreviation f there exists a principal operator f^{⋆} that typically takes more arguments. For instance, f(x_{1}, x_{2}) could be an abbreviation of f^{⋆}(x_{1}, x_{1}, x_{2}). The rules for the abbreviations are completely determined by the rules for the principal operators, and for principal operators patience rules suffice, i.e. one does not need the full generality of bifurcation rules. Moreover, the simply cool formats can be characterised by the requirement that all operators are principal. These observations make it possible to define the cool formats of Bloom without mentioning bifurcation rules altogether. It also enables a drastic simplification of the congruence proofs, namely by establishing the congruence results for the simply cool formats first, and reducing the general case to the simple case by means of some general insights in abbreviation expansion.

In fact, I will present a general algorithm that given any rule format, guaranteeing that a certain equivalence, coarser than or equal to strong bisimulation equivalence, is a congruence, extends this format with a mechanism for abbreviation expansion. Bloom’s general formats can then be obtained by applying this algorithm to his simple formats.

Even though any operation that fits the cool formats can also be defined using merely the simply cool formats, in practice it may be handy to work with the full generality of the cool formats. The unary copying operator cp of [6] (page 257) for instance does not fit the cool formats directly, but can be made to fit by adding an auxiliary binary copying operator to the language, of which the unary one is an abbreviation. Dumping the abbreviation from the language would appear unnatural here, as the unary operator motivates the rules for both itself and its binary expansion, the latter being needed merely to make it work.

Another simplification contributed here is in the description of the RWB cool format. Bloom requires for every operational rule with target t the existence of two terms t_{1} and t_{2}, and seven types of derived operational rules. I show that without limitation of generality it is always possible to choose t_{2} = t, thereby making four of those seven types of rules redundant. Thus, the same format is obtained by requiring only t_{1} and two types of derived rules (the third being a bifurcation rule, that was already required for its own sake).

After defining the basic concepts in Section 2, I present the congruence proofs for the simply cool languages in Section 3. To that end, I first prove the result from [6] that strong bisimulation equivalence is a congruence for all GSOS operators. Then I change this proof in minimal ways so as to obtain the congruence results for the simply cool languages. In doing so, for each simply cool format I state a lemma that tells exactly what is needed to make the congruence proof work. Section 4 defines the simply cool formats for the unrooted case, in such a way that the lemmas hold. As an example I show a version of the language CSP [7, 15] to be simply WB cool, implying that weak and branching bisimulation equivalence are congruences on this language. Section 5 presents the theory of abbreviations that lifts the results from the simple to the general congruence formats, and Section 6 deals with the rooted congruence formats. Section 7 compares my definitions of the cool formats with the ones of Bloom. In Section 8 I generalise the RWB cool format to what I call GSOS languages with lookahead. Section 9 recapitulates the method of [1] to provide finite equational axiomatisations of strong bisimulation equivalence that are sound and complete for finite processes on an augmentation of any given GSOS language, and Section 10 extends this work to the rooted weak equivalences. Section 11 discusses extensions of Bloom’s formats that occur in the literature. Finally, Section 12 presents a fairly intuitive GSOS language for which the existing congruence formats fall short and further improvement is called for.

Acknowledgements. My thanks to Simone Tini for inspiration, and to the referees for their proposals of improvements in presentation.

2 Preliminaries

In this paper V = {x_{1}, x_{2}, …} and Act are two sets of variables and actions.

Definition 1 A signature is a collection Σ of function symbols f ∉ V equipped with a function ar : Σ → IN. The set T T(Σ) of terms over a signature Σ is defined recursively by:

• V ⊆ T T(Σ),

• if f ∈ Σ and t_{1}, …, t_{ar(f)} ∈ T T(Σ) then f(t_{1}, …, t_{ar(f)}) ∈ T T(Σ).

A term c() is abbreviated as c. For t ∈ T T(Σ), var(t) denotes the set of variables that occur in t. T (Σ) is the set of closed terms over Σ, i.e. the terms p ∈ T T(Σ) with var(p) = ∅. A Σ-substitution σ is a partial function from V to T T(Σ). If σ is a substitution and S is any syntactic object, then σ(S) denotes the object obtained from S by replacing, for x in the domain of σ, every occurrence of x in S by σ(x). In that case σ(S) is called a substitution instance of S. A Σ-substitution is closed if it is a total function from V to T (Σ).

Definition 2 Let Σ be a signature. A positive Σ-literal is an expression t ⟶^{a} t′ and a negative Σ-literal an expression t −̸→^{a} with t, t′ ∈ T T(Σ) and a ∈ Act. A transition rule over Σ is an expression of the form \frac{H}{α} with H a set of Σ-literals (the premises of the rule) and α a positive Σ-literal (the conclusion). The left- and right-hand side of α are called the source and the target of the rule, respectively. A rule \frac{H}{α} with H = ∅ is also written α. A transition system specification (TSS), written (Σ, R), consists of a signature Σ and a collection R of transition rules over Σ. A TSS is positive if the premises of its rules are positive.

Definition 3 [6] A GSOS rule is a transition rule such that

• its source has the form f(x_{1}, …, x_{ar(f)}) with f ∈ Σ and x_{i} ∈ V,

• the left-hand sides of its premises are variables x_{i} with 1 ≤ i ≤ ar(f),

• the right-hand sides of its positive premises are variables that that are all distinct, and that do not occur in its source,

• its target only contains variables that also occur in its source or premises.

A GSOS language, or TSS in GSOS format, is a TSS whose rules are GSOS rules.

Definition 4 A transition over a signature Σ is a closed positive Σ-literal. With structural recursion on p one defines when a GSOS language L generates a transition p ⟶^{a} p′ (notation p ⟶^{a}_{L} p′):

f(p_{1}, …, p_{n}) ⟶^{a}_{L} q iff L has a transition rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t} and there is a closed substitution

σ with σ(x_{i}) = p_{i} for i = 1, ..., n and σ(t) = q, such that p_{i} ⟶^{c}_{L} σ(y) for (x_{i} ⟶^{c} y) ∈ H and

¬∃r(p_{i} ⟶^{c}_{L} r) for (x_{i} −̸→^{c}) ∈ H.

Henceforth a GSOS language L over a signature Σ is assumed, and closed Σ-terms will be called processes. The subscript L will often be suppressed. Moreover, Act = A ._{∪} {τ} with τ the silent move or hidden action.

Definition 5 Two processes t and u are weak bisimulation equivalent or weakly bisimilar (t\underline{↔}_{w} u) if tRu for a symmetric binary relation R on processes (a weak bisimulation) satisfying, for a ∈ Act,

if pRq and p ⟶^{a} p′ then there are q_{1}, q_{2}, q′ such that q ⟹ q_{1} ⟶^{(a)} q_{2} ⟹ q′ and p′Rq′. (*)

Here p ⟹ p′ abbreviates p = p_{0} ⟶^{τ} p_{1} ⟶^{τ} ⋯ ⟶^{τ} p_{n} = p′ for some n ≥ 0, whereas p ⟶^{(a)} p′ abbreviates (p ⟶^{a} p′) ∨ (a = τ ∧ p = p′). t and u are η-bisimilar (t\underline{↔}_{η} u) if in (*) one additionally requires pRq_{1}; t and u are delay bisimilar (t\underline{↔}_{d} u) if in (*) one additionally requires q_{2} = q′; t and u are branching bisimilar (t\underline{↔}_{b} u) if in (*) one requires both pRq_{1} and q_{2} = q′; t and u are strongly bisimilar (t\underline{↔} u) if in (*) one simply requires q ⟶^{a} q′.

Two processes t and u are rooted weak bisimulation equivalent (t\underline{↔}_{rw} u), if they satisfy

if t ⟶^{a} t′ then there are u_{1}, u_{2}, u such that u ⟹ u_{1} ⟶^{a} u_{2} ⟹ u′ and t′ \underline{↔}_{w} u′, and
if u ⟶^{a} u′ then there are t_{1}, t_{2}, t such that t ⟹ t_{1} ⟶^{a} t_{2} ⟹ t′ and t′ \underline{↔}_{w} u′.

They are rooted η-bisimilar (t\underline{↔}_{rη} u) if above one additionally requires u_{1} = u, t_{1} = t, and t′ \underline{↔}_{η} u′, they are rooted delay bisimilar (t \underline{↔}_{rd} u) if one requires u_{2} = u′, t_{2} = t′ and t′ \underline{↔}_{d} u′, and they are rooted branching bisimilar (t\underline{↔}_{rb} u) if one requires u_{1} = u, u_{2} = u′, t_{1} = t, t_{2} = t′ and t′ \underline{↔}_{b} u′.

It is well known and easy to check that the nine relations on processes defined above are equivalence relations indeed [2, 12], and that, for x ∈ {weak, η, delay, branching, strong}, x-bisimulation equivalence is the largest x-bisimulation relation on processes [13, 4, 11, 12]. Moreover, p \underline{↔}_{rx} q implies p\underline{↔}_{x} q.

Definition 6 An equivalence relation ∼ on processes is a congruence if for all f ∈ Σ

p_{i} ∼ q_{i} for i = 1, …, ar(f) ⇒ f(p_{1}, …, p_{ar(f)}) ∼ f(q_{1}, …, q_{ar(f)}).

This is equivalent to the requirement that for all t ∈ T T(Σ) and closed substitutions σ, ν : V → T (Σ)

σ(x) = ν(x) for x ∈ var(t) ⇒ σ(t) = ν(t).

This note, and Bloom [5], deal with syntactic conditions on GSOS languages that guarantee that the equivalence notions of Definition 5 are congruences.

3 The congruence proofs for the simply cool rule formats

In this section I first prove the result from [6] that strong bisimulation equivalence is a congruence for all GSOS operators. Then I change this proof in minimal ways so as to obtain the congruence results for the simply cool GSOS languages. In doing so, for each simply cool GSOS format I state a lemma that tells exactly what is needed to make the congruence proof work. Later on, the simply cool congruence formats will be defined in such a way that these lemmas hold.

Theorem 1 [6] On any GSOS language, strong bisimulation equivalence is a congruence.

Proof: Let R be the smallest relation on processes satisfying

• if p\underline{↔} q then pRq, and

• if p_{i}Rq_{i} for i = 1, …, ar(f) then f(p_{1}, …, p_{ar(f)})Rf(q_{1}, …, q_{ar(f)}).

It suffices to show that R is a strong bisimulation, because this implies that R equals \underline{↔}, and by construction R is a congruence. Because \underline{↔} is symmetric, so is R. So it remains to show that

if pRq and p ⟶^{a} p′, with a ∈ Act, then there is a q′ such that q ⟶^{a} q′ and p′Rq′.

This I will do with induction on the number of applications of the second clause in the definition of R above in establishing that pRq. Note that this number is the same for qRp.

Base case: Let p \underline{↔} q and p ⟶^{a} p′. Using that \underline{↔} is a strong bisimulation, there must be a process q′ such that q ⟶^{a} q′ and p′ \underline{↔} q′, hence p′Rq′.

Induction step: Let p = f(p_{1}, …, p_{n}) and q = f(q_{1}, …, q_{n}) where p_{i}Rq_{i} for i = 1, …, n, and p_{i}Rq_{i} is established in less applications of the second step than pRq. By induction, one may assume

if p_{i} ⟶^{c} p′ then there is a q′ such that q_{i} ⟶^{c} q′ and p′Rq′  (1)
if q_{i} ⟶^{c} q′ then there is a p′ such that p_{i} ⟶^{c} p′ and p′Rq′  (2)

for i = 1, ..., n and c ∈ Act. Let p ⟶^{a} p′. By Definition 4, there must be a rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t} in L

and a closed substitution σ with σ(x_{i}) = p_{i} for i = 1, ..., n and σ(t) = p′, such that p_{i} ⟶^{c} σ(y) for

(x_{i} ⟶^{c} y) ∈ H and ¬∃r(p_{i} ⟶^{c} r) for (x_{i} −̸→^{c}) ∈ H.

For (x_{i} ⟶^{c} y) ∈ H, using that p_{i} ⟶^{c} σ(y), by (1) there is a q_{y} such that q_{i} ⟶^{c} q_{y} and σ(y)Rq_{y}. For (x_{i} −̸→^{c}) ∈ H, using that ¬∃r(p_{i} ⟶^{c} r), by (2) there can not be a s ∈ T (Σ) with q_{i} ⟶^{c} s.

Let ν be a substitution with ν(x_{i}) = q_{i} for i = 1, …, n and ν(y) = q_{y} if y is the right-hand side of a premise in H, taking ν(z) = σ(z) for all other variables z; by the third clause of Definition 3 such a substitution ν does indeed exist. I now have σ(x)Rν(x) for all x ∈ V, and hence σ(t)Rν(t) by the definition of R. Take q′ = ν(t). So p′Rq′. Moreover, q_{i} ⟶^{c} ν(y) for (x_{i} ⟶^{c} y) ∈ H and

¬∃r(q_{i} ⟶^{c} r) for (x_{i} −̸→^{c}) ∈ H. Thus, by Definition 4, q = f(q_{1}, …, q_{n}) ⟶^{a} ν(t) = q′. □

In Sections 4 and 6 I define 8 simply cool formats in such a way that the following theorem holds.

Theorem 2 On any simply WB cool GSOS language, \underline{↔}_{w} is a congruence.

On any simply RWB cool GSOS language, \underline{↔}_{rw} is a congruence.

On any simply DB cool GSOS language, \underline{↔}_{d} is a congruence.

On any simply RDB cool GSOS language, \underline{↔}_{rd} is a congruence.

On any simply HB cool GSOS language, \underline{↔}_{η} is a congruence.

On any simply RHB cool GSOS language, \underline{↔}_{rη} is a congruence.

On any simply BB cool GSOS language, \underline{↔}_{b} is a congruence.

On any simply RBB cool GSOS language, \underline{↔}_{rb} is a congruence.

The proofs are simple variations of the proof of Theorem 1 that merely require the following lemmas. These lemmas could have been taken as definitions of the simply cool rule formats, albeit not very syntactic ones. The real definitions will consist of the simplest syntactic requirements that guarantee these lemmas to hold. For now, all one needs to know about the cool formats is that

• (simply) WB, RWB, DB, RDB, HB and BB cool GSOS languages are required to be positive— hence one doesn’t need a counterpart of equation (2) above,

• the targets of all rules in simply RXB languages (X∈ {W,D,H,B}) belong to a simply XB cool sublanguage,

• the simply XB cool languages only have rules of the form \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} for I ⊆ \{1, …, n\}.

I write p ⟹⟶^{a} p′ for ∃p^{pre}(p ⟹ p^{pre} ⟶^{a} p′), and similarly for other relation compositions.

Lemma WB Let L be simply WB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution.

If for each premise x ⟶^{c} y in H one has ν(x) ⟹⟶^{(c)}⟹ ν(y), then ν(s) ⟹⟶^{(a)}⟹ ν(t).

Lemma RWB Let L be simply RWB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substi-

tution. If for each premise x ⟶^{c} y in H one has ν(x) ⟹⟶^{c}⟹ ν(y), then ν(s) ⟹⟶^{a}⟹ ν(t).

Lemma DB Let L be simply DB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution.

If for each premise x ⟶^{c} y in H one has ν(x) ⟹⟶^{(c)} ν(y), then ν(s) ⟹⟶^{(a)} ν(t).

Lemma RDB Let L be simply RDB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution.

If for each premise x ⟶^{c} y in H one has ν(x) ⟹⟶^{c} ν(y), then ν(s) ⟹⟶^{a} ν(t).

Lemma HB Let L be simply HB cool, let \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} be a rule in L, and let ρ, ν be closed

substitutions satisfying ρ(x_{i}) ⟹ ν(x_{i}) ⟶^{(c_{i})}⟹ ν(y_{i}) for i ∈ I and ρ(x_{i}) = ν(x_{i}) for i ∉ I. Then

ρ(f(x_{1}, ..., x_{n})) ⟹ ν(f(x_{1}, ..., x_{n})) ⟶^{(a)}⟹ ν(t).

Lemma RHB Let L be simply RHB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution

such that ν(x) ⟶^{c}⟹ ν(y) for each positive premise x ⟶^{c} y in H and ¬∃r (ν(x) −̸→^{c} r) for each negative premise x −̸→^{c} in H. Then ν(s) ⟶^{a}⟹ ν(t).

Lemma BB Let L be simply BB cool, let \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} be a rule in L, and let ρ, ν be closed

substitutions satisfying ρ(x_{i}) ⟹ ν(x_{i}) ⟶^{(c_{i})} ν(y_{i}) for i ∈ I and ρ(x_{i}) = ν(x_{i}) for i ∉ I. Then

ρ(f(x_{1}, ..., x_{n})) ⟹ ν(f(x_{1}, ..., x_{n})) ⟶^{(a)} ν(t).

Lemma RBB Let L be simply RBB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution

such that ν(x) ⟶^{c} ν(y) for each positive premise x ⟶^{c} y in H and ¬∃r (ν(x) −̸→^{c} r) for each negative premise x −̸→^{c} in H. Then ν(s) ⟶^{a} ν(t).

By Definition 4, the last lemma holds trivially. The others will be obtained in Sections 4 and 6. With these lemmas the proof of Theorem 2 is easy. I will only present the representative cases of (rooted) weak and branching bisimulation equivalence.

Theorem 2WB On any simply WB cool GSOS language, \underline{↔}_{w} is a congruence.

Proof: Let R be the smallest relation on processes satisfying

• if p\underline{↔}_{w} q then pRq, and

• if p_{i}Rq_{i} for i = 1, …, ar(f) then f(p_{1}, …, p_{ar(f)})Rf(q_{1}, …, q_{ar(f)}).

It suffices to show that R is a weak bisimulation, because this implies that R equals \underline{↔}_{w}, and by construction R is a congruence. Because \underline{↔}_{w} is symmetric, so is R. So it remains to show that

if pRq and p ⟶^{a} p′, then there is a q′ such that q ⟹⟶^{(a)}⟹ q′ and p′Rq′.

This I will do with induction on the number of applications of the second clause in the definition of R above in establishing pRq.

Base case: Let p \underline{↔}_{w} q and p ⟶^{a} p′. Using that \underline{↔}_{w} is a weak bisimulation, there must be a process q′ such that q ⟹⟶^{(a)}⟹ q′ and p′ \underline{↔}_{w} q′, hence p′Rq′.

Induction step: Let p = f(p_{1}, …, p_{n}) and q = f(q_{1}, …, q_{n}) where p_{i}Rq_{i} for i = 1, …, n, and p_{i}Rq_{i} is established in less applications of the second step than pRq. By induction, one may assume

if p_{i} ⟶^{c_{i}} p′_{i} then there is a q′_{i} such that q_{i} ⟹⟶^{(c_{i})}⟹ q′_{i} and p′_{i}Rq′_{i}  (3)

for i = 1, ..., n and c_{i} ∈ Act. Let p ⟶^{a} p′. By Definition 4, there must be a rule \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} in L

and a closed substitution σ with σ(x_{i}) = p_{i} for i = 1, …, n and σ(t) = p′, such that p_{i} ⟶^{c_{i}} σ(y_{i}) for i ∈ I. So by (3), for i ∈ I there is a q′_{i} such that q_{i} ⟹⟶^{(c_{i})}⟹ q′_{i} and σ(y_{i})Rq′_{i}. Let ν be a substitution with ν(x_{i}) = q_{i} for i = 1, …, n and ν(y_{i}) = q′_{i} for i ∈ I, taking ν(z) = σ(z) for all other variables z. I now have σ(x)Rν(x) for all x ∈ V, and hence σ(t)Rν(t) by the definition of R. Take q′ = ν(t). Then p′Rq′. Moreover, ν(x_{i}) ⟹⟶^{(c_{i})}⟹ ν(y_{i}) for each i∈I. Thus, by Lemma WB,

q = ν(f(x_{1}, …, x_{n})) ⟹⟶^{(a)}⟹ ν(t) = q′. □

Theorem 2RWB On any simply RWB cool GSOS language, \underline{↔}_{rw} is a congruence.

Proof: Let f be an operator of arity n, and let p_{i} \underline{↔}_{rw} q_{i} for i = 1, …, n. I have to show that f(p_{1}, …, p_{n}) \underline{↔}_{rw} f(q_{1}, …, q_{n}). Let f(p_{1}, …, p_{n}) ⟶^{a} p′. By Definition 4, there must be a rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t} in L and a closed substitution σ with σ(x_{i}) = p_{i} for i = 1, ..., n and σ(t) = p′,

such that p_{i} ⟶^{c} σ(y) for (x_{i} ⟶^{c} y) ∈ H. For any (x_{i} ⟶^{c} y) ∈ H, using that p_{i} \underline{↔}_{rw} q_{i}, there is a q_{y} such that q_{i} ⟹⟶^{c}⟹ q_{y} and σ(y) \underline{↔}_{w} q_{y}. Let ν be a substitution with ν(x_{i}) = q_{i} for i = 1, …, n and ν(y) = q_{y} if y is the right-hand side of a premise in H, taking ν(z) = σ(z) for all other variables z; by the last clause of Definition 3 such a substitution ν does indeed exist. I now have σ(x) \underline{↔}_{w} ν(x) for all x ∈ V, and hence σ(t) \underline{↔}_{w} ν(t) by Theorem 2WB. Take q′ = ν(t). So p′ \underline{↔}_{w} q′. Moreover, ν(x_{i}) ⟹⟶^{c}⟹ ν(y) for each premise (x_{i} ⟶^{c} y) ∈ H. Thus, by Lemma RWB,

f(q_{1}, …, q_{n}) = ν(f(x_{1}, …, x_{n})) ⟹⟶^{a}⟹ ν(t) = q′.

The case assuming f(q_{1}, …, q_{n}) ⟶^{a} q′ follows by symmetry. □

Theorem 2BB On any simply BB cool GSOS language, \underline{↔}_{b} is a congruence.

Proof: Let R be the smallest relation on processes satisfying

• if p\underline{↔}_{b} q then pRq, and

• if p_{i}Rq_{i} for i = 1, …, ar(f) then f(p_{1}, …, p_{ar(f)})Rf(q_{1}, …, q_{ar(f)}).

It suffices to show that R is a branching bisimulation, because this implies that R equals \underline{↔}_{b}, and by construction R is a congruence. Because \underline{↔}_{b} is symmetric, so is R. So it remains to show that

if pRq and p ⟶^{a} p′ then there are q^{pre}, q′ such that q ⟹ q^{pre} ⟶^{(a)} q′, pRq^{pre} and p′Rq′.

This I will do with induction on the number of applications of the second clause in the definition of R above in establishing pRq.

Base case: Let p\underline{↔}_{b} q and p ⟶^{a} p′. Using that \underline{↔}_{b} is a branching bisimulation, there must be

processes q^{pre}, q′ such that q ⟹ q^{pre} ⟶^{(a)} q′, p\underline{↔}_{b} q^{pre} and p′ \underline{↔}_{b} q′, hence pRq^{pre} and p′Rq′.

Induction step: Let p = f(p_{1}, …, p_{n}) and q = f(q_{1}, …, q_{n}) where p_{i}Rq_{i} for i = 1, …, n, and p_{i}Rq_{i} is established in less applications of the second step than pRq. By induction, one may assume

if p_{i} ⟶^{c_{i}} p′_{i} then there are q_{i}^{pre}, q′_{i} such that q_{i} ⟹ q_{i}^{pre} ⟶^{(c_{i})} q′_{i}, p_{i}Rq_{i}^{pre} and p′_{i}Rq′_{i}  (4)

for i = 1, ..., n and c_{i} ∈ Act. Let p ⟶^{a} p′. By Definition 4, there must be a rule \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} in L

and a closed substitution σ with σ(x_{i}) = p_{i} for i = 1, …, n and σ(t) = p′, such that p_{i} ⟶^{c_{i}} σ(y_{i})

for i ∈ I. So by (4), for i ∈ I there are q_{i}^{pre}, q′_{i} such that q_{i} ⟹ q_{i}^{pre} ⟶^{(c_{i})} q′_{i}, p_{i}Rq_{i}^{pre} and σ(y_{i})Rq′_{i}.

Let ν be a substitution with ν(x_{i}) = q_{i}^{pre} and ν(y_{i}) = q′_{i} for i ∈ I and ν(x_{i}) = q_{i} for i ∉ I, taking ν(z) = σ(z) for all other variables z. I now have σ(x)Rν(x) for all x ∈ V, and hence σ(t)Rν(t) and σ(f(x_{1}, …, x_{n})Rν(f(x_{1}, …, x_{n}) by the definition of R. Take q^{pre} = ν(f(x_{1}, …, x_{n})) and q′ = ν(t). So pRq^{pre} and p′Rq′. Moreover, q_{i} ⟹ ν(x_{i}) ⟶^{(c_{i})} ν(y) for each i∈I. Thus Lemma BB, taking ρ to be a closed substitution with ρ(x_{i}) = q_{i}, yields q ⟹ q^{pre} ⟶^{(a)} q′. □

Theorem 2RBB On any simply RBB cool GSOS language, \underline{↔}_{rb} is a congruence.

Proof: Let f be an operator of arity n, and let p_{i} \underline{↔}_{rb} q_{i} for i = 1, …, n. I have to show that f(p_{1}, …, p_{n}) \underline{↔}_{rb} f(q_{1}, …, q_{n}). Let f(p_{1}, …, p_{n}) ⟶^{a} p′. By Definition 4, there must be a rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t} in L and a closed substitution σ with σ(x_{i}) = p_{i} for i = 1, ..., n and σ(t) = p′, such

that p_{i} ⟶^{c} σ(y) for (x_{i} ⟶^{c} y) ∈ H and ¬∃r(p_{i} ⟶^{c} r) for (x_{i} −̸→^{c}) ∈ H.

For any (x_{i} ⟶^{c} y) ∈ H, using that p_{i} \underline{↔}_{rb} q_{i}, there is a q_{y} such that q_{i} ⟶^{c} q_{y} and σ(y)\underline{↔}_{b} q_{y}. For any (x_{i} −̸→^{c}) ∈ H, using that p_{i} \underline{↔}_{rb} q_{i}, there can not be a s ∈ T (Σ) with q_{i} ⟶^{c} s.

Let ν be a substitution with ν(x_{i}) = q_{i} for i = 1, …, n and ν(y) = q_{y} if y is the right-hand side of a premise in H, taking ν(z) = σ(z) for all other variables z; by the last clause of Definition 3 such a substitution ν does indeed exist. I now have σ(x) \underline{↔}_{b} ν(x) for all x ∈ V, and hence σ(t) \underline{↔}_{b} ν(t) by Theorem 2BB. Take q′ = ν(t). So p′ \underline{↔}_{b} q′. Moreover, ν(x_{i}) ⟶^{c} ν(y) for each premise x_{i} ⟶^{c} y in H and ¬∃r(ν(x_{i}) ⟶^{c} r) for each premise x_{i} −̸→^{c} in H. Thus, by Lemma RBB, or Definition 4,

f(q_{1}, …, q_{n}) = ν(f(x_{1}, …, x_{n})) ⟶^{a} ν(t) = q′.

The case assuming f(q_{1}, …, q_{n}) ⟶^{a} q′ follows by symmetry. □

4 Simply cool GSOS languages

In this section I will define the simply XB cool rule formats (X∈ {W,D,H,B}) and show that they satisfy Lemma XB. Let L be a positive GSOS language.

Definition 7 For an operator f in L, the rules of f are the rules in L with source f(x_{1}, ..., x_{ar(f)}).

• An operator in L is straight if it has no rules in which a variable occurs multiple times in the left-hand side of its premises. A operator is smooth if moreover it has no rules in which a variable occurs both in the target and in the left-hand side of a premise.

• An argument i ∈ IN of an operator f is active if f has a rule in which x_{i} appears as left-hand side of a premise.

• A variable x occurring in a term t is receiving in t if t is the target of a rule in L in which x is the right-hand side of a premise. An argument i ∈ IN of an operator f is receiving if a variable x is receiving in a term t that has a subterm f(v_{1}, …, v_{n}) with x occurring in v_{i}.

• A rule of the form \frac{x_{i} ⟶^{τ} y}{f(x_{1}, …, x_{n}) ⟶^{τ} f(x_{1}, …, x_{n})[y/x_{i}]} with 1 ≤ i ≤ n is called a patience rule

for the i^{th} argument of f. Here t[y/x] denotes term t with all occurrences of x replaced by y.

Non-straight operators in positive GSOS languages rarely occur in the literature.

Definition 8 A GSOS language L is simply WB cool if it is positive and

1. all operators in L are straight,

2. patience rules are the only rules in L with τ-premises,

3. every active argument of an operator has a patience rule,

4. every receiving argument of an operator has a patience rule,

5. all operators in L are smooth.

The formats simply DB cool, simply HB cool and simply BB cool are defined likewise, but skipping Clause 4 for DB and BB, and Clause 5 for HB and BB.

The simply WB and BB cool formats above coincide with the ones of [5], whereas the simply DB cool format coincides with the eb format of [19].

Example 1 Consider the following fragment of the language Communicating Sequential Processes (CSP), for a given set A of visible actions. The set P of CSP expressions is defined inductively by

0  ∈ P  (inaction)
a.P ∈ P for a ∈ A and P ∈ P  (action prefix)
P ⊓ Q ∈ P for P, Q ∈ P  (internal choice)
P □ Q ∈ P for P, Q ∈ P  (external choice)
P ∥_{S}Q ∈ P for P, Q ∈ P and S ⊆ A (parallel composition)
P \a ∈ P for P ∈ P and a ∈ A  (abstraction)

Roughly, the meaning of these process constructions is as follows. The process 0 never performs any actions. a.P denotes a process which first performs the action a and then behaves as P. P ⊓ Q is a process that first makes a choice between P and Q and subsequently behaves like the chosen process. P □ Q is a process that behaves either like P or like Q, the choice being made by the occurrence of any visible action of either P or Q, which in turn may be influenced by the environment. P ∥_{S}Q denotes the parallel composition of processes P and Q. Actions a ∈ S enforce synchronisation between P and Q; they can only happen when both arguments can partake in performing them. Actions a ∉ S of either P and Q will be interleaved. P \a behaves like P, but with the action a made invisible or internal.

The following operational semantics of CSP stems from Olderog and Hoare [15]; it is shown to be consistent with the original denotational semantics of Hoare, Brookes & Roscoe [7]. It models the making of an internal choice through an internal action τ ∉A and captures the interplay between internal and external choice by assuming that in P □Q, as long as no visible actions occurs, the internal actions of P and Q happen in parallel. Below, a and b range over Act = A ._{∪} {τ}.

a.x_{1} ⟶^{a} x_{1}  x_{1} ⊓ x_{2} ⟶^{τ} x_{1}  x_{1} ⊓ x_{2} ⟶^{τ} x_{2}

\frac{x_{1} ⟶^{a} y_{1}}{x_{1} □ x_{2} ⟶^{a} y_{1}} (a ≠ τ) \frac{x_{2} ⟶^{a} y_{2}}{x_{1} □ x_{2} ⟶^{a} y_{2}} (a ≠ τ) \frac{x_{1} ⟶^{τ} y_{1}}{x_{1} □ x_{2} ⟶^{τ} y_{1} □ x_{2}} \frac{x_{2} ⟶^{τ} y_{2}}{x_{1} □ x_{2} ⟶^{τ} x_{1} □ y_{2}}

\frac{x_{1} ⟶^{a} y_{1}}{x_{1}∥_{S}x_{2} ⟶^{a} y_{1}∥_{S}x_{2}} (a ∉ S) \frac{x_{2} ⟶^{a} y_{2}}{x_{1}∥_{S}x_{2} ⟶^{a} x_{1}∥_{S}y_{2}} (a ∉ S) \frac{x_{1} ⟶^{a} y_{1} x_{2} ⟶^{a} y_{2}}{x_{1}∥_{S}x_{2} ⟶^{a} y_{1}∥_{S}y_{2}} (a ∈ S)

\frac{x_{1} ⟶^{a} y_{1}}{x_{1}\a ⟶^{τ} y_{1}\a} \frac{x_{1} ⟶^{b} y_{1}}{x_{1}\a ⟶^{b} y_{1}\a} (b ≠ a)

This makes CSP into a WB cool GSOS language. Hence, \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η} and \underline{↔}_{b} are congruences on this language.

Example 2 The GSOS language with 0, action prefix operators a.P for a ∈ Act and the unary operator n with rules \frac{x_{1}⟶^{τ}y_{1}}{n(x_{1})⟶^{τ}n(y_{1})} and \frac{x_{1}−̸→^{a}}{n(x_{1})⟶^{c}0} (for a specific action a) is not positive, but otherwise meets the requirements of Definition 8. Yet, \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η} and \underline{↔}_{b} fail to be congruences on this language. Namely a.0 \underline{↔}_{b} τ.a.0 yet n(a.0)\underline{↮}_{w} n(τ.a.0), as only the latter process can perform a c-transition. (Here I use that \underline{↔}_{b} is the finest equivalence of \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η} and \underline{↔}_{b}, and \underline{↔}_{w} the coarsest. Thus we have a.0\underline{↔}_{x} τ.a.0 yet n(a.0)\underline{↮}_{x} n(τ.a.0) for any x ∈ \{w, d, η, b\}.) This shows that the requirement that L be positive cannot simply be skipped.

Example 3 An operator q with a rules \frac{x_{1}⟶^{τ}y_{1}}{q(x_{1})⟶^{τ}q(y_{1})} and \frac{x_{1}⟶^{a}y, x_{1}⟶^{b}z}{q(x_{1})⟶^{c}q(y)} (for three specific actions

a, b, c ∈ A) would not be straight, although it satisfies the other requirements of Definition 8. A process p with p ⟶^{a} q and p ⟶^{b} r (and no other outgoing transitions) is branching bisimilar to processes p′ as well as p′′ with p′ ⟶^{τ} p′′, p′′ ⟶^{τ} p′, p′ ⟶^{a} q and p′′ ⟶^{b} r (and p′ and p′′ having no other outgoing transitions). Yet q(p) can do a c-action, whereas q(p′) cannot. This shows that in general \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η} and \underline{↔}_{b} fail to be congruences on languages incorporating this operator. Hence requirement 1 of Definition 8 cannot be skipped.

Example 4 The GSOS language with 0, action prefix operators a.P for a ∈ Act and the unary operator m with rules \frac{x_{1}⟶^{τ}y_{1}}{m(x_{1})⟶^{τ}m(y_{1})} and \frac{x_{1}⟶^{τ}y_{1}}{m(x)⟶^{c}m(y_{1})} fails requirement 2 of Definition 8 only. As

0 \underline{↔}_{b} τ.0 but m(0)\underline{↮}_{w} m(τ.0), given that only the latter process can do a c-transition, \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η} and \underline{↔}_{b} fail to be congruences on this language. Thus also requirement 2 cannot be skipped.

Example 5 The GSOS language with 0, action prefix operators a.P for a ∈ Act and the unary operator i with rule \frac{x_{1}⟶^{a}y_{1}}{i(x)⟶^{c}0}, and no patience rule, fails requirement 3 of Definition 8 only, con-

sidering that the argument of i is active but not receiving. As a.0 \underline{↔}_{b} τ.a.0 but i(a.0)\underline{↮}_{w} i(τ.a.0), given that only the former process can ever do a c-transition, \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η} and \underline{↔}_{b} fail to be congruences on this language. Thus also requirement 3 cannot be skipped.

Example 6 The GSOS language with 0, □, ⊓, action prefix operators a.P for a ∈ Act and the unary operators f, g with rules \frac{x_{1}⟶^{τ}y_{1}}{f(x_{1})⟶^{τ}f(y_{1})}, \frac{x_{1}⟶^{a}y_{1}}{f(x_{1})⟶^{a}g(y_{1})} and g(x) ⟶^{c} x, fails requirement 4 of Definition 8 only, considering that the argument of g is receiving but not active. Hence \underline{↔}_{d} and \underline{↔}_{b} are congruences on this language. One has a.(b.0 ⊓ d.0)\underline{↔}_{η} a.(b.0 ⊓ d.0) □ a.b.0, yet

f(a.(b.0 ⊓ d.0))\underline{↔} a.c.(b.0 ⊓ d.0)\underline{↮}_{w} a.c.(b.0 ⊓ d.0) □ a.c.b.0\underline{↔} f(a.(b.0 ⊓ d.0) □ a.b.0)

given that only the right-hand process can do an a-transition (possibly followed or preceded by internal actions) and reach a state in which the possibility to ever do a d-transition is ruled out. Hence \underline{↔}_{w} and \underline{↔}_{η} fail to be congruences on this language. Thus also requirement 4 cannot be skipped for the simply WB and HB cool formats.

Example 7 An example of a straight but not smooth operator is the operator s of [12, Section 10(4)] that allows a process (its argument) to proceed normally, but in addition can report that the process is ready to perform a visible action, without actually doing it. It supposes an alphabet Act = L ._{∪} {Can do ‘a’ | a ∈ L} ._{∪} {τ}, and its rules are

\frac{x ⟶^{a} y}{s(x) ⟶^{a} s(y)} (a ∈ Act) \frac{x ⟶^{a} y}{s(x) ⟶^{Can do ‘a’} s(x)} (a ∈ L)

It is not smooth because in the latter rule x occurs in the target as well as in the left-hand side of its premise. The GSOS language that combines this operator with 0, action prefix operators a.P for a∈Act, and constants p and q with rules p ⟶^{a} 0, p ⟶^{τ} b.0, q ⟶^{a} 0, q ⟶^{τ} b.0 and q ⟶^{b} 0, satisfies requirements 1–4 of Definition 8 but not requirement 5. Hence \underline{↔}_{η} and \underline{↔}_{b} are congruences on this language. Yet \underline{↔}_{d} and \underline{↔}_{w} are not, for p \underline{↔}_{d} q whereas s(p)\underline{↮}_{w} s(q). Namely only s(q) can report “can do ‘b’” and then do a (see Figure 7 in [12]). Thus also requirement 5 cannot be skipped for the simply WB and DB cool formats.

Lemma 1 Suppose L satisfies Clause 4 in the definition of simply WB cool above, and let μ, ν be closed substitutions. If μ(y) ⟹ ν(y) for every y ∈ var(t) that is receiving in t, and μ(x) = ν(x) for every x ∈ var(t) that is not receiving in t, then μ(t) ⟹ ν(t).

Proof: By structural induction on t. If t is a variable, the statement follows by assumption. Otherwise, t = f(t_{1}, …, t_{n}). It suffices to show that for i = 1, …, n one has

f(ν(t_{1}), ..., ν(t_{i−1}), μ(t_{i}), μ(t_{i+1}), ..., μ(t_{n})) ⟹ f(ν(t_{1}), ...ν(t_{i−1}), ν(t_{i}), μ(t_{i+1}), ..., μ(t_{n})). (5)

If t_{i} contains no variable that is receiving in t, then μ(t_{i}) = ν(t_{i}) by assumption, which yields (5). If t_{i} does contain such a variable, then, by definition, i is a receiving argument of f. By induction, μ(t_{i}) ⟹ ν(t_{i}), and the patience rule for the i^{th} argument of f yields (5). □

Proof of Lemma WB: Let L be simply WB cool, let r = \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} be a rule in L and let μ, ν be closed substitutions such that

• ν(x_{i}) ⟹ μ(x_{i}) ⟶^{(c_{i})} μ(y_{i}) ⟹ ν(y_{i}) for i∈I,

• ν(x) = μ(x) for all variables x that do not occur in the premises of r.

I need to show that ν(f(x_{1}, …, x_{n})) ⟹⟶^{(a)}⟹ ν(t).

In case r is a patience rule—so I = {k}, c_{k} = τ and t = f(x_{1}, …, x_{n})[y_{k}/x_{k}] with 1 ≤ k ≤ n—

one has ν(f(x_{1}, ..., x_{n})) ⟹ μ(f(x_{1}, ..., x_{n})) ⟶^{(τ)} μ(f(x_{1}, ..., x_{n})[y_{k}/x_{k}]) ⟹ ν(f(x_{1}, ..., x_{n})[y_{k}/x_{k}])

by repeated application of r.

Otherwise, ⟶^{(c)} = ⟶^{c} by Clause 2 of Definition 8. Now ν(f(x_{1}, …, x_{n})) ⟹ μ(f(x_{1}, …, x_{n})) by Clause 3, and μ(f(x_{1}, …, x_{n})) ⟶^{a} μ(t) by application of r. Clause 5 yields that μ(x) = ν(x) for all variables x ∈ var(t) that are not receiving in t, so μ(t) ⟹ ν(t) by Lemma 1. □

The Proof of Lemma DB proceeds likewise, but taking μ(x) = ν(x) for all variables x that do not occur in the left-hand side of premises. Clause 5 now implies that μ(t) = ν(t). □

Proof of Lemma HB: Let L be simply HB cool, let r = \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} be a rule in L and let ρ, μ, ν be closed substitutions such that

• ρ(x_{i}) ⟹ ν(x_{i}) ⟶^{(c_{i})} μ(y_{i}) ⟹ ν(y_{i}) for i∈I,

• ρ(x_{i}) = ν(x_{i}) = μ(x_{i}) for i∉I, and

• ν(x) = μ(x) for all variables x that do not occur as right-hand sides of premises in H.

I need to show that ρ(f(x_{1}, …, x_{n})) ⟹ ν(f(x_{1}, …, x_{n})) ⟶^{(a)}⟹ ν(t).

Note that ν(f(x_{1}, …, x_{n})) = μ(f(x_{1}, …, x_{n})).

In case r is a patience rule—so I = {k}, c_{k} = τ and t = f(x_{1}, …, x_{n})[y_{k}/x_{k}] with 1 ≤ k ≤ n—

one has ρ(f(x_{1}, ..., x_{n})) ⟹ ν(f(x_{1}, ..., x_{n})) ⟶^{(τ)} μ(f(x_{1}, ..., x_{n})[y_{k}/x_{k}]) ⟹ ν(f(x_{1}, ..., x_{n})[y_{k}/x_{k}])

by repeated application of r.

Otherwise, ⟶^{(c)} = ⟶^{c} by Clause 2 of Definition 8. Now ρ(f(x_{1}, …, x_{n})) ⟹ ν(f(x_{1}, …, x_{n})) by Clause 3, ν(f(x_{1}, …, x_{n})) ⟶^{a} μ(t) by application of r; and μ(t) ⟹ ν(t) by Lemma 1. □

The Proof of Lemma BB proceeds likewise, but omitting μ. □

5 Cool GSOS languages

In this section I will extend the simply XB cool rule formats to XB cool rule formats and establish the associated congruence theorems (X∈ {W,D,H,B}).

Definition 9 A GSOS language is two-tiered if its operators are partitioned into abbreviations and principal operators, and for every abbreviation f a principal operator f^{⋆} is specified, together with a substitution σ_{f} : {x_{1}, …, x_{ar(f^{⋆})}} → {x_{1}, …, x_{ar(f)}}, such that the rules of f are

\{\frac{σ_{f}(H)}{f(x_{1}, …, x_{ar(f)}) ⟶^{a} σ_{f}(t)} | \frac{H}{f^{⋆}(x_{1}, …, x_{ar(f^{⋆})}) ⟶^{a} t} is a rule of f^{⋆} \} .

Write f(i) for the j such that σ_{f}(x_{i}) = x_{j}; take f^{⋆} = f and f(i) = i in case f is a principal operator.

Trivially, any positive GSOS language can be extended (straightened) to a two-tiered GSOS language whose principal operators are (straight and) smooth [1].

Example 8 Let L have a binary operator f with as only rule \frac{x_{1}⟶^{a}y, x_{1}⟶^{b}z}{f(x_{1},x_{2})⟶^{a}f(x_{1},(f(y,x_{2}))}.

Then L can be straightened by adding a operator f^{⋆} with rule \frac{x_{1}⟶^{a}y, x_{2}⟶^{b}z}{f^{⋆}(x_{1},x_{2},x_{3},x_{4})⟶^{a}f(x_{3},f(y,x_{4}))}. In this case σ_{f}(x_{4}) = x_{2} and σ_{f}(x_{1}) = σ_{f}(x_{2}) = σ_{f}(x_{3}) = x_{1}.

Equally trivial, f(p_{1}, ..., p_{ar(f)}) ⟶^{a} t iff f^{⋆}(p_{f(1)}, ..., p_{f(ar(f^{⋆}))}) ⟶^{a} t;

so f(p_{1}, ..., p_{ar(f)})\underline{↔} f^{⋆}(p_{f(1)}, ..., p_{f(ar(f^{⋆}))}).

Definition 10 A two-tiered GSOS language L is WB cool if it is positive and

1. all principal operators in L are straight,

2. patience rules are the only rules of principal operators with τ-premises,

3. every active argument of a principal operator has a patience rule,

4. if argument f(i) of operator f is receiving, then argument i of f^{⋆} has a patience rule,

5. all principal operators in L are smooth.

The formats DB cool, HB cool and BB cool are defined likewise, but skipping Clause 4 for DB and BB, and Clause 5 for HB and BB. Clause 4 may be weakened slightly; see Section 5.2.

Note that the simply cool formats defined before are exactly the cool formats with the extra restriction that all operators are principal.

Theorem 3 On any WB cool GSOS language, weak bisimulation equivalence is a congruence. On any DB cool GSOS language, delay bisimulation equivalence is a congruence. On any HB cool GSOS language, η-bisimulation equivalence is a congruence. On any BB cool GSOS language, branching bisimulation equivalence is a congruence.

Given that the cool GSOS languages differ from the simply cool GSOS languages only by the addition of operators that can be regarded as syntactic sugar, the theorems above are a simple consequence of the corresponding theorems for simply cool GSOS languages. Below I go through the details.

Definition 11 Let L be a two-tiered GSOS language, with signature Σ. Let Σ^{⋆} be the subcollection of principal operators in Σ, and Σ^{∗} = {f^{∗} | f ∈ Σ^{⋆}} be a collection of fresh names for the latter. For f ∈ Σ an abbreviation, write f^{∗} for (f^{⋆})^{∗}. Define the translation ^{∗} : T (Σ) → T (Σ^{∗}) recursively by x^{∗} = x for x ∈ V and (f(t_{1}, …, t_{ar(f)}))^{∗} = f^{∗}(t_{f(1)}^{∗}, …, t_{f(ar(f^{∗}))}^{∗}). Let L^{∗} be the GSOS language

with signature Σ^{∗} and rules _{\frac{H}{f^{∗}(x_{1},...,x_{ar(f)})⟶^{a}t^{∗}}} for f ∈ Σ^{⋆} and _{\frac{H}{f(x_{1},...,x_{ar(f)})⟶^{a}t}} a rule of L.

Observation 1 Let L be XB cool, with X∈ {W,D,H,B}. Then L^{∗} is simply XB cool.

Any equivalence relation ∼ on processes defined in terms of the transitions between them, naturally extends to an equivalence relation on the disjoint union of T (Σ) and T (Σ^{∗}), with L generating the transitions between processes from T (Σ) and L^{∗} generating the transitions between processes from T (Σ)^{∗} (see Definition 4).

Lemma 2 Let L be a two-tiered GSOS language, with signature Σ. Then p^{∗} ⟶^{a}_{L^{∗}} p′_{next} iff ∃p_{next}(p′_{next} = p_{next}^{∗} ∧ p ⟶^{a}_{L} p_{next}).

Proof: Note that any term in L^{∗} has the form t^{∗}, with t a term in L, uniquely determined by t^{∗}. Using this, the statement of the lemma can be simplified to p^{∗} ⟶^{a}_{L^{∗}} p_{next}^{∗} iff p ⟶^{a}_{L} p_{next}.

“If”: Suppose p^{∗} ⟶^{a}_{L^{∗}} p_{next}^{∗}. Let p^{∗} := f^{∗}(p_{1}^{∗}, ..., p_{n}^{∗}). By Definition 4, L^{∗} has a transition rule \frac{H}{f^{∗}(x_{1},...,x_{n})⟶^{a}t^{∗}} and there is a closed substitution σ^{∗} : V → T T(Σ^{∗}) with σ^{∗}(x_{i}) = p_{i}^{∗} for

i = 1, ..., n and σ^{∗}(t^{∗}) = p_{next}^{∗}, such that p_{i}^{∗} ⟶^{c}_{L} σ^{∗}(y) for (x_{i} ⟶^{c} y) ∈ H and ¬∃r^{∗}(p_{i}^{∗} ⟶^{c}_{L} r^{∗})

for (x_{i} −̸→^{c}) ∈ H. Let σ : V → T T(Σ) be the closed substitution with σ^{∗}(x) = σ(x)^{∗} for all x ∈ V. Then σ(t) = p_{next}. By induction, p_{i} ⟶^{c}_{L} σ(y) for (x_{i} ⟶^{c} y) ∈ H and ¬∃r(p_{i} ⟶^{c}_{L} r) for (x_{i} −̸→^{c}) ∈ H. Using Definition 11, L must have a transition rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t}. So by Definition 4,

p = f(p_{1}, ..., p_{n}) ⟶^{a}_{L} p_{next}.

“Only if”: Suppose p ⟶^{a}_{L} p_{next}. Let p := f(p_{1}, ..., p_{n}). I first deal with the case that f ∈ Σ^{⋆}. By Definition 4, L has a transition rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t} and there is a closed substitution σ : V → T T(Σ)

with σ(x_{i}) = p_{i} for i = 1, ..., n and σ(t) = p_{next}, such that p_{i} ⟶^{c}_{L} σ(y) for (x_{i} ⟶^{c} y) ∈ H and ¬∃r(p_{i} ⟶^{c}_{L} r) for (x_{i} −̸→^{c}) ∈ H. Let σ^{∗} : V → T T(Σ^{∗}) be the closed substitution with σ^{∗}(x) = σ(x)^{∗} for all x ∈ V. Then σ^{∗}(t^{∗}) = p_{next}^{∗}. By induction, p_{i}^{∗} ⟶^{c}_{L} σ^{∗}(y) for (x_{i} ⟶^{c} y) ∈ H and ¬∃r^{∗}(p_{i}^{∗} ⟶^{c}_{L} r^{∗}) for (x_{i} −̸→^{c}) ∈ H. Using Definition 11, L^{∗} must have a transition rule

\frac{H}{f^{∗}(x_{1},...,x_{n})⟶^{a}t^{∗}}. So by Definition 4, p^{∗} = f^{∗}(p_{1}^{∗}, ..., p_{n}^{∗}) ⟶^{a}_{L^{∗}} p_{next}^{∗}.

Next, consider the case that f ∉ Σ^{⋆}. Then q ⟶^{a}_{L} p_{next} with q := f^{⋆}(p_{f(1)}, ..., p_{f(ar(f^{⋆}))}). As f^{⋆} ∈ Σ^{⋆}, the previous case of this proof yields q^{∗} ⟶^{a}_{L^{∗}} p_{next}^{∗}. But p^{∗} = f^{∗}(t_{f(1)}^{∗}, …, t_{f(ar(f^{∗}))}^{∗}) = q^{∗}, by Definition 11. □

Corollary 1 Let L be a two-tired GSOS language, and ∼ be any equivalence relation on processes satisfying p\underline{↔} q ⇒ p ∼ q. Then p^{∗} ∼ q^{∗} iff p ∼ q.

Proof: We have p \underline{↔} p^{∗} for all p ∈ T (Σ), because the relation \{(p, p^{∗}), (p^{∗}, p) | p ∈ T (Σ)\} is a strong bisimulation by Lemma 2. Hence if p ∼ q then p^{∗} \underline{↔} p ∼ q \underline{↔} q∗, implying p^{∗} ∼ q^{∗}, and if p^{∗} ∼ q^{∗} then p\underline{↔} p^{∗} ∼ q^{∗} \underline{↔} q, implying p ∼ q. □

Corollary 2 Let L be a two-tiered GSOS language such that ∼ is a congruence on L^{∗}, for ∼ an equivalence relation satisfying p\underline{↔} q ⇒ p ∼ q. Then ∼ is a congruence on L.

Proof: Let ar(f) = n. Suppose p_{i} ∼ q_{i} for i = 1, ..., n. By Corollary 1, p_{i}^{∗} ∼ q_{i}^{∗} for i = 1, ..., n. By assumption, (f(p_{1}, ..., p_{n}))^{∗} ∼ (f(q_{1}, ..., q_{n}))^{∗}. Thus, by Corollary 1, f(p_{1}, ..., p_{n}) ∼ f(q_{1}, ..., q_{n}). □

Proof of Theorem 3: Let L be XB cool, with X∈ {W,D,H,B}. By Observation 1, L^{∗} is simply XB cool. So by Theorem 2, \underline{↔}_{X} is a congruence on L^{∗}. Apply Corollary 2. □

In fact, Theorem 3 can be obtained as an instance of a more general theorem.

Theorem 4 Let ∼ be any equivalence relation on processes defined in terms of the transitions between them, satisfying p\underline{↔} q ⇒ p ∼ q, and let F be a format on transition system specifications, so that on any language in F -format, ∼ is a congruence. Define a two-tiered language L to be in the two-tiered F -format iff L^{∗} is in F -format. Now ∼ is a congruence on any language in the two-tiered F -format.

This follows by the very same proof as of Theorem 3. Note that the XB cool format is exactly the two-tiered simply XB cool format, for X ∈ {W, D, B, H}.

5.1 Bifurcation rules

Let L be BB cool. If argument f(i) of operator f is active, then argument i of f^{⋆} must also be active, so Clause 3 of Definition 10 says that f^{⋆} has a patience rule \frac{x_{i}⟶^{τ}y}{f^{⋆}(x_{1},...,x_{n})⟶^{τ}f^{⋆}(x_{1},...,x_{n})[y/x_{i}]}.

By Definition 9 this implies that f must have a rule \frac{x_{f(i)}⟶^{τ}y}{f(x_{1},...,x_{ar(f)})⟶^{τ}σ_{f} (f^{⋆}(x_{1},...,x_{n})[y/x_{i}])}.

This rule is called a bifurcation rule of f [5]. By Clause 2 of Definition 10, bifurcation rules are the only rules of f with τ-premises.

5.2 A small extension

Say that an argument i of an operator f is ignored if f^{⋆} has no argument k with f(k) = i. In that case there can be no rule with source f(x_{1}, …, x_{ar(f)}) with x_{i} in its premises or in its target. A subterm u of a term t is irrelevant if occurs within an ignored argument v_{i} of a subterm f(v_{1}, …, v_{ar(f)}) of t. Now Definition 7 of an argument of an operator being receiving may be strengthened by replacing “a subterm f(v_{1}, …, v_{n}) with x occurring in v_{i}” by “a relevant subterm f(v_{1}, …, v_{n}) with x a relevant subterm of v_{i}”. This yields a slight weakening of Clause 4 in Definition 10. The weakened clause is still sufficient to obtain Observation 1 and hence Theorem 3.

Example 9 Let L have a rule \frac{x_{1} ⟶^{a} y}{g(x_{1}) ⟶^{a} f(h(f(x_{1}, y)), k(y))}. By Definition 7 both the arguments

of h and k are receiving, so Clause 4 in Definition 10 demands patience rules for both h^{⋆} and k^{⋆}. Now suppose that h^{⋆} = h, k^{⋆} = k, ar(f^{⋆}) = 1 and σ_{f}(x_{1}) = x_{1}. This means that f(x_{1}, x_{2}) is an abbreviation for f^{⋆}(x_{1}) and the second argument of f is ignored. In such a case one has f(p, q) \underline{↔} f(p, r) for all closed terms p, q and r. Now the weakened Clause 4 does not demand a patience rule for either h^{⋆} or k^{⋆}, since the arguments of h and k are no longer receiving. Namely, y is an irrelevant subterm of f(x_{1}, y) and k(y) is an irrelevant subterm of f(h(f(x_{1}, y)), k(y)).

The remainder of this section establishes a result that helps to relate my formulation of the cool formats to Bloom’s [5]; for all other purposes it can be skipped. Proposition 1 below uses the concept of a ruloid; please consult Definition 14 and Example 10 in the next section first.

Above a definition of an argument of an operator being receiving was proposed that is more restrictive than Definition 7. This definition can be rephrased as follows.

Definition 12 Let L be a two-tiered GSOS language. Define the translation ^{⋆} : T (Σ) → T (Σ) recursively by x^{⋆} = x for x ∈ V and (f(t_{1}, …, t_{n}))^{⋆} = f^{⋆}(t_{f(1)}^{⋆}, …, t_{f(n)}^{⋆}).

An argument i ∈ IN of an operator f is truly receiving if a variable x is receiving in a term t that has a subterm v = f(v_{1}, …, v_{n}) with v^{⋆} a subterm of t^{⋆} and x ∈ var(v_{i}^{⋆}).

Here the requirement “v^{⋆} is a subterm of t^{⋆}” is equivalent to “v is a relevant subterm of t” and “x ∈ var(v_{i}^{⋆})” to “x is a relevant subterm of v_{i}”. Note that for any term u one has var(u^{⋆}) ⊆ var(u), but not always var(u^{⋆}) = var(u). In Example 9, y ∉ var(f(x_{1}, y)^{⋆}) = var(f^{⋆}(x_{1})) = {x_{1}} and k(y)^{⋆} = k(y) is not a subterm of f(h(f(x_{1}, y)), k(y))^{⋆} = f^{⋆}(h(f(x_{1}, y))^{⋆}).

The weakened version of Clause 4 of Definition 10 that was proposed above reads:

4^{G}. if argument f(i) of operator f is truly receiving, then argument i of f^{⋆} has a patience rule.

Here I reformulate this clause in such a way that it resembles the corresponding requirement in Bloom [5].

Definition 13 A term u ∈ T T(Σ) is univariate if no variable occurs more than once in u.

Trivially, any term can be written as σ(u) with u a univariate term and σ : V → V.

Proposition 1 In the definition of WB and HB cool GSOS languages, Clause 4^{G} is equivalent to

4^{B}. if x ∈ var(t) is receiving in t, u is a univariate term, y ∈ var(u), and σ : V → V is a substitution such that σ(u) = t^{⋆} and σ(y) = x, then there is an L-ruloid \frac{y⟶^{τ}z}{u⟶^{τ}u[z/y]}.

Proof: 4^{G} ⇒ 4^{B}: Suppose L satisfies Clause 4^{G}, x ∈ var(t) is receiving in t, u is a univariate term, y ∈ var(u), and σ : V → V is a substitution such that σ(u) = t^{⋆} and σ(y) = x. With structural induction on subterms w of u that contain y, I show that there is an L-ruloid \frac{y⟶^{τ}z}{w⟶^{τ}w[z/y]}. For every

such w there is a subterm v of t with σ(w) = v^{⋆} a subterm of t^{⋆} and x ∈ var(t^{⋆}). Base case: w = y. By definition, there is a ruloid \frac{y⟶^{τ}z}{y⟶^{τ}z}. Induction step: Let v = f(v_{1}, …, v_{ar(f)}) and w = f^{⋆}(w_{1}, …, w_{n}), and let i ∈ {1, …, n} be the unique argument of f^{⋆} with y ∈ var(w_{i}). Then σ(w_{i}) = v_{f(i)}^{⋆}, so x ∈ var(v_{f(i)}^{⋆}) ⊆ var(v_{f(i)}). Thus f(i) is a truly receiving argument of f, and L has a patience rule \frac{x_{i}⟶^{τ}z′}{f^{⋆}(x_{1},...,x_{n})⟶^{τ}f^{⋆}(x_{1},...,x_{n})[z′/x_{i}]}. By induction, there is an L-ruloid \frac{y⟶^{τ}z}{w_{i}⟶^{τ}w_{i}[z/y]}, so by Definition 14 one obtains the required L-ruloid

\frac{y⟶^{τ}z}{f^{⋆}(w_{1},...,w_{n})⟶^{τ}f^{⋆}(w_{1},...,w_{n})[z/y]}.

4^{B} ⇒ 4^{G}: Suppose L satisfies Clause 4^{B}, and argument f(i) of operator f is truly receiving. Then there must be a term t with a subterm v = f(v_{1}, …, v_{ar(f)}) such that v^{⋆} is a subterm of t^{⋆} and variable x ∈ var(v_{f(i)}^{⋆}) is receiving in t. Let u be a univariate term, and σ : V → V a substitution such that σ(u) = t^{⋆}. Let w = f^{⋆}(w_{1}, …, w_{n}) be the subterm of u with σ(w) = v^{⋆}. Then σ(w_{i}) = v_{f(i)}^{⋆}, and w_{i} (and hence u) must contain a variable y with σ(y) = x. By Clause 4^{B} there is an L-ruloid \frac{y⟶^{τ}z}{u⟶^{τ}u[z/y]}. By Clause 2 of Definition 10, patience rules are the only rules for the operators of u with τ-premises. Hence, by Definition 14, this ruloid can only be obtained by stacking patience rules. As u is univariate, its subterm w_{i} contains the only occurrence of y in u, so one of the patience rules applied must be the one for argument i of f^{⋆}. □

6 Rooted cool GSOS languages

In this section I will define the (simply) RWB, RDB, RHB and RBB cool rule formats and establish the associated congruence theorems. In order to formulate the requirements for the RWB and RDB cool GSOS languages I need the concept of a ruloid, this being a kind of derived GSOS rule.

Definition 14 For r transition rule, let RHS(r) denote the set of right-hand sides of its premises. Let L be a positive GSOS language. The class of L-ruloids is the smallest set of rules such that

• \frac{x⟶^{a}y}{x⟶^{a}y} is an L-ruloid, for every x, y ∈ V and a ∈ Act;

• if σ is a substitution, L has a rule \frac{H}{s⟶^{a}t}, and for every premise x ⟶^{c} y in H there is an L-ruloid r_{y} = \frac{H_{y}}{σ(x)⟶^{c}σ(y)} such that the sets RHS(r_{y}) are pairwise disjoint and each RHS(r_{y}) is disjoint

with var(σ(s)), then the transition rule ^{\frac{⋃_{y∈H} H_{y}}{σ(s)⟶^{a}σ(t)}} is an L-ruloid.

Note that a transition α, seen as a rule \frac{∅}{α}, is an L-ruloid iff it is generated by L in the sense of Definition 4. The left-hand sides of premises of a ruloid are variables that occur in its source, and the right-hand sides are variables that are all distinct and do not occur in its source. Its target only contains variables that also occur elsewhere in the rule.

Example 10 Let L contain the rule \frac{x_{1} ⟶^{a} y_{1} x_{2} ⟶^{b} y_{2}}{f(x_{1}, x_{2}) ⟶^{a} g(x_{1}, y_{1})}.

Then L has ruloids \frac{x ⟶^{a} x′ y ⟶^{b} y′}{f(x, y) ⟶^{a} g(x, x′)} and \frac{x ⟶^{a} x′ y ⟶^{b} y′ z ⟶^{b} z′}{f(f(x, y), z) ⟶^{a} g(f(x, y), g(x, x′))}.

Lemma 3 Suppose an L-ruloid has a premise with right-hand side x and a target t containing a subterm f(t_{1}, …, t_{n}) with x ∈ var(t_{i}). Then i is a receiving argument of f.

Proof: By Definition 14 there must be terms w_{1}, …, w_{n}, variables y_{1}, …, y_{n}, and substitutions σ_{1}, …, σ_{n}, such that t=σ_{1}(w_{1}), y_{i} is receiving in w_{i} (i=1, ..., n), σ_{i}(y_{i})=σ_{i+1}(w_{i+1}) (i=1, ..., n−1), and σ_{n}(y_{n}) = x; and moreover one of the w_{k} has a subterm f(w_{k}^{1}, …, w_{k}^{m}) with y_{k} ∈ var(w_{k}^{i}). It follows that i is an receiving argument of f. □

Definition 15 A GSOS language L is RWB cool if the operators can be partitioned in tame and wild ones, such that

1. the target of every rule contains only tame operations;

2. the sublanguage L^{tame} of tame operators in L is WB cool;

3. L is positive, and for each rule \frac{H}{s⟶^{a}t} there is a term u and a substitution σ : var(u) → var(s) such that

– there is an L-ruloid \frac{K}{u⟶^{a}v} with σ(K) = H and σ(v) = t,

– and for every premise x ⟶^{c} y in K, L has a rule \frac{σ(x)⟶^{τ}y}{s⟶^{τ}σ(u[y/x])};

(4. if argument f(i) of operator f is receiving in L, then argument i of f^{⋆} has a patience rule.)

The formats RDB cool, RHB cool and RBB cool are defined likewise, adapting “WB cool” in the second clause appropriately, but skipping the third clause for RHB and RBB, and the last one for RDB and RBB. The last clause cannot be skipped for RHB. The simply RXB cool rule formats (X∈{W,D,H,B}) are obtained by requiring the sublanguage of tame operators to be simply XB cool.

Note that in the third clause, u, σ and the ruloid can always be chosen in such a way that v = t. The instance of this clause with s = f(x_{1}, …, x_{ar(f)}) for a tame operator f is redundant, as it vacuously holds when taking u^{⋆} = f^{⋆}(x_{1}, …, x_{ar(f^{⋆})}) and σ = σ_{f}; the rule required in the second subclause is then the bifurcation rule derived in Section 5.1.

The last clause above appeared before as Clause 4 in Definition 10 of the WB and HB cool formats. Given that a term with a receiving variable cannot contain wild operators, this clause is almost implied by Clause 2 above. All it adds, is that the requirement of Clause 4 for the sublanguage of tame operators applies to “receiving in L” instead of merely “receiving in L^{tame} ”. Thus, the rules for the wild operators help determine which variables in a term t count as receiving.

Proposition 2 In the definition of the RWB cool format above, the last clause is redundant.

Proof: Let argument i of operator f be L-receiving. I will show that it is already L^{tame}-receiving. Let t be a term with a subterm f(t_{1}, …, t_{n}) such that y ∈ var(t_{i}) and y is L-receiving in t. So there is a rule r = \frac{H}{f(x_{1},...,x_{n})⟶^{a}t} in L with y occurring as the right-hand side of a premise in H. Let u and σ be the term and substitution that must exists for r by the third clause of Definition 15. Definition 15 implies that the operators in u are tame, and there is an L-ruloid, hence an L^{tame}- ruloid, \frac{K}{u⟶^{a}v} with σ(K) = H and σ(v) = t. Let f(v_{1}, …, v_{n}) be the subterm of v with σ(v_{i}) = t_{i} for i = 1, …, n. By the third clause of Definition 3, y ∉ range(σ). Hence, as y ∈ var(σ(v_{i})), y ∈ var(v_{i}). Given that dom(σ) = var(u), σ does not effect the right-hand sides of K, so y is the right-hand side of a premise in K. By Lemma 3, i is an L^{tame}-receiving argument of f. □

When working with the slightly stronger definition of receiving contemplated in Section 5.2, the proof above remains valid with trivial adaptations.

Now I will prove the remaining lemmas of Section 3, thereby completing the proof of Theorem 2.

Proof of Lemma RHB: Let L be simply RHB cool, let r = \frac{H}{s⟶^{a}t} be a rule in L, and let ν

be a closed substitution such that ν(x) ⟶^{c}⟹ ν(y) for each positive premise x ⟶^{c} y in H and ¬∃r (ν(x) −̸→^{c} r) for each negative premise x −̸→^{c} in H. I need to show that ν(s) ⟶^{a}⟹ ν(t). By assumption, there is a closed substitution μ such that • ν(x) ⟶^{c} μ(y) ⟹ ν(y) for each premise x ⟶^{c} y in H, and

• ν(x) = μ(x) for all variables x that do not occur as right-hand sides of premises in H.

Thus ν(s) = μ(s) ⟶^{a} μ(t) by application of r, and μ(t) ⟹ ν(t) by Lemma 1. □

Lemma 4 Let L be simply WB cool, let r = \frac{H}{s⟶^{a}t} be an L-ruloid, and let ν be a closed substitution.

If for each premise x ⟶^{c} y in H one has ν(x) ⟹⟶^{c}⟹ ν(y), then ν(s) ⟹⟶^{a}⟹ ν(t).

Proof: The case that r is a rule in L is proven exactly as in Lemma WB, just writing a for (a), etc. The general case now follows by a straightforward structural induction on s. □

Proof of Lemma RWB: Let L be simply RWB cool, let r = \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a

closed substitution such that ν(x) ⟹⟶^{c}⟹ ν(y) for each premise x ⟶^{c} y in H. I need to show

that ν(s) ⟹⟶^{a}⟹ ν(t).

Case 1: Suppose that there is a closed substitution μ such that

• ν(x) ⟶^{c} μ(y) ⟹ ν(y) for each premise x ⟶^{c} y in H, and

• ν(x) = μ(x) for all variables x that do not occur as right-hand sides of premises in H.

Then ν(s) = μ(s) ⟶^{a} μ(t) by application of r, and μ(t) ⟹ ν(t) by Lemma 1. Case 2: Suppose that there is a premise x^{0} ⟶^{c} y^{0} in H such that ν(x^{0}) ⟶^{τ} p ⟹⟶^{c}⟹ ν(y^{0}) for a closed term p. Let u, σ and r′ = \frac{K}{u⟶^{a}v} be the term, substitution and ruloid that exists for r by the third clause of Definition 15, and let x^{1} be the unique variable in u such that K has a premise x^{1} ⟶^{c} y^{0} (using that σ(y^{0}) = y^{0}). Hence σ(x^{1}) = x^{0}. Let μ be the closed substitution with μ(y^{0}) = p and μ(z) = ν(z) for all variables z ≠ y^{0}. Now μ(σ(x^{1})) = μ(x^{0}) = ν(x^{0}) ⟶^{τ} μ(y^{0}).

By Clause 3 of Definition 15, L has a rule \frac{σ(x^{1})⟶^{τ}y^{0}}{s⟶^{τ}σ(u[y^{0}/x^{1}])}; hence ν(s) = μ(s) ⟶^{τ} μ(σ(u[y^{0}/x^{1}])).

Let ρ be the closed substitution with ρ(x^{1}) = p and ρ(z) = ν(σ(z)) for all variables z ≠ x^{1}. Then μ(σ(u[y^{0}/x^{1}]) = ρ(u), the operators in u are tame, and ρ(x) ⟹⟶^{c}⟹ ρ(y) for each premise x ⟶^{c} y in K. Lemma 4 yields ρ(u) ⟹⟶^{a}⟹ ρ(v). By Clause 5 of Definition 8, x^{1} ∉ var(v), so

ρ(v) = ν(σ(v)) = ν(t). Thus ν(s) = μ(s) ⟶^{τ} μ(σ(u[y^{0}/x^{1}])) = ρ(u) ⟹⟶^{a}⟹ ρ(v) = ν(t). □

The Proof of Lemma RDB proceeds likewise, using a DB cool counterpart of Lemma 4. □

This completes the Proof of Theorem 2. □

Example 11 The following fragment of CCS has the constant 0, unary operators a. , binary operators + and ∥ (usually written |), and instances of the GSOS rules below. Here a ranges over Act = N ._{∪} \overline{N} ._{∪} \{τ\} with N a set of names and \overline{N} = \{\overline{a} | a ∈ N \} the set of co-names. The function \overline{·} extends to N ∪ \overline{N} (but not to Act) by \overline{\overline{a}} = a.

\begin{matrix}\frac{x_{1} ⟶^{a} y_{1}}{x_{1} + x_{2} ⟶^{a} y_{1}} \frac{x_{2} ⟶^{a} y_{2}}{x_{1} + x_{2} ⟶^{a} y_{2}} a.x_{1} ⟶^{a} x_{1} \\ \frac{x_{1} ⟶^{a} y_{1}}{x_{1}∥x_{2} ⟶^{a} y_{1}∥x_{2}} & \frac{x_{2} ⟶^{a} y_{2}}{x_{1}∥x_{2} ⟶^{a} x_{1}∥y_{2}} & \frac{x_{1} ⟶^{a} y_{1} x_{2} ⟶^{\overline{a}} y_{2}}{x_{1}∥x_{2} ⟶^{τ} y_{1}∥y_{2}} \end{matrix}

The sublanguage without the + is simply WB cool, and the entire GSOS language is simply RWB cool. Clause 3 of Definition 15 applied to the i^{th} rule for the + is satisfied by taking u = x, σ(x) = x_{i}, and the ruloid \frac{x⟶^{a}y_{i}}{x⟶^{a}y_{i}}; indeed the language has a ruloid \frac{x_{i}⟶^{τ}y_{i}}{x_{1}+x_{2}⟶^{τ}y_{i}}.

Example 12 Extend the GSOS language of Example 11 with the binary operators ∥− and | with

rules \frac{x_{1} ⟶^{a} y_{1}}{x_{1}∥−x_{2} ⟶^{a} y_{1}∥y_{2}} and \frac{x_{1} ⟶^{a} y_{1} x_{2} ⟶^{\overline{a}} y_{2}}{x_{1}|x_{2} ⟶^{τ} y_{1}∥y_{2}} with a ranging over Act. These are the left merge

and the communication merge of Bergstra & Klop [3] but adapted to fit (the communication format of) CCS rather then ACP. (I wrote ∥ for the CCS parallel composition to avoid name clashes with this communication merge.) In [3] these operators are introduced in order to give a finite complete equational axiomatisation of strong bisimulation equivalence on the language ACP, and the same approach works for CCS.

The first argument of ∥− and both arguments of | are active, whereas no arguments of ∥− and | are receiving. Since the active arguments of ∥− and | do not have patience rules, both operators need to be classified as wild. Requirements 1, 2 and 4 of Definition 15 are clearly satisfied. Hence this GSOS language is RHB cool, and \underline{↔}_{rη} and \underline{↔}_{rb} are congruences on the entire language.

Requirement 3 applied to the rule for the ∥− is satisfied by taking u = x∥x_{2}, σ(x) = x_{1},

σ(x_{2}) = x_{2} and the ruloid \frac{x ⟶^{a} y_{1}}{x∥x_{2} ⟶^{a} y_{1}∥x_{2}} . Indeed the language has a ruloid \frac{x_{1} ⟶^{τ} y_{1}}{x_{1}∥−x_{2} ⟶^{τ} y_{1}∥x_{2}} .

Hence the language with ∥− but without | is RWB cool, guaranteeing that also \underline{↔}_{rw} and \underline{↔}_{rd} are congruences. However, requirement 3 applied to either rule of the communication merge is not satisfied. In fact \underline{↔}_{rw} and \underline{↔}_{rd} fail to be congruences for this operator: one has τ.a.0\underline{↔}_{rd} τ.a.0+a.0 but

0\underline{↔} (τ.a.0|\overline{a}.b.0)\underline{↮}_{rw} ((τ.a.0 + a.0)|\overline{a}.b.0)\underline{↔} τ.b.0.

This shows that this part of requirement 3 of Definition 15 cannot be skipped.

Example 13 The GSOS language with 0, action prefix operators a.P for a ∈ Act and the unary operator np with the rule \frac{x_{1}−̸→^{a}}{np(x_{1})⟶^{c}0} (for specific actions a, c) is not positive, but otherwise meets the requirements of Definition 15. Yet, \underline{↔}_{rw} and \underline{↔}_{rd} fail to be congruences on this language. Namely τ.a.0 \underline{↔}_{rd} τ.a.0 + a.0 yet np(τ.a.0) \underline{↔} c.0\underline{↮}_{w} 0 \underline{↔} np(τ.a.0 + a.0). This shows that the requirement that L be positive cannot simply be skipped in the RWB and RDB cool formats.

Negative premises of wild operators are allowed in the RHB and RBB cool formats. This is possible because the first transitions of rooted branching (or η-)bisimilar processes need to be matched without preceding τ-transitions, just as for strong bisimulation. A good example of an RBB cool GSOS operator with negative premises is the initial priority operator of [8].

Example 14 The GSOS language L with 0, □, ⊓, action prefix operators a.P for a ∈ Act and the unary operators f, g with rules \frac{x_{1}⟶^{a}y_{1}}{f(x_{1})⟶^{a}g(y_{1})} and g(x) ⟶^{c} x (for specific actions a, c) satisfies requirements 1 and 2 of Definition 15, provided one classifies the argument of f as wild and that of g as tame. Hence \underline{↔}_{rb} is a congruence on L. However, L fails requirements 3 and 4. Here the argument of g is receiving in L as a whole, although not in L^{tame}. In fact, \underline{↔}_{rw} (, \underline{↔}_{rd}) and \underline{↔}_{rη} fail to be congruences on L. One has a.(b.0 ⊓ d.0)\underline{↔}_{η} a.(b.0 ⊓ d.0) □ a.b.0, yet

f(a.(b.0 ⊓ d.0))\underline{↔} a.c.(b.0 ⊓ d.0)\underline{↮}_{w} a.c.(b.0 ⊓ d.0) □ a.c.b.0\underline{↔} f(a.(b.0 ⊓ d.0) □ a.b.0)

as in Example 6. Thus requirement 4 cannot be skipped for the RHB cool format.

Theorem 5 On any RWB cool GSOS language, \underline{↔}_{rw} is a congruence.

On any RDB cool GSOS language, \underline{↔}_{rd} is a congruence.

On any RHB cool GSOS language, \underline{↔}_{rη} is a congruence.

On any RBB cool GSOS language, \underline{↔}_{rb} is a congruence.

Proof: Let L be RBB cool. Regard L as a two-tiered GSOS languages by classifying all wild operators as principal ones. The GSOS language L^{∗} constructed in Definition 11 is simply RBB cool, by Observation 1, so by Theorem 2RBB \underline{↔}_{rb} is a congruence on L^{∗}. Apply Corollary 2.

The other cases go likewise, except that in checking that L^{∗} is simply RWB or RDB cool, one has to check that Clause 3 of Definition 15 is satisfied. Let u and σ be a term and substitution that satisfy Clause 3 for a rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t} with f wild. I claim that u^{∗} and σ are appropriate

for the rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t^{∗}}, existing in L^{∗}. Namely, by a straightforward structural induction on u,

if \frac{K}{u⟶^{a}v} is an L-ruloid then \frac{K}{u^{∗}⟶^{a}v^{∗}} is an L^{∗}-ruloid. Moreover, σ(v) = t implies σ(v^{∗}) = t^{∗}. By

construction, for every premise x ⟶^{c} y in K, L^{∗} has a rule \frac{σ(x)⟶^{τ}y}{f(x_{1},...,x_{n})⟶^{τ}σ(u^{∗}[y/x])}. □

As the above shows, for X ∈ {W, D, B, H}, the RXB cool format is exactly the two-tiered simply RXB cool format, so Theorem 5 is obtained as an application of Theorem 4 to Theorem 2.

7 Comparison with Bloom’s formats

Not counting a host of notational differences, Bloom’s definitions of the cool formats differ in five ways from mine.

First of all Bloom requires bifurcation rules for all operators in L^{tame}, whereas I merely require patience rules for the principal operators. As principal operators in L^{tame} are straight, and bifurcation rules for straight operators are exactly patience rules, the difference is that I dropped the bifurcation requirement for abbreviations (non-principal operators). This is possible, because by Definition 9, which corresponds to Definition 3.5.5 in [5], the rules for the abbreviations are completely determined by the rules for their straightenings, and it turns out that a bifurcation rule of an abbreviation f is exactly what is determined by the corresponding patience rule for its straightening f^{⋆}.

Bloom’s WB cool format requires the existence of bifurcation/patience ruloids for receiving variables in any term, whereas I require them for receiving arguments of operators, which is a more syntactic and easy to check requirement. The two approaches are shown equivalent in Proposition 1 when using the extension of my formats of Section 5.2, this being the reason behind that extension.

Bloom’s WB and RWB cool formats use a so-called ε-presentation. This entails that rules may have premises of the form x ⟶^{ε} y. In terms of Definition 4, the meaning of such premises is given by the requirement that σ(x) = σ(y) for (x ⟶^{ε} y) ∈ H. By using ε-premises, any rule can be given a form in which the target is a univariate term, having no variables in common with the source. This allows a simplification of the statement of the bifurcation ruloids. Any ε-presented GSOS language can be converted to ε-free form by substitution, in each rule r, x for y for every premise

x ⟶^{ε} y of r.

Bloom’s rendering of the RWB cool format doesn’t feature Clause 4 (and in view of Proposition 2, neither does mine), but Clause 3 is much more involved. For every rule with conclusion s ⟶^{a} t Bloom requires the existence of two terms t_{1} and t_{2} and seven types of derived operational rules, such that the diagram

s  t t_{1}  t_{2}_{a}_{a}_{a}_{a}_{τ}  _{τ}_{τ}  _{τ}

on the right commutes. My Clause 3 stems from the observation that, given Bloom’s other restrictions, t necessarily has the rules required for t_{2}, so that one may always choose t_{2} = t. This leaves only t_{1} (called u in Definition 15) and three types of rules, one of which (the t_{1}-loop in the diagram above) is in fact a bifurcation rule whose existence is already implied by the requirements of Definition 10.

In Clause 3 of Definition 15, Bloom requires that

var(u) = \{y′ | y ∈var(t)\} and σ(y′) = \begin{cases}x if H contains a premise x ⟶^{c} y \\ y otherwise. \end{cases}  (6)

In order to match Bloom’s format I could have done the same, but this condition is not needed in the proof and reduces the generality of the format.

Example 15 Consider the following GSOS language, with unary operators f and g and constant 0.

f(x_{1}) ⟶^{b} x_{1}  \frac{x_{1} ⟶^{a} y_{1}}{f(x_{1}) ⟶^{a} 0} \frac{x_{1} ⟶^{τ} y_{1}}{f(x_{1}) ⟶^{τ} g(y_{1})} \frac{x_{1} ⟶^{a} y_{1}}{g(x_{1}) ⟶^{a} 0} \frac{x_{1} ⟶^{τ} y_{1}}{g(x_{1}) ⟶^{τ} g(y_{1})}

The sublanguage without f is simply WB cool, and the entire language simply RWB cool. In fulfilling Clause 3 of Definition 15 take for the first rule u := f(x_{1}) and for the second and third rules u := g(x_{1}), in each case with σ the identity.

However, this language is not RWB cool in the sense of Bloom, as the restriction above forbids rules \frac{H}{s⟶^{a}t} with H ≠ ∅ and var(t) = ∅, where the operator in s is wild.

Proposition 3 A GSOS language is WB cool, respectively RWB, BB or RBB cool, as defined here, with the extension of Section 5.2 and the restriction (6) above, iff it is WB cool, resp. RWB, BB or RBB cool, as defined in Bloom [5].

The proof consists of converting Bloom’s rule formats to ε-free form and eliminating a number of other notational differences, together with the issues addressed above. □

Moreover, my proofs that cool languages are compositional for bisimulation equivalences greatly simplify the ones of Bloom [5] by using a reduction of the general case to the simple case, instead of treating the general formats directly.

8 Cool GSOS languages with lookahead

The RWB cool format can be extended by allowing wild operators f, besides GSOS rules satisfying Clause 3 of Definition 15, also to have rules of which all premises have the form x ⟹⟶^{c} y with c ∈ A. For such rules Clause 3 is not required, but in fulfilling Clause 4, they do count in determining which arguments are receiving. A similar extension applies to the RDB cool format.

Definition 16 Let Σ be a signature. A GSOS rule with lookahead is an expression of the form \frac{H}{α} with α a positive Σ-literal (the conclusion) and H a set of expressions of the form x ⟹⟶^{a} y (the premises of the rule), satisfying the four conditions of Definition 3. A GSOS language with lookahead is a TSS whose rules are either GSOS rules or GSOS rules with lookahead. The transitions generated by a GSOS language with lookahead L are defined exactly as in Definition 4, where a premise (x_{i} ⟹⟶^{c} y) ∈ H gives rise to a hypothesis p_{i} ⟹_{L}⟶^{c}_{L} σ(y), using the relational composition of ⟹_{L} and ⟶^{c}_{L}. The notion of a receiving variable in term of Definition 7 extends straightforwardly to GSOS languages with lookahead.

Definition 17 A GSOS language with lookahead L is RWB cool if the operators can be partitioned in tame and wild ones, such that

1. the target of every rule contains only tame operations;

2. the sublanguage L^{tame} of tame operators in L is a WB cool GSOS language (without lookahead);

3. L is positive, and for each GSOS rule \frac{H}{s⟶^{a}t} (without lookahead) there is a term u and a substitution σ : var(u) → var(s) such that

– there is an L-ruloid \frac{K}{u⟶^{a}v} with σ(K) = H and σ(v) = t,

– and for every premise x ⟶^{c} y in K, L has a rule \frac{σ(x)⟶^{τ}y}{s⟶^{τ}σ(u[y/x])};

4. if argument f(i) of operator f is receiving in L, then argument i of f^{⋆} has a patience rule.

The format RDB cool is defined likewise, adapting “WB cool” in the second clause to “DB cool”, but skipping the last clause. The simply RXB cool rule formats (X∈ {W,D}) are obtained by requiring the sublanguage of tame operators to be simply XB cool.

With these definitions, Lemmas RWB and RDB extend to the case that L is a GSOS language with lookahead, using premises x ⟹⟶^{x} y in case of GSOS rules with lookahead. Namely, the statements quantify over rules in L; when such a rule is a GSOS rule, the proof given in Section 6 applies, and when it is a GSOS rule with lookahead, the statement follows from Definition 16 and Lemma 1.

Theorem 6 On any RWB cool GSOS language with lookahead, \underline{↔}_{rw} is a congruence. On any RDB cool GSOS language with lookahead, \underline{↔}_{rd} is a congruence.

Proof: Using the same argument as in the proof of Theorem 3 I may restrict attention to simply RWB or RDB cool GSOS languages with lookahead. Here the proof of Section 3 applies again. □

Example 16 Extend the GSOS language of Example 11 with the binary operator | and the single rule \frac{x_{1}⟹⟶^{a}y_{1} x_{2}⟹⟶^{\overline{a}}y_{2}}{x_{1}|x_{2}⟶^{τ}y_{1}∥y_{2}} . This is the variant of the communication merge of [3] (cf. Example 12),

given in Bergstra & Klop [4] (and here again adapted to fit CCS rather then ACP_{τ}). The result is a GSOS language with lookahead, that moreover is RWB cool. Thus \underline{↔}_{rw} and \underline{↔}_{rd} are congruences on this language. In [4] this variant of the communication merge is used as an auxiliary operator in giving a finite complete equational axiomatisation of \underline{↔}_{rw} on a language with ∥; this is not known to be possible using only auxiliary GSOS operators.

9 Turning GSOS Rules into Equations

This section recapitulates the method of [1] to provide finite equational axiomatisations of \underline{↔} on an augmentation of any given GSOS language.

Definition 18 A process p, being a closed term in a GSOS language, is finite if there are only finitely many sequences of transitions p ⟶^{a_{1}} p_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} p_{n}. The length n of the longest sequence of this form is called the depth of p.

Definition 19 An equational axiomatisation Ax over a signature Σ is a set of equations t = u, called axioms, with t, u ∈ T T(Σ). It respects an equivalence relation ∼ on T (Σ) if σ(t) ∼ σ(u) for any closed substitution σ : V → T (Σ).

An instance of axiom t = u is an equation σ(C[t/x]) = σ(C[u/x]) where σ is a substitution and C a term with var(C)={x}, and x occurring only once in C. An equation p = q is derivable from Ax, notation p =_{Ax} q, if there is a sequence p_{0}, …, p_{n} of terms with n ≥ 0 such that p = p_{0}, q = p_{n} and for i = 1, …, n the equation p_{i−1} = p_{i} is an instance of one of the axioms.

Ax is sound for ∼ if p =_{Ax} q implies p ∼ q for p, q ∈ T (Σ). Ax is complete for ∼ on finite processes if p ∼ q implies p =_{Ax} q for finite processes p and q.

Note that Ax is sound for ∼ iff Ax respects ∼ and ∼ is a congruence.

Definition 20 A GSOS language L extends BCCS (basic CCS) if it contains the operators 0, a. and + of Example 11. A basic process is a closed term build from the operators mentioned above only. A head normal form is a closed term of the form 0 + a_{1}.p_{1} + ⋯ + a_{n}.p_{n} for n ≥ 0. An axiomatisation on L is head normalising if any term f(p_{1}, …, p_{ar(f)}) with the p_{i} basic processes can be converted into head normal form.

Proposition 4 Let L be a GSOS language extending BCCS, and Ax a head normalising equational axiomatisation, respecting \underline{↔}, and containing the axioms A1–4 of Table 1. Then Ax is sound and complete for \underline{↔} on finite processes.

Proof: Using induction on the depth of p and a nested structural induction, the axioms can convert any finite process p into a basic process. Here one uses that strongly bisimilar processes have the same depth. Now apply the well-known fact that the axioms A1–4 are sound and complete for \underline{↔} on basic processes [13]. □

x + (y + z) = (x + y) + z A1  x∥y = x∥−y + y∥−x + x|y CM1
x + y = y + x  A2  a.x∥−y = a.(x∥y)  CM2
x + x = x  A3  0∥−y = 0  CM3
x + 0 = x  A4  (x + y)∥−z = x∥−z + y∥−z  CM4
a.x|\overline{a}.y = τ.(x∥y)  CM5
a.(τ.(x + y) + x) = a.(x + y) T1  a.x|b.y = 0  (if b ≠ \overline{a}) CM6
τ.x + x = τ.x  T2  0|x = x|0 = 0  CM7
a.(τ.x + y) + a.x = a.(τ.x + y) T3  (x + y)|z = x|z + y|z  CM8
x|(y + z) = x|y + x|z  CM9

Table 1: Complete equational axiomatisations of BCCS and the parallel composition For the parallel composition operator ∥ of CCS no finite equational head normalising axiomatisation respecting strong bisimulation equivalence exists [14]. However, Bergstra & Klop [3] gave such an axiomatisation on the language obtained by adding two auxiliary operators, the left merge ∥−

and the communication merge |, with rules \frac{x_{1} ⟶^{a} y_{1}}{x_{1}∥−x_{2} ⟶^{a} y_{1}∥x_{2}} and \frac{x_{1} ⟶^{a} y_{1} x_{2} ⟶^{\overline{a}} y_{2}}{x_{1}|x_{2} ⟶^{τ} y_{1}∥y_{2}} , provided

the alphabet Act of actions is finite. See Example 12. The axioms are CM1–9 of Table 1, in which + binds weakest and a. strongest, and a, b range over Act.

Aceto, Bloom & Vaandrager [1] generalise this idea to arbitrary GSOS languages with finitely many rules, each with finitely many premises, and assuming a finite alphabet Act. I recapitulate their method for positive languages only. A smooth operator (Definition 7) only

has rules of the form \frac{\{x_{i} ⟶^{c_{i}} y_{i} | i∈I\}}{f(x_{1}, …, x_{n}) ⟶^{a} t}. The trigger of such a rule is the partial function ↑_{r}:

{i, …, n} ⇀ Act given by ↑_{r} (i) = c_{i} if i∈I, and ↑_{r} (i) is undefined otherwise.

Definition 21 [1] A smooth GSOS operator f is distinctive, if no two rules of f have the same trigger, and the triggers of all rules of f have the same domain.

All operators of CCS, as well as ∥− and |, are smooth. The operators 0, a. , ∥− and | are distinctive, but ∥ is not. Its triggers have domains {1}, {2} and {1, 2}.

For every smooth and distinctive operator f, Aceto, Bloom & Vaandrager declare four types of axioms. First of all, for every rule r as above there is an axiom f(σ(x_{1}), …, σ(x_{n})) = a.σ(t), where σ : {x_{1}, …, x_{n}} → T T(Σ) is the substitution given by σ(x_{i}) = c_{i}.y_{i} for i ∈ I and σ(x_{i}) = x_{i} for i∉I. Such an axiom is called an action law. Examples are CM2 and CM5 in Table 1.

Secondly, whenever I is the set of active arguments of f, but f has no rule of the form above (where the name of the variables y_{i} is of no importance), there is an axiom f(σ(x_{1}), …, σ(x_{n})) = 0, with σ as above (for an arbitrary choice of distinct variables y_{i}). Such an axiom is an inaction law. An example is CM6. If f has k active arguments, in total there are |Act|^{k} action and inaction laws for f, one for every conceivable trigger with as domain the active arguments of f.

Finally, for any active argument i of f, there are laws

f(x_{1}, … x_{i−1}, 0, x_{i+1}, …, x_{n}) = 0 and
f(x_{1}, …, x_{i} + x′_{i}, …, x_{n}) = f(x_{1}, …, x_{i}, …, x_{n}) + f(x_{1}, …, x′_{i}, …, x_{n}).

Examples for the second type of inaction law are CM3 and CM7, and examples of distributivity laws are CM4, CM8 and CM9.

It is not hard to see that all axioms above respect \underline{↔} and that together they bring any term f(p_{1}, …, p_{ar(f)}) with the p_{i} basic processes in head normal form.

The method of [1] makes three types of additions to a given finite GSOS language L, and provides an equational head normalising axiomatisation on the resulting language, that respects strong bisimulation.

First of all, the operators 0, a. and + are added, if not already there. The corresponding axioms are A1–4 of Table 1. If all other operators are smooth and distinctive, for each of them the axioms just described are taken, which finishes the job. (In the presence of negative premises, this step is slightly more complex.)

In case there are operators f that are smooth but not distinctive, the set of operational rules of f is partitioned into subsets D such that no two rules in D have the same trigger, and the triggers of all rules in D have the same domain. Note that such a partition can always be found— possibly by taking exactly one rule in each subset D. Now for any subset D in the partition, an operator f_{D} with ar(f_{D}) = ar(f) is added to the language, whose rules are exactly the rules in that subset, but with f_{D} in the source. By definition, f_{D} is distinctive. Now add an axiom f(x_{1}, …, x_{ar(f)}) = ∑ f_{D}(x_{1}, …, x_{ar(f)}), where the sum is taken over all subsets in the partition, and apply the method above to the operators f_{D}. Again, it is trivial to check that the axioms respect \underline{↔} and are head normalising. Applied to the ∥ of CCS, this technique yields the left merge and communication merge as auxiliary operators, as well as a right merge, and the axiom CM1.

In case of operators f that are not smooth, a smooth operator f^{⋆} is added to L, of which f is an abbreviation in the sense of Definition 9 (cf. Example 8). The treatment of f^{⋆} proceeds as above, and the project is finished by the axiom

f(p_{1}, ..., p_{ar(f)}) = f^{⋆}(p_{f(1)}, ..., p_{f(ar(f^{⋆})))}).

Besides completeness for finite processes, using an infinitary induction principle the method of [1] even yields completeness for arbitrary processes. I will not treat this here, as it does not generalise to weak equivalences.

10 Turning Cool GSOS Rules into Equations

The method of [1] does not apply to \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η}, and \underline{↔}_{b}, because these equivalences fail to be congruences for the +. However, Bloom [5] shows that the method applies more or less verbatim to \underline{↔}_{rb}. This section observes that the same holds for \underline{↔}_{rη}, and finds an adaptation to yield finite equational axiomatisations of \underline{↔}_{rw} (resp. \underline{↔}_{rd}) that are sound and complete for finite processes on an augmentation of any RWB cool (resp. RDB cool) GSOS language.

On basic processes, the axioms A1–4 together with T1–T3 are complete for \underline{↔}_{rw} [13], whereas complete axiomatisations for \underline{↔}_{rd}, \underline{↔}_{rη} and \underline{↔}_{rb} are obtained by dropping T3, T2 or both, respectively [12]. So in order to get axiomatisations of these equivalences that are complete for finite processes, all that is needed is head normalisation. The simplest approach is to use the same head normalising axioms as in the previous section, reasoning that axioms that respect \underline{↔} surely respect a coarser equivalence like \underline{↔}_{rb} or \underline{↔}_{rw}. The only way this approach could fail is when the auxiliary operators generated by [1] fail to be congruences for the equivalence relation at hand. The operators 0, a. and + are WB cool, and thus unproblematic. As observed in [5], for any RBB cool GSOS language, the augmented language is also RBB cool. Namely, the new operators do not show up in targets of new rules, so classifying all auxiliary operators as wild is sufficient. Since the auxiliary operators do not increase the collection of receiving arguments of operators either, it follows likewise that for any RHB cool GSOS language, the augmented language is also RHB cool. Hence one obtains

Theorem 7 The method of [1], together with axiom T1 (and T3), yields finite equational axiomatisations of \underline{↔}_{rb} (resp. \underline{↔}_{rη}) that are sound and complete for finite processes on an augmentation of any RBB cool (resp. RHB cool) GSOS language. □

For \underline{↔}_{rw} and \underline{↔}_{rd} this approach fails. In particular, these equivalences fail to be congruences for the communication merge, as shown in Example 12.

Conjecture. There exists no GSOS language including the parallel composition of CCS and ≥ 2 visible actions that admits a finite equational axiomatisation of weak bisimulation equivalence that is sound and complete for finite processes.

Nevertheless, such an axiomatisation was found by Bergstra & Klop [4], using a variant of the communication merge that is not a GSOS operator; cf. Example 16. Their axiomatisation of ∥ is obtained from the one in Table 1 by requiring a, b ≠ τ in CM6, and adding the axioms τ.x|y = x|τ.y = x|y. Here I generalise their approach to arbitrary RWB cool (or RDB cool) GSOS languages.

In an RWB (or RDB) cool language, the smooth operators f^{⋆} that are needed to axiomatise a non-smooth operator f are unproblematic. For tame operators f, they are already in the language, and for a wild f it is not hard to define them in such a way that the augmented language remains RWB (or RDB) cool. Of the operators f_{D} needed to axiomatise a non-distinctive operator f, those that have exactly one active argument can be made to satisfy Clause 3 of Definition 15 by including the relevant τ-rule in D. This applies to the left merge, for example. All operators f_{D} with another number of active arguments cannot have τ-premises, by Definitions 15 and 10. These operators f_{D} are replaced by counterparts f′_{D}, obtained by replacing each premise x ⟶^{c} y in a rule for f_{D} by x ⟹⟶^{c} y. By Theorem 6, \underline{↔}_{rw} (or \underline{↔}_{rd}) is a congruence for f′_{D}.

Lemma 5 For any processes p_{1}, ..., p_{n} one has f(p_{1}, …, p_{ar(f)})\underline{↔}_{rd} ∑ f′_{D}(p_{1}, …, p_{ar(f)}).

Proof: Suppose ∑ f′_{D}(p_{1}, …, p_{ar(f)}) ⟶^{a} q. Then there is a \frac{H′}{f′_{D}(x_{1},...,x_{n})⟶^{a}t} and a closed substitu-

tion σ with σ(x_{i}) = p_{i} for i = 1, ..., n and σ(t) = q, such that p_{i} ⟹⟶^{c}_{L} σ(y) for (x_{i} ⟹⟶^{c} y) in H′. This rule has been constructed from a rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t}, where in H the premises are of the

form x_{i} ⟶^{c} y. By Lemma RDB, one obtains f(p_{1}, …, p_{ar(f)}) ⟹⟶^{a} q.

That f(p_{1}, …, p_{ar(f)}) ⟶^{a} q implies ∑ f′_{D}(p_{1}, …, p_{ar(f)}) ⟶^{a} q follows straightforwardly. □

Now the required axiomatisation is obtained by omitting all inaction laws for the modified operators f′_{D} with σ(x_{i}) = τ.y_{i} for some active argument i, and instead adding τ-laws

f′_{D}(x_{1}, …, τ.x_{i}, …, x_{n}) = f′_{D}(x_{1}, …, x_{i}, …, x_{n})

for each active argument i of f′_{D}. One obtains

Theorem 8 The above adaptation of the method of [1], together with axioms T1, T2 (and T3), yields finite equational axiomatisations of \underline{↔}_{db} (resp. \underline{↔}_{rw}) that are sound and complete for finite processes on an augmentation of any RDB cool (resp. RWB cool) GSOS language. □

11 Further work

The main contribution of Bloom’s RBB cool format is the classification of operators in wild and tame ones. In Fokkink [8] this classification is refined into a classification on the arguments of operators, thereby allowing operators that have wild as well as tame arguments. This allows, for instance, capturing the Kleene star within the format, which is not possible in the approach presented here. Additionally, [8] transcends beyond the GSOS format, by allowing arbitrary terms in the left-hand side of premises. This allows capturing recursive specification, by the method of introducing constants rather than variable binding constructs. In [9] this work is generalised slightly further, using a new method to establish congruence formats, while in [10] this method is applied to generalise the simply RHB cool format presented here. Generalising the simply RWB and RDB cool formats along the same line requires further work.

12 A Challenge

All equivalences of Definition 5 are congruences of the GSOS language with rules

\frac{x_{1} ⟶^{a} y}{f(x_{1}) ⟶^{a} g(y)} \frac{x_{1} ⟶^{τ} y}{g(x_{1}) ⟶^{τ} g(y)} g(x_{1}) ⟶^{τ}!x_{1}

\frac{x_{1} ⟶^{a} y}{!x_{1} ⟶^{a} y∥!x_{1}}  \frac{x_{1} ⟶^{a} y_{1}}{x_{1}∥x_{2} ⟶^{a} y_{1}∥x_{2}}  \frac{x_{2} ⟶^{a} y_{2}}{x_{1}∥x_{2} ⟶^{a} x_{1}∥y_{2}}

for a ∈ Act. Here, the operator !x can be understood as a parallel composition of infinitely many copies of x. The rules for f, g and ∥ are WB cool, but the one for ! is not. It is not even RBB safe in the sense of [8].

Open problem. Find a congruence format that includes the language above.

References

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

[2] T. Basten (1996): Branching bisimulation is an equivalence indeed! Information Processing Letters 58(3), pp. 141–147.

[3] J.A. Bergstra & J.W. Klop (1986): Algebra of communicating processes. In J.W. de Bakker, M. Hazewinkel & J.K. Lenstra, editors: Mathematics and Computer Science, CWI Monograph 1, North-Holland, Amsterdam, pp. 89–138.

[4] J.A. Bergstra & J.W. Klop (1985): Algebra of communicating processes with abstraction. Theoretical Computer Science 37(1), pp. 77–121.

[5] B. Bloom (1995): Structural operational semantics for weak bisimulations. Theoretical Computer Science 146, pp. 25–68.

[6] B. Bloom, S. Istrail & A.R. Meyer (1995): Bisimulation can’t be traced. Journal of the ACM 42(1), pp. 232–268.

[7] S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A theory of communicating sequential processes. Journal of the ACM 31(3), pp. 560–599.

[8] W.J. Fokkink (2000): Rooted branching bisimulation as a congruence. Journal of Computer and System Sciences 60(1), pp. 13–37.

[9] W.J. Fokkink, R.J. van Glabbeek & P. de Wind (2006): Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation. In F.S. de Boer, M.M. Bonsangue, S. Graf & W.-P. de Roever, editors: Revised Lectures Fourth International Symposium on Formal Methods for Components and Objects, FMCO 2005, Amsterdam, LNCS 4111, Springer, 2006, pp. 195-218.

[10] W.J. Fokkink, R.J. van Glabbeek & P. de Wind (2005): Divide and Congruence Applied to η-Bisimulation. In P. Mosses & I. Ulidowski, editors: Proceedings of the Second Workshop on Structural Operational Semantics, SOS 2005, Lisbon, Electronic Notes in Theoretical Computer Science 156(1), pp. 97-113.

[11] R.J. van Glabbeek (2005): A characterisation of weak bisimulation congruence. In A. Middeldorp, V. van Oostrom, F. van Raamsdonk & R. de Vrijer, editors: Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, LNCS 3838, Springer, pp. 26–39.

[12] R.J. van Glabbeek & W.P. Weijland (1996): Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), pp. 555–600.

[13] R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242. Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, 1980.

[14] F. Moller (1990): The nonexistence of finite axiomatisations for CCS congruences. In Proceedings 5^{th} Annual Symposium on Logic in Computer Science, Philadelphia, USA, IEEE Computer Society Press, pp. 142–153.

[15] E.-R. Olderog & C.A.R. Hoare (1986): Specification-oriented semantics for communicating processes. Acta Informatica 23, pp. 9–66.

[16] G.D. Plotkin (2004): A structural approach to operational semantics. The Journal of Logic and Algebraic Programming 60–61, pp. 17–139. Originally appeared in 1981.

[17] R. de Simone (1985): Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science 37, pp. 245–267.

[18] I. Ulidowski (1992): Equivalences on observable processes. In Proceedings 7^{th} Annual Symposium on Logic in Computer Science, Santa Cruz, California, IEEE Computer Society Press, pp. 148–159.

[19] I. Ulidowski & I. Phillips (2002): Ordered SOS rules and process languages for branching and eager bisimulations. Information and Computation 178(1), pp. 180–213.

[20] I. Ulidowski & S. Yuen (2000): Process languages for rooted eager bisimulation. In C. Palamidessi, editor: Proceedings of the 11th International Conference on Concurrency Theory, CONCUR 2000, LNCS 1877, Springer, pp. 275–289.