数理解析研究所講究録996 巻 1997 年 23-38

23

Speed-Sensitive Orders

for Communicating Processes
Ichiro Satoh*
Department of Information Sciences, Ochanomizu University
2-1-1 Otsuka Bunkyo-ku Tokyo 112 Japan

Abstract
This paper proposes two process calculi for synchronously communicating real-timeprocesses and asynchronously ones. They are extensions of existing process calculi
with the ability to express a time-dependent constructor, representing execution
time and delayed processing. We also construct a theoretical framework for the
performance analysis of communicating processes. It is formulated as two algebraic
order relations for synchronously communicating processes and asynchronously ones.
The relations can order two behaviorally equivalent processes with respect to theirrelative execution speeds. It provides a suitable method to verify and optimize
real-time communicating systems.

1

Introduction

Over the last few years, many researchers have explored time-extended process calculi forthe specification and the verification of real-time systems, for example see [7, 10, 16, 18, 19,23]. Most of them are extensions of existing untimed process calculi, like CSP [11], CCS[14], and ACP [3], with the ability to quantitatively express temporal features, for example
delayed processing, timeout handling, and so on. Some of the researchers also havedeveloped time-sensitive equivalences by extending existing untimed equivalences such as
bisimulation [14] and testing equivalence [9] with the notion of time. These equivalences
equate two real-time processes when both their functionally behavioral properties andtheir temporal properties are completely matched with each other.
However, the equivalences may often be too strict in the analysis of most timedependent systems, including non-strict real-time systems. This is because most systems have various temporal uncertainties, for example unpredicted transmission delays
in communication, and unexpected interruptions in processors. Therefore, the temporal properties of implementations in the real world are never the same as those of their
specification exactly. Also, we can often say that an implementation is able to satisfy its
specification, only when the implementation can perform the behavioral properties given
in its specification at earlier timings than those given in the specification.
*Email: ichiro@is.ocha.ac.jp

24
Therefore, it is convenient to construct a verification framework that can decide
whether two processes can perform the same behaviors and whether one of them (e.g.
an implementation of a system) can perform the behaviors faster than the other (e.g. thespecification of the system). Moreover, in real communicating systems, interprocess communication is often realized by means of asynchronous style as well as synchronous one.
In asynchronous communication settings, the sender of a message cannot know whenthe message is actually consumed as opposed to synchronous ones. Consequently, theverification of asynchronously communicating processes requires another time-sensitive
framework. We address both synchrony and asynchrony in communication.
This paper proposes such a framework. It is formulated through two algebraic orderrelations on real-time processes with respect to their execution speeds. The relations canorder two processes when they have the same behavioral properties and one of them canperform the properties earlier than the another. To clarify our exposition, we first develop
two new time-extended calculi towards synchrony and asynchrony in communication. Oneof them aims to model synchronous interactions among real-time processes and the other is
to model asynchronous interactions among ones. We next equip each calculus with its own
speed-sensitive order relation, which corresponds to its communication fashion. We have
many occasions to replace a slower subsystem in a system with a faster subsystem. In sucha reconstruction, we need to guarantee that the slower subsystem can really be replacedby the faster one without altering the behavioral properties or lowering the execution
speed of the whole system. We thus investigate the substitutability of speed-sensitively
ordered processes.
The organization of this paper: The organization of this paper is as follows: In
the next section we briefly present our basic ideas concerning the process calculi andthen define their syntax and semantics. In Section 3 we define two speed-sensitive orderprocesses and study theirrelations on synchronously
basic properties. In Section 4 we compare with related work and in the final section wegive some concluding remarks.
$/\mathrm{a}\mathrm{s}\mathrm{y}\mathrm{n}\mathrm{c}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{n}\mathrm{o}\mathrm{u}\mathrm{S}\mathrm{l}\mathrm{y}\mathrm{C}\mathrm{o}\mathrm{m}\mathrm{l}\mathrm{n}\mathrm{u}\mathrm{n}\mathrm{i}_{\mathrm{C}\mathrm{a}\mathrm{t}}\mathrm{i}\mathrm{n}\mathrm{g}$2Calculi

This section constructs two calculi by extending CCS [14] with the notion of quantitative
time.

2.1

Basic Framework

Before defining the calculi, we summarize our basic ideas of them.

Time Values
We assume that time is interval between events instead of any absolute time, and is
discrete, instead of continuous time. Time values are denoted as positive natural numbers
including zero.

25
The Passage of TimeTime passes in all processes at the same speed. Also, all processes follow the same clock,or different ones but well-synchronized clocks. The advance of time is modeled as a specialtransition which is labeled by a quantity of time to indicate the amount of the advance,
for example$Prightarrow P’\langle t\rangle$. It means that process$P$

become $P’$ after$t$time units.

Instantaneous Action
To preserve the pleasant properties of the original calculus, all communication and internal actions are assumed to be instantaneous. Instead, we introduce a special language
construction to express temporal costs, including the execution time of processes.
Time-Dependent Behavior
We introduce a new prefix operator whose contents are dependent on the passage of time,called delay operator. This operator suspends a process for a specified period, written asmeans a process which is, where is the amount of the suspension. For instance,idle for time units and then behaves as .
$\langle t\rangle.P$$t$$\langle t\rangle$$P^{1}$$t$

IdlingWe assume that when an internal or communication action is enabled, processes must
perform the action immediately without imposing unnecessary idling.2 This assumption
is the same as the notion of maximal progress shown in [10, 19, 23]. It lets us measure
the minimum cost in synchronization among parallel processes, and enables the calculus
to preserve the observation properties of CCS.
Asynchronous Communication
The word asynchrony here means that sender processes can send messages without synchronizing any processes. However, most of existing process calculi, including CCS [14]are formulated based on synchronous communication, they can have the expressive powerof asynchronous communication. A way to express asynchronous communication is to, in the original calculus to the case where is a terrestrict the formation of a term,
minate process, written as . That is, an asynchronous output, , followed by a process,. This approach is essentially similar to, is the same as the parallel composition
several existing ones, for example see [1, 4, 12]. We also assume that the order of message
arrival is indeterminate.3$P$$\overline{a}.P$

$0$

$P$

$\overline{a}$$\overline{a}.0|P$

1We can introduce some operators which restrict the possibility of particular actions due to the passageof time, but leave a calculus with such operators to other paper, e.g. [19]. That result is available in thecalculi presented here.
2On the contrary, we can assume that when an internal or conununication action is enabled, processes
may not perform the action soon. We leave further details of this alternative model to another paper[20].
3In this paper, we assume that communication delay is negligible. In [20], we present a calculus
for communicating systems where processes are located remotely and communication delay cannot beignored.

26

Definition

3

This section defines the syntax and the semantics of the calculi.

Timed Calculus for Synchronous Communication

3.1

We present a calculus for synchronous interactions among real-time processes. The calculus is called TSCS (Timed calculus for Synchronously Communicating Systems) and is
an extension of Milner’s CCS [14].
SyntaxThe syntax of the calculus is coincide with all the construction of CCS except for a new
time-dependent operators, called delay operator. We first define the notations of timevalues.

Definition 3.1 Let
call time domain.

denote the set of the positive natural numbers including . We$\mathcal{T}$$0$$\mathcal{T}$$\square$Next, we define symbols to present the events of processes.

Definition 3.2$\bullet$

Let $A$ be an infinite set of names denoting communication actions. Its elements aredenoted as $a,b,\ldots$
Let be an infinite set of -names. Its elements are denoted asLet
be a set of communication action names. Elements of the set are
written as.
Let denote an internal action.
Let be the set of actions corresponding the amount of the passage of time. Elements of the set are denoted as, , where.
Letbe the set of operational actions. Its elements are denoted as.
$\overline{A}$$\bullet$$\bullet$$\mathcal{L}\equiv A\cup\overline{A}$$\ell,$$\bullet$$\bullet$$\overline{a},\overline{b},\ldots$$\mathrm{c}\mathrm{o}$$\ell’,$$\ldots$$\tau$$\Gamma$$\langle t_{1}\rangle,$$\bullet$$\langle$$t_{2})$$t_{1},$$\ldots$$t_{2},$$\ldots\in \mathcal{T}$$Act\equiv \mathcal{L}\cup\{\tau\}$$\alpha,\beta,\ldots$$\square$is the complementary action of . -action represents all handshake communications
and is considered to be unobservable from outside environments.

$\overline{a}$$a$$\tau$

Definition 3.3 The setof TSCS expressions ranged over by $P,$
recursively by the following abstract syntax:$\prime \mathcal{P}_{s}$

$P$

$::=$
$|$

$|$

$|$

(Terminate Process)(Summation)(Action Restriction)(Delay Prefix)$0$$P_{1}+P_{2}$$P\backslash L$$\langle t\rangle.P$$\alpha.P$$|$$P_{1}|P_{2}$

$|$

A

$|$

$\mathrm{d}=^{\mathrm{e}\overline{1}}P$$P_{1},$$P_{2},$$\ldots$

is defined(Action Prefix)(Composition)(Recursive Definition)

where is an element of and is a subset ofis a process variable in set . We
assume that in
is always closed, and each occurrence of in is only withinsome subexpressions
where is not empty, or $t).A$ where $t>0$ .
$t$$\mathcal{T}$$A$$\mathrm{d}=^{\mathrm{e}t}P,$

$L$

$A$

$\mathcal{L}.$$P$$\alpha.A$$\mathcal{K}$$A$$\alpha$$P$$\langle$$\square$27
The informal meaning of each process constructor is as follows:$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$is a terminate process which can perform no internal nor communication action.
is a process to perform action and then behaves like , where is an input,
output, or internal action.
$P_{1}+P_{2}$ represents a process which may behave as eitheror .
represents that process
andmay run in parallel.
behaves like but it is prohibited to communicate with external processes atactions in.
means that is defined as , where may include .
represents a process which is suspended for time units and then behaves like.
$0$$\alpha.P$$P$$\alpha$$P_{1}$$P_{1}|P_{2}$$P_{1}$$\alpha$$P_{2}$$P_{2}$$P$$P\backslash L$$L\cup\overline{L}$$\bullet$$\bullet$

$A$

$A$

$\mathrm{d}=^{\mathrm{e}\mathrm{f}}P$

$P$

$P$

$\langle t\rangle.P$

$A$

$t$

$P$

We need the notion of action sort later.

Definition 3.4

when A$\mathrm{d}\mathrm{e}\mathrm{f}=P$

The syntactic sort of each process,$\mathcal{L}(0)$$=$$\mathcal{L}(\overline{a}.P)$$=$, is defined inductively by:$\emptyset$$\mathcal{L}(a.P)$$=$$\{a\}\cup \mathcal{L}(P)$$\{\overline{a}\}\cup \mathcal{L}(P)$$\mathcal{L}(\tau.P)$$=$$\mathcal{L}(P)$$\mathcal{L}(P_{1}|P_{2})$$=$$\mathcal{L}(P_{1})\cup \mathcal{L}(P_{2})$$\mathcal{L}(\langle d\rangle.P)$$=$$\mathcal{L}(P)$$\mathcal{L}(P_{1}+P_{2})$$=$$\mathcal{L}(P_{1})\cup \mathcal{L}(P_{2})$$\mathcal{L}(P\backslash L)$$=$$\mathcal{L}(P)-(L\cup\overline{L})$, we have$\mathcal{L}(P)$$\mathcal{L}(P)\subseteq \mathcal{L}(A)$. We often call sort simply.

$\square$Semantics
The operational semantics of the calculus can computationally encompass that of CCS andembody the notion of time. The semantics is defined as two tiers of labeled transition rules.
One of them defines the semantics of functional behaviors of processes, called behavioral
transition, written as $arrow(arrow\subseteq P_{s}\cross Act\cross\prime p_{S})$ and the another defines the passage$\alpha$of time on processes, called temporal transition, written

Definition 3.5$\mathrm{a}\mathrm{s}arrow\langle t\rangle(arrow\subseteq \mathcal{P}_{s}\cross\Gamma\cross P_{s})$.

TSCS is a labeled transition system, $Act\cup\Gamma,$. The transition relation
defined by two kinds of structural
induction rules given in Figure 1 and 2.
$\langle$$\mathcal{E}_{s}|\mu\in Act\cup\Gamma\}\rangle$$\{arrow\mu\subseteq P_{s}\cross$$\mathcal{P}_{s}$$arrow \mathrm{i}\mathrm{s}$$\square$In giving the rules, we adopt the convention that the transition below the horizontal line
may be inferred from the transitions above the line.

Example 3.6(1)

We show some basic examples of processes in

is a process which performs output action
behaves like .
$\langle 2\rangle.\overline{a}.P_{1}$$\overline{a}$$\mathcal{P}_{s}$as follows:

after 2 time units and then$P_{1}$$\langle 2\rangle.\overline{a}.P_{1}arrow\overline{a}.P_{1}\langle 2\ranglerightarrow P_{1}\overline{a}$(2)is a process which can receive either input action
units, and then behaves likeor .
$\langle 3\rangle.(a.P_{2}+b.P_{3})$$P_{2}$$P_{3}$

$a$

or

$b$

after 3 time28(3) After three time units, (and$2\rangle.\overline{a}.P_{1}|\langle 3\rangle.(a.P_{2}+b.P_{3})$performs a communicate between

at action name .

$\langle 3\rangle.(a.P_{2}+b.P_{3})$$\langle 2\rangle.\overline{a}.P_{1}$$a$$\langle 2\rangle.\overline{a}.P_{1}|\langle 3\rangle.(a.P_{2}+b.P_{3})arrow\overline{a}.P_{1}\langle 3\rangle|(a.P_{2}+b.P_{3})-^{\tau}P_{1}|P_{2}$$\square$We present some basic properties of the semantics of the calculus.

Proposition 3.7(1) Maximal Progress

If $P-^{\tau}P’$ then, there is not some(2) Time Determinacy

such that$P^{JJ}$$Prightarrow P^{u}\langle t\rangle$

where $t>0$ .

$\langle t\rangle$

If$Parrow P’\langle t\rangle$

and $Parrow P^{\prime/}$ t hen $P’$ and $P’$ are syntactically identical.

$\square$

The first property means that if a process has an executable communication or an internal
action, it must perform the action immediately without imposing unnecessary idling. This
property allows us to estimate synchronization time in communication exactly. The secondmeans that time is deterministic in the sense that the passage of time does not interferewith any non-determinism.
The transition
not distinguish between observable and unobservableactions. We define two transition relations due to the non-observationability of .
$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}arrow \mathrm{d}\mathrm{o}\mathrm{e}\mathrm{s}$$\tau$

Definition 3.8
(i)
(ii)
(iii)

$P\Rightarrow^{\alpha}P’$$P\Rightarrow^{\alpha}P’\wedge$)$P\Rightarrow\langle t$$P’$is defined as
is defined as $P(-^{\tau})^{*}$$P(arrow)^{*}-\tau\alpha \mathcal{T}(arrow)^{*}P’$$\alpha$$7^{-}$$arrow(arrow)^{*}\langle t_{1}\rangle\tau P^{;}$

if$\tau$$\alpha\neq\tau \mathrm{a}\mathrm{n}\mathrm{d}\mathrm{o}\mathrm{t}\mathrm{h}\mathrm{e}_{\mathcal{T}}\mathrm{r}\mathrm{w}\mathrm{i}\mathrm{s}\mathrm{e}P(arrow)^{*}\tau\langle t_{n}\rangle P^{J}$

is defined as $P(-^{\tau})^{*}-(-)^{*}\cdots(arrow)^{*}-(-)^{*}P$ ;

$(t=$

.
is a mathematical addition over two numbers.

$t_{1}+\cdots+t_{n})$$\mathrm{w}^{\mathrm{p}}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}+$3.2$\square$Timed Calculus for Asynchronous Communication

We now define a calculus for asynchronous interactions among real-time processes, called
TACS (Timed calculus for Asynchronously Communicating Systems). It is a subset ofthe previous calculus where there is not any output prefix. We also disallow output
guards in any alternative choice. This is because in asynchronous communication settings,
it is difficult to realize output guards on choice points without synchronization at theimplementation level.

Definition 3.9 The set
expressions:

where

$a$

$P$

$::=$

$G$

$::=$

$\overline{a}$$0$$P_{a}$of TACS expressions, $P,$

$P_{1}|P_{2}$

$|$

$|$

$a.P$

is a message name in $A,$

$|$

$|$

$t$

$\langle t\rangle.P$$\tau.P$$|$$|$$P_{1},$$P\backslash L$$P_{2},$$|$$\ldots$A

is defined by the followirig$\mathrm{d}=^{\mathrm{e}\mathrm{f}}P$
$|$

$G$

$G_{1}+G_{2}$is an element of$\mathcal{T}$. We often denote$\overline{a}\mathrm{a}\mathrm{S}\overline{a}.0$.

$\square$29$\frac{P_{1}arrow P_{1}’\alpha}{P_{1}+P_{2}arrow P_{1}’\alpha}$$\alpha.Parrow P-\overline{\alpha}$$\frac{P_{1}arrow P_{\rceil}’\alpha}{P_{1}|P_{2}arrow P’|\alpha 1P_{2}}$$\frac{P_{2}arrow P_{2}’\alpha}{P_{1}+P_{2}arrow P_{2}^{J}\alpha}$$\frac{P_{1}arrow P_{1}^{;},P2arrow P_{9}^{J}l\overline{l}}{P_{1}|P_{2}arrow P_{1}’|\tau P_{2}’}$$\frac{P_{2}arrow P_{9}^{J}\alpha}{P_{1}|P_{2}arrow P1|\alpha P_{2}^{;}}$$\frac{Parrow P’\alpha}{Aarrow P\alpha},$$\frac{Parrow P’,\alpha \mathit{4}nL\cup\overline{L}\alpha}{P\backslash Larrow P’\backslash L\alpha}$(A$\mathrm{r}$$\mathrm{d}=^{\mathrm{e}}P$)$\frac{Parrow P’\alpha}{\langle 0\rangle.Parrow\alpha P’}$

Figure 1: Inference Rules for Behavioral Transition$\frac{P_{1}arrow P_{1}^{;},P_{2}\langle t\rangle\langlearrow Pt\rangle 9\prime}{P_{1}+P_{2}arrow\langle t\rangle P_{1}’+P’2}$$\overline{0arrow 0\langle t\rangle}-$$\overline{\ell.Prightarrow\ell\langle t)}-.P$$\frac{P_{1}arrow P’,P_{2}\langle t\rangle\rceilarrow P\langle t\rangle 2\prime}{\langle t\rangle}(\neg\exists P’ : P_{1}|P_{2}arrow \mathcal{T}P’)$$P_{1}|P_{2}arrow P_{1}’|P^{J}2$$\frac{Parrow\langle t\rangle P’}{\langle t\rangle}$$P\backslash L\langle t\ranglearrow P’\backslash L$$\frac{Parrow P’}{\langle t\rangle}$$\frac{Parrow\langle t\rangle P^{J}}{\langle t\rangle}$(A$\mathrm{d}\mathrm{e}t=P$)$Aarrow P’$$-\overline{\langle t\rangle}(t+t’>0)$$\langle 0\rangle.Parrow P’$$\langle t+t’\rangle.Earrow\langle t’\rangle.E$

Figure 2: Inference Rules for Temporal Transition
We give the intuitive meanings of some important expressions in the language below.
$\bullet$represents a process that sends message without synchronizing any processes
and behaves like . Note that corresponds to the asynchronous message itself.
corresponds to the subsequent computation.
$a.P$ represents a process that receives message
and then behaves like $P$ .
$(\overline{a}|P)$

$a$

$P$

$\bullet$$P$$\overline{a}$$a$Semantics
All the expressions in the present calculus are included in those in the previous one. The
semantics of the present calculus is defined through that of the previous one.

Definition 3.10 The operational semantics of TACS is defined from the transition
relation rules given in Definition 3.5.
$\square$Example 3.11
(1)

We show some basic examples of processes in

is a process which sends asynchronous message
then behaves like .
$\langle 2\rangle.(\overline{a}|P_{1})$$P_{1}$$\langle 2\rangle.(\overline{a}|P_{1})arrow\langle 2\rangle(\overline{a}|P_{1})arrow P_{1}\overline{a}$$P_{a}$$a$as follows:

after 2 time units and30(2) ( $3\rangle.(a.P_{2}+b.P_{3})$ is a process which can receive either message or after 3 timeor .
units and behaves like
performs a communication at action name .
(3)$a$$P_{2}$$b$$P_{3}$$\langle 2\rangle.(\overline{a}|P_{1})|\langle 3\rangle.(a.P_{2}+b.P_{3})$$a$$\langle 2\rangle.(\overline{a}|P_{1})|\langle 3\rangle.(a.P_{2}+b.P_{3})arrow\overline{a}\langle 3)|P_{1}|(a.P_{2}+b.P_{3})-^{\tau}P_{1}|P_{2}$$\square$

In asynchronous communication settings, sender processes cannot observe how the messages which they send will be treated by the other processes. We introduce weak labeledtransitions for asynchronous communication.

Definition 3.12 The operational semantics of TACS is redefined from the transition
relation rules given in Definition 3.5 and the following rules:$(t\in \mathcal{T})$$\overline{a}|Parrow P\uparrow a$where we often abbreviate$Parrow\langle_{t}\rangle\downarrow a\langle t\rangle.\overline{a}|P$$\langle 0)\downarrow a\mathrm{t}_{0}\downarrow a$.

$\square$We give intuitive meaning of the above transitions.
means that a conceptual observer or the environment receives message
and behaves like $P’$ .

$P-^{\mathrm{t}a}P’$$\bullet$

$a$

from

$P$

$P$

$\langle_{t})_{)a}$$\bullet$$Parrow P’$ means that after

message

$a$

and

$P$

becomes$P’$$t$time units, an observer or the environment sends.

Definition 3.13
(1)

(2)

4

$P\Rightarrow^{a}P\langle_{t}\rangle_{1\prime}$$P\Rightarrow^{\uparrow a}P’$is given as$P(-^{\mathcal{T}})^{*}arrow(\langle_{t^{\rangle\}a}}\tau-)^{*}P’$.

is given as$P(-^{\mathcal{T}})^{*}arrow(-\dagger a\tau)^{*}P^{J}$.

Speed-Sensitive Prebisimulations

Based on time-extended process calculi, several researchers have explored time-sensitive
equivalences which are based on trace equivalence, failure equivalence, testing equivalence, and bisimulation equivalence like ours, for example see [10, 16, 18, 19, 23]. These
equivalences equate two processes if they cannot be distinguished from each other in theirtemporal properties as well as their behavioral one. This section develops algebraic orderrelations on processes with respect to their speeds based on the bisimulation concept.

4.1

An Order for Synchronously Communicating Processes

We define a speed-sensitive relation for synchronously communicating processes based on
the bisimulation technique.
$\mathrm{r}$31
is a -synchronous prebisimulation$(P_{1}, P_{2})\in \mathcal{R}_{t}(t\geq 0)$ implies, for all

A binary relation
over synchronously communicating processes if;

Definition 4.1$t$$\mathcal{R}\subseteq(P_{s}\cross P_{s})\cross \mathcal{T}$$\alpha\in A_{Ct}$(i)$\forall d\forall P_{1}’:P_{1}\Rightarrow\Rightarrow\langle d\rangle\alpha P_{1}’\langle d\rangle\langle d’\rangle then$and$\wedge\alpha$$\exists d’\exists P_{2}^{;}:P_{2}\Rightarrow\Rightarrow\Rightarrow P_{2}’$(ii)$\langle d)$$(P_{1}’, P_{2}J)\in \mathcal{R}_{t+d’}$then$\alpha$$\forall d\forall P_{2}^{J}:P_{2}\Rightarrow\Rightarrow P_{2}’$$\langle d)$$\wedge\alpha$$\langle t\rangle$$\exists P_{1}’:P_{1}\Rightarrow\Rightarrow\Rightarrow P_{1}’$and$(P_{1,2}’P’)\in \mathcal{R}_{0}$$\square$is a family of relations indexed by a non-negative time value
In the above definition,and that of ; that is,. Intuitively, is the relative difference between the time ofby time units.4 The following order relation starts withprecedesit means that) and can change as the bisimulation proceeds
a prebisimulation indexed by (i.e.,
only if $t\geq 0$ .
$\mathcal{R}_{t}$$P_{2}$$P_{1}$

$t$

$t$

$t$

$P_{2}$$P_{1}$$t$$t$$\mathcal{R}_{t}^{L}$

if there exists some -synchronous prebisimulation suchDefinition 4.2 We let
speed-sensitive order on synchronously. We callthat.
asprocesses. We shall often abbreviate$t$$P_{1}\leq_{s}^{t}P_{2}$$(P_{1}, P_{2})\in \mathcal{R}_{t}$$\leq_{s}^{t}$$\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{m}\mathrm{u}\mathrm{n}\mathrm{i}\mathrm{C}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}\coprod$$\leq_{S}^{0}$

Hereafter, we usually consider
relation below.

Proposition 4.3(1)(2)

Let $P,$$\leq_{S}$$P_{1},$ $P_{2},$$\leq_{S}$only. We show several algebraic properties of the order$P_{3}\in P_{s}$. Then,$P\leq_{S}P$$P_{1}\leq_{S}P_{2}$andFrom these results, we see that.
and
$P_{1}\leq_{s^{1}}^{t}P_{2}$then $P_{1}\leq_{S}P_{3}$$P_{2}\leq_{S}P_{3}$$\leq_{S}$$\square$is a preorder relation. We also have$P_{1}\leq_{S}^{t_{1}}+t_{2}P_{3}$Proposition 4.4

Let$P_{1},$ $P_{2}\in \mathcal{P}_{s’ 1}t,$ $t_{2}\in \mathcal{T}$such that$t_{1}\leq t_{2}$. Then,$\langle t_{1}\rangle.P\leq S(t2\rangle.P$$\square$

The above proposition shows an important characteristic of
Example 4.5
(1)
(2)
(3)
(4)

We show some basic examples of$\leq_{S}$$\leq_{S}$.

as follows:$a.P\leq_{S}\langle 1\rangle.a.P$$\langle 1\rangle.\overline{a}.\langle 2\rangle.\overline{b}.P\leq_{S}\langle 1\rangle.\overline{a}.\langle 3\rangle.\overline{b}.P$$a.P_{1}|\langle 1).b.P_{2}\leq_{S}\langle 1\rangle.a.P_{1}|\langle 1\rangle.b.P_{2}$$\langle 1\rangle.(a.P_{1}+b.P_{2})|\langle 2\rangle.\overline{a}.P_{3}\leq_{S}\langle 2\rangle.(a.P_{1}+b.P_{2})|\langle 2\rangle.\overline{a}.P_{3}$Proposition 4.6(1)

if$P_{2}\leq_{s^{2}}^{t}P_{3}$Let$P_{1},$$P_{2},$$Q\in P_{s}$such that$P_{1}\leq_{S}P_{2}$$\square$. Then$\alpha.P_{1}\leq_{S}\alpha.P_{2}$4This means that the performance of$P_{1}$

is at most$t$time units faster than that of$P_{2}$

.

32
(2)
(3)

$P_{1}\backslash L\leq_{S}P_{2}\backslash L$$\langle t).P_{1}\leq_{S}\langle t\rangle.P_{2}$$\square$

It is convenient to develop a precongruence with respect to speeds in order to guarantee thesubstitutability between two ordered processes in any parallel context. However, there
is an undesirable problem in defining such a pre-congruence with temporal inequality.
. We clearly, andSuppose three objects:)
andbut cannot expect that $A_{1}|B\leq_{S}A_{2}|B$ , because
have. This anomaly is traced to contexts that restrict the capability to
execute a particular computation due to the passage of time, for example timeout handlingin $B$ . In order to define a rational pre-congruence with respect to speed, we need to impose
certain syntactic restrictions on processes that may be composed in parallel.
$A_{1}=\mathrm{d}\mathrm{e}\mathrm{f}\langle 2\rangle.\overline{a}.0,$$B^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}}a.P_{1}+b.P_{2}|\langle 3\rangle.\overline{b}.0$$A2=\mathrm{d}\mathrm{e}\mathrm{f}\langle 4\rangle.\overline{a}.0$$A_{1}|B^{\langle}-^{2\rangle\tau}-P_{1}|\langle 1$$A_{1}\leq_{S}A_{2}$$.\overline{b}.0$$A_{2}|B(3Iarrow\tau\langle 1\rangle.\overline{a}.0|P_{2}$Definition 4.7
is defined as
is called confluent summation.
.
is defined as
(2)
.
and

(1)

$(\alpha_{1}|\cdots|\alpha_{n}).P$$\Sigma_{1\leq i\leq n}\alpha_{i}$$(P_{1}|P_{2})\backslash L$$P_{1}||{}_{L}P_{2}$, where$P_{1}||{}_{L}P_{2}$$(\alpha).P\equiv\alpha.P$.

$(\alpha_{1}|\cdots|\alpha_{i-1}|\alpha_{i}+1|\cdot.\cdot\cdot|\alpha_{n}|).P$

is confluent composition if$\mathcal{L}(P_{1})\cap \mathcal{L}(P_{1})=\emptyset$$\overline{\mathcal{L}(P_{1})}\cap \mathcal{L}(P_{1})\subseteq L\cup\overline{L}$$\square$Definition 4.8 $P\in P_{s}$ is time-stable if is built using only terminate process, action
prefix, delay prefix, action restriction, confluent composition, confluent summation, andrecursion given in Definition 3.3.
$P$$\square$Example 4.9 We show some basic examples of time-stable processes:$\langle 3\rangle.(a.b.P+b.a.P)$ , and A
are time-stable processes.
, where $P,$$\overline{a}.0,$$(\langle 3\rangle.\overline{a}.P_{1}|a.P_{2})\backslash \square$$\mathrm{d}=^{\mathrm{e}\mathrm{f}}\overline{a}.b.A$$\{a\},$$P_{1},$$P_{2}$

This restriction allows processes to perform executable actions in any order. When we
focus on processes cooperating only with particular processes, there may indeed be moresuitable forms which cover a class of such processes. We here give a lemma before proving
is preserved in a parallel composition.
that$\leq_{S}$Lemma 4.10

Let

$P_{1},$ $P_{2},$ $Q_{1},$$P_{1}\leq_{s}^{t}P_{2}$$Q_{2}\in/P_{S}$andbe time-stable processes. Then,$Q_{1}\leq_{s}^{t}Q_{2}$then$P_{1}|Q_{1}\leq_{s}^{t}P_{2}|Q_{2}$$\square$

We now come to the main result of this subsection.
Theorem 4.11

Let

$P_{1},$ $P_{2},$$Q\in 7^{\mathit{2}_{s}}$$P_{1}\leq_{S}P_{2}$be time-stable processes. Then,then$P_{1}|Q\leq_{S}P_{2}|Q$$\square$Intuitively, the above result tells that a parallel composition between the faster processes
can really perform faster than one between the slower ones. That is, a system whenembedding the faster processes can still perform faster than when embedding the slower
ones.

33
An Order for Asynchronously Communicating Processes

4.2

In asynchronous communication settings, sender processes do not have to synchronize
their receiver processes and thus can send messages as soon as they can- Therefore, inthe settings real-time processes do not need to completely match their own temporal
specification, and need only to deliver their required messages to receiver processes at
earlier timings than those given in their specification. This means that in the verificationof asynchronous communicating real-time processes, a speed-sensitive order relation canbe often more suitable than in that of synchronous ones.

Definition 4.12 A binary relation
ulation over asynchronously communicating processes$b\in A$ , and;is a -asynchronous prebisimimplies, for all
if$t$$\mathcal{R}\subseteq(\mathcal{P}_{a}\cross\prime p_{a})\cross \mathcal{T}$$P_{a}$$(P_{1}, P_{2})\in.\mathcal{R}_{t}$$d\in \mathcal{T}$

$a,$

(i)

$\forall t_{1}\forall P_{1}’:P_{1}\Rightarrow^{a}\langle d\rangle\}\langle t\Rightarrow\Rightarrow\rangle 1\pi P_{1}’$then$\langle_{d}\rangle_{\mathrm{J}a}\langle t_{2}\rangle$$1b$$\exists t_{2}\exists P_{2}’:P_{2}\Rightarrow\Rightarrow\Rightarrow P_{2}’$(ii)$\forall t_{2}\forall P_{2}’:P_{2}\Rightarrow\Rightarrow^{2}\Rightarrow^{\uparrowb}(d\rangle$$\downarrow a\langle
t\rangle$1b$$\exists t_{1}\exists P_{1}’:P_{1}\Rightarrow\Rightarrow\Rightarrow P_{1}’$

$a,$

$b$

$(P_{1}’, P_{2}J)\in \mathcal{R}_{t-t_{1}+t_{2}}$and$(P_{1}’, P_{2}J)\in \mathcal{R}_{t-t_{1}+t_{2}}$then

P_{2}’$$\langle_{d}\rangle_{\rfloor a}\langle t_{1}\rangle$

where

and

may be empty names and$t,$$t_{1},$$t_{2},$ $d\in \mathcal{T}$.

$\square$As -synchronous prebisimulation,
is a family of relations indexed by a non-negative
time value , where corresponds to the relative difference between the time of the firstprocess and the second one.
$t$$\mathcal{R}_{t}$

$t$

$t$

Definition 4.13 We let
if there exists a -asynchronous prebisimulation suchthat
. We call
speed-sensitive order on asynchronously
processes. We shall often abbreviate.
as$P_{1}\leq_{a}^{t}P_{2}$$(P_{1}, P_{2})\in \mathcal{R}_{t}$$t$$\leq_{a}^{t}$$\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{m}\mathrm{u}\mathrm{n}\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}\square$$\leq_{a}$$\leq_{a}^{0}$. We first assume. ThisWe here state the informal meaning ofassumption means precedes by time units. An observer sends message to after
time units (written as
in ). It also sends the same message toafter timeunits (written asin). And then the observer receives return message from;in), and fromafter time units (written as
after time units (written. If the arrival time of the return message fromasinis earlier than that
$P_{1}\leq_{a}^{t}P_{2}$$(P_{1}, P_{2})\in \mathcal{R}_{t}$$t$$P_{2}$$P_{1}$$P_{1}$$a$$P_{1}\Rightarrow\langle d\rangle\downarrow a$

$d$

$d$

$P_{2}$$(\mathrm{i})$$P_{2}\Rightarrow\langle d\rangle\downarrow a$$b$$(\mathrm{i}\mathrm{i})$$P_{1}$$\langle t4\rangle\uparrow b\Rightarrow P_{1}$$t_{1}$$(\mathrm{i})$$P_{2}$$t_{2}$$\langle t\Rightarrow_{\Rightarrow}\rangle\uparrow b$$P^{J}2$$P_{1}$$(\mathrm{i}\mathrm{i}))$from , and if
andcan be successfully observed inin theandcan perform the same behaviors but
can perform the behaviors
same way,properties
.
of
the
order
relation below.
than
We
show
severalalgebraic
faster$P_{2^{5}}$$P_{2}’$$P_{1}’$$P_{1}$$(P_{1}’, P_{2}’)\in \mathcal{R}_{t-t_{1}+t_{2}}$$P_{1}$$P_{2}$$P_{2}$

Proposition 4.14
(1)
(2)

Let $P,$$P_{1},$$P_{2},$$P_{3}\in 7^{\mathit{2}_{a}}$. Then,$P\leq_{a}P$$P_{1}\leq_{a}P_{2}$

and

then

$P_{2}\leq_{a}P_{3}$$P_{1}\leq_{a}P_{3}$$\square$by time units. Thus, the relative difference between the arrival
already precedes
5Note thatis $t-t_{1}+t_{2}$ .
and that fromtiming of the message from
$P_{1}$$P_{2}$$P_{2}$$t$$P_{1}$

34
The above proposition says that.
and$\leq_{a}$is a preorder relation. We also have$P_{1}\leq_{a^{1}}^{t+t_{2}}P_{3}$$P_{2}\leq_{a^{2}}^{t}P_{3}$$P_{1}\leq_{a^{1}}^{t}P_{2}$Proposition 4.15

Let

$P_{2}\in \mathcal{P}_{a},$$P_{1},$$t_{1},$

such that$t_{2}\in \mathcal{T}$$t_{1}\leq t_{2}$. Then,$\square$$\langle t_{1}\rangle.P\leq_{a}\langle t_{2^{\rangle.P}}$

Example 4.16
(1)
(2)
(3)
(4)

if

We show some basic examples of$\leq_{a}$as follows:$\overline{a}\leq_{a}\langle 1\rangle.\overline{a}$$a.P\leq_{a}\langle 1\rangle.a.P$$a.P_{1}|\langle 1\rangle.b.P_{2}\leq_{a}\langle 1\rangle.a.P_{1}|\langle 1\rangle.b.P_{2}$$\langle 1\rangle.(\overline{a}|\langle 3\rangle.(\overline{b}|P))\leq_{a}\langle 2\rangle.(\overline{a}|\langle 2).(\overline{b}|P))c.f$.

$\langle 1\rangle.\overline{a}.\langle 3\rangle.\overline{b}.P\not\leq_{s}\langle 2\rangle.\overline{a}.(2\rangle.\overline{b}.P$$\square$In the above example, (4) shows a difference between synchrony and asynchrony in communication.

Proposition 4.17
(1)
(2)
(3)

Let

$P_{2},$$P_{1},$$Q\in’\rho_{a}$such that$P_{1}\leq_{a}P_{2}$. Then,$a.P_{1}\leq_{a}a.P_{2}$$P_{1}\backslash L\leq_{a}P_{2}\backslash L$$\square$$\langle t\rangle.P_{1}\leq_{a}\langle t\rangle.P_{2}$. Next, we show
when
From the above result, we directly know thatis precongruent with respect to parallel composition. We establish a convention
that
that at most one process in parallel compositions can receive any given message, for thesake of substitutability. As the same of the synchronous communication setting, we needa syntactic restriction on expressions on .
$P_{1}\leq_{a}P_{2}$$\overline{a}|P1\leq_{a}\overline{a}|P_{2}$$\leq_{a}$$\mathcal{P}_{a}$is time-stable if is built using only terminate process, action
Definition 4.18
prefix, delay prefix, action restriction, confluent summation, composition, and recursion.
and when any subsequence of occurs in form
$P$

$P\in 7^{\mathit{2}_{a}}$$P$

Note thatproving it.

$\mathcal{L}(P)\cap A$

Lemma 4.19

Let$\mathcal{L}(P_{1})\cap \mathcal{L}(P_{1})\cap A=\emptyset$

means all the action names included in$P_{1},$ $P_{2},$ $Q_{1},$$P_{1}\leq_{a}^{t}P_{2}$Theorem 4.20

$P_{1}|P_{2},$Let$Q2\in P_{a}$and$P_{1},$ $P_{2},$$P_{1}\leq_{a}P_{2}$. We need a lemma before

be time-stable processes. Then,$Q_{1}\leq_{a}^{t}Q_{2}$$Q\in 7^{\mathit{2}_{a}}$$P$$\square$then$P_{1}|Q_{1}\leq_{a}^{t}P_{2}|Q_{2}$$\square$be time-stable processes. Then,then$P_{1}|Q\leq_{a}P_{2}|Q$$\square$Intuitively, the result shows that if two processes are behaviorally equivalent and one ofthem can perform faster than the other, the faster process can be behaviorally substituted
for the slower one in a parallel composition. That is, a parallel composition between thefaster processes can really perform faster than one between the slower ones. That is, asystem embedded with the faster processes can really perform faster than one embeddedwith the slower ones.

35
Remarks The definition of each relation can reveal essential differences between synchrony and asynchrony in interactions among processes in time-sensitive contexts. In synchronous communication settings, processes must be blocked until their partner processes
are ready to communicate.
can order two synchronously communicating processes
when a conceptual observer cannot distinguish between them incommunications,and when t.he timings of the communications with one of them are earlier than those withthe another. On the other hand, in asynchronous communication settings, the observer
cannot exactly know when the messages which it sends are received by processes. It canknow only the arrival timings of return messages. In, an observer sends arbitrary messages to processes and waits for return messages from them. It orders the two processes
when the return messages cannot be distinguished from each other, and when the arrival
timings of the messages from one of them are earlier than those from the another.
$\leq_{S}$$\mathrm{t}\dot{\mathrm{h}}\mathrm{e}\mathrm{i}\mathrm{r}$$\leq_{a}$5Related WorkWe here survey some related work. There have indeed been many process calculi fortime-dependent systems, for example see [7, 10, 16, 18, 19, 22, 23]. Most of the calculi
have been equipped with time-sensitive equivalences as verification methods. However,there have been a few researchers that studied inequalities for time-dependent processes.
Moller and Tofts in [16] proposed a preorder relation over processes with respect totheir relative speeds, based on the bisimulation technique. Unlike ours, their calculus
assumes to permit an executable communication to be suspended for arbitrary periodsof time. As a result, the relation shows only that a process may possibly execute fasterthan the other. Recently, Vogler in [22] and Jenner and Vogler in [13] presented speedsensitive preorder relations based on the testing equivalence technique [9]. The relation
can relate asynchronously communicating processes according to their relative speeds,
but its semantics is formulated based on causality between events on the assumptionthat actions are not instantaneous, unlike ours. Also, some researchers have explored theperformance analysis by means of process algebras, for example see [5]. However, mostof them are based on non-instantaneous actions. The other assumes that every processproceeds in lockstep and at every instant performs a single action.
Arun-Kumar and Hennessy in [2] propose an approach to relate processes with respect
to their relative efficiencies based on the bisimulation technique [14]. Cleaveland andZwarico in [6] Natarajan and Cleaveland [17] propose a similar approach based on thetesting equivalence technique [9]. These approaches relate two processes whether their
behavioral properties are equivalent and one of them can perform less internal actions
than the other. That is to say, a process which needs to take more actions to executethe same properties than the other, is a slower process. However, it is very difficult toreflect the execution cost of real systems upon the number of -actions exactly in thedescription of the systems.
On the other hand, there have been several process calculi with the ability to express
asynchronous communication (e.g. [1, 4, 8, 12]). Among them, in [4] Baeten and Bergstra
proposed a time-extended process calculus with the ability to express asynchronous communication. It represents asynchronous message transmission as the creation of a process
corresponding to the message like the methods developed in [12]. However, it provides$\tau$$\tau$$\tau$

36
just a language to describe asynchronously communicating real-time processes and it does
not provide any method to analyze the performance of processes.

Concluding Remarks

6

In this paper, we proposed two time-extended calculi to specify and analyze synchronousinteractions among real-time processes and asynchronous ones. They are extensions of
CCS with the ability to express quantitatively temporal properties of processes. They
us to describe the behavioral and temporal properties of interactions among realtime processes.
Based on the calculi, we define algebraic order relations that can distinguish between
behaviorally equivalent processes performing at different speeds. The relations can provethat a faster process can behaviorally replace a slower process without altering any behavioral properties nor the performance of the whole system. They can provide a theoreticalframework to verify and optimize communicating systems.
This paper gives only a starting point for understanding communications among realtime processes. There are many issues that we leave in this paper, One of the mostimportant issues is to study further refinements of the calculi and the relations. We arealso interested in formulating inequalities based on the order relations, and investigating
how the relation of each calculus is related with each other.
$\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{o}\mathrm{w}\sim$

References[1] Amadio, R.M., Castellani, I, and Sangiorig, D., On Bisimulation for the Asynchronous-calculus, Proceedings of CONCUR’96, p148-162, Springer-Verlag, August, 1996.
[2] Arun-Kumar, S. and Hennessy, M., An Efficiency Preorder for Processes, Acta Informatica,
Vo1.29, p737-760, 1992.
[3] Baeten, J. C. M., and Bergstra, J. A., Process Algebra, Cambridge University Press, 1990.
$\pi$[4] Baeten, J. C. M., and Bergstra, J. A., Asynchronous Communication in Real Space Process
Algebra, Proceedings of Formal Techniques in Real-Time and Fault-Tolerant System, LNCS
rlag, May, 1991.
591, p473-491,[5] Chen. X. J., Corradini, F., and Gorrieri, R., A Study on the Specification and Verificationof Performace Properties, Proceedings of Algebraic Methodology and software Technology,
LNCS Vol. 1011, Springer-Verlag, 1996.
[6] Cleaveland, R and Zwarico, A.E., Theory of Testing for Real- Time, Proceedings, 6th IEEE
Symposiu.m on Logic in Computer Science, p110-119, 1990.
[7] Davies, J. W., Specification and Proof in Real- Time CSP, Cambridge University Press,$\mathrm{S}\mathrm{p}\mathrm{r}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{e}\mathrm{r}- \mathrm{V}\dot{\mathrm{e}}$1994.
[8] de Bore, F.S., Klop, J.W., and Palamidessi, Asynchronous Communication in Process Algebra, Proceedings of LICS’92, p137-147, June, 1992.
[9] de Nicola, E. and Hennessy, M., Testing Equivalence for Processes, Theoretical Computer
Science, No.34, 1984.
[10] Hennessy, M., On Timed Process Algebra: a Tutorial, Technical Report 2/93, University of
Sussex, 1993

37[11] Hoare, C.A.R., Communicating Sequential Processes, Prentice-Hall, 1985.

[12] Honda, K., and Tokoro, M., An Object Calculus for Asynchronous Communication, Proceedings of ECOOP’91, LNCS 512, p133-147, June, 1991.
[13] Jenner, L., and Volger, W., Faster Asynchronous Systems in Dense Time, Proceedings of
ICALP’96, p75-86, LNCS Vol. 1099, Springer-Verlag, 1996.
[14] Milner, R., Communication and Concurrency, Prentice Hall, 1989.
[15] Milner, R., Parrow. J., Walker, D., A Calculus of Mobile Processes, Information and Computation, Vo1.100, p1-77, 1992.
[16] Moller, F., and Tofts, C., Relating Processes with Respect to Speed, Proceedings of CONCUR’91, LNCS 527, Springer-Verlag, August, 1991.
[17] Natarajan, V., and Cleaveland, R., An Algebraic Theory of Process Efficiency, Proceedingsof LICS’96, p63-72, June, 1996.
[18] Nicollin. X., and Sifakis, J., An Overview and Synthesis on Timed Process Algebms, Proceedings of Computer Aided Verification, LNCS 575, p376-398, Springer-Verlag, June, 1991.
[19] Satoh, I., and Tokoro, M., A Formalism for Real-Time Concurrent Object-Oriented $C_{om}-$
puting, Proceedings of ACM Conference on Object Oriented Programming Systems, Langauges, and Applications (OOPSLA’92), p315-326, 1992.
[20] Satoh, I., and Tokoro, M., A Formalism for Remotely Interacting Processes, Proceedingsof Workshop on Theory and Practice of Parallel Programming (TPpp’94), LNCS 907,
p216-228, Springer-Verlag, 1995.
[21] Satoh, I., and Tokoro, M., Time and Asynchrony in Interactions among Distributed RealTime Objects, Proceedings of European Conference on Object-Oriented Programming(ECOOP’95), LNCS 952, p331-350, Springer-Verlag, 1995.
[22] Volger, W., Faster Asynchronous Systems, Proceedings of CONCUR’95, p299-312, LNCS
962, Springer-Verlag, 1995.
[23] Wang, Y., $CCS+Time=an$ Interleaving Model for Real Time Systems, In proceedings ofAutomata, Languages and Programming’91, LNCS 510, Springer-Verlag, 1991.

Appendix
It is often useful to give time-sensitive equivalences for the present calculi in studying theirbasic properties, although such equivalences are often too strict in the verification of realsystems. We thus develop time-sensitive bisimulation relations over process expressionsasby extending CCS’s bisimulation with the notion of time. We denote bothandlater.
$\prime \mathcal{P}_{S}$$\mathcal{P}_{o}$$\mathcal{P}$Definition 6.1
implies, for all

A binary relation,
and t$\alpha\in Act$

(i)
(ii)
$P_{1}$$\mathcal{R}$$\forall P_{1}’:P_{1}arrow-P_{1}’\langle t\rangle\alpha$$\mathcal{R}$is symmetric.

$\mathcal{R}\subseteq \mathcal{P}\cross P$

then$(P_{1}, P_{2})\in \mathcal{R}$,$\exists P_{2}’:P_{2}arrowarrow P_{2}\langle t\rangle\alpha$andare strongly equivalent, writtensuch that.
$P_{2}$

is a strong bisimulation if$(P_{1}, P_{2})\in \mathcal{R}$$\in \mathcal{T}$$P_{1}\sim\tau P_{2}$and$(P_{1}’, P_{2}^{J})\in \mathcal{R}$.

, if there exists a strong bisimulation$\square$38
are strongly equivalent, they cannot be distinguished from one
andIntuitively, if
is symmetric, reflexive,
another in their behaviors and timings. We can know thattransitive, and congruent. We show a set of laws which are sound with respect to thestrong equivalence below.
$P_{2}$$P_{1}$$\sim\tau$

Proposition 6.2$P_{1}+P_{2}$$P|0$$\sim\tau$$\sim\tau$$(P_{1}|P_{2})\backslash L$$\sim\tau$$(P_{1}+P_{2})\backslash L$$\sim\tau$$\langle t\rangle.(P_{1}+P_{2})$$\sim\tau$$\langle t_{1}+t_{2}\rangle.P$$P_{1}|(P_{2}|P_{3})$$P_{2}|P_{1}$$\sim\tau$$P\backslash L$

$P+0$

$P$

$\sim\tau$$P_{1}|P_{2}$$P_{1}+(P_{2}+P_{3})$$P_{2}+P_{1}$$\sim\tau$$P+P$$\sim\tau$$\sim\tau$$\sim\tau$$(P_{1}+P_{2})+P_{3}$$P$$(P_{1}|P_{2})|P_{3}$

$P$

if
if

$P$
$P_{1}\backslash L|P_{2}\backslash L$$\mathcal{L}(P)\cap(L\cup\overline{L})=\emptyset$$\mathcal{L}(P_{\mathrm{I}})\cap\overline{(P_{2})}\cap(L\cup\overline{L})=\emptyset$$P_{1}\backslash L+P_{2}\backslash L$$\langle t\rangle.(P_{1}|P_{2})$$\langle t\rangle.P_{1}+\langle t\rangle.P_{2}$$\langle \mathrm{O}\rangle.P$$\langle t_{1}\rangle.\langle t_{2}\rangle.P$$\sim\tau$$\sim\tau$$\sim\tau$$\langle t\rangle.P_{1}|\langle t\rangle.P_{2}$$P$

口We define an equivalence with the concept of observation.
A binary relation$\alpha\in Act$ and,Definition 6.3
implies, for all(i)(ii)$P_{1}$$\mathcal{R}$is a weak bisimulation if$(P_{1}, P_{2})\in \mathcal{R}$$t\in \mathcal{T}$$\forall P_{1}’:P_{1}\Rightarrow\Rightarrow P_{1}’\langle t\rangle\alpha$$\mathcal{R}$$\mathcal{R}\subseteq P\cross P$

is symmetric.

then$\exists P_{2}’:P_{2}\Rightarrow\Rightarrow^{\alpha}\langle t\rangle\wedge P_{2}’$andare observation-equivalent, written.
such that$P_{2}$$P_{1}\approx_{\mathcal{I}}P_{2}$and$(P_{1}^{;}, P_{2}^{J})\in \mathcal{R}$.

, if there exists a weak bisimulation$(P_{1}, P_{2})\in \mathcal{R}$$\square$must be matched
are observation-equivalent, each action ofandIntuitively, ifwith the same visible contents and timing, and conversely.
by a sequence of actions ofis symmetric, reflexive, transitive. We know that it is congruent except summation,.
ifand$P_{1}$$P_{2}$$P_{1}$$P_{2}$$\approx\tau$$P_{1}\approx_{\mathcal{I}}P_{2}$$P_{1}\sim\tau P_{2}$Proposition 6.4$\tau.P$$\tau.P+P$$\langle t\rangle.\tau.P$$\approx\tau$$P$$\approx\tau$$\tau.P$$\approx\tau$$\alpha.\tau.P$$\alpha.(\tau.P+Q)$$\approx\tau$$\approx\tau$$\alpha.P$$\alpha.(\tau.P+Q)+\alpha.Q$$\langle t\rangle.P$日

On the basis of the two equivalence relations, we can have sound and complete equationaland , but we leave them to other papers.
laws over finite processes on$\prime p_{s}$$\mathcal{P}_{a}$