数理解析研究所講究録902 巻 1995 年 64-79

64

Cost Graphs for Concurrent Calculi
久保誠*

Makoto Kubo

Department of Computer Science, Keio University
3-14-1 Hiyoshi, Kohoku-ku, Yokohama, 223, Japan

Abstract
We present a theory of cost of concurrent programs, which is an importantmeasure to evaluate their quality. The basic idea is to assign each program a setof graphs which give derivation of a program argumented with cost information,then order two progra.m by comparing these two sets. According to the ways ofcomparing these sets, various orderings which capture specific aspects of efficiency
of concurrent programs arise. We show that the efficiency preorder presented by
Arun-Kumar and Hennessy, is closely related with one of these orders, thus showing
our theory is a conservative extension of their construction.
$\mathrm{s}$1Introduction

One essential quality of a program is its efficiency or cost of computation. If two programs
can achieve the same thing, we always prefer the one which runs faster or at least theone which does the work “in time”1. In fact this is one of the most important concerns
in theoretical computer science, where the formal transformation methods for program
optimization is along-lasting and still active field of study. Now for any such methodology,
we should have a basic notion of what we mean by cost of programs. While this may
not be easy in the real applications, some clean idea in the abstract setting should surely
help, giving the basic criteria and a reference framework for further ramifications, offering
a formal way of evaluating the quality of software components.
In the sequential programs, one clean answer exists, which says an abstract cost of
a program can be measured in terms of the number of (elementary) computation steps
needed for it to reach the final answer. This is the basis of the theory of computational
complexity and Levy’s notion of optimal $reduction[7]$ . This idea comes from the fact thatsequential computation may not make sense if a program has nontermination. Yet when
we turn to the concurrency world, where the computation proceeds by processes or objects
which communicate with each other, this simple answer cannot be adapted easily, since
the underlying semantic framework is quite different. Specifically:*kubo@mt.cs.keio.ac.jp
1The present paper does not consider so-called space-cost of programs.

65$\bullet$$\bullet$$\bullet$In concurrency, it is often the case that the intermediate action sequence matters.
In fact, in many cases concurrent programs are made not to compute the single
answer, but to interact with the outside world, e.g. operating systems or banking
systems.

Relatedly, concurrent computation may make sense even if a program has nontermination. In fact the banking system is not expected to stop at all!
In addition, concurrent computation is essentially non-deterministic due to theexistence of interference (or competition). So there can be many possible nondeterministic branching executions of the same program.

Therefore we should consider not only the number of computation steps but also theproperties such as nondeterminism, nontermination, intermediate steps, etc. This makes
it difficult to have a clean idea about what cost means in concurrency, even in the abstract
setting. Considering the importance of cost in software evaluation, we think that a formal
framework for concurrent computing in this regard is absolutely needed since a program
becomes meaningful only when they are implemented to run in the real machine andarchitecture.
Under the above background, this paper introduces an elementary theory of cost or
efficiency for concurrent programs, based on thecture called cost graphs. Just as thetheoretical study of sequential programs often uses -calculi as its theoretical basis, we
use process calculi (e.g.
-calculus [11] and many others) as ouricformal theories of concurrent computation. A cost graph is a graph which traces theactions a processtake considering their cost as well as branching structures. Dueto a nondeterministic behaviour, a program can be given a set of cost graphs, which areessentially isomorphic to each other, if we forget the cost information. Cost of programs
evaluated in terms of the whole set of such graphs. While we assume that the cost ofcomputation is the number of transition steps as in -calculi, the ways of measuring andcomparing cost are quite different from those in sequential programs.
There exists earlier work [1] by Arun-Kumar and Hennessy, which considers the costof computation in the concurrency setting. [1] defines the order over CCS terms by
the number of transitions of the labelled transition system of CCS, taking the nondeterministic behaviour into consideration. The definition of the ordering is inductive
just like bisimulation, offering a convenient proof methods. Assuming a prior knowledgeof CCS [9]: let us give a definition of efficiency prebisimulation over CCS terms. It is abinary relationsuch that, for every $<P,$ $Q>\in R$ ,$\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{u}\backslash$$\lambda$$\mathrm{C}\mathrm{S}\mathrm{P}[4],$$\mathrm{C}\mathrm{C}\mathrm{S}[9],$$\mathrm{b}\mathrm{a}s$$\pi$$\mathrm{m}\dot{\mathrm{a}}\mathrm{y}$$\overline{\mathrm{i}}\mathrm{s}$$\lambda$$\tau$$R\subseteq P\cross P$

1. $Parrow P’s$$\Rightarrow\exists s’s\leq s’\exists Q^{\prime_{Q}}sarrow Q’\wedge’<P’,$$Q’>\in R$

2. $Qs’arrow Q’$$\Rightarrow\exists ss\leq s\exists\prime P/Psarrow P’\wedge<P’,$$Q’>\in R$

where
is the sequence of labels and $s\leq s’$ is given as
etc. The
theory offers, as far as we know, the first coherent notion of concurrency cost in the lineof behavioural equivalence over processes. Note that the ordering relation is essentiallyconvex, thus expressing a relative notion of cost between two terms. Thus even if $P$ isordered as superior to $Q,$ $P$ may not run faster than if we have a bad luck.
$s,$

$s’$

$\alpha.\tau.\beta.0\leq\alpha.\beta.0$

$Q$

66

Regarding Arun-Kumar-Hennessy construction as an important precursor, we notethat there might be several features which we may need for a cost theory of computation
but which cannot be covered by the above notion. For example, there seems to be no
obvious way of defining “absolute” comparison (one program runs absolutely faster thananother, etc.). Moreover we may face a subtle situation where we may want a different
and $\tau.a.P$ , where
measure of evaluating cost. Let us think of two terms,
and $P$ is semantically equal w.r.t. bisimilarity). From a viewpoint of cost,(note. At the worst case, however, it takes
the former takes at least one step to reach
steps
for the latter to reach in any cases.
two
infinite steps. In contrast, it always takes
They cannot be compared in efficiency bisimulation in general, but certainly there arewhile
situations where we prefer one to the other (e.g. a “speculative” person likes-case analysis seems difficult in thea “steady” person will like $a.\tau.P$ ). Suchframework of efficiency bisimulation.
Theory of cost graphs are our trial to provide a comprehensive theoretical framework
formalism,
for the study of cost in concurrent computation. We take CCS as aconstruction,
partly due
Arun-Kumar-Hennessy
thepartly to retain the continuity fromto its simplicity and popularity. However the result can be transplanted in any CCS-likeformalism for which labelled transition relation as well as -action are definable. We show
how the set of cost graphs are derivable from a CCS term based on its derivation graph,
how we compare two different cost graphs, and, based on the ordering obtained in thisway, how various orderings over CCS terms are obtained, each with distinct emphasis on
the feature of cost which we may be concerned with. One of such orderings is closely
related with efficiency bisimulation
The remainder of the paper is organized as follows. In section 2, we show the construction of derivation of cost graphs.from labelled transition systems. Section 3 describe
the ordering of the cost graph. And, we explain the examples of comparison of concurrent
programs using the presented orders. Section 4 describe the embedding into efficiency
preorders. Finally, Section 5 describe the further issues and conclude.
$\Omega^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}}\tau.\Omega$$a.P|\Omega$$P|\Omega$$P|\Omega$$P$$a.P|\Omega$$\mathrm{w}\mathrm{o}\mathrm{r}\mathrm{s}\mathrm{t}/\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}$$\mathrm{b}\mathrm{a}s\mathrm{e}$$\tau$

2

Cost graph of concurrent computation

2.1

CCS and Its labelled transition systems

CCS $[8, 9]$ is a well-known process calculus. The discussions in this paper are
CCS and its labelled transition system, which we summarize below.

$\mathrm{b}\mathrm{a}s$

ed onDefinition 2.1 (the syntax of $CCS$ )be a countable set
Let and be a countable set of names and co-,names. Let$Act=L\cup\{\tau\}$of actions, ranged
setcountable
be a
. Let
of labels, ranged over by.
. Let $A$ is a countable set of process variables, ranged over by $X,$
over by$Q,$$P,$, as follows:
We define the set of processes , ranged over by$A$$L=A\cup\overline{A}$$\overline{A}$$l,$ $l’,$$\alpha,\beta,$$\ldots$$Y,$$\ldots$$P$$\ldots$$P=\alpha.P|P|Q|P\backslash L|P+Q|X$

where$X^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}}P$.

$\ldots$

67

Definition 2.2 (The operational semantics of $CCS$ )the transitionis satisfying the following conditions.
$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}arrow\subseteq\alpha P\cross Act\cross P$

ACT$\alpha.P-^{\alpha}P$$COM$$l.P|\overline{l}.Qarrow P|\mathcal{T}Q$

PAR$P-^{\alpha}P’$$P|Q-^{\alpha}P’|Q$$\Rightarrow$$RES$$Parrow P’\alpha\Rightarrow P\backslash Larrow P\alpha/\backslash L$$SUM_{1}$$P-^{\alpha}P’\Rightarrow P+Qarrow P’\alpha$$SUM_{2}$$Qarrow Q’\alpha\Rightarrow P+Qarrow Q’\alpha$$REC$$P\alphaarrow P’$

and$X^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}}P\Rightarrow X\alphaarrow P’$

Definition 2.3 (The labelled transition system of $CCS$ )Let $P$ be a set of processes and Act be a set of actions and $-^{l}$ be a transition relation.
Triple $T=(P, Act,$ $-^{\alpha}\alpha\in Act)$ is called a labelled transition, in short) of(
CCS.
$\mathrm{L}\mathrm{T}\mathrm{S}$$\mathrm{s}\mathrm{y}_{\mathrm{S}\mathrm{t}}\mathrm{e}\mathrm{m}$Definition 2.4 (Sequence of label)$s\in Act^{*}$ is the sequence of actions.

$\hat{s}\in L^{*}$

is the sequence of label.

$\bullet$$PSarrow Q=^{\mathrm{f}}Parrowarrow P_{2^{arrow}}\mathrm{d}\mathrm{e}\tau*\alpha_{1}\mathcal{T}*\ldotsarrowarrowarrow Q\tau*\alpha_{n}\tau*$

where$\bullet$$P\hat{s}arrow Q=^{\mathrm{e}}Parrowarrow P12^{arrow}\mathrm{d}\mathrm{f}\mathcal{T}*l\tau*\ldotsarrowarrowarrow\tau*l_{n}\tau*Q$

where

Definition 2.5 reach$s=\alpha_{1}\cdots\alpha_{n}$$\hat{s}=l_{1}\cdots l_{n}$$(P)=^{\mathrm{e}}\mathrm{d}\mathrm{f}\{P’\in P|P\in P\alphaarrow P’\}*$

Definition 2.6 (Derivative graph of process )Let
be a processes. An derivative graph of processsatisfying the following conditions.
$P$

$P$

1. $N$ is a set of nodes such that

2.

$E$

$P$

is a triple $DG(P)=(N, E)$$N^{\mathrm{d}\mathrm{e}\mathrm{f}}=reaCh(P)$is a set of labeled directed edge iff$E^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}}\{<P, \alpha, P’>|P-^{\alpha*}P’\}$.

Definition 2.7 (Weak-bisimilarity)
A binary relation
is a weak bisimulation if $\forall(P, Q)\in R$ and$R\subseteq P\cross P$

1. $Psarrow P’$
2. $Q-^{s}Q’$$\mathrm{P}$$\Rightarrow\exists Q’Q\hat{s}arrow Q’$

A $(P’, Q’)\in R$$\exists P’Parrow\hat{s}P’$

A $(P’, Q’)\in R$$\Rightarrow$weak bisimilar Q,written $P\approx Q$ , iff

2.2$\exists$

weak bisimulation $R,$$\blacksquare$$P\mathrm{R}Q$

Construction of cost graph

If we use a labelled transition system to define the semantics of computation, the numberof transition steps is naturally used to compare two concurrent programs. So we add thecost data to transition relation as a label, i.e. $P-^{l}Q$ becomes $P<l_{C},>arrow Q$ where istransition cost. Next, two programs compared with respect to cost should be semanticallyequal. In this paper, we assume “semantic equality” means weak-bisimilarity, one of themost stable semantic notions for process calculi.
$c$

68

Figure 1: Derivative graph and abstract derivative graphs

Figure 2: cost graphs from Figure 1

69

2.3

Formal definitions of cost graphIn this section, we define formally the notion of cost graphs. To show the idea, weintroduce possibly the most condensed way of presenting transitions
a graph.
The structure is later annotated by cost to become a cost graph. Mathematically, thisunderlying structure is a graph whose nodes are equivalence classes of , and whoseedges are “semantically atomic” transitions between the equivalence classes, annotatedby self-directed edges at each node.
$\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{u}\mathrm{l}\mathrm{o}\approx \mathrm{a}\mathrm{s}$$\approx$

Notation 2.8
1.
2.

3.

$Parrow_{\approx}P^{\prime^{\mathrm{d}}}\mathcal{T}=P\mathrm{e}\mathrm{f}arrow P^{J}\tau$

A $P\approx P’$$P\tauarrow 0,1P^{\prime^{\mathrm{d}}}=P\mathrm{e}\mathrm{f}’Parrow P’\tau$$P \frac{/\backslash }{/\prime}=\mathrm{d}\mathrm{e}\mathrm{f}$for no$\alpha \mathit{8}.t$.

$Parrow\alpha$Definition 2.9 (Abstract derivative graph)
Let $DG(P)=(N, E)$ be the derivative graph of a process $P,$
the weak-bisimilarity
on . Let $L^{+}=L\cup\{\epsilon\}$ be the set of abstracted-labels, ranged over by. $DG_{\approx}(P)=$is called an abstracted-derivative graph iff$\approx \mathrm{b}\mathrm{e}$$P$$k,$ $k’$$(N_{\approx}^{P}, E_{\approx})$

1.

by

2.

a set of equivalence classes of reach $(P)$ induced, with a distinguished element.

$N_{\approx}^{P^{\mathrm{d}\mathrm{e}\mathrm{f}}}=N/\approx \mathrm{i}\mathrm{s}$$\mathit{0},\mathit{0}’,$$\ldots$$\mathrm{b}\mathrm{y}\approx$, ranged over$[P]_{\approx}$$E_{\approx}\subseteq N_{\approx}\cross L^{+}\cross N_{\approx}$

is a set ofis written$\mathrm{l}\mathrm{a}\mathrm{b}\mathrm{e}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{d}\mathrm{d}k\mathrm{i}\mathrm{r},\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{e}\mathrm{d}$conditions.

$<\mathit{0},$$E_{\approx}=\mathrm{d}\mathrm{e}\mathrm{f}\{${{$k,$ $\mathit{0}’>\in E_{\approx}$$\mathit{0}arrow \mathit{0}$edges$\mathrm{s}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{S}}\varpi$

ing the following.

}$<\mathit{0},$$l,$ $O’>|_{\mathit{0},\mathit{0}’}\in N_{\approx}$A$P_{1}arrowarrow P_{2}\tau*\approx l\wedge P_{1}\in O\wedge P_{2}\in \mathit{0}’$$<\mathit{0},$$O’>|\mathit{0},$ $O’\in N_{\approx}$A$P_{1}arrowarrow\tau*\tau\approx 0,1P_{2}\wedge P_{1}\in O\wedge P_{2}\in \mathit{0}’$$\epsilon,$$\cup$}$\blacksquare$

As seen in Proposition 2.10, 2.11, and 2.13, the graph is the faithful and “condensed”
representation of transition graphs modulo weak bisimilarity, where no extra edges arepresent (except adjoined edge) but all possible transition paths can be generated fromit. We do not know whether this construction has appeared in the literature or not.
The following proposition is important. It shows that the restriction of an abstractededge into a “semantically atomic” transition may not be restrictive.
$\epsilon$$DG_{\approx}(P)$Proposition 2.10 Suppose$*larrow P’\in o’$$Parrow wehav\tau*\approx^{arrow P’}eParrow\tau 0,1\tau\approx$.

in an abstract derivative graph. Then for any
for some $P’$ . Similarly if
for any $P\in o$ we have$\mathit{0}arrow o’l$$P\in \mathit{0}$$\mathit{0}-^{\epsilon}o’$

Proof: We only show the first case. The second case is similar. Suppose not. Then,
while for some$Q\in \mathit{0}$$Qarrowarrow Q’\tau*l\in\tilde{O}’\approx$

70

for some$P\in \mathit{0}$, for no$P^{\prime/}$,$Parrow_{\approx}P’\tau*/arrow P/\in Ol/$

Take
contradiction, So$\{P_{i}\}_{i\in I}s.t$.

$Parrow_{\approx^{arrow\#}}\mathcal{T}*\mathcal{T}P_{i}arrow lP’$

$P_{i}\approx Q\approx P$. But if no$P_{i}$

is bisimilar to $Q,$

, as required.

’$P\not\simeq Q.$

can also be considered as a tree just by unfolding the derivaNow the graphtives, which is denote by $DG_{\approx}^{t}(P)=(N^{L}, E)$ , assuming each node is labeled by equivaa labelling function .
lence classes on, whose proof relies on the conThe following is an important property ofstruction of Definition 2.9.
$DG_{\approx}(P)$$L$$[P]_{\approx^{\mathrm{V}\mathrm{i}}}\mathrm{a}$$DG_{\approx}(P)$Proposition 2.11 For any
or not) is always identity.

$DG_{\approx}^{t}(P)=(N^{L}, E_{\approx})$, its automorphism (either respecting.

$L$

can have the isomorphic unfolding. If they do,
Proof: Since no two nodes inthen we can easily construct a bisimulation by which we are forced to adjoin these two
nodes. Details are by induction on the depth of the first nodes rleted automorphism: See[6].
$DG_{\approx}(P)$$\blacksquare$

Definition 2.12 A graph $G=(N^{L}, E)$ is isomorphic to another graph $G’=(N^{\prime L}, E’)$respecting $e.g$ . labelling function , written $(N^{L}, E)\simeq(N^{\prime L}, E)$ , by usual graph theory.
$L$

The following proposition shows that “semantically equivalent” programs have theas asame abstract graphs, and vice versa. By the result we are going to regard
semantic basis of our cost theories.
$DG_{\approx}(P)$Proposition 2.13 $DG_{\approx}(P)\simeq Dc\approx(Q)$$\Leftrightarrow P\approx Q$

are isomorphic graphs,
and, Since
Outline of Proof: In the caseand vice versa.
to the edge inthere exists a corresponding edge in$\{(P,Q)|Dc_{\approx}(P)\simeq
Dc_{\approx}(Q)\}$
direct fromInthebisimulation.
a
weak
is
Easily,)Proposition 2.10. (note: reach$\mathrm{o}\mathrm{f}\Rightarrow$$DG_{\approx}(P)$$DG_{\approx}(Q)$$DG_{\approx}(Q)$$DG_{\approx}(P)$$\mathrm{c}\mathrm{a}\mathrm{s}\mathrm{e}\Leftarrow \mathrm{i}\mathrm{s}$$(P)_{WB}=reaCh(Q)_{\approx^{\mathrm{i}\mathrm{f}}}P\approx Q$$\blacksquare$

Examples 2.14 (Example of abstract derivative graphs)
A part of abstract graph of Figure 1 is as follows:$[a.(\mathcal{T}.

\cdot P+\mathcal{T}.\tau.P)]_{\approx}\Rightarrow[aP]_{\approx}$

Now we about to define a cost graph. Before it, we define a pre-cost graph as any
abstract derivative graph with cost data. A cost graph is defined as a pre-cost graphwhich correspond to a possible execution of a program, including branching structures.

Definition 2.15 (Pre-Cost graph)
A pre-cost graph $(N^{L}, E, \rho)$ is an abstract derivative graph $DG_{\approx}(P)=(N^{L}, E)$ with acost function $\rho:Earrow Nat\cup\{\omega\}$ .

71

Notation 2.16
i n a pre-cost graph, whose cost function is $\rho(e)=n$ , is denoted by$O\iota$$\mathrm{A}\mathrm{n}\mathrm{e}\mathrm{d}\mathrm{g}\mathrm{e}oarrow<l,n>,.=eo\Rightarrow O’$

Definition 2.17 (Cost graph)
A cost graph, denoted by $cg,cg’$ , is a pre-cost graph $(N^{L}, E, \rho)$ for which there exists a
map : $Narrow P$ such that:$\Psi$

1.
2.

$\mathit{0}arrow O<l,n>/$$\Rightarrow$$\Psi(\mathit{0})arrowarrow\Psi-1l(\tau nO’)\approx$

where$\Psi(\mathit{0})arrowarrow\tau nn-1\approx\#^{\Psi(\mathit{0}’}\tau)$$\mathit{0}^{<}arrow\epsilon,n>O’\Rightarrow\{$and$\Psi(\mathit{0})\in \mathit{0}^{L}$

where$\Psi(\mathit{0}’)\in \mathit{0}^{\prime L}$

and
and

$\Psi(\mathit{0})\in \mathit{0}^{L}$$\Psi(\mathit{0})arrow\Psi(\tau \mathit{0}’\approx)\neqarrow \mathrm{w}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}\Psi(\mathit{0})\in \mathit{0}^{L}$.

$\Psi(\mathit{0}’)\in \mathit{0}^{\prime L}$$\Psi(\mathit{0}’)\in \mathit{0}^{\prime L}$$(n\geq 1)$

3.

$\mathit{0}^{<}arrow\epsilon,\omega>O’$$\Rightarrow\forall n\Psi(\mathit{0})arrow\Psi(\tau no’)\approx$

where$\Psi(\mathit{0})\in \mathit{0}^{L}$

4. Moreover, if none of the above conditions hold forand$L(\mathit{0})$$\Psi(\mathit{0}’)\in \mathit{0}^{\prime L}$, we let.

$\mathit{0}-<\epsilon,0>O’$.

Some discussions on Definition 2.17 are given.
1. By Proposition 2.10, 1 is well defined.

2. For 2 and 3, if
originally with$n\neq0$
with
can be:$\mathit{0}-^{\epsilon}\mathit{0}’$$L(\mathit{0})=L(\mathit{0}’)$, a corresponding transition$P\tau-_{\approx}^{n}$(a) $P’$ has further transition(b)$P’arrow andl/orP^{\prime_{arrow\#}}\mathcal{T}$$\mathrm{o}\mathrm{f}-_{\approx}^{\tau*}$.

, or $P’\star$ .

If (a) is the only case, we keep
. If not (a), then we select (anyof) the holding cases. If both, we can again select either. Whatever’ by
Proposition 2.10, for each original, we have a corresponding.
$\mathrm{a}\mathrm{d}\mathrm{i}\mathrm{o}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g}arrow\approx\tau$$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{c}\mathrm{a}\mathrm{s}\mathrm{e}<\alpha,n>,$$\mathit{0}-^{\alpha}\mathit{0}’$$\mathit{0}arrow \mathit{0}$3. In the above scheme, if (a) continues to hold forever, then.

$\mathit{0}arrow \mathrm{r}<\epsilon,\omega>\mathrm{e}\mathrm{s}\mathrm{u}\mathrm{l}\mathrm{t}\mathrm{s}$4. Note, if, necessarily. Conversely, suppose
with. Givenor$0>$ .
the above labelling is possible, so we use$\mathit{0}-<\epsilon,0>O’$$\Psi(\mathit{0})\equiv\Psi(\mathit{0}’)$$\Psi(\mathit{0})\equiv\Psi(\mathit{0})$$\Psi(\mathit{0}),$$\Psi(\mathit{0})arrow P’\tau\Rightarrow\Psi(\mathit{0})\not\simeq P’$$\mathit{0}-^{\epsilon}o’(\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{i}\mathrm{n}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{y})$$\neg\Psi(\mathit{0})-^{\mathcal{T}}$, none of$<\epsilon,$

5. To summarize, the schemea program needs for it to achieve any
meaningful event(state change,). Note that state change
should be considered to respect branching structures of underlying bisimilarity. If
we take other equivalences, other ideas would be adapted. But the present one ismost faithful to the underlying semantic structure, i.e.
.
$\mathrm{C}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{t}\mathrm{s}-^{\tau}\approx \mathrm{s}\mathrm{t}\mathrm{e}\mathrm{P}\mathrm{s}$$\mathrm{n}\mathrm{o}\mathrm{n}- \mathcal{T}\mathrm{a}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n},\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{i}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$DG_{\approx}(P)$

Examples 2.18 (Examples of cost graph of programs)

72

1.

$a.\tau.0$

Using the case 1 and second half of 2 of Definition 2.17,, we have
.
Since
.
and
and
Here
$a.\tau.0arrow \mathcal{T}a.0arrow 0\mathcal{T}1$$\mathit{0}^{L}=a.\tau.0$$\mathit{0}arrow \mathit{0}arrow O<a,1>/<\epsilon,1>//$$0^{\prime/L}=0$$0^{\prime L}=\tau.0$

2. $\tau.a+\tau.b$
Using the case 1 and first half of 2 of Definition 2.17 since.
Since $\tau.a+\tau.barrow aarrow 0\tau a$ , we have$\tau.a+\tau.b\tauarrow barrow 0b$.
, we have
Since
.
and
and
and
Here

$\tau.a+\tau.b\not\simeq a\not\simeq b$,$\mathit{0}arrow Oarrow<\epsilon,1><aa’ 1>O’$$\mathit{0}arrow obarrow O’<\epsilon,1><b,1>$$\mathit{0}^{L}=\tau.a+\tau.b$3.

$\mathit{0}_{b}^{L}=b$$\mathit{0}_{a}^{L}=a$$0^{\prime L}=0$$\Omega^{\mathrm{d}\mathrm{e}\mathrm{f}}=\tau.\Omega$

Using the case 3 of Definition, we have.
Since$2.17,<\epsilon,\omega>$$\forall ns.t$$\Omega\tauarrow n_{\Omega}$$\mathit{0}arrow \mathit{0}$where$\mathit{0}^{L}=\Omega$.

There may be several execution paths of a program , since a concurrent system includes the branching structure whose components are “semantically” equal. The following
is defined considering this property.
$P$

Definition 2.19 (Cost graphs of a program ), is a set of all cost graphs for
A cost graphs of$P$$P,\mathrm{w}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{t}\mathrm{e}\mathrm{n}c\mathcal{G}(P)$$P$.

Examples 2.20 (Examples of cost
A part of a cost graph of Figure 1 is defined as follows:a cost graph$graph_{\mathit{8})}$$a.(\mathcal{T}.P+\mathcal{T}.\mathcal{T}.P)<_{\Rightarrow^{>}P}a,2$

and a cost graph$a.(\tau.P+\tau.\tau.P)\Rightarrow^{>}P<a,3$

These cost graphs are shown in Figure 2.
The following definition and proposition shows that, for any cost graph of $P$ , the costgraph is isomorphic to the abstracted derivative graph of $P$ .
)Definition 2.21 (Function from $cg$ to$cg=(N^{L},E)\in
C\mathcal{G}(P)$andLet
is defined as follows:::$DG_{\approx}(P)$$DG_{\approx}(P)=(N_{\approx}, E_{\approx})$$\phi_{N}$$Narrow N_{\approx},$$\phi_{E}$.

$\phi=<\phi_{N},$ $\phi_{E}>$such that$E\cross\rhoarrow E_{\approx}$$\phi_{N}(\mathit{0})=O$$\phi_{E}(\mathit{0}^{<^{\iota,m}>}arrow \mathit{0})/=\phi N(\mathit{0})\Rightarrow^{l}\phi_{N}(\mathit{0}’)$By Proposition 2.13, we have the following essential result. We omit the easy proof.

Proposition 2.22 $\phi(cg)\simeq DG_{\approx}(P)$ iff $cg\in DG_{\approx}(Q)$ with $P\approx Q$
This proposition allows us to compare between two programs which are semanticallyequal.

73

3Various orderings on terms using cost graphs
In this section, we show several orderings on CCS-terms using cost graphs. Then we show
the orderings between the sets of cost graphs using the order over cost graphs.

3.1

Comparison between two cost graphs

There are several ways to compare two cost graphs. This comparison is the basis tocompare concurrent programs in terms of cost.

Definition 3.1 (Comparable graphs)
Two cost graphs, say $cg$ and $cg’$ , are comparable iff $\phi(cg)\simeq\phi(cg’)$ .
By proposition 2.22, $cg$ and $cg’$ are comparable iff they are bisimilar programs.

Definition 3.2 (Cost order on cost graph)
Let $cg=(N^{L}, E, \rho)$ and $cg’=(N^{\prime L}, E’, \rho)$’ be two comparable cost graphs. Then $cg$ isfaster than $cg’$ , written $cg\leq_{c}cg’$ , iff for a bijection from, we have, for sometosuch that $n\geq m$ ,$N^{L}$$\Psi$$N^{\prime L}$$n$$\Psi(\mathit{0})^{<\alpha,n>}arrow\Psi(\mathit{0})/$where$\geq \mathrm{i}\mathrm{s}$$\Leftrightarrow \mathit{0}^{<\alpha,m>}arrow \mathit{0}/$the usual order relation on natural numbers.

$\blacksquare$

Note that by Proposition 2.11, when two comparable cost graphs are given, there is
only one way to define such .
$\Psi$

Proposition $3.3\leq_{C}$ is a preorder relation.
Proof: Clearly, $cg\leq_{C}cg$ . Moreover$cg\leq_{C}cg’\leq_{C}cg^{\prime/}$$\Rightarrow cg\leq_{C}cg^{\prime/}$.

$\blacksquare$

If a cost graph of one program is comparable to that of another program then they
are bisimilar, by Proposition 2.22 and Definition 3.1 and 3.2.
Proposition 3.4

3.2$cg\leq_{c}cg’\wedge cg\in C\mathcal{G}_{P}\wedge cg\in C\mathcal{G}_{Q}$$\Rightarrow P\approx Q$$\blacksquare$

Comparison between two sets of cost graphs

There are several ways to compare two sets of cost graphs. In concurrent programs, there
are several possible execution paths. Thus, in general, several cost graphs are generated
by programs. Thus comparison between two sets of cost graphs means comparison
between every possible execution paths of two programs. By the way of ordering the setsof cost graph, there are several ways of ordering two sets of cost graphs.
$a$

74

Definition 3.5 (Cost Preorders on Program)We define cost preord,ers on program as follows.

$\{$

1
2
3
4
5
6
7
8

.
.
.

$P\subseteq_{rand}omQ$$\Leftrightarrow$$\exists cg_{p}\in C\mathcal{G}(P)$$P\subseteq_{ro}Q$$\Leftrightarrow$$\forall cg_{q}\in c\mathcal{G}(Q)$$P\subseteq_{rw}Q$$\Leftrightarrow$$\forall cg_{p}\in c\mathcal{G}(P)$$P\subseteq_{r}Q$$\Leftrightarrow$$P\subseteq_{r}Q\wedge P\subseteq_{r’}Q$$P\subseteq_{\mathit{0}}Q$$\Leftrightarrow$$\exists \mathrm{c}g_{p}\in c\mathcal{G}(P)$$P\subseteq_{w}Q$$\Leftrightarrow$$\exists cg_{q}\in C\mathcal{G}(Q)$$P\subseteq_{\sigma w}Q$$\Leftrightarrow$$P\subseteq_{\mathit{0}}Q\wedge P\subseteq_{w}Q$$P\subseteq_{SO}Q$$\Leftrightarrow$$\forall cg_{p}\in c\mathcal{G}(P)$.
.
.

$\exists cg_{q}\in c\mathcal{G}(Q)$$\exists \mathrm{c}gp\mathcal{G}(\in cP)$$\exists cgq\mathcal{G}(\in cQ)$$\forall cgq\mathcal{G}(\in cQ)$$\forall cg_{p}\in c\mathcal{G}(P)$$\forall cg_{q}\in C\mathcal{G}(Q)$.

.

$Cg_{p}\leq cg_{q}$$cg_{p}\leq Cg_{q}$.

$cgp\leq cg_{q}$.

$cgp\leq cg_{q}$.

$Cg_{p}\leq cg_{q}$. $cgp\leq cg_{q}$is called random cost preorder.
is called relative optimal cost preorder.
iscalled relative worst cost preorder.
is called optimal
is called relative cost preorder.
isis called worst cost order.
is called optimal-worst cost order.
cost order.
called strong optimal cost order.
$\subseteq_{random}$$\subseteq_{ro}$$\subseteq_{rw}$$\subseteq_{r}$$\subseteq_{\mathit{0}}$$\subseteq_{w}$$\subseteq_{so}$$\subseteq_{\sigma w}$$\blacksquare$

Discussion 3.6
1. $P\subseteq_{random}Q$ shows that If$\mathrm{o}\mathrm{f}Q$

2.

3.

$P$

.

and

$Q$

run, the run ofmeans in comparison with any run of , thata speculative order.

$P\subseteq_{ro}Q$$Q$

may be faster than the run$P$

may run faster. So this is

is important: This says that is more stable than , in the sense that,
if we let run, it is always possible that does worse than that.
$P$$P\subseteq_{rw}Q$

$P$

4.

$P$

$P\subseteq_{r}Q$

$Q$

$Q$

is a sound way of combing previous two.

5. Sometimes we require that, if does its (one of) the best, then it always beats, measuring
efficiency at its best,.
this is$\mathrm{P}$$P’ \mathrm{s}$$P\subseteq_{\mathit{0}}Q$

6.

$P\subseteq_{w}Q$

ening

7.
8.

compares$\mathrm{o}\mathrm{f}\subseteq_{rw}$$P\subseteq_{\sigma w}Q$

.

$P$

and

$Q$

at

$Q$

:

$\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{e}\mathrm{n}\mathrm{g}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g}\subseteq_{ro}$$Q’ \mathrm{s}$(one of the) worst. This is clearly the strength-

is a sound way of combing the previous two.

assures that at any possible run, is always faster. In other words, theworst runs of is better than the best runs of .
$P$

$P\subseteq_{\theta O}Q$

$P$

$Q$

We show the examples of various ordering
Examples 3.7 (Examples of comparison $ofcost<a,1>$ graph)
For $a+\tau.\tau.a$ , there are two cost graphs
and
.
graph
$\mathit{0}arrow o’$$\mathit{0}^{<}arrow a,3>O’$. For$\tau.a$, there is a cost$\mathit{0}arrow \mathit{0}<a,2>$

1.

But,
and
.
$a+\tau.\tau.a$. But,
andis not always faster
Their means is always faster thanis reduced to at two steps( and ) . $a+\tau.\tau.a$than $a+\tau.\tau.a$ . Precisely speaking,takes at least one step, while at most three steps.
$a\subseteq_{so}\tau.a$$a\subseteq_{so}a+\tau.\tau.a$$a$$\tau.a\not\subset_{so}a+\tau.\tau.a$$\tau.a$$\tau.a$$\tau.a$$0$$\mathcal{T}$

$a$

75

Figure 3: Inclusion relation on cost orders
2.

$\tau.a\subseteq_{w}a+\tau.\tau.a$. But,$\tau.a\not\in_{\mathit{0}}a+\tau.\tau.a$

There exists a run
is slower than a runof a term. So
is stable.
cost. But, This also means thatis not
ter than every run(path) of $a+\tau.\tau.a$ .
{. cost.
That isis not always faster than $a+\tau.\tau.a$ . So,
is not optimal$\tau.\tau.a$$\tau.a$$\tau.a$$\tau.a$3.

$\tau.a$$\tau.a$$\mathrm{w}.\mathrm{r}.\mathrm{t}$$\mathrm{w}.\mathrm{r}.$. But,
This example is reverse of the previous example. $a+\tau.\tau.a$ contains the optimal run. But
not contain the worst path.
$a+\tau.\tau.a\not\subset_{w}\tau.a$$a+\tau.\tau.a\subseteq_{\mathit{0}}\tau.a$

$a$

4.

$\tau.a$$\mathrm{f}\mathrm{a}s$$\tau.a$$a+\mathcal{T}.\mathcal{T}.a\not\subset_{SO}a+\mathcal{T}.\mathcal{T}.a$

It means that$\subseteq_{so}$is not a preorder since it is not reflexive.

The following shows inclusion among these preorders.

Proposition 3.8 ($Inclu\mathit{8}ion$

relation among cost orders)

1.

$\subseteq_{so}\subseteq\subseteq \mathit{0}\subseteq\subseteq_{ro}\subseteq\subseteq_{random}$

2.

$\subseteq_{so}\subseteq\subseteq_{w}\subseteq\subseteq_{rw}\subseteq\subseteq_{random}$$\blacksquare$

Proof: 1 and 2 are direct from definitions of each preorder.

$\blacksquare$

The inclusion results are shown in Figure 3. Other than the transitive closures of the
inclusion, no comparison is possible. Moreover all depicted inclusions are proper at least
for CCS terms.

76

4Relationship between orders of cost graphs andefficiency preorder
Efficiency preorder

4.1

In Introduction, we discussed the efficiency preorder for CCS, which was proposed in [1].
:This preorder is based on the number of transitions. The preorder is defined as$\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{l}\mathrm{o}\mathrm{W}\mathrm{s}^{2}$$\tau$

Definition 4.1 (Orders on label)and $s\leq s$ i.e.
generated by inequations
the binary relation on
Letclosed under reflexivity, transitivity, and substitution under catenation contexts.
$Act^{*}$$\leq \mathrm{b}\mathrm{e}$$s\leq\tau s$$\leq \mathrm{i}\mathrm{s}$$\blacksquare$

Definition 4.2 (Efficiency Prebisimulation)is an efficiency prebisimulation if $\forall(P, Q)\in R$ andA binary relation$R\subseteq P\cross \mathcal{P}$’

1. $Psarrow P’$$\Rightarrow\exists s’s\leq S\exists Q’/QSarrow Q’$

A $(P’, Q’)\in R$

2. $Qs’arrow Q’$$\Rightarrow\exists \mathit{8}S\leq s’\exists P’Parrow sP’$

A $(P’, Q’)\in R$$\blacksquare$

Definition 4.3 (Efficiency $preorder\subseteq_{E}$ ){ $R|R$ is a efficient prebisimulation}

1.

$\subseteq_{E}=\cup$

2.

$P\subseteq_{E}Q$

Lemma 4.4

4.2

iff

$\exists$

efficiency prebisimulation $R,$

$P\subseteq_{E}Q$$\Rightarrow$$P\mathrm{R}Q$$\blacksquare$$P\approx Q$

Correspondence between cost preorder and efflciency preorder

In this section, we show the correspondence between cost preorder presented in this paperand efficiency preorder. Firstly, we show the following lemma that cost preorder canbe defined inductively. Then, we show that cost relative order is indeed an efficiency
bisimulation.

Lemma 4.5 The subtree of a cost graph is a cost graph.
Lemma 4.6
$P\subseteq_{r}Q$

iff$Parrowarrow P’\mathcal{T}mn\approx\alpha\Rightarrow$$\exists n$s.t.m$\leq n\wedge Q\tau_{\mathcal{T}}arrowarrow\alpha n\approx_{m}Q’\wedge P’\subseteq_{r}Q’$$\{$$Q\tauarrowarrow Q’\approx\alpha\Rightarrow\exists ms.t.m\leq n\wedge Parrowarrow P’\approx\alpha\wedge P’\subseteq_{r}Q’\blacksquare$

Proof:. Since three cases are similar, we show one of: We should prove three casesthem.
2Our definition reverses left and right for original definition$\mathrm{o}\mathrm{f}-^{\alpha}$$(\Rightarrow)$

77

1.

$P-_{\approx}^{\tau m}-^{l}P/$. By Definition 2.17,$Parrowarrow P’\tau ml\approx\Rightarrow Oarrow \mathit{0}<l,m+1>/\wedge \mathit{0}^{L}=P\wedge \mathit{0}=/LP’$

By Assumption for any, there exists $cg’\in C\mathcal{G}(Q)$ such that $cg\leq cg’$ .
$cg’=(N’,E^{\prime/},\rho)$ .
$cg=(N,E,\rho)$
Let
and
Then by Definition 3.1, there exists abijection :such that $m\leq n$ and$cg\in C\mathcal{G}(P)$$N^{L}arrow N^{\prime L}$$\Psi$$o^{<l,m}arrow \mathit{0}+1>/\Leftrightarrow\Psi(\mathit{0})^{<}\iota_{n},+1arrow>\Psi(\mathit{0}’)$If, then$cg\leqcg’$, then for any
ifof $cg’\in C\mathcal{G}(Q)$ such that$\Psi(\mathit{0})<l\underline{n+},\rangle 1>\Psi(\mathit{0}’)$where $\Psi(0)^{L}=Q$ and $\Psi(0)^{L}=P’$ . While, there exists
which is a subtree. Hence.

$Parrow_{\sim}arrow P’\tau nl$$cg^{\prime/}\in C\mathcal{G}(P’)\sim$$\mathrm{c}g’’\leq cg^{\prime\prime/}$2.

$Parrow_{\approx}arrow\not\simeq^{P’}\tau m\tau$3.

$P-^{\tau m+1}\approx P’$$(\Leftarrow)$.

$cg^{\prime/\prime}\in C\mathcal{G}(Q’)$$P’\subseteq_{r}Q’$,
In both cases, similarly to 1 using the edge$<\epsilon,n>arrow$.

: We should prove that for any $cg\in C\mathcal{G}(P)$ there exists $cg’\in C\mathcal{G}(Q)$ such that
. There are three type of the edge.

$cg\leq \mathrm{c}g’$

1. Case$\mathit{0}^{<l,>}-^{n}O’$:$o^{<l,>}-^{n}\mathit{0}’$$\Rightarrow$$\Rightarrow$$P-_{\approx}^{m}\mathcal{T}l-P/\wedge \mathit{0}^{L}=P$$\Rightarrow$$\Rightarrow$A$\exists n.(m\leq n)$$\mathit{0}^{\prime/}arrow<l,n>\mathit{0}^{\prime/}$’

A $0^{\prime L}=Q$$Qarrowarrow Q\tau m\iota\approx/\wedge P’\subseteq_{r}Q’$

A $0^{\prime/L}=Q$ A$0^{\prime\prime/L}=Q’\wedge P’\subseteq_{r}Q’$(Definition 2.17)(Assumption)(Definition 2.17)$\mathit{0}arrow//<l,n>/\prime\prime O\bigwedge_{\mathit{0}’=}/LQ\wedge \mathit{0}^{\prime/}=/LQ’$(Definition 3.5)$\wedge\forall cg^{\prime/}\in C\mathcal{G}(P’)\exists cg///\in C\mathcal{G}(Q)s.t.cg^{\prime/}\leq cg^{\prime//}$Then for any $cg$ containing

2. Case$cg^{\prime/}$, there exists$cg’\in C\mathcal{G}(Q)$containing $cg”’$ .

: Therefore, we divide two cases. That is. In both cases, we can prove similarly to 1.

$\mathit{0}<\epsilon,n>arrow \mathit{0}’$$P-_{\approx}^{m+1}\tau Q$

Theorem 4.7$P-_{\approx}^{m}\mathcal{T}\mathcal{T}arrow\not\simeq Q$

and$\blacksquare$$P\subseteq_{r}Q\Rightarrow P\subseteq_{E}Q$$\blacksquare$

Proof: Assumes that there is a transition $Psarrow P’$ . This transition can be divided into
$Parrowarrow\#^{P_{1}^{1}}\tau m^{0}\tau\approxarrow\tau m_{1}^{1}\tau\approxarrow\ldots {}_{\#}P^{j}1arrowarrow^{1}\tau m_{j}^{1}l\tau m_{1}^{2}\approx P_{1}arrow\tau j\approxarrow\not\simeq\cdots P_{i}arrow\tau m_{\dot{j}}\approx P’$

Then, by Lemma 4.6,
$P\subseteq_{r}Q$$P_{1}^{1}\subseteq_{r}Q_{1}^{1}$

.

then
then

$Parrowarrow\mu Prm^{0}\tau\approx 11$$\Rightarrow\exists n^{0_{S.t}.}m\leq n^{0}\wedge Qarrowarrow\not\simeq\approx Q_{1}\tau n^{0}\tau 1\wedge P_{1}^{1}\subseteq_{r}Q_{1}^{1}$$P_{1}^{1}arrow-\tau m_{1}^{1}\tau P^{2}\approx\# 1\Rightarrow$..

$\exists n_{1}^{1}S.t.m^{1}1\leq n_{1}^{1}$

A$Q_{1}^{1}arrowarrow\not\simeq Q’rn_{1}^{1}\tau\approx$A$P_{1}^{2}\subseteq_{r}Q_{1}^{2}$$\cdot$$.\cdot$$P_{i}^{j}\subseteq_{r}Q_{i}^{j}$then$P_{i}^{j}arrow P’\tau m_{j}\approx:\Rightarrow\exists n_{j^{S}}^{i.i}t.m_{j}\leq n_{j}^{i}\wedge Q_{i}^{j}arrow_{\approx}\tau n_{\acute{\dot{j}}}Q’\wedge P’\subseteq_{r}Q’$

Then, $P\subseteq_{r}Q\Rightarrow Parrow P’s\Rightarrow$
By Definition 4.2, this$\exists s’s\leq \mathit{8}’\exists Q’Qs’arrow Q’$$\mathrm{s}\mathrm{h}\mathrm{o}\mathrm{w}\mathrm{S}\subseteq_{r}$A$P’\subseteq_{r}Q’$

is an efficiency prebisimulation.

We do not know whether the converse inclusion holds or not.

.
$\blacksquare$

78

5Conclusion

In this section we compare our construction with Arun-Kumar-discuss some further issues.

Comparison with efflciency preorder
There are several differences between our work and Arun-Kumar-Hennessy’s construction. As was discussed already, our cost graphs are intended to provide a comprehensive
framework for evaluating and analysing concurrent programs in regard of their efficiency.
Specifically varied ways of measuring efficiency of programs according to the need area feature not found in the precursor. Especially the relative optimal and strongly optimal orderings seem to have practical significance. The second difference is the semantic
framework. Efficiency preorder is based on inductive definition, which would make thereasoning easier for some cases. However we believe, especially in the case when the reasoning can be performed semi-algorithmically, both methods may not differ so much inpractice. Finally we should note that two frameworks are different in the ways of counting cost of two different transitions which do the same thing but whose
but not in ours). Indeed it cansemantic points” may be different (this is counted
which shows how ourwitheasilycoincides
point,
this
that,
we
relax
if
provedbe. While this and other options are possible, ouris at least close
construction
intention is to start from the formulation which is most faithful to the underlying semantic structure, i.e. abstract derivation graphs. In practice various ramifications should beconsidered.

$‘(\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{e}\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{t}\mathrm{e}$$\mathrm{i}\mathrm{n}\subseteq_{E}$$\subseteq_{r}$$\mathrm{o}\mathrm{f}\subseteq_{r}$$\subseteq_{E}$$\mathrm{t}\mathrm{o}\subseteq_{E}$IssuesThere are several problems which are to be solved for the application of the present theory.
The first thing, maybe the most difficult, is how the present framework can be mapped to
the real cost of execution environments. In this context, cost theory should also include
the soundness of mapping between programs and their execution, w.r.t. cost orderings.
But the significance of the present construction also lies in that, at least in the stipulated
criteria, ways of ordering programs, either their execution images or source programs, arenow present.
As a theoretical basis for pragmatic development, algorithmic aspects of cost theory
should be performed. Apart from such issues as algorithmic construction of cost graphs
for e.g. finite-state programs, not only comparison of programs but also optimization
methodologies can be developed, once we are given a firm criteria about efficiency. We
hope that many optimization technologies in sequential programs will be adaptable ina special method may be needed for concurrent
concurrency settings, but very
systems. This point is also related with the optimal execution graph of a given program,as well as the existence of optimal programs among weakly bisimilar ones.
In conclusion, in this paper we have investigated the possibility of capturing the notionof cost in concurrency (specifically the one of the execution time) in a rigorous formal
framework. While many things remain to be solved, we hope that our work provides a
possible formal foundation for measuring efficiency of concurrent programs.
$\mathrm{P}^{\mathrm{r}\mathrm{o}\mathrm{b}\mathrm{a}\mathrm{b}1}\mathrm{y}$79Acknowledgments
The author thank Kohei Honda for discussions and comments on the paper and proofreading.

References[1] S. Arun-Kumar and M. Hennessy. An efficiency preorder for processes. Acta Informatica 29, pages 737-760, Springer-Verlag, 1992.
[2] H. Barendregt. The Lambda $CalculuS:It_{S}$ syntax and semantics. North Holland,
revised edition edition, 1984.

[3] J. Hindley and J. Seldin. Introduction to
University Press, 1986.

$c_{om}binator\mathit{8}$and$\lambda$

calculus. Cambrige[4] T. Hoare. Comunicating Sequential Processes. 1978.
[5] K. Honda and M. Tokoro. An Object Calculus for Asynchronous Communication.
ECOOP’91, LNCS 512, pp.21-52, Springer-Verlag 1991.
[6] M. Kubo. Notes on unfolding cost graph, manuscript.

[7] J-L. Levy. Optimal reduction in th lambda-calculus. In J-P. Seldin and J-R. Hindley, editors, To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus andFormalism, pages pp159-191, Academic Press, 1980.
[8] R. Milner. A Calculus of Communicating Systems. LNCS 92, Springer-Verlag, 1980.
[9] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[10] R. Milner. Function as ProceS8eS. Mathematical Structure in Computer Science, 2(2),pp.119-146, 1992.

[11] R. Milner, J. Parrow, and D. Walker. A calculus of Mobile Proce8SeS $PartI/II$. Technical Report ECS-LFCS-89-85/86, Laboratory for Foundations of Computer Science,
University of Edinburgh, June 1989.