数理解析研究所講究録996 巻 1997 年 195-206

195

ORDERED SOS RULES AND WEAK BISIMULATION
IAIN PHILLIPS
Department of Computing, Imperial $College_{f}$ London $SW7\mathit{2}Bz$ .
IREK ULIDOWSKI
Research Institute for Mathematical $ScienCeS_{f}$ Kyoto University,$I\zeta yoto$, Japan

One of the main reasons for developing formats of rules with negative antecedents,for example the GSOS format, was to enable natural description of process operators like the sequential composition, priority and broadcast paraUel. We propose analternative method for defiming these and similar operators, which does not rely on
with negative antecedents. Instead, we use ordinary rules but with an ordering on them which indicates the order of their application. We show that operators
which are definable by our method preserve a version of weak bisimulation.
$\mathrm{n}4\mathrm{e}\mathrm{s}$1Introduction

Structured Operational Semantics (SOS) is considered to be the standard
method for defining operational meaning of process operators in an arbitrary
process language. It was originated by Milner for CCS $[1, 2]$ and formalised
by Plotkin [3]. The meaning of each operator on processes is given by a setof transition rules. Each of the rules describes how the behaviour of a process, constructed with the operator and some subprocesses, depends on the
behaviour of these subprocesses. For example, the following is one of the rules
for ffl, the CSP external choice operator,$Xarrow aX’$
$X$

ffl

$Yarrow x\prime a$.

The rule allows to infer that a process
may perform action since its
ffl
subprocess
may itself perform .
Process operators can be classified accordingly to the form of rules defining
their operational meaning. A format of rules is a collection of forms of rules.
We say that an operator is in a certain format if its rules belong to that format.
Most of the popular process operators are in the De Simone format [4].
However, there is a number of process operators which cannot be adequately defined by De Simone rules alone. The most important examples ofthese are the sequential composition, priority and broadcast parallel operators. These operators are usually defined by rules with negative antecedents,
i.e. expressions like
. Consider, for example, the rules for the sequential$a.\mathrm{O}$$a.\mathrm{O}$$a$$X\neq^{a}*$$b.\mathrm{O}$

$a$

196
composition operator ;$Xarrow\alpha X’$$X;\mathrm{Y}arrow X^{/}\alpha;$$\forall\alpha$$Y$.

$X\wedge\alpha$$Yarrow Y’\beta$$X;Yarrow\rho Y^{J}$,

where and are any visible or silent actions. Given a process $0;a.0$ we candeduce, using the second rule for and the fact that $a.0$ can perform , thatthe process itself can perform .
Transition rules with negative antecedents as means to give operationalsemantics to general process operators were originally considered by Bloom,
Istrail and Meyer [5, 6, 7]. They proposed a general format of rules called
the GSOS format. Groote [22] proposed a more general format called the$ntyfl/nxyfl$ format.
Another issue concerning the formats of transition rules is the use of silent
actions. The original De Simone and GSOS formats treated both silent andvisible actions in the same way, i.e. as visible. This resulted in many difficulties when weak equivalences over De Simone or GSOS process languages wereconsidered. The problem was studied by Bloom $[8, 9]$ , Vaandrager [10] and thesecond author $[11, 12]$ . He proposed the ISOS format, which offers a soundand intuitive treatment of silent actions as well as use of negative antecedents
and copying.
In this paper we will only consider those formats of rules which treat silent
actions as invisible; for example the formats in [8, 10, 11, 9, 12]. A numberof important results were established for these formats. Firstly, certain weakequivalences were shown to be preserved by all process operators in these
congruences with respect toformats [10, 9, 12]. Secondly, (completed)these formats were discovered $[10, 11]$ . Thirdly, algorithms for generatingcomplete axiomatisations of some weak equivalences were developed [13, 14,
15].
The main conceptual contribution of the paper is a new method for defining
process operators, including the sequential composition and priority operators,
by transition rules with $no$ negative antecedents. Our method is based on asimple idea of ordering the transition rules for each operator. The behaviourof a process can then be determined by examining the rules of its main operator, starting with the rules highest in the ordering and then considering therules lower in the ordering. As a result, a rule lower in the ordering can only
be applied if none of the rules above it can. Intuitively, this has the effectof applying a rule with negative antecedents. A simple example is given toillustrate our method. Consider a priority operator , which gives a priority$\alpha$$\beta$

$a$

$a$

$a$

.ace

$\mathrm{t}\mathrm{r}$$\theta$$a$

197
over , defined by the following rules.
$b$$Xarrow X’b$

$X\wedge a$$Xarrow X^{J}\dot{a}$$\theta(X)arrow a\theta(X’)$$\theta(X)arrow b\theta(X’)$. Employing our method we only need theWe easily deduce
first rule and a similar rule for (but with no negative antecedents) together
with an ordering which puts the first rule above the second. Clearly, the first,. But, sincerule cannot be applied to the process
ffl
by the second rule.
obtainThe main technical problem we address is how to combine orderings onrules with the intended use of silent actions. It is known that all ISOS operators, which include most of popular process operators, preserve a version of
weak bisimulation [12]. However, it is not difficult, as will be shown in theforthcoming sections, to come up with a positive ISOS operator and a carelessordering on its rules such that the operator does not preserve weak bisimulation. In order to avoid such operators we propose a number of conditions onorderings such that if they are satisfied then the defined operator is.guaran.t.eed
to preserve weak bisimulation.
$\theta(b.0ffl_{C}.0)arrow b\theta(0)$$b$$\theta(b.\mathrm{O} \mathrm{f}\mathrm{f}\mathrm{l} c.\mathrm{O})$$b.\mathrm{O}$$c.\mathrm{o}arrow b0$$\theta(b.\mathrm{O} \mathrm{f}\mathrm{f}\mathrm{l} c.\mathrm{o})arrow\theta(0b)$$\mathrm{w}_{\vee}\mathrm{e}$2Preliminaries$Y,$
Let Var be a countable set of variables ranged by $X,$
. A signature
is a set of pairs $(f, n)$ , whereis an arity of . An element $(g, 0)$ ofis called a constant symbol and it is abbreviated as . The set of open terms, denoted by, is ranged by $P,$ $Q,$ .
over with variables in$\ldots.var(T)$ denotes, is ranged by
The set of closed terms, written as
the set of variables appearing in a term . We use
for syntactic equality.
context withholes $C[X_{1}, \ldots , X_{n}]$ is a member of.
A proper context is a context where each variable occurs at most once. If,
areterms thenis a term obtained by substituting$1\leq i\leq n$ . Anbyis the congruence if for allcontexts $C[X]$ we have $t\sim t’$ implies $c[t]\sim C[t’]$ . Similarly, an operator $(f, n)$
for all -ary vectors of closed terms and with $t\sim t’$ we have$f(t)\sim f(t’)$ . A substitution. The substitution
is a mapping from Var to,extends to a mappingin a standard way. Act
Vis, is a finite set of actions, where Vis is the set of visible actions,ranged by, and is a silent, internal action which is not in.
ranged by
In this paper we only consider weak equivalence on processes. The main
characteristic of weak equivalences is the type of process behaviour which is$X_{i},$$\ldots$$f$$n\in \mathrm{N}$$\Sigma$$Y_{i},$$\Sigma$$g$$\Sigma$$\mathrm{T}(\Sigma, V)$$V\subseteq \mathrm{V}\mathrm{a}\mathrm{r}$$\mathrm{T}(\Sigma)$$p,$ $q,$$T$$\Sigma$$t_{1},$$X_{\dot{i}}$$\ldots$$\equiv$$\mathrm{T}(\Sigma, \{X_{1}, \ldots, X_{n}\})$$n$$\ldots$$C[t_{1}, \ldots, t_{n}]$$\Sigma$$t_{n}$$t_{i},$$\Sigma$$\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{i}\mathrm{v}\mathrm{a}\mathrm{l}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}\sim \mathrm{o}\mathrm{n}\mathrm{T}(\Sigma)$

$t$

$n$

$\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{s}\mathrm{e}\mathrm{r}\mathrm{v}\mathrm{e}\mathrm{s}\sim \mathrm{i}\mathrm{f}$$\rho$$\mathrm{T}(\Sigma)arrow \mathrm{T}(\Sigma)$$\rho$$\alpha,$$t’$$\mathrm{T}(\Sigma)$$\cup\{\tau\}$$=$$\ldots$$a,$ $b,$$\mathrm{V}_{\mathrm{I}}\mathrm{s}$$*\cdot.$$\tau$

198
used to determine which processes are related–only visible behaviour is taken
into account. In particular this means that only the visible actions of processes
are recorded and the. silent actions are abstracted away. If one is interested inusing weak equivalences and if one searches for a general format of rules withsilent actions then, we believe, it is reasonable to havea suitable
the following minimal requirement concerning the form of rules: All operators
defined in the format should preserve the chosen weak equivalence.
The first attempt to accommodate silent actions in formats of rules is due
to Bloom [8]. The important idea of silent rules, called there patience rules, wasintroduced there but the overa..ll treatment of silent actions was not completely
satisfactory: one could define operators which would count the number of silent
actions processes can perform. Vaandrager in [10] modified the original De
Simone format [4] by using the silent rules and showed that failure equivalence
is preserved by all operators definable in the modified format. Then, the second
author introduced in [11] the ISOS format–a general format of rules withnegative antecedents and a suitable treatment of silent actions. He provedthat ISOS operators preserve a version of weak bisimulation [12] (sometime
called delay bisimulation) and refusal simulation preorder [11]. Also, similar
modifications to those used in the ISOS format and some new ideas wereapplied to positive GSOS rules in [9]. As a result a number of formats were
proposed and a number of weak equivalences, including rooted branching andweak bisimulations, were shown to be preserved by the operators in theseformats. Finally, the second author showed in [15] that testing preorder of De
Nicola&Hennessy [16] is preserved by De Simone (with silent rules) operators.
In this paper we shall consider only those rules which belong to (a slightly
extended) ISOS format as described in $[11, 12]$ . The ISOS rules have two
distinctive forms. We will use the following notational agreement: we write$\mathrm{t}\mathrm{r}\mathrm{e}\mathrm{a}\mathrm{t}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}\vee \mathrm{o}\mathrm{f}$.
instead ofDefinition 1 An action rule has the following form

$Xarrow X\sim\alpha$$X\wedge\wedge\tau\alpha$$\{X_{j}\overline{\beta_{jkarrow}}X_{j}\}_{jK_{j}}\in J,k\in$$\{X_{i}arrow a_{i}X_{i}’\}_{i\in I}$$f(X_{1}, \ldots, X_{n})arrow\alpha C[\mathrm{Y}]$

,

, all
are finite
where
are all different variables, and, ,subsets of natural numbers andcontains atthe variables
may appear
where $Y_{i}=X_{i}’$ if $i\in I$ and $Y_{i}=X_{i}$ otherwise. Note that eacha number of time or not at all. The notions of the operator of theinrule, the action, positive and negative antecedents and the consequent are asor, in other words, if it does not haveusual. The action rule is positive if
any negative antecedents. We say that $(f, n)$ tests its m-th argument and the$X_{i},$$I$$X_{i}’$$C[\mathrm{Y}]$$J\subseteq\{1, \ldots , n\}$$I\backslash _{j}^{J’}$$\mathrm{m}\mathrm{o}\mathrm{s}\mathrm{t}\wedge$$Y_{1},$$Y_{i}$$C[\mathrm{Y}]$$J=\emptyset$$\ldots$$Y_{n}$

199
m-th argument for $(f, n)$ is active if there is an action rule for $(f, n)$ within the antecedents. The antecedents and the consequent of a rule are written
as ante $(r)$ and $conS(r)$ respectively.
A silent rule, or -rule, for an operator is any of the following rules for$1\leq i\leq n$ , hereafter written as
or simply as when is known from thecontext,$X_{m}$$r$$f$$\tau$$f$$\tau_{i}$$\tau_{f:}$$X_{i}arrow x_{\dot{i}}\tau/$$f(x_{1}, \ldots, X_{i}, \ldots, X_{n})arrow f(\tau X_{1}, \ldots, x_{\dot{i}}’, \ldots, Xn)$.

An action rule is -producing if $\alpha=\tau$ , otherwise it is Vis-producing. Let
rules $(f)$ be the set of all action rules and -rules with $f(X)$ in the consequent. The
argument is active in some action rule if
appears in theantecedents of , and it is active in a set $S\subseteq rules(f)$ if it is active in someaction rule in . Denote the set of such by active $(S)$ , and write active $(f)$ instead of active $(ru\iota_{e}S(f))$ . Let $tau(S)$ be $\{i|\tau_{i}\in S\}$ , and write $tau(f)$ insteadof $tau(ruleS(f))$ . A -rule
is associated with if theisargumactive.
Definition 2 With the notations as in the previous definition, a set of rules$S\subseteq rules(f)$ is in the ISOS format (positive ISOS format) if it satisfies
active $(S)=tau(S)$ (and all its action rules are positive). A process operator is an ISOS (positive ISOS) operator if the set of its defining rules is in the
ISOS (positive ISOS) format. An ISOS (positive ISOS) process language is a
triple ( , AU), where is a finite set of ISOS (positive ISOS) operators,, A is finite andis a finite set of rules for operators in .
Most of the operators in commonly used process languages are positive ISOS
except, for example, for the CCS and ACP choice operator
the ACP
left-merge operator. They are not positive ISOS because they do not havethe associated -rules. But, there are positive ISOS versions of these operators
which arefor most of the purposes. For example, the CSP external
choice operator ffl is one of the positive ISOS choice. It is definedby the following rule schema$\tau$$\tau$$i\mathrm{t}\mathrm{h}$$X_{i}$

$r$

$r$

$S$

$i$

$\tau$$\Sigma$$\{\tau\},$$f$$\tau_{i}$$R$$i\mathrm{t}\mathrm{h}$$\mathrm{e}\mathrm{n}\mathrm{t}$of..f$\Sigma$$R$$\mathrm{A}\subseteq \mathrm{V}_{\mathrm{I}}\mathrm{s}$$\Sigma$$+\mathrm{a}\mathrm{n}\mathrm{d}$$\tau$$\mathrm{a}\mathrm{p}\mathrm{P}^{\Gamma \mathrm{o}\mathrm{p}\mathrm{r}}\mathrm{i}\mathrm{a}\mathrm{t}\mathrm{e}$$\mathrm{o}\mathrm{p}\mathrm{e}\mathrm{r}\mathrm{a}.\mathrm{t}\mathrm{o}.\Gamma \mathrm{s}$$Xarrow X’a$$X$

$Yarrow Y’a$ffl $Yarrow x’a$$X$

ffl $Yarrow Y’a$

together with two appropriate -rules. Also, the CSP internal choice operator
and the mixed choice defined in [12] are positive ISOS operators.
Given an ISOS process language ( , AU), a fabeled transition system
can be defined in a standard way; the details can be found, for example, in[5, 17, 7, 12]. A labeled transition system for the above language is a structure$\tau$$\Sigma$$\{\tau\},$

$R$

200
is a set of process terms or processes andis the unique transition relation generated by thetransition system the basic transition systemlanguage. We will often calland, wherefor a given language. Expressions of the form
, are called transitions. They are varied by $T’$ . With the notationAU.
valid (holds)
as above, we say that: for $(p, a, q)\inarrow$ we write $parrow aq$
We will use some standard
and interpret it as process performs and in doing so becomes . The. $parrow aq$ andforabbreviations we will use are,such that $p=p_{1}$ ,. Also,means $p=q$ or
to mean...
and $p_{n}=q$ . Using the above we write
for some .
Next, we define a version of weak bisimulation relation which is based onin [18, 19, 12]. This
weak bisimulation (or observation equivalence)version is often called delay bisimulation $[20, 21]$ .
systems for a given ISOS process
Definition 3 Assume the basic.
language with the set of actions A($\mathrm{T}(\Sigma)$,A$\cup\{\tau\},$$arrow$), where$\mathrm{T}(\Sigma)$$arrow\subseteq \mathrm{T}(\Sigma)\cross \mathrm{A}\cup\{\tau\}\cross(\mathrm{T}(\Sigma)$$\mathrm{t}\mathrm{h}|‘ \mathrm{s}$$tarrow\alpha t’$$\alpha\in$$t,$ $t’\in \mathrm{T}(\Sigma)$$T,$$\{\tau\}$$\mathrm{t}_{\Gamma \mathrm{a}\mathrm{n}}\mathrm{S}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}tarrow t\alpha/\mathrm{i}\mathrm{s}$$\mathrm{i}\mathrm{n}arrow \mathrm{i}\mathrm{f}(t, \alpha, t’)\inarrow$$\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$

$a$

$p$

$parrow a$$q$$p\neq^{a}*\mathrm{f}\mathrm{o}\mathrm{r}\neg\exists q\in$$\exists q\in \mathrm{T}(\Sigma)$$p\Rightarrow^{\tau}q$$\exists p_{1},$$\mathrm{T}(\Sigma)\mathcal{T}^{\cdot}parrow qa\tau$$\ldots$$p_{n}$$p\Rightarrow aq$$arrow p_{n}$$p_{1}arrow$$p\Rightarrow p’\tauarrow qa$$p’$$\mathrm{d}\mathrm{i}_{\mathrm{S}\mathrm{C}}\mathrm{u}\mathrm{s}\mathrm{s}\mathrm{e}\mathrm{d}$$\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{S}\mathrm{i}\mathrm{t}\mathrm{i}_{0}\mathrm{n}$$\cup\{\tau\}$

1. A binary relation $R$ on processes is a weak bisimulation if $pRq$ implies,,
for all$\alpha\in \mathrm{A}\cup\{\tau\}$2.

$p\approx q$$\forall p’$.

$parrow p’\alpha$$\forall q’$.

$qarrow q’\alpha$implies (implies ($\exists q’’$$\exists p’$

and $p’Rq’$ ),. $p3p’$ and $p’Rq’$ ).
.

$q\Rightarrow\alpha q’$

if there exists a weak bisimulation$R$such that $pRq$ .

The difference between our definition of weak
and the standard
notion as defined, for example, in [2] and denoted here bylies in the: in [2]meaning ofmeans
for some $p’,$ . It is
worth noting
finersince the third -law not soundOne of the reasons for choosing this version of weak bisimulation is thatthe standard version is not preserved by many
positive ISOS operators.
In fact, there are much simpler De Simone operators [15], foractionrefinement-like operators,
fail to preserve the standard version.
Finally, we state the congruence result
and ISOS operators.
Proposition 4 Let $G=$ ( , A) be any (positive) ISOS process language. Then is preserved by all operators, that is for all $(f, n)\in\Sigma$ wehave.
implies $f(p_{1}, \ldots, p_{n})\approx f(q_{1}, \ldots, q_{n})$ .
$\mathrm{b}\mathrm{i}\mathrm{s}\mathrm{i}\mathrm{m}\mathrm{u}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}$$\approx_{B}$$p\Rightarrow aq$$p\Rightarrow p’\tauarrow aq’\Rightarrow\tau q,$$p\Rightarrow aq$$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{n}\approx_{B}$$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}\approx \mathrm{i}\mathrm{s}\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{i}_{\mathrm{C}}\mathrm{t}\mathrm{l}\mathrm{y}$$q’$$\mathrm{i}_{\mathrm{S}}$$\tau$$\mathrm{f}\mathrm{o}\mathrm{r}\approx.$$\mathrm{s}\mathrm{i}\mathrm{m}\mathrm{P}^{\mathrm{l}\mathrm{e}}$$\mathrm{e}\mathrm{x}\mathrm{a}\mathrm{m}_{\mathrm{P}^{\mathrm{l}\mathrm{e}}}$$\mathrm{w}\mathrm{h}\mathrm{i}\mathrm{C}\mathrm{h}$$\mathrm{f}_{\mathrm{o}\mathrm{r}}\approx$$\Sigma$$R$$\Sigma$$\approx$$\forall 1\leq i\leq n$$\cup\{\tau\},$$p_{i}\approx q_{i}$The proof is similar to that of Theorem 9.5.1 in [12], thus it is omitted.

201
3

Ordering on Rules

The antecedents of ISOS rules, unlike those of positive ISOS rules, refer to boththe positive and negative behaviour of subprocesses. We will use a priority
ordering on positive ISOS rules in order to achieve the effect of rules withnegative antecedents. The ordering specifies the r.der in which the rules areto be applied when deriving transitions of terms.
Example 5 Consider an operator such that $f(p)$ behaves like except thatwhenever cannot perform then $f(p)$ can perform a new action . Operator
can be defined by the following ISOS rules.
$.0$

$f$

$p$

$\tilde{b}$

$b$

$p$

$f$

$\tau b$$Xarrow X’\alpha$$X\wedgearrow$$f(X)arrow\alpha f(X’)$$f(X)arrow\overline{b}f(X)$But, $f$ can also be defined as follows, for$Xarrow x’\alpha$$\alpha\neq b$,$Xarrow X’\tau$$\overline{f(X)\alphaarrow f(x’)}r_{1}$$\overline{f(X)\tauarrow f(x’)}\tau_{1}$$Xarrow x’b$.

.

$f(X)arrow\overline{b}f(X)$$r_{2}$$r_{3}$$f(X)arrow f(x’)b$$r_{3}<r_{2}$ . We notice that, using ISOS rules,
with the ordering
ifand only if. Applying the positive ISOS rules with the above ordering$f(p)arrow\overline{b}$$r_{3}<\tau_{1},$$\tau b$$p\neq*arrow$

we can deduce
only if rules
andcannot be applied for $f(p)$ : thatis whenand.
Let
be a relation on rules $(f)$ . $r<_{f}r’$ means that has a lower priority
than
(and
has a higher priority than ) when deriving the transitions of$f(p)$ , any . By this we mean that a rule can only be applied when no rules withhigher priority can be applied. We do not assume irreflexivity or transitivityof the relation. Given positive ISOS language $G<c$ , or simply
if isclear from the context, is.
Definition 6 An ordered process language is a pair $(G, <)$ , whereis apositive ISOS process language andthe ordering on its rules as describedabove.
Next, we describe how to associate a transition relation with $(G, <)$ . Our
method is
ed on that originated in [22]. We will need a function$f(p)arrow\tilde{b}$$\tau_{1}$$r_{2}$$p\wedge b$$p\wedge \mathcal{T}$$r$$<_{f}$

$r’$

$r’$

$r$

$p$

$G$

$<$

$<_{f}$$\bigcup_{f\in\Sigma_{G}}<_{j}$$G$$<\mathrm{i}\mathrm{s}$$\mathrm{b}\mathrm{a}s$$d:\mathrm{T}(\Sigma)arrow$

202$\mathrm{N}$$\Sigma$to specify the depth of operator names in a ground term over a signature. Function is defined inductively:$d$$\bullet$$\bullet$$d(t)=0$ if$t$

is a constant,$d(g(t_{1}, \ldots , t_{f}))=1+\max\{d(t_{i})|1\leq i\leq r\}$.

The extension of to transitions is defined as expected: $d(tarrow*t’)=d(t)$ .
Also, the following will be useful: higher $(r)=\{r’\in rules(f)|r<_{f}r’\}$ , andcorrespondingly lower $(r)$ .
$d$Definition 7 Given $(G, <)$ we associate a transition relation,, defined as follows:, where transition relationsare:$arrow\subseteq \mathrm{T}(\Sigma)\cross$$\mathrm{A}\cup\{\tau\}\cross \mathrm{T}(\Sigma)$$arrow=\bigcup_{l<\omega}$$arrow^{l}$$arrow^{l}\subseteq \mathrm{T}(\Sigma)\cross \mathrm{A}\cup\{\tau\}\cross \mathrm{T}(\Sigma)$$T\inarrow l$

iff $d(T)=l$ &$\exists r\in R,$$\rho$:&\rho (ante$Varrow \mathrm{T}(\Sigma)$

$(r)$

)

. $[\rho(ConS(r))=T$$\in\bigcup_{k<l}arrow k$$\ \forall r’\in higher(r)$. $\rho(ante(r);)\not\in\bigcup_{k<l}arrow k]$ .

Similarly as in [22] it is easy to show that the transition
with a given $(G, <)$ agrees with it. Intuitively, it means that all transitions inderivable by rules of under the ordering . In general, there may be
a number of transition relations which agree with $(G, <)$ . But, we claim thatthe transition relation associated with $(G, <)$ is the unique transition relation
which agrees with $(G, <)$ . The definitions of the basic and derived transition
systems for $(G, <)$ are then straightforward.

$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}arrow \mathrm{a}\mathrm{s}\mathrm{s}\mathrm{o}\mathrm{c}\mathrm{i}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{d}$$arrow \mathrm{a}\mathrm{r}\mathrm{e}$

4

$G$

$<$

Ordered Rules with Silent Actions

One may wonder if all process operators which are defined by ordered positive
ISOS rules preserve our version of weak bisimulation. The answer is negative.
We will give a number of examples to prove our claim. Moreover, these examples will help us to find a number of conditions such that all operators, which
can be defined by rules satisfying these conditions,.
: In order to shorten the presentation of the forthcoming conditions we will leave out the outermost universal quantifiers binding $f\in\Sigma$ and$r\in rules(f)$ . Also, all the rules mentioned in the conditions, i.e.
and ,are understood to belong to rules $(f)$ .
$\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{s}\mathrm{e}\Gamma \mathrm{v}\mathrm{e}\approx$$\mathrm{N}\mathrm{o}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$$\tau_{i},$

$r$

$r’$

203
Consider an interleaving parallel operator

defined as follows:$||$$Xarrow x’a$

$Xarrow x’\tau$$r_{a*}$$\tau_{1}$$X||Yarrow \mathrm{x}^{J}a||Y$$X||Yarrow X^{J}\tau||Y$$Yarrow Y’a$

$Yarrow Y’\mathcal{T}$$r_{*a}$$\tau_{2}$$X||Yarrow X\mathcal{T}||Y’$$X||Y\underline{\backslash }Xa||Y’$

The names of rules and rule schemas accompany them on the right., The. Now we haveordering is
, but
and
.
Thus, we need to find a conditions on the ordering relation which would
not allow the above ordering. The first condition might be as follows.
if$r$$a||\tau b\Rightarrow b$$a||b\Rightarrow^{b}$$b\approx\tau b$$r_{a*}>\tau_{2}$is a -rule then higher$\tau$$(r)=\emptyset$

The intuition is that -rules should not have lower priority. But, although thecondition is quite natural it is also restrictive. For example, let be a binary
operator. When deriving the behaviour of $f(p, q)$ one may want to give priority
to the first subprocess (like with the sequential composition operator). This
may result in some rules associated with the first subprocess being above .
We can allow such orderings provided that all the rules, which are above ,are above all the rules with active second argument. This can be written as
follows.
$\tau$$f$$\tau_{2}$$\tau_{2}$if$r\in higher(\mathcal{T})\dot{i}$then$l_{owe}r(\tau_{i})=\emptyset$$\forall r’$and. if $i\in active(r’)$ then $r\in higher(r’)$(1)

The condition implies
no action rule can be above any of its -rules.
There are operators, definable by
ISOS rules satisfying condition(1), which do not preserve weak bisimulation. Consider the priority operator
which gives priority over . It is defined by the following rule schema, for$\tau$$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}\sim$$\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{i}\mathrm{t}\prime \mathrm{i}\mathrm{V}\mathrm{e}$$d$$\theta$$\alpha\in\{b, d, \tau\}$

$b$

,

.
$Xarrow X^{J}\alpha$$\theta(X)arrow\theta(x’)\alpha$.

The action rules are denoted byand , and the -rule is . Suppose$r_{d}>r_{b}$ . Let $p=b||\tau d$ and $q=b||d$ , whereis theinterleaved parallel$\tau$$r_{d}$$r_{b}$$||$

composition operator. Then,
we additionally require.

$p\approx q$$\tau_{1}>r_{b}$and$\theta(p)\Rightarrow^{b}$

usu.a1, but$\theta(q)\Rightarrow b$$\tau_{1}$. To repair this204

This example leads to the following condition.
(2)

if $i\in active(higher(r))$ then $\tau_{i}\in higher(r)$The intuition here is that in order to apply the rule we need to make surethat no other rules with higher priority (and thus their -rules) can be applied.
Next, we claim our main result.
Theorem 8 Let $(G, <)$ be an ordered process language, where $G=(\Sigma,$$R)$ is any positive ISOS process language and the orderingsatisfies
conditions (1) and (2). Then defined over the derived transition system for$(G, <)$ is preserved by all
operators.
is proved similarly as, for example, in [1.7, 6, 12]. Due to the lackTheof space the proof is omitted.
$r$$\tau$$\mathrm{A}\cup$$<$$\{\tau\},$$\approx$$\Sigma$$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{e}_{\vee}\mathrm{m}$5Applications

Sequential composition is often defined by rules with negative antecedents
as, for example in $[5, 7]$ . However, it can be defined by the following ordered:
rule schemas, where$a,$$b\in \mathrm{A}$$\mathrm{Y}arrow Y’b$

$Xarrow X’a$’
$X;\mathrm{Y}arrow X;\mathrm{Y}a$$r_{*b}$$r_{a*}$.

$X;Yarrow \mathrm{Y}’b$and . The ordering on the rules
together with the appropriate -rules
satisfies $r_{a*}>r_{*b},$ for all
and the conditions (1) and (2).
are employed in process languages to represent such phenomena
visible actions
as time-outs and interrupts. For a given partial order
is a restriction of $X$ such that action can only happen only if no $b>a$ ispossible. This can be defined operationally by the first of the following rules.
$\tau$$\tau_{2}$$a,$$\tau_{1}$$\tau_{2}$$b$$\mathrm{P}\mathrm{r}\mathrm{i}\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{e}\mathrm{s}$$\theta(X)$$<\mathrm{o}\mathrm{n}$$a$$Xarrow X’\alpha$$Xarrow X’a$

$X\wedge\beta(\forall\beta>\alpha)$$r_{a}$$\theta(X)arrow a\theta(X’)$$\theta(X)arrow\alpha\theta(X’)$

However, can be defined by a set of ordered positive ISOS rules, like thesecond rule above for each $a\in$ A and the -rule . The ordering requires$r_{a}<r_{b}$ whenever $a<b$ , andwhenever there exist an action rulesuch that $r_{a}\in higher(r_{b})$ . In [23], the first author surveyed a number ofapproaches to priorities in process algebras. He showed how these approaches
might be fitted into a common operational framework based on ordered rules.
$\theta$$\tau$$\tau_{1}>r_{b}$$r_{a}$$\tau_{1}$205
The broadcast parallel operator
tive ISOS rules$Xarrow X’a$

$Yarrow Y’a$

$X||Yarrow Xl|a|Y’$

denoted by6$r_{aa},$ $r_{a*}$and$r_{*a}$$||$can be defined by the following posi-$Xarrow X’a$

$Yarrow Y’a$

$X||Yarrow Xa’||Y$$X||Yarrow x|a|Y’$ ,respectively, with the ordering $r_{aa}>r_{a*},$$r_{*a}$.

$\mathrm{C}_{\mathrm{o}\mathrm{n}}\mathrm{C}\mathrm{l}\mathrm{u}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{S}$We have introduced a new method for operationally defining arbitrary process operators which are normally defined by transition rules with negative
antecedents. Our method relies on rules without negative antecedents but weequip the rules with an ordering. It specifies the order in which the rules areapplied when deriving transitions of process terms. We have also proposed two
conditions on rule orderings which guarantee that all operators definable byrules satisfying these conditions preserve weak bisimulation.

References
1. R. Milner. A Calculus for Communicating Systems. Springer-Verla.g,
Berlin, 1980. LNCS 92.
2. R. Milner. Communication and Concurrency. Prentice Hall, 1989.
3. G. Plotkin. A structural approach to operational sema,ntics. Technical. Report DAIMI FN-19, Aarhus University, 1981.
4. R. de Simone. Higher-level synchronising devices in ME. IJE-SCCS. Theoretical Computer Science, Vol. 37, pp. 245-267, 1985.
5. B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation
be traced:preliminary report. In Conference Record of the 15th ACM Symposiumon Principles of Programming Languages, San Diego, California, 1988.
6. B. Bloom. Ready simulationf bisimulation, and the $semanti_{CS}$ of CCS.
like languages. PhD thesis, MIT, 1990.
B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can’t be traced.
Journal of ACM, Vol. 42(1),, 1995. Also appeared as Technical Report
TR 90-1150, Cornell, 1990.
8. B. Bloom. Strong process equivalence in the presence of hidden moves.
Preliminary. report, MIT, 1990.
9. B. Bloom. Structural operational semantics for weak bisimulations. Theoretical Computer Science, Vol. 146, pp. 27-68, 1995. Also appeared as
Technical Report TR 93-1373, Cornell, 1993.
$\mathrm{c}\mathrm{a}\mathrm{n}^{)}\mathrm{t}$

7..

206
10. F.W. Vaandrager. On the relationship between process algebra and inautomata. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, 1991.
11. I. Ulidowski. Equivalences on observable processes. In P. roceedings ofthe 7th Annual IEEE Symposium on Logic in Computer Science, Santa
Cruz, California, 1992.
12. I. Ulidowski. Local Testing and Implementable Concurrent Processes.
PhD thesis, Imperial College, University of London, 1994.
13. L. Aceto, B. Bloom, and F.W. Vaandrager. Turning SOS rules into
equations. In Proceedings of the 7th Annual IEEE Symposium on Logicin Computer Science, Santa Cruz, California, 1992.
14. I. Ulidowski. Axiomatisations of weak equivalences for De Simone languages. In I. Lee and S.A. Smolka, editors, Proceedings of the 6th International Conference on Concurrency Theory CONCUR’95, Philadelphia,
1995. Springer-Verlag. LNCS 962.
15. I. Ulidowski. Finite axiom systems for testing preorder and De Simone
process languages. In Proceedings of the 5th $Internationa\iota c_{\mathit{0}}nference$ on
Algebraic Methodology and Soflware Technology AMAST’96, M\"unchen,
Germany, 1996.
16. R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, Vol. 34, pp. 83-133, 1984.
17. J.F. Groote and F. Vaandrager. Structured operational semantics andbisimulation as a congruence. Information and Computation, Vol. 100,
pp. 202-260, 1990.
18. R. Milner. A modal cha.r acterisation of bservable machine behaviours.
In G. Astesiano and C. B\"ohm, editors, CAAP 81, pp. 25-34, Berlin,
1981. Springer-Verlag. LNCS 112.
19. S. Abramsky. Observation equivalence as a testing equ‘ivalence. Theoretical Computer Science, Vol. 53, pp. 225-241, 1987.
20. W.P. Weijland. Synchrony and Asynchrony in Process Algebra. PhD
thesis, University of Amsterdam, 1989.
21. R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction
Processing
in bisimulation semantics. In G.X. Ritter, editor,
89, pp. 613-618. Elsevier Science Publishers B. V. (North-Holland),
1989. To appear in JACM.
22. J.F. Groote. Transition system specifications with negative premises.
In J.C.M. Baeten and J.W. Klop, editors, Proceedings of CONCUR’90,
Amsterdam, 1990. Springer-Verlag. LNCS 458.
23. I.C.C. Phillips. Approaches to priority in process algebras. Unpublishedmanuscript, 1994.
$\mathrm{p}\mathrm{u}\mathrm{t}/\mathrm{o}\mathrm{u}\mathrm{t}\mathrm{p}\mathrm{u}\mathrm{t}$$.0$$Inf_{\mathit{0}r}mation$