Axiomatising ST-Bisimulation Equivalence

Nadia Busi^{a} ^{∗} Rob van Glabbeek^{b} ^{†} Roberto Gorrieri^{c} ^{∗}

aDipartimento di Matematica, Università di Siena Via del Capitano, 15, I-53100 Siena, Italy e-mail: busi@cs.unibo.it

bComputer Science Department, Stanford University Stanford, CA 94305, USA e-mail: rvg@cs.stanford.edu

cDipartimento di Matematica, Università di Bologna Piazza di Porta S. Donato 5, I-40127 Bologna, Italy e-mail: gorrieri@cs.unibo.it

A simple ST operational semantics for a process algebra is provided, by defining a set of operational rules in Plotkin’s style. This algebra comprises TCSP parallel composition, ACP sequential composition and a refinement operator, which is used for replacing an action with an entire process, thus permitting hierarchical specification of systems. We prove that ST-bisimulation equivalence is a congruence, resorting to standard techniques on rule formats. Moreover, we provide a set of axioms that is sound and complete with respect to ST-bisimulation. The intriguing case of the forgetful refinement (i.e. when an action is refined into the properly terminated process) is dealt with in a new, improved manner.

1 Introduction

Among the non-interleaving equivalences, one of the most relevant is ST-bisimulation equivalence, originally proposed in [13] over Petri Nets, from which it takes the name (S and T are the initials of the German words for Place and Transition). This semantics drops the assumption that actions are atomic activities, hence, unobservable in the middle of their evolution. This is implemented by splitting every action in two distinct phases: the beginning and the ending which, instead, are considered atomic. Additionally, in order to prevent possible confusion in the presence of autoconcurrent actions, every ending phase is unambiguously related to its own beginning phase through some supplementary information. In the version of ST semantics we exploit, a causal link connects every ending phase to the corresponding beginning phase [15]. This is achieved by equipping each ending phase of an action with a “relative pointer” to indicate the number of phases which have occurred from the beginning of that action.

∗The first and third authors have been supported by CNR, MURST and Esprit project 8130 LOMAPS.

†The second author has been funded by ONR under grant number N00014-92-J-1974.

ST semantics expresses an elementary form of duration, as many action phases can be executed in between a beginning and its end. Moreover, ST semantics is the semantics for the operation of action refinement. This operation substitutes the execution of a process for an action, thereby introducing the possibility of relating descriptions of the same system at different levels of detail. It has been extensively studied in the semantic domain of event structures [12, 6], where an event is replaced by a whole structure. STbisimulation equivalence has been proved to be a congruence for this operation in [9] and the coarsest congruence contained in interleaving bisimulation in [24].

In this paper, we define an ST operational semantics in SOS style [22] for a process algebra equipped with the TCSP parallel composition operator, the ACP sequential composition operator and the refinement one. The transition system we define is labelled on action phases; hence, two agents are ST-bisimulation equivalent if their corresponding states are strongly bisimilar. The transition system specification (TSS, for short) we propose fits the tyft format of [16]. Therefore, we can exploit a nice result of that paper, namely that strong bisimulation is a congruence. Then, we provide a sound and complete axiomatization for ST-bisimulation: to obtain this, we conservatively extend the TSS by adding some auxiliary operators, following the lines of the algorithm defined in [1].

We claim that the operational description we provide for the operator of action refinement is in perfect agreement (apart from the way the empty refinement is dealt with) with the denotational one in terms of flow event structures described in [12]. Our claim is based on a similar proof, provided in [5], where a slightly different language and a slightly different version of ST semantics are considered. We argue that our way of dealing with the empty refinement, which can be useful in applications [12], is more satisfactory than the one of [11], and that event structures are not expressive enough to model this type of refinement.

2 Labelled Transition Systems

We recall the basic, relevant notions about transition system specification from [16], incorporating a recent improvement reported in [8, 10].

Let V be a denumerable set of variables; x, y, z are typical elements of V. A single sorted signature Σ is a pair (F, ♯), where F is a set of function names disjoint with V, and ♯ : F → ω is a rank function which gives the arity of a function name. With TT(Σ) and T (Σ) we denote the set of open and closed terms respectively over signature Σ. V (t) ⊆ V denotes the set of variables in a term t. A substitution σ is a mapping V → TT(Σ), extended homomorphically to terms.

Definition 2.1 A transition system specification (TSS) is a triple (Σ, A, R) with Σ a

signature, A a set of labels and R a set of rules of the form \frac{\{t_{i} →^{a_{i}} t′_{i} | i ∈ I\}}{t →^{a} t′} with I an

index set, t_{i}, t′_{i}, t, t′ ∈ TT(Σ), a_{i}, a ∈ A for i ∈ I.

If r is a rule satisfying the above format, then the elements of {t_{i} →^{a_{i}} t′_{i} | i ∈ I} are called the premises of r and t →^{a} t′ is called the conclusion of r. A rule of the form _{\frac{∅}{t →^{a} t′}} is

called an axiom, which, if no confusion can arise, is also written as t →^{a} t′. An expression of the form t →^{a} t′ with a ∈ A and t, t′ ∈ TT(Σ) is called a transition (labelled with a). The letters ϕ, ψ, χ are used to range over transitions. The notions ‘substitution’, ‘V (·)’ and ‘closed’ extend to transitions and rules as expected.

Definition 2.2 Let P = (Σ, A, R) be a TSS. A proof of a transition ψ from P is a wellfounded, upwardly branching tree of which the nodes are labelled by transitions t →^{a} t′ with t, t′ ∈ TT(Σ) and a ∈ A, such that: the root is labelled with ψ, and if χ is the label of a node q and {χ_{i} | i ∈ I} is the set of labels of the nodes directly above q, then there

is a rule \frac{\{ϕ_{i} | i ∈ I\}}{ϕ} in R and a substitution σ such that χ = σ(ϕ) and χ_{i} = σ(ϕ_{i}) for

i ∈ I. If there exists a proof of ψ from P, then ψ is provable from P (notation P ⊢ ψ).

Definition 2.3 A labelled transition system (LTS) is a structure (S, A, →) where S is a set of states, A an alphabet, and →⊆ S × A × S a transition relation. We write t →^{a} t′ to indicate that (t, a, t′) ∈→.

Definition 2.4 Let A = (S, A, →) be an LTS. A relation R ⊆ S × S is a (strong) bisimulation if it satisfies:

• if (s, t) ∈ R and s →^{a} s′, then there exists t′ ∈ S with t →^{a} t′ and (s′, t′) ∈ R;

• if (s, t) ∈ R and t →^{a} t′, then there exists s′ ∈ S with s →^{a} s′ and (s′, t′) ∈ R. Two states s, t ∈ S are bisimilar in A, notation A : s \underline{↔} t, if there exists a bisimulation containing the pair (s, t). Note that bisimilarity is an equivalence relation.

Definition 2.5 Let P = (Σ, A, R) be a TSS. The transition system T S(P) specified by P is the triple T S(P) = (T (Σ), A, →_{P}) where the relation →_{P} is defined by: t →^{a} _{P} t′ iff

P ⊢ t →^{a} t′.

We say that two terms t, t′ ∈ T (Σ) are (P -)bisimilar, notation t \underline{↔}_{P} t′, if T S(P) : t\underline{↔} t′. We write t\underline{↔} t′ if it is clear from the context what P is.

TSSs do not always generate LTSs for which bisimulation is a congruence, but they do if their rules satisfy the format below.

Definition 2.6 Let Σ = (F, ♯) be a signature and let P = (Σ, A, R) be a TSS. A rule in

R is in tyft format if it has the form \frac{\{t_{i} →^{a_{i}} y_{i} | i ∈ I\}}{f(x_{1},…, x_{♯(f)}) →^{a} t} with f a function name from

F, x_{i} (1 ≤ i ≤ ♯(f)) and y_{i} (i ∈ I) are all different variables, a_{i}, a ∈ A and t_{i}, t ∈ TT(Σ) for i ∈ I. P is in tyft format if all the rules in R are in tyft format.

Theorem 2.7 Let Σ = (F, ♯) be a signature and P = (Σ, A, R) a TSS. If P is in tyft format then strong bisimulation is a congruence for all function names in F.

Definition 2.8 Let P = (Σ, A, R) be a TSS and let r be a rule in R. The bound variables of r are recursively defined as the ones that occur in the left hand side of the conclusion or in the right hand side of a premise t →^{a} t′, where t contains bound variables only. A rule r is pure if all variables that occur in it are bound. The TSS P is called pure if all rules in R are pure.

Given two TSSs P_{0} and P_{1} we use P_{0} ⊕P_{1} to denote their componentwise union, which is only defined if function names that occur in both the signatures of P_{0} and P_{1} are given the same arity. If P_{0} and P_{1} are in tyft format and some other conditions are satisfied, we have that the outgoing transitions in the transition system defined by P_{0} of terms in the signature of P_{0} are the same as the outgoing transitions of these terms in the transition system defined by P_{0} ⊕ P_{1}.

Definition 2.9 Let P_{i} = (Σ_{i}, A_{i}, R_{i}) (i = 0, 1) be two TSSs with P = P_{0} ⊕ P_{1} defined. Let P = (Σ, A, R). We say that P is a conservative extension of P_{0} and that P_{1} can be added conservatively to P_{0} if for all t ∈ T (Σ_{0}), a ∈ A and t′ ∈ T (Σ):

P ⊢ t →^{a} t′ ⟺ P_{0} ⊢ t →^{a} t′

Note that if P is a conservative extension of P_{0}, P is also a conservative extension up to bisimulation, i.e. for t, t′ ∈ T (Σ_{0}): t\underline{↔}_{P} t′ ⟺ t\underline{↔}_{P_{0}} t′.

Theorem 2.10 Let P_{0} = (Σ_{0}, A_{0}, R_{0}) be a TSS in pure tyft format and let P_{1} = (Σ_{1}, A_{1}, R_{1}) be a TSS in tyft format such that no rule of R_{1} contains a function name from Σ_{0} in the source of its conclusion. Let P = P_{0} ⊕ P_{1} be defined. Then P_{1} can be added conservatively to P_{0}.

3 The Language

Let Act be a countable set of actions; a, b, c, d range over Act and S over the subsets of Act. The process terms are generated by the following syntax:

t ::= ε | δ | a | t · t′ | t + t′ | t ∥_{S} t′ | t[a ⇝ t′]

Intuitively, ε is the successfully terminated process, whereas δ is the deadlocked process. The operators · and + are the ACP sequential and alternative composition, respectively. With ∥_{S} we mean the TCSP parallel composition, where synchronisation over actions in S is required^{1}. When set S is empty (i.e. when no synchronization is allowed), we usually omit the subscript S in ∥_{S}. Finally [a ⇝] is the refinement operator as defined e.g. in [7].

Recursion can be added and modelled in our operational approach in the usual way (see [14] for a possible operational ST semantics for recursion). However, as our main concern is the axiomatisation, we prefer to restrict our attention to the finite calculus above.

1One could consider also more general parallel operators, like the ACP one. Our work can be easily adapted to ACP and similar languages.

4 Operational Semantics

To define the operational semantics, we need a more generous signature to represent the states. Let k range over integers. Let Σ = (F, ♯), where

F = {ε, δ, +, ·} ∪ {a | a ∈ Act} ∪ {a^{1} | a ∈ Act} ∪ {[k] | k ≠ 0}

∪{ ∥_{S} | S ⊆ Act} ∪ {[a ⇝] | a ∈ Act} ∪ {▷◁^{k} | k > 0}

♯(ε) = ♯(δ) = ♯(a) = ♯(a^{1}) = 0

♯([k]) = 1

♯(+) = ♯(·) = ♯( ∥_{S}) = ♯([a ⇝]) = ♯(▷◁^{k}) = 2

As any action is split in two phases, we need a unary operator to represent the state of its intermediate execution. An action a performs its beginning (denoted, with abuse of notation, a as well), reaching a^{1}. This performs the ending of the action a, where the superscript 1 states that this ending refers to the just performed transition. In general, the causal pointer from an ending to its beginning is implemented as a superscript number k stating that its beginning has been executed k transitions before. The delay operator [k] suitably updates the pointers. It will be introduced in a context of parallel composition and refinement. The merge operator ▷◁^{k} is used when merging the executions of a refined agent and the activated refining agent. Intuitively, it is a restricted form of parallel composition, as illustrated in Section 6.

Let Act^{ω} = {μ^{k} | μ ∈ Act ∧ k > 0} be the set of endings; let Act_{ST} = Act ∪ Act^{ω} be the set of phases, where a label in Act is called a beginning; η ranges over Act_{ST} and θ ranges over Act_{ST} ∪ {√}, where action √ (sometimes called “tick”) denotes clean termination.

Let P = (Σ, A, R) be the TSS where A = Act_{ST} ∪ {√} and R is the set of rules listed in Table 2 commented upon below. The auxiliary functions used in the rules are defined in Table 1. The functions name and index are intuitively clear. They extract from a label

name(a) = a  index(a) = 0 f(a, k) = a
name(a^{k}) = a index(a^{k}) = k f(a^{h}, k) = \begin{cases}a^{h+sg(k)} & if h ≥ |k| \\ a^{h} & otherwise \end{cases}
name(√) = √  f(√, k) = √
sg(k) = \{ \begin{matrix}1 & if k > 0 \\ −1 & if k < 0 \end{matrix}  inc(k) = k + sg(k)

Table 1: Auxiliary functions on action phases

the name of the action and the associated index, respectively. Function sg(k) returns the sign of the integer k, while inc(k) increases the absolute value of k. Finally, function f updates the index of the label to which it is applied.^{2}

2From the definition of f we cannot exclude to obtain action endings with a zero or negative index.

However, we have that terms reachable from elements of the language contain positive indexes only.

\begin{matrix}(ACT 1) & a →^{a} a^{1} & (ACT 2) & a^{1} →^{a^{1}} ε \\ (T ICK) & ε →^{√} δ & (DELAY) & \frac{x →^{θ} x′}{[k]x →^{f(θ,k)} [inc(k)]x′} \\ (SEQ1) & \frac{x →^{η} x′}{x · y →^{η} x′ · y} & (SEQ2) & \frac{x →^{√} x′ y →^{θ} y′}{x · y →^{θ} y′} \\ (ALT 1) & \frac{x →^{θ} x′}{x + y →^{θ} x′} & (ALT 2) & \frac{y →^{θ} y′}{x + y →^{θ} y′} \end{matrix}

(P AR1) \frac{x →^{η} x′}{x ∥_{S} y →^{η} x′ ∥_{S} [1]y} name(η) ∉ S

(P AR2) \frac{y →^{η} y′}{x ∥_{S} y →^{η} [1]x ∥_{S} y′} name(η) ∉ S

(P AR3) \frac{x →^{θ} x′ y →^{θ} y′}{x ∥_{S} y →^{θ} x′ ∥_{S} y′} name(θ) ∈ S ∪ \{√\}

\begin{matrix}(REF 1) & \frac{x →^{θ} x′}{x[a ⇝ y] →^{θ} x′[a ⇝ y]} & θ ≠ a \\ (REF 2) & \frac{x →^{a} x′ y →^{η} y′}{x[a ⇝ y] →^{η} x′[a ⇝ y]▷◁^{1}y′} \\ (REF 3) & \frac{x →^{a} x′ x′ →^{a^{1}} x′′ [−1][−1](x′′[a ⇝ y]) →^{θ} x′′′ y →^{√} y′}{x[a ⇝ y] →^{θ} x′′′} \\ (MERGE1) & \frac{x →^{η} x′}{x▷◁^{k}y →^{η} x′ ▷◁^{k+1}[1]y} & index(η) ≠ k \\ (MERGE2) & \frac{y →^{η} y′}{x▷◁^{k}y →^{η} [1]x ▷◁^{k+1}y′} \\ (MERGE3) & \frac{x →^{a^{k}} x′ [−1]x′ →^{θ} x′′ y →^{√} y′}{x▷◁^{k}y →^{θ} x′′} \end{matrix}

Table 2: Rules for basic operators

Axiom (ACT 1) represents the starting of an action, while (ACT 2) accounts for the execution of the ending. (TICK ) is the rule for the term ε, which performs √ and terminates. The rules for sequential and alternative composition are standard (see e.g. [16]). The rules for the TCSP-like parallel composition are almost standard. According to (PAR1), the asynchronous execution of a phase from the left subagent can be performed if this phase is part of an action not in the synchronisation set S; note, however, that the right subagent is delayed (i.e. the delay [1] operator is applied to it), because the pointers of all ending phases it will execute that point back to before the current state must be incremented by one, as they refer to transitions which are one step further back. Rule (PAR3) needs no delay as both subagents take part in the synchronisation; note that the termination signal √ can only be performed synchronously by the two subagents. The rule for the delay operator might appear a bit clumsy, as it works for integers k which can also be negative. A negative delay is needed when skipping some transitions, as now the pointers are to be decreased. The operator [k] increments pointers by 1 if k is positive; it decrements by 1 if k is negative. Thus decrementing by 2 needs to be expressed as [−1][−1]; not as [−2]. The value of |k| specifies which pointers need to be adapted; namely all pointers that point back at least k phases before the current state.

More interesting are the rules for refinement. Rule (REF 1) accounts for the case when the performed phase belongs to an action which is not to be refined. On the contrary, (REF 2) states that whenever the agent under refinement, x, starts the execution of the action to be refined, a, then x[a ⇝ y] performs the first, non tick, phase the refining agent y is able to do; the reached state is the merge of the two subagents, where the parameter 1 of the merge operator remembers the index of the ending phase of the refined action. Particular care should be devoted to rule (REF 3) which deals with the case when y can properly terminate, as in the so-called empty refinement [a ⇝ ε] (see Section 6 for a longer discussion). If x is ready to start the execution of a, then it will complete it, becoming x′′, and then we will take the first transition the refinement of x′′ is able to do, remembering to update the pointers, as we have skipped two transitions (the one for a and the other for a^{1}). The three rules for the merge operator state that the refined agent x can always perform a phase asynchronously, provided that this phase is not the ending of the action which has been refined (see rule (MERGE1) with its side condition); that the refining agent can proceed without any constraint (see rule (MERGE2)); and that the merged execution of the two ends when x is ready to perform the ending of the refined action and y can terminate properly.

It is worth-while observing that the transitions are labelled with parameters that range over actions and natural numbers, and not directly with actions, as required by the tyft format; so, every rule in our TSS is a rule schema corresponding to an infinite set of rules.

Proposition 4.1 P is pure and in tyft format. Strong bisimulation is a congruence for all function names in F.

5 Axiomatisation

In this section we introduce a set of auxiliary operators; then we define an axiomatisation and prove its soundness and completeness with respect to bisimulation.

5.1 Auxiliary Operators

First we introduce a set of auxiliary operators, that are necessary to obtain the axiomatisation. Let Σ′ = (F′, ♯′), where:

F′ = F ∪ {a^{+} | a ∈ Act} ∪ {a^{k} | a ∈ Act ∧ k ≥ 2}

∪{ _{S} , |_{S} | S ⊆ Act} ∪ {<^{k}, >^{k} | k > 0} ∪ {≫}

if f ∈ F then ♯′(f) = ♯(f)

♯′(a^{+}) = ♯′(a^{k}) = 0

♯′( _{S}) = ♯′( |_{S}) = ♯′(<^{k}) = ♯′( >^{k}) = ♯′(≫) = 2

In this setting, it is essential to introduce a syntactical distinction between actions and beginnings. To this aim, we introduce the auxiliary beginnings of the form a^{+}, which can perform the beginning a and then terminate successfully. The operators of the form a^{k}, for any k ≥ 2, are needed as we have labels of this kind in the operational rules of the previous section. The left-parallel _{S} and the synchronisation-parallel |_{S} are useful for the axiomatisation of the parallel operator ∥_{S}. They play the same rôle as the left-merge and communication merge of ACP [3]. However, whereas the left-merge of [3] insists that the first action in a parallel composition comes from the argument on the left, our S only insists that the first phase comes from the argument on the left. As far as the mnemonics concerns, _{S} points to the left, whereas the left merge is shaped like an L; there is no need for a right-merge here. The auxiliary operators <^{k} and >^{k} play a similar rôle in the axiomatisation of the ▷◁^{k}. Due to the asymmetry between the refined and the refining process both are needed here. ≫ is used to axiomatise the refinement operator.

Let P′ = (Σ′, A, R′) a TSS, where R′ is the set of rules listed in Tables 2 and 3. The

\begin{matrix}(ACT 3) & a^{+} →^{a} ε & (ACT 4) & a^{k} →^{a^{k}} ε k > 1 \\ (RT OM1) & \frac{y →^{η} y′}{x≫y →^{η} x▷◁^{1}y′} & (RT OM2) & \frac{x →^{a^{1}} x′ [−1][−1]x′ →^{θ} x′′ y →^{√} y′}{x≫y →^{θ} x′′} \\ (RME1) & \frac{y →^{η} y′}{x >^{k}y →^{η} [1]x ▷◁^{k+1}y′} & (RME2) & \frac{x →^{a^{k}} x′ [−1]x′ →^{θ} x′′ y →^{√} y′}{x >^{k}y →^{θ} x′′} \end{matrix}

(LME)  \frac{x →^{η} x′}{x<^{k}y →^{η} x′ ▷◁^{k+1}[1]y} index(η) ≠ k

(LP AR) \frac{x →^{η} x′}{x _{S} y →^{η} x′ ∥_{S} [1]y} name(η) ∉ S

(SY NC) \frac{x →^{θ} x′ y →^{θ} y′}{x |_{S} y →^{θ} x′ ∥_{S} y′} name(θ) ∈ S ∪ \{√\}

Table 3: Rules for auxiliary operators

only rules we comment on are those for ≫. The first rule states that the next transition, if not tick, must be taken from the right subagent; the reached state is the merge of the two, with pointer one. The second rule, instead, covers the case when y can terminate. This rule is similar to (REF 3). In this way x≫y behaves exactly like x[a ⇝ y] when the latter is about to start refining an action a.

Proposition 5.1 P′ is in tyft format. Strong bisimulation is a congruence for all function names in F′. P′ is a conservative extension of P.

The binary operators are left associative and binding priority is defined in decreasing

order as follows: · > [k] > [a ⇝] > ∥_{S} , _{S} , |_{S} , ▷◁^{k}, <^{k}, >^{k}, ≫ > +.

5.2 Axiomatisation

Let Act^{+} = {μ^{+} | μ ∈ Act}. Let λ range over Act^{+} ∪ Act^{ω} ∪ {δ}. We extend the auxiliary functions introduced in the previous section in the following way:

name(a^{+}) = a index(a^{+}) = 0 f(a^{+}, k) = a^{+}
name(δ) = δ index(δ) = 0 f(δ, k) = δ

Let T be the axiom set in Tables 4 and 5. Our axioms for the interaction between ∥ and the empty process is a mild variation on the treatment of [25]. While the axioms for the alternative, sequential and parallel composition are almost standard, the other axioms are not so usual. First, observe axiom (act). It states that any action a should be intended as composed of the sequence of its beginning and its ending (with pointer 1). The three axioms for the delay operator reflect clearly its operational definition. More intriguing is the case of refinement; in particular, (ref 2) shows that the refinement can start by dropping the beginning of the refined action and giving priority to the refining subagent y. Note that no action has been extracted from the term, so, no phase has been “executed”. This is done by the first application of axiom (rtom1), if y is not terminated,

or of (rtom2), if y terminates properly. The axioms for <^{k} and >^{k} are intuitively clear, as (lmerge1) corresponds to the operational rule (MERGE1), (rmerge1) to (MERGE2) and

(rmerge2) to (MERGE3). Finally, note that the axioms for ≫ and >^{k} are very similar: they differ only in the application of the delay operator in the first two axioms.

5.3 Soundness and Completeness

We cannot apply the algorithm presented in [1] because the rules of our TSS do not fit the GSOS format used in that paper, due to the presence in our TSS of lookahead and of an infinite set of rules and operators. However, we follow the lines presented there.

Given a set E of equations between terms, and t = t′ another equation, we write E ⊢ t = t′ to indicate that the equation t = t′ is derivable from E by means of equational logic. The rules of equational logic assert that equality is a congruence that it is preserved by instantiation of variables. For a formal definition see, e.g. [17].

In the following we state that the theory T is sound and complete with respect to \underline{↔}.

\begin{aligned}(alt1) & x + y & = & y + x & (seq1) & (xy)z & = & x(yz) \\ (alt2) & (x + y) + z & = & x + (y + z) & (seq2) & (x + y)z & = & xz + yz \\ (alt3) & x + x & = & x & (seq3) & δx & = & δ \\ (alt4) & x + δ & = & x & (seq4) & εx & = & x \\ & & & & (seq5) & xε & = & x \end{aligned}

(act) a = a^{+}a^{1}

(par) x ∥_{S} y = x _{S} y + y _{S} x + x |_{S} y

(lpar1)  λx _{S} y = λ(x ∥_{S} [1]y)  if name(λ) ∉ S
(lpar2)  λx _{S} y = δ  if name(λ) ∈ S
(lpar3)  ε _{S} x = δ
(lpar4) (x + y) _{S} z = x _{S} z + y _{S} z
(sync1)  λx |_{S} λy = λ(x ∥_{S} y)  if name(λ) ∈ S
(sync2) λx |_{S} λ′y = δ  if name(λ) ∉ S ∨ λ ≠ λ′
(sync3)  ε |_{S} λy = δ
(sync4)  ε |_{S} ε = ε
(sync5) (x + y) |_{S} z = x |_{S} z + y |_{S} z
(sync6)  x |_{S} y = y |_{S} x

\begin{aligned}(delay1) & [k](λx) & = & f(λ, k)([inc(k)]x) \\ (delay2) & [k]ε & = & ε \\ (delay3) & [k](x + y) & = & [k]x + [k]y \end{aligned}

Table 4: Axioms for all the operators (except refinement)

(ref 1)  (λx)[a ⇝ y] = λ(x[a ⇝ y])  if λ ≠ a^{+}
(ref 2)  (a^{+}x)[a ⇝ y] = (x[a ⇝ y])≫y
(ref 3)  ε[a ⇝ y] = ε
(ref 4)  (x + y)[a ⇝ z] = x[a ⇝ z] + y[a ⇝ z]
(rtom1)  x≫λy = λ(x▷◁^{1}y)
(rtom2)  a^{1}x≫ε = [−1][−1]x
(rtom3)  λx≫ε = δ  if index(λ) ≠ 1
(rtom4)  ε≫ε = δ
(rtom5)  (x + y)≫ε = x≫ε + y≫ε
(rtom6)  x≫(y + z) = x≫y + x≫z
(merge)  x▷◁^{k}y = x<^{k}y + x >^{k}y
(lmerge1)  λx<^{k}y = λ(x ▷◁^{k+1}[1]y)  if index(λ) ≠ k
(lmerge2)  λx<^{k}y = δ  if index(λ) = k
(lmerge3)  ε<^{k}x = δ
(lmerge4)  (x + y)<^{k}z = x<^{k}z + y<^{k}z
(rmerge1)  x >^{k}λy = λ([1]x ▷◁^{k+1}y)
(rmerge2)  a^{k}x >^{k}ε = [−1]x
(rmerge3)  λx >^{k}ε = δ  if index(λ) ≠ k
(rmerge4)  ε >^{k}ε = δ
(rmerge5)  (x + y) >^{k}ε = x >^{k}ε + y >^{k}ε
(rmerge6)  x >^{k}(y + z) = x >^{k}y + x >^{k}z

Table 5: Axioms for the refinement operator Theorem 5.2 If (t = t′) ∈ T then for any closed substitution ρ we have ρ(t)\underline{↔} ρ(t′).

Proof. We report the proofs for a selected set of significant axioms. Let ρ be a closed substitution. (ref2) We want to prove that ρ((a^{+}x)[a ⇝ y])\underline{↔} ρ((x[a ⇝ y])≫y), that is (a^{+}ρ(x))[a ⇝ ρ(y)]\underline{↔} (ρ(x)[a ⇝ ρ(y)])≫ρ(y).

If (a^{+}ρ(x))[a ⇝ ρ(y)] →^{θ} t three cases may occur.

• The transition is obtained by applying (REF 1). Then the transition a^{+}ρ(x) →^{θ} is derivable, with θ ≠ a. This transition can be obtained in two ways: by (SEQ1), so we need that a^{+} →^{θ}, but the only transition for a^{+} is a^{+} →^{a} ϵ, hence θ = a (contradiction); or by (SEQ2), but we need that a^{+} →^{√} (contradiction).

• The transition is obtained by applying (REF 2). Then we have that θ ≠ √, a^{+}ρ(x) →^{a} u, ρ(y) →^{θ} v and t = u[a ⇝ ρ(y)]▷◁^{1}v. The transition a^{+}ρ(x) →^{a} u can be obtained only by an application of (ACT 3) and (SEQ1), so we have that u = ερ(x), from which t = ερ(x)[a ⇝ ρ(y)]▷◁^{1}v. Applying (RTOM 1) to the transition ρ(y) →^{θ} v (remember that θ ≠ √) we obtain (ρ(x)[a ⇝ ρ(y)])≫ρ(y) →^{θ} (ρ(x)[a ⇝ ρ(y)])▷◁^{1}v. From the soundness of axiom (seq4) we have that ερ(x) \underline{↔} ρ(x), thus from the congruence property of \underline{↔} we have t\underline{↔} (ρ(x)[a ⇝ ρ(y)])▷◁^{1}v.

• The transition is obtained by applying (REF 3). Then we have a^{+}ρ(x) →^{a} u, u →^{a^{1}} u′, [−1][−1](u′[a ⇝ ρ(y)]) →^{θ} t and ρ(y) →^{√} v. As in the previous case, we have u = ερ(x). The only explanation for the transition ερ(x) →^{a^{1}} u′ is through (SEQ2) and (TICK ), thus it must be that ρ(x) →^{a^{1}} u′. Being a^{1} ≠ a, with an application of (REF 1) to this transition we obtain ρ(x)[a ⇝ ρ(y)] →^{a^{1}} u′[a ⇝ ρ(y)]. Applying (RTOM 2) yields (ερ(x)[a ⇝ ρ(y)])≫ρ(y) →^{θ} t.

Symmetrically, we obtain that if (ρ(x)[a ⇝ ρ(y)])≫ρ(y) →^{θ} t there exists an u such that

(a^{+}ρ(x))[a ⇝ ρ(y)] →^{θ} u and t\underline{↔} u.

(delay1) We want to prove that [k](λρ(x))\underline{↔} f(λ, k)([inc(k)]ρ(x)).

Suppose that [k](λρ(x)) →^{θ} t. This transition can be obtained only by (DELAY ); so there exist θ′ and u such that λρ(x) →^{θ′} u, θ = f(θ′, k) and t = [inc(k)]u. From λρ(x) →^{θ′} u we can derive that λ ≠ δ, θ′ = λ and u = ερ(x). Hence f(λ, k) = θ and with (ACT 3 or 4) and (SEQ1) we obtain that f(λ, k)([inc(k)]ρ(x)) →^{θ} ε([inc(k)]ρ(x)). From the soundness of axiom (seq4) and the congruence property of \underline{↔} we have that [inc(k)]ερ(x)\underline{↔} ε([inc(k)]ρ(x)).

The other direction of the proof is similar. (rtom2) We want to prove that (a^{1}ρ(x))≫ε\underline{↔} [−1][−1]ρ(x).

Suppose that (a^{1}ρ(x))≫ε →^{θ} t. Because the only possible transition for ε is ε →^{√} δ, the transition above cannot be obtained by an application of the rule (RTOM 1). Hence (RTOM 2) has been applied. As the only transition for a^{1}ρ(x) is a^{1}ρ(x) →^{a^{1}} ερ(x) it must be that [−1][−1]ερ(x) →^{θ} t. From the soundness of axiom (seq4) and the congruence property of \underline{↔} we have that [−1][−1]ερ(x)\underline{↔} [−1][−1]ρ(x), so we have that [−1][−1]ρ(x) →^{θ} u and t\underline{↔} u.

Again the other direction of the proof is similar.

Corollary 5.3 If T ⊢ t = t′ then for any closed substitution ρ we have ρ(t)\underline{↔} ρ(t′).

Definition 5.4 A term t ∈ T (Σ′) is in normal form if it can be generated by the following grammar:

n ::= ε | δ | a^{+} · n | a^{k} · n | n + n′

A term t ∈ T (Σ′) can be brought in normal form if there is a term n in normal form with T ⊢ t = n.

Definition 5.5 Let n be a term in normal form. The length of n is defined in the following way:

l(ε) = 1 l(a^{+} · n) = l(n) + 1
l(δ) = 1 l(a^{k} · n) = l(n) + 1
l(n + n′) = l(n) + l(n′) + 1

Lemma 5.6 Let n and m be terms in normal form. Then

1. the term n · m can be brought in normal form;

2. for all k ≠ 0 there exists a term n′ in normal form with T ⊢ [k]n = n′ and l(n′) = l(n);

3. the terms n _{S} m, n |_{S} m and n ∥_{S} m can be brought in normal form;

4. for all k > 0 the terms n >^{k}m, n<^{k}m and n▷◁^{k}m can be brought in normal form;

5. the term n≫m can be brought in normal form;

6. and the term n[a ⇝ m] can be brought in normal form.

Proof. We establish part 4 with induction on the sum of the length of n and m. The other parts proceed likewise. Let n and m be two terms in normal form and l(n) + l(m) = i. We first prove that there

exists a term p in normal form such that T ⊢ n >^{k}m = p.

• if m is ε we can have the following cases:

– if n is ε, we have that ε >^{k}ε = δ (rmerge4), and δ is in normal form.

– if n is δ, we use that δ = δx (seq3). Thus, using (rmerge3) we have δ >^{k}ε =

δx >^{k}ε = δ.

– if n is a^{+}n′ we have a^{+}n′ >^{k}ε = δ, by (rmerge3).

– if n is a^{h}n′ and h ≠ k, we also have a^{h}n′ >^{k}ε = δ.

– if n is a^{k}n′, we have a^{k}n′ >^{k}ε = [−1]n′ by (rmerge2), on which we apply part 2 of the lemma.

– if n is n′+n′′, we have (n′+n′′) >^{k}ε = n′ >^{k}ε+n′′ >^{k}ε by (rmerge5). As l(n′), l(n′′) < l(n), we may apply the induction hypothesis, so there must be terms p′ and p′′ in

normal form such that n′ >^{k}ε = p′ and n′′ >^{k}ε = p′′. It follows that (n′ + n′′) >^{k}ε = p′ + p′′.

• if m is δ: n >^{k}δ =^{seq3} n >^{k}(δx) =^{rmerge1} δ([1]n ▷◁^{k+1}x) =^{seq3} δ.

• if m is a^{+}m′: by (rmerge1) we obtain n >^{k}(a^{+}m′) = a^{+}([1]n ▷◁^{k+1}m′). By part 2 of the lemma there exists a term n′ in normal form such that [1]n = n′ and l(n) = l(n′). As equality is a congruence we have [1]n ▷◁^{k+1}m′ = n′ ▷◁^{k+1}m′. Moreover, l(n′) + l(m′) < i, so, by induction, there exists a term p′ in normal form such that n′ ▷◁^{k+1}m′ = p′; it follows that n >^{k}a^{+}m′ = a^{+}p′, where a^{+}p′ is in normal form.

• if m is a^{k}m′, the proof is equal to the above one.

• if m is m′ + m′′, by (rmerge6) we obtain n >^{k}(m′ + m′′) = n >^{k}m′ + n >^{k}m′′, which by induction can be brought in normal form.

Following the same lines, we can bring n<^{k}m in normal form. Finally, n▷◁^{k}m is brought in normal form through an application of (merge), using the normalisation of n >^{k}m and

n<^{k}m.

Theorem 5.7 Let t ∈ T (Σ′). There exists then a term n in normal form such that T ⊢ t = n.

This theorem follows by induction from lemma 5.6. Due to the presence of axioms like (rtom2), lemma 5.6 cannot be replaced by a simpler lemma, only obtaining head normal forms, as in [1].

Lemma 5.8 Let n, m be closed terms in normal form. If n\underline{↔} m then T ⊢ n = m.

Proof. Standard (see [19]).

Corollary 5.9 Let t, t′ ∈ T (Σ′). If t\underline{↔} t′ then T ⊢ t = t′.

6 Concluding Remarks

In this section, we discuss some further issues. First we provide an alternative operational description of refinement which exploits the parallel composition operator (with synchronisation allowed on a special end action e only). Then, we compare the various approaches to the empty refinement (i.e. when the refining agent is properly terminated) that appear in the literature. Finally, we comment on related work on other operational versions of ST semantics and definitions of action refinement.

6.1 Coding Refinement with Parallel Composition

The operational description of action refinement and its axiomatisation we provide in Sections 4 and 5 have the merits of being “context-free”, in the sense that these rules and axioms can be “plugged in” in any other operational and axiomatic description of a process algebra, provided that this algebra is equipped with choice and action-prefix operators.

Anyway, it is easy to see that the merge operator is indeed a kind of parallel composition, preventing synchronisations between the refined agent and the refining one. Hence, with the aim at minimising the number of rules and axioms, here we present an alternative description of action refinement which implements the merge through a slight modification of parallel composition, using also the sequential composition operator. In the following, operators ▷◁^{k}, ≫, >^{k} and <^{k} are no longer used. On the other hand, we introduce a new constant e, exploited to signal termination of the refining agent (not to be confused with √), and a new unary operator skip which “skips” the transitions labelled by e.

The idea consists in replacing the ending phase of the currently refined action with the special action e, which will be added also at the end of the refining term. Then we put in parallel the remaining part of the refined term with the refining one, preventing any synchronisation on normal actions, but forcing the synchronisation on label e. Subsequently, the now “useless” e-labelled transitions are skipped via the new unary operator skip. In the following, labels η and θ range also over e. The rules for the new operators are listed below:

(END)  e →^{e} ε

(SKIP 1) \frac{x →^{θ} x′}{skip(x) →^{θ} skip(x′)} θ ≠ e

(SKIP 2) \frac{x →^{e} x′ [−1]x′ →^{θ} x′′}{skip(x) →^{θ} x′′}

The rules for parallel composition are to be modified slightly in order to cope with the new label e, which is always a synchronisation action (similarly to √). The other rules in the original TSS are unchanged, except for the fact that now the variables η and θ can take also the value e. The three rules for refinement are now replaced by the two rules below, where the second one covers also the case of empty refinement.

(REF 1)  \frac{x →^{θ} x′}{x[a ⇝ y] →^{θ} x′[a ⇝ y]}  θ ≠ a

(REF 2) \frac{x →^{a} x′ skip([−1](x′[a ⇝ y]) ∥ ye) →^{θ} y′}{x[a ⇝ y] →^{θ} y′}

The delay rule remains the same, but function f is changed by substituting the end action e for the ending phase of the refined action.

f(a^{h}, k) = \{ \begin{matrix}a^{h} & if h ≤ |k| − 1 \\ e & if h = −k \\ a^{h+sg(k)} & otherwise \end{matrix}

Note that the value of f(a^{h}, −h) is not significant in the preceding sections; if we would have had an action e, we could just as well have defined f as above from the beginning.

Also for the axiomatisation, all the axioms related to the dropped operators are removed. Moreover, the axioms for the synchronisation merge take into account the fact that e is a synchronisation action. Below the axioms for the new operators and for the new definition of action refinement are reported, where now λ can also take the value e.

(ref1)  (λx)[a ⇝ y] = λ(x[a ⇝ y]) if λ ≠ a^{+}
(ref2) (a^{+}x)[a ⇝ y] = skip([−1](x[a ⇝ y]) ∥ ye)
(ref3)  ε[a ⇝ y] = ε
(ref4) (x + y)[a ⇝ z] = x[a ⇝ z] + y[a ⇝ z]
(skip1)  skip(λx) = λskip(x) if λ ≠ e
(skip2)  skip(ex) = [−1]x
(skip3)  skip(ε) = ε
(skip4)  skip(x + y) = skip(x) + skip(y)

The reader can easily get convinced that this formulation is equivalent to the one of Sections 4 and 5.

6.2 Empty Refinements

There exists no general agreement on what an empty refinement, i.e. the refinement of an action into a successfully terminated process, should be. Our proposal differs from those that already appeared in the literature.

In [11] an interpretation of the empty refinement is offered in the domain of prime event structures, according to which events refined into the empty structure are simply erased; a consequence of this decision is that the congruence result for ST bisimulation semantics does not hold in this approach, as shown in [9]. Moreover they argue that these forgetful refinements can drastically change the behaviour of concurrent systems and can not be explained by a change in the level of abstraction at which these systems are regarded [12]. In [7], the empty refinement is treated as if the refining agent were deadlocked. The justification for this proposal is that empty refinement is an erroneous step in the top-down development procedure. In this way, the congruence property is kept. We could obtain the same result by skipping rule (REF 3).

Now we introduce an example to illustrate the differences among these interpretations of empty refinement. Let t = (ab ∥_{b} (b + c) ∥_{c} cd) ∥_{ad} ad. In Figure 1 this expression is depicted as an event structure. The densely dotted line indicates syntactic conflict, as specified by the +-operator in t. The sparsely dotted line indicates inherited or semantic conflict: the events b and d cannot occur in the same run as c is a prerequisite of d and in (syntactic) conflict with b.

If we refine the action c into ε in t, following the paradigm of [7], event c is blocked and the resulting system is equivalent to abδ, corresponding with the ST transition system in Figure 2a. If we, in the spirit of [11], simply erase event c in a model of event structures (such as flow event structures [4]) where semantic conflict is merely a matter of interpretation, we would obtain a system that is equivalent to a(b∥d), in which the conflict between b and d is dropped. However, the forgetful refinements of [11, 9] are considered on prime event structures [21], were semantic conflict has the same status as syntactic conflict. Here the result is a(b + d), corresponding to the ST transition system in Figure

[figure: a; b; c; d; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·]

Figure 1: Event structure representation of t

[figure: a); a; a^{1}; b; b^{1}; a; a^{1}; b; b^{1}; d; d^{1}; √; √; b); a; a; a^{1}; a^{1}; b; d; b^{1}; d^{1}; d; d^{1}; √; √; √; c)]

Figure 2: t[c ⇝ ε] according to a) [7], b) [11] and c) [25]

2b. A reason to dislike this result is that the choice between b and d is made only after the a occurred, whereas in the original system a commitment to do d could be made earlier through the occurrence of c. Hence this notion of forgetful refinement can mask deadlock behaviour of concurrent systems. In [25] the empty refinement is called ‘renaming into ε’ and [a ⇝ ε] is denoted ε_{{a}}. His solution would yield a(b + d) + ad, which better captures the branching structure between the executions ab and ad. But [25] works in interleaving semantics (and doesn’t consider other types of action refinement) and consequently his solution cannot capture the fact that the choice between these executions can be made at any moment during the execution of a. This is captured by the operational semantics defined in Section 4. We obtain the transition system in Figure 3.

[figure: a; a; a^{1}; a^{1}; a^{1}; b; b^{1}; d; d^{1}; √; √; d; d^{1}; √; d; d^{1}; √]

Figure 3: The ST transition system for t[c ⇝ ε] according to our rules.

As this transition system cannot be obtained as the image of an event structure, it follows that event structures are not expressive enough for this type of empty refinement.

6.3 Related Work

In this section, we briefly describe some related work on alternative operational ST semantics and on alternative operational definitions of action refinement.

Different Approaches to ST Semantics We restrict our attention to those proposals for which ST-bisimulation semantics is defined as standard bisimulation on a transition system labelled on suitable phases of actions.

In [2] Aceto and Hennessy study a finite process algebra equipped with a parallel composition operator which does not permit synchronisation. For this simple language they define, as we do here, a transition system labelled on action phases, where however the endings are not provided with pointers. Standard bisimulation equivalence gives rise to an equivalence relation called by the authors timed equivalence, which is also known in the literature under the name of split_{2} equivalence [9, 15]. Timed equivalence coincides with ST-bisimulation equivalence because of the limited expressive power of the language they investigate. An elegant equational characterisation of timed equivalence is provided.

An operational ST semantics for full CCS [20] is reported in [14] where the pointers from endings to beginnings are “absolute”, i.e. the index k in a^{k} indicates that the ending refers to the k-th started action. This makes the definition of an operational semantics much more involuted because there is the need of a global counter (states are pairs ⟨t, z⟩, where t is a process term and z is a natural number) in order to implement the absolute referencing, and rules must be specialised to beginnings and endings (hence, duplicated) because only at beginnings pointers are increased. In this paper, no axiomatisation is proposed and action refinement is not considered.

In [18], an operational semantics with “weak” transitions (i.e. transitions corresponding to those of weak bisimulation [20]) for a CCS-like language is presented. However, the transition system generated is infinitely-branching also for finite (i.e. recursion free) agents. Moreover, the operational rules for parallel composition are context-dependent. On this basis, a non-standard proof system is proposed, composed of conditional, contextdependent equations. Also in this paper action refinement is not considered.

Other Operational Semantics for Action Refinement There are three papers dealing with this problem, the first one working with timed semantics [2], the second one with a causal semantics [7] and the last one with the even finer semantics of event isomorphism [23].

In [2] an operational semantics in SOS style for the operator of action refinement — x[a ⇝ y] — is defined following tightly the inductive structure of the term x to which the operator is applied. For instance, if x = x_{1} +x_{2}, then x[a ⇝ y] can do whatever x_{1}[a ⇝ y] and x_{2}[a ⇝ y] are able to do. This definition is equivalent to making a complete syntactic subsitution of the refining agent y for any occurrence of a in x before executing the agent. (Compare the classic notion of the “dynamic” copy rule opposed to the static one for the implementation of procedure calls.) This operational semantics, however, does not scale easily to langauges which include communication and restriction; moreover, the basic intuition of refinement in such a case is no longer in full agreement with the corresponding operation on Event Structures.

In [7] a causal operational semantics is introduced for action refinement in a finite language which is very close to ours (the only difference is that we take ACP sequential composition instead of CCS action prefixing). This work relies upon previous work [6], where Darondeau and Degano prove that the inductive definition of action refinement they propose on Causal Trees coincides with the one they propose on a special subclass of Event Structures, called Δ-free. Our work owes some basic intuition to [7], which is similar in spirit, except for the way the empty refinement is dealt with.

In [23] Rensink shows that action refinement can receive a simple operational treatment when working with the very concrete semantics induced by event isomorphism. This definition is proved to agree with a denotational operation of refinement defined over his model of families of posets.

In our opinion, the main merit of our proposal w.r.t. the last two is that we (arguably) use the “right” semantics, as ST-bisimulation equivalence has been proved to be the coarsest congruence contained in interleaving bisimulation [24]. However, the other two proposals define transition systems which are smaller because actions do not have to be split in phases.

References

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

[2] L. Aceto & M. Hennessy (1993): Towards action-refinement in process algebras. Information and Computation 103(2), pp. 204–269.

[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] G. Boudol (1990): Flow event structures and flow nets. In I. Guessarian, editor: Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, La Roche Posay, France, LNCS 469, Springer-Verlag, pp. 62–95.

[5] N. Busi (1993): Raffinamento di azioni in linguaggi concorrenti. Master’s thesis, Università di Bologna.

[6] Ph. Darondeau & P. Degano (1993): Refinement of actions in event structures and causal trees. Theoretical Computer Science 118(1), pp. 21–48.

[7] P. Degano & R. Gorrieri: A causal operational definition of action refinement. Information and Computation. To appear.

[8] W.J. Fokkink (1994): The tyft/tyxt format reduces to tree rules. In Proc. Theoretical Aspects of Computer Science, Sendai, Japan, LNCS 789, Springer-Verlag, pp. 440–453.

[9] R.J. van Glabbeek (1990): The refinement theorem for ST-bisimulation semantics. In M. Broy & C.B. Jones, editors: Proceedings IFIP TC2 Working Conference on Programming Concepts and Methods, Sea of Gallilea, Israel, North-Holland, pp. 27–52.

[10] R.J. van Glabbeek (1993): Full abstraction in structural operational semantics (extended abstract). In M. Nivat, C. Rattray, T. Rus & G. Scollo, editors: Proceedings of the Third International Conference on Algebraic Methodology and Software Technology (AMAST’93), Twente, The Netherlands, June 1993, Workshops in Computing, Springer-Verlag, pp. 77–84.

[11] R.J. van Glabbeek & U. Goltz (1989): Equivalence notions for concurrent systems and refinement of actions. In A. Kreczmar & G. Mirkowska, editors: Proceedings Mathematical Foundations of Computer Science 1993 (MFCS), Pora_{....._{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}}bka-Kozubnik, Poland, LNCS 379, Springer-Verlag, pp. 237–248.

[12] R.J. van Glabbeek & U. Goltz (1990): Refinement of actions in causality based models. In J.W. de Bakker, W.P. de Roever & G. Rozenberg, editors: REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, Mook, The Netherlands 1989, LNCS 430, Springer-Verlag, pp. 267–300.

[13] R.J. van Glabbeek & F.W. Vaandrager (1987): Petri net models for algebraic theories of concurrency. In J.W. de Bakker, A.J. Nijman & P.C. Treleaven, editors: Proceedings PARLE conference, Eindhoven, Vol. II (Parallel Languages), LNCS 259, Springer-Verlag, pp. 224–242.

[14] R. Gorrieri & C. Laneve (1991): The limit of split_{n} bisimulations for CCS agents. In A. Tarlecki, editor: Proceedings Mathematical Foundations of Computer Science 1991 (MFCS), Poland, LNCS 520, Springer-Verlag, pp. 170–180.

[15] R. Gorrieri & C. Laneve: Split and ST bisimulation semantics. Information and Computation. To appear.

[16] J.F. Groote & F.W. Vaandrager (1992): Structured operational semantics and bisimulation as a congruence. Information and Computation 100(2), pp. 202–260.

[17] M. Hennessy (1988): Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts.

[18] M. Hennessy (1991): A proof system for weak ST bisimulation over a finite process algebra. Technical report, Computer Science Department, University of Sussex.

[19] M. Hennessy & R. Milner (1985): Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), pp. 137–161.

[20] R. Milner (1989): Communication and Concurrency. Prentice-Hall International, Englewood Cliffs.

[21] M. Nielsen, G.D. Plotkin & G. Winskel (1981): Petri nets, event structures and domains, part I. Theoretical Computer Science 13(1), pp. 85–108.

[22] G.D. Plotkin (1981): A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University.

[23] A. Rensink (1993): Models and Methods for Action Refinement. PhD thesis, University of Twente.

[24] W. Vogler (1993): Bisimulation and action refinement. Theoretical Computer Science 114(1), pp. 173–200.

[25] J.L.M. Vrancken (1986): The algebra of communicating processes with empty process. Report FVI 86-01, Dept. of Computer Science, University of Amsterdam.