KURENAI : Kyoto University Research Information Repository
Title

Semantic Characterizations for Reachability and Trace
Equivalence in a Linear Logic-Based Process Calculus :Preliminary Report

Author(s)Okada, Mitsuhiro; Terui, Kazushige

Citation

数理解析研究所講究録 (1997), 976: 146-168

Issue Date

1997-02

URL

http://hdl.handle.net/2433/60798

Right

Type

Textversion

Departmental Bulletin Paper

publisher

Kyoto University

146

数理解析研究所講究録976 巻 1997 年 146-168

Semantic Characterizations for Reachability and Trace
Equivalence in a Linear Logic-Based Process Calculus(Preliminary Report)($\varpi$

田老弘)($\Theta_{\backslash \sim\backslash }.\rho$

芹

$-$

歳)

Mitsuhiro Okada
Kazushige Terui
Department of Philosophy, Keio University
Abstract
We give semantic characterizations for reachability and trace equivalence in a version ofasynchronous process calculus based on linear logic.
Usually the reachabtlity relation in linear logic-based process calculi is characterized by
the logical notion of provability, which is in turn characterized by model-theoretic semantics
such as phase semantics. We introduce considerably simplified phase models, which we callnaive phase models, and show that reachability is also characterized by the completeness withrespect to the naive phase models.
On the other hand, logical provability does not provide any satisfactory notion of equivalence on processes. We consider the trace equivalenceon our process calculus andintroduce certain algebraic models, which we call trace models. Then the trace equivalence ischaracterized by the completeness with respect to the trace models.
$(\mathrm{H}\mathrm{o}\mathrm{a}\mathrm{r}\mathrm{e}[7])$\S 1Introduction

We investigate a version of asynchronous process calculus based on linear logic. In our framework,
formulas are identified with processes and inference rules are identified with actions in terms of“message passing”-based process calculi. Then a bottom-up proof construction of a formula isnaturally interpreted as a computation of the process (cf. \S 2).
Under these identifications, various notions which have been discussed in the framework ofprocess calculi are brought into logical study. This paper attempts to give a logical analysis tothese new notions from process calculi in the framework of traditonal model-theoretic semantics.
Usually the logical notion of provability captures the reachability relation from the inputs tothe outputs. On the other hand, the provability is characterized by logical semantics, . phasesemantics, via the completeness theorem in the traditional framework of logic. However, the usual
logical semantics complete for full linear logic, . phase semantics, is of rather abstract nature;such a semantics interpretes a formula on a certain model-theoretic domain, but the interpretationof a formula is usually so complicated that one could hardly catch any intuitive meaning of aformula from such a semantics. For
phase semantics requires a certain closure condition
to be complete with respect to full linear logic, and requires a formula to be interpreted by acertain “
set, called a fact (cf. \S 3.1), which makes the intuitive meaning of the formula
$A$

$A$

$\mathrm{e}\mathrm{g}$$\mathrm{e}\mathrm{g}$$\mathrm{e}\mathrm{x}\mathrm{a}\mathrm{m}\mathrm{p}\mathrm{l}\mathrm{e}\rangle$)$\mathrm{c}1_{\mathrm{o}\mathrm{s}\mathrm{e}}\mathrm{d}’$ambiguous.
Our theory of process calculus uses only a very restricted fragment, essentially Horn fragmentof linear logic. Hence there is a possibility to obtain simpler semantics that is complete withrespect to the framgent. In \S 3.2, we introduce a simplified semantics for the Horn fragment, called
naive phase semantics, which is obtained from phase semantics by dropping the closure condition.
Naive phase semantics gives more intuitive meaning of formula than the original phase semantics.
Our first main result says (in \S 3.2),

147

1. The reachability relation is characterized by the completeness with respect to the naive phasemodels.

The next problem which we address in this paper is to characterize certain notion of equivalence
on processes in the traditional framework of model-theoretic semantics. The identification of
formulas with processes naturally leads us to the following question, what is an appropriate notionof equivalence on
from the viewpoint of process calculi? One might expectthat logical equivalence, defined in terms of logical provability, provides such an adequate notionof equivalence;
and $B$ are logically equivalent if $A\vdash B$ and $B\vdash A$ are provable in linear logic.
Logical equivalence is, however, too coarse in a sense and too fine in another sense to be an adeqate
notion of equivalence on processes. Consider two processes
and.
intuitively means
receive , then receive and send ”, while $\beta-0\alpha-0\gamma$ intuitively means“first receive , then receive and send ”. So they behave quite differently, whereas the logicalequivalence identifies them. On the other hand, it is reasonable to think that&\mbox{\boldmath $\gam a$}-0
and
are equivalent with respect to their behavior, whereas
they are not logically equivalent. Heremeans “receive a and invoke ”,means “sendand invoke $A’$ ), A&B means “choose
or $B$ ”. (Seefor a slightly
different view of logical equivalence.)
The leading principle to find an adequate notion of equivalence is that processes should beequivalent if they are indistinguishable by an external observer. What makes two processes equiv$\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}}1\mathrm{a}\mathrm{s}/\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}\mathrm{e}\mathrm{s}$$A$$\alpha-0\beta-0\gamma$$\beta-0\alpha-0\gamma$$\alpha-0\beta-0\gamma$($‘ \mathrm{f}\mathrm{i}\mathrm{r}\mathrm{s}\mathrm{t}$$\beta$$\alpha$$\beta$$\alpha$$\gamma$$\gamma$$(\alpha-0\beta)\otimes(\gamma-0\delta)$$\alpha-0$ $(\beta\otimes (\gamma-0 \delta))$$((\alpha-0\beta)\otimes\delta))$$\alpha-0$ $A$$A$$\alpha$$A$$\alpha\otimes A$$\mathrm{K}\mathrm{o}\mathrm{b}\mathrm{a}\mathrm{y}\mathrm{a}\mathrm{s}\mathrm{h}\mathrm{i}\ \mathrm{Y}_{0}\mathrm{n}\mathrm{e}\mathrm{z}\mathrm{a}\mathrm{W}\mathrm{a}[11]$alent or distinct is their observable behavior. Under this principle, various notions of equivalence
have been proposed in the literature (cf. van). Among those, we deal with trace
equivalence in this paper.
Trace equivalence, presented by Hoare[7], is known to be one of the simplest notion of equivalence; roughly,
andare trace equivalent if they can perform the same set of sequences ofobservable actions. Trace equivalence provides a better notion of equivalence on processes thanthat of logical equivalence from the observational point of view. As a matter of fact, it is easily
shown thatand $\beta-0\alpha-0\gamma$ are not trace equivalent, and that&\mbox{\boldmath $\gam a$}-0
and
are trace equivalent. Trace equivalence is sometimes
considered to be too weak to identify processes in the sense that it identifies too many processes.
In particular, it possibly identifies a deadlocking process with one that does not deadlock (see Example 3(2) in \S 4.1). Nevertheless it is of significance as the basis for other equivalence notions ofprocesses. Trace equivalence provides a simple formalization of our basic intuition that processes
are equivalent if they are observationally indistiguishable, and any equivalence naturally definedon the basis of this intuition can be seen as a refinement of trace equivalence.
In \S 4.1 we consider the trace equivalence in our framework, defined in terms of observablebehavior of processes, and in \S 4.2 we introduce certain algebraic models, which we call tracemodels. Trace models are defined in the traditional frame work of algebraic semantics. Then our
second main result says (in \S 4.2);$\mathrm{G}\mathrm{l}\mathrm{a}\mathrm{b}\mathrm{b}\mathrm{e}\mathrm{e}\mathrm{k}[29][30]$

$A$

$B$

$\alpha\infty\beta-0\gamma$$\alpha-0$ $(\beta\otimes (\gamma-0 \delta))$$(\alpha-0\beta)\otimes(\gamma-0\delta)$$((\alpha\infty\beta)\otimes\delta))$

2. Trace equivalence is characterized by the completeness with respect to the trace models.
For the completeness proof we use the technique similar to the phase-semantic completenessproof.
In this preliminary report, we only deal with the systems that can be developed in propositional
fragment of linear logic.

\S 2

Syntax and Operational Semantics

Through this paper, we consider the following correspondence between the logical notions and thenotions from the theory of “message passing”-based process calculi;

148$\mathrm{T}\mathrm{a}\mathrm{h}1_{\mathrm{P}}\rceil$

propositional variables
logical connectives
inference rules
formulassequents
bottom-up proof construction

$=$
$=$
$=$

$=$
$=$
$=$

tokens or messages
action names
transition rules
processes
process configurations
computation

We identify a propositional variable with a token or a message, and each logical connective symbol with an action name. Then the operational meaning of an action, namely the transition rule
determining the behavior of the action, is described in terms of a logical inference rule corresponding to the logical connective associated to the action. A formula constructed from propositionalvariables and logical connectives is viewed as a process and a sequent (in the sequent-calculus
formulation of logic) is viewed as a process configuration. A logical inference is interpreted as astate-transition by reading them bottom-up, thus, . a logical inference of the form$\mathrm{e}\mathrm{g}$$\frac{A,B,\Gamma\vdash}{A\otimes B,\Gamma\vdash}\otimes$

is read as “statetransforms to state $A,$ $B,$ by Parallel. Then a bottom-up”
proof construction for a sequentcorresponds to a computation starting from a process
configuration”.
We introduce the system , a version of asynchronous concurrent process calculus
ed onlinear logic proof search, that is essentially a subsystem of the system considered by.
is based on left one-sided sequent calculus. However, nothing important is missing for theoretical issues compared with process calculi based on two-sided (classical) sequent calculi such as$A\otimes B,$$\Gamma$$\Gamma$$\mathrm{a}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\otimes^{)}’$“ $\Gamma\vdash$“ $\Gamma\vdash$$S$$\mathrm{b}\mathrm{a}s$$\mathrm{O}\mathrm{k}\mathrm{a}\mathrm{d}\mathrm{a}[20][21]$$S$

Andreoi&Pareschi[2]’s LO and

ACL, althoughformulation would be convenient for practical issues like the logic programming languages design.
Let us begin by defining the language $L(S)$ of our system . We presuppose that a setof propositional variables is given. As mentioned before, logical constants and connectives canbe naturally interpreted by actions in our process calculus. In the following definition, we givethe action names corresponding to the outermost logical connectives. Their precise operational
meanings will be given below in terms of logical inference rules of linear logic.
$\mathrm{t}\mathrm{w}(\succ \mathrm{S}\mathrm{i}\mathrm{d}\mathrm{e}\mathrm{d}$$\mathrm{K}\mathrm{o}\mathrm{b}\mathrm{a}\mathrm{y}\mathrm{a}\mathrm{S}\mathrm{h}\mathrm{i}\ \mathrm{Y}_{\mathrm{o}\mathrm{n}}\mathrm{e}\mathrm{Z}\mathrm{a}\mathrm{w}\mathrm{a}[10][12]’ \mathrm{s}$$S$$\mathcal{P}$Definition 1 The language $L(S)$ is defined as follows;
1. If
2.

$\alpha\in \mathcal{P}$, then $\alpha\in L(S)$ (Token or Message).

$1\in \mathcal{L}(S)$(Suicide-action).

3. If $A,$
, thencalled a Sending-action$B\in \mathcal{L}(S)$4. If$\alpha_{1},$5. If $A,$$\ldots,$$A\otimes B\in \mathcal{L}(S)$$\alpha_{n}\in \mathcal{P}(n\geq 1)$$B\in \mathcal{L}(S)$and(Parallel-action), in particular if$B\in \mathcal{L}(S)$, then$\alpha\in \mathcal{P}$$\alpha_{1}\otimes\cdots\otimes\alpha_{n}-\mathrm{o}B\in \mathcal{L}(S)$, then$\alpha\otimes B$

is(Receiving-action).

, then A&B\in L(S) (Choice-action).

6. If $A\in L(S)$ , then$!A\in \mathcal{L}(S)$(Bang-action).

Thus our language
is a subset of that of the usual intuitionistic linear logic;
lacks, and implications are restricted to the Horn implications inthat require antecedents
to be of the form
for.
Roughly speaking, the formulas incorrespond to the processes inandin the way described in Table 2.
$\mathcal{L}(S)$$\mathrm{T},$$0,$ $\perp,$$\mathcal{L}(S)$$\oplus$$\mathcal{L}(S)$$\alpha_{1}\otimes\cdots\otimes\alpha_{n}$$\alpha_{i}\in \mathcal{P}$$\mathcal{L}(S)$$\mathrm{C}\mathrm{C}\mathrm{S}[16]$$\pi- \mathrm{c}\mathrm{a}\mathrm{l}\mathrm{C}\mathrm{u}\mathrm{l}\mathrm{u}\mathrm{s}[19][18]$149

Table 2: Correspondence between formulas in$S$

and processes in CCS and -calculus$\pi$

It should be noted, however, that there are some serious differences between them; is an as ynchronous calculus in the sense explained later whereas CCS and -calculus are synchronous, andis based on proof-theoretic notions whereas CCS and -calculus are based on algebraic notions.
(An asynchronous version of -calculus was also introduced inon the basis of algebraic
notions.)
A finite multiset of formulas inis called a process configuration. A sequent of of the$A,$ $B,$
form
identified with a process configuration F. In the sequel,range overrange over, andrange over the process configurations ofrange overthe finite sequences of propositional variables. If
stands for.
In particular, if
is the empty sequence,stands for 1. We write
to denote a formula. A formula of the form !A is called a modal formula.
$S$

$\pi$

$S$

$\pi$

$\pi$

$\mathrm{H}\mathrm{o}\mathrm{n}\mathrm{d}\mathrm{a}[9]$$S$$\mathcal{L}(S)$$\Gamma\vdash \mathrm{i}\mathrm{s}$$\alpha,$$\mathcal{L}(S)$$\Gamma,$$\Delta,$$\beta,$$\mathcal{P},$$\ldots$$\ldots$$\mathcal{L}(S).\vec{\alpha},\vec{\beta},$$\ldots$$\ldots$$\vec{\alpha}=\alpha_{1},$$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\otimes\vec{\alpha}$$\ldots,$$\vec{\alpha_{i}}$$\alpha_{1}\otimes\cdots\otimes\alpha_{n}$$\alpha_{n},$$A^{n}$$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\otimes\vec{\alpha}$$\sim A\otimes\cdots\otimes A$

$n$

times

The inference rules of , which corresponds to the transition rules in process calculi (whenread bottom-up), are essentially those of linear logic restricted to our language. It should be
noted that below is considered as a multiset, hence the exchange rule is implicit.
$S$.

$\mathcal{L}(S)$$\Gamma$Parallel Action$(\otimes)$$\frac{A,B,\Gamma\vdash}{A\otimes B,\Gamma\vdash}\otimes$(Parallel action
invokes processes
is the Sending Action$A\otimes B$

$A$

and

$B$

in parallel.) A special case of this action$\alpha B\mathrm{r}\vdash$,–,.

$\alpha\otimes B,$$\otimes$$\Gamma\vdash$(Sending action$\alpha\otimes B$

sends a token$\alpha$and invokes $B.$ )Receiving Action $(-0)$$\frac{(\vec{\alpha}\vdash\otimes\vec{\alpha})A,\mathrm{r}\vdash}{arrow}-0$$\alpha,$$\otimes\vec{\alpha}-\mathrm{o}A,$$\Gamma\vdash$where denotes. (Receiving action
receives tokens from theenvironment and invokes $A.$ ) We treat thisas if it had only one premise. This
convention is justified by the fact that the left premise of this rule is always provable, (hence
the proof construction of the left premise terminates immediately.)$\vec{\alpha}$$\alpha_{1},$$\ldots,$$\alpha_{n}(n\geq 1)$$\otimes\vec{\alpha}-0$$A$$\vec{\alpha}$$\mathrm{r}\mathrm{u}\mathrm{l}\mathrm{e}/\mathrm{a}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$.
.

Choice Action (&)$\frac{A,\Gamma\vdash}{A\ B,\Gamma\vdash}\$$\frac{B,\Gamma\vdash}{A\ B,\Gamma\vdash}\$(Choice action A&B chooses either A or$\mathrm{B}$, and invokes it.)

Suicide Action (1)$\frac{\Gamma\vdash}{1,\Gamma\vdash}1$.

(Suicide action 1 terminates itself.)

Bang Action (!)$\underline{!A,A,\Gamma\vdash}!$$!A,$$\Gamma\vdash$(Bang action !A produces a copy $A$ and invokes it.)

Note that the above Bang ! rule is slightly different fromoriginal bang (modality)
rules; ours is derivable from Girard’s, but not vice versa. Our bang ! is sometimes called Milner’s$\mathrm{G}\mathrm{i}\mathrm{r}\mathrm{a}\mathrm{r}\mathrm{d}[5]’ \mathrm{S}$150bang because it behaves like the one Milner introduced in [18] for his theory of -calculus. It canbe shown that these two versions of bang ! are equivalent up to reachability and trace equivalence
defined later (in this section and in \S 4.1).
Listed below are some useful derived rules in .
$\pi$

$S$

(1)
$\frac{\frac{B,\Gamma\vdash}{\beta,\beta-\mathrm{o}B,\Gamma\vdash}}{\beta,\alpha-\mathrm{o}A\ \beta-\circ B,\mathrm{r}\vdash}$$\frac{\frac{A,\Gamma\vdash}{\alpha,\alpha-\mathrm{o}A)\Gamma\vdash}}{\alpha,\alpha-\mathrm{o}A\ \beta-\mathrm{o}B,\Gamma\vdash}$

The process$\alpha-0$

A&\beta -o$B$selects

$A$

or

$B$

depending on$\alpha$or$\beta$which the process receives.

(2)$\frac{}{\vec{\alpha},!(\otimes\vec{\alpha}-\mathrm{O}\otimes\vec{\beta}),\Gamma,\vdash}\frac{\vec{\beta},!(\otimes\vec{\alpha}-0\otimes\vec{\beta}),\Gamma,\vdash}{\vec{\alpha},\otimes\vec{\alpha}-\circ\otimes\vec{\beta},!(\otimes\vec{\alpha}-0\otimes\vec{\beta}),\mathrm{r},\vdash}$

The process$!(\otimes\vec{\alpha}-0\otimes\vec{\beta})$transforms tokens$\vec{\alpha}$

into , while the process itself remains unchanged.
$\vec{\beta}$(3)$\frac{\frac{A,B,\Gamma\vdash}{\alpha,A,\alpha-\mathrm{o}B,\Gamma\vdash}}{\alpha\otimes A,\alpha-\mathrm{o}B,\mathrm{r}\vdash}$. Note that this communication ocpasses a message to the receiver
The sendercurs asynchronously in the sense that the sender can send a message without synchronizing withthe receiver. This is the most important difference from synchronous concurrent process calcului
is said to be an
CSP, and so on, and for this reason our
CCS,such as).
asynchronous concurrent process calculus (also cf.
$\alpha\otimes A$$\alpha-\mathrm{o}B$$\alpha$$S$$\mathrm{H}\mathrm{o}\mathrm{a}\mathrm{r}\mathrm{e}[8]’ \mathrm{s}$$\mathrm{M}\mathrm{i}\mathrm{l}\mathrm{n}\mathrm{e}\mathrm{r}[16]’ \mathrm{S}$$\mathrm{H}\mathrm{o}\mathrm{n}\mathrm{d}\mathrm{a}[9]$Example 1 Consider the detafolw diagram below;
Figure 1: A dataflow diagram

is a process
and denote channels in the above dataflow network. Process
andtochannelto receive two messages (tokens) from the channel and to produce two tokens
Here,$\alpha,\beta,$$\gamma,$$\delta,$$P_{1}$$\lambda$$\eta$$\alpha$$\beta$151

one token to channel concurrently. This is specified byin . We abbreviate
this as !
. The bang (modality) ! means that this process can be repeated infinitely
many times.
is waiting- for three tokens through channel then sending two tokens throughchannel .
is specified by.
is waiting for two tokens through channel 7 thensending one token through channel .
is specified by.
receives two tokens fromchannel and two from concurrently, then produces one output token through channel .
iswritten as.
Then the whole network is described as , where$S$$!(\alpha\otimes\alpha-0\beta\otimes\beta\otimes\gamma)$$\gamma$$(\alpha^{2}-0\beta^{2} \copyright 7)$$P_{2}$$\delta$$\beta$$!(\beta^{32}-0\delta)$$P_{2}$$\eta$$P_{3}$$!(\gamma^{2}-0\eta)$$P_{3}$$P_{4}$$\delta$$\lambda$$\eta$$P_{4}$$!(\delta^{2}\otimes\eta^{2}-0\lambda)$$\Gamma$$\Gamma\equiv!(\alpha^{2}-\circ\beta 2\otimes\gamma),$!

$(\beta^{3}-\mathrm{O}\delta 2),$$!(\gamma-\circ 2\eta),$$!(\delta^{2}\otimes\eta^{2}-0\lambda)$.

Now consider an initial channel state $m$ , say. This means that the network is started
with channel state $m$ , i.e., two tokens at channel , one token at channel and five tokens atchannel .
By using derived rule (2) above, we observe that the following is a derivation in ;$\alpha^{2},$$\beta,$$\gamma^{5}$$\beta$$\alpha$$\gamma$$S$$\frac{\lambda,\gamma^{2},\Gamma\vdash}{\delta^{2},\eta^{2},\gamma^{2},\Gamma\vdash}$$\frac{\delta^{2},\eta,\gamma^{4},\Gamma\vdash}{\delta^{2},\gamma^{6},\Gamma\vdash}$$\frac{\beta^{3})\gamma^{6},\mathrm{r}\vdash}{\alpha^{2},\beta,\gamma^{5},\Gamma\vdash}$the channel state in which there are one token at channel andtwo tokens at channel . Then the above derivation expresses that channel state is reachable
from channel state $m$ under specification F. The channel stateis also reachable from $m$ under, but the state
is not.
Let us denote by$n(\equiv\lambda, \gamma^{2})$$\lambda$$n$$\gamma$$\lambda,$$\eta$$\lambda^{2}$$\Gamma$$\blacksquare$

Example 2 If we incorporate such an infinitary expression
trary index set, into the language, and add an inference rule$\mathrm{a}s\ _{i\in I}A_{i}$, where $I$ denotes an arbi-$\frac{A_{j},\Gamma\vdash}{\ _{i\in I}Ai\Gamma\vdash},$,where $j\in I$ , then we can express value passing between two processes in this extended system.
where is a natural number. Let
Assume that
includes propositional variables of the form
us writeto denote . Nonatomic formulas are treated as if they were first-order formulas;
we write $A(i)$ to indicate some occurrences of subscript attached to propositional variables in .
.
We abbreviate awhere $N$ is the set of natural numbers by
Then we see$i$$\mathcal{P}$$\alpha_{i}$$\alpha(i)$$a_{i}$$A$$i$$\alpha(x)-\mathrm{O}B(X)$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}\ _{i\in N}\alpha(i)-\mathrm{O}B(i)$$\frac{A,B(n),\Gamma\vdash}{\alpha(n),A,\alpha(n)-\mathrm{o}B(n),\mathrm{r}\vdash}$$\frac{\alpha(n),A,\alpha(X)-\circ B(X),\mathrm{r}\vdash}{\alpha(n)\otimes A\alpha()X)-\circ B(_{X)\Gamma\vdash}\rangle}$

passes value tois a derivation in this extended system. This expresses that the sender
the receiverthrough channel .
All results shown in this paper would still hold by this extension. Later we shall introduce thisinfinitary&formally in \S 4.1.
$\alpha(n)\otimes A$$\alpha(x)-\mathrm{O}B(X)$$n$$\alpha$$\blacksquare$If$\frac{\Gamma_{2}\vdash}{\Gamma_{1}\vdash}$152

is an instance of an inference rule of , then the pair ofandis called a transition (and wedenote the transition relation by). A (finite or infinite) sequenceofprocess configurations is a transition sequence if for each a transition relation
holds.
The transitive reflexive closure
written. Hencemeans that there exists
a finite transition sequence from to .
Let bebe,
and be a process configuration, i.e. asequence of formulas of. Then we say is reachable from under if
for somesequenceof modal formulas.
$S$$\Gamma_{1}$$\Gamma_{2}$$\Gamma_{1}arrow\Gamma_{2}$$\mathrm{r}_{0},$$\Gamma_{1},$$\Gamma i,$$\ldots,$$i$$\Gamma’$$\Gamma$$\alpha_{m}(m\geq 0),\check{\beta}$$\vec{\alpha}$$\alpha_{1},$$\Gammaarrow^{*}\Gamma’$$\mathrm{a}\mathrm{s}arrow^{*}$$\mathrm{o}\mathrm{f}arrow \mathrm{i}\mathrm{s}$$\ldots$$\Gamma_{i-1}arrow\Gamma_{i}$$\beta_{1},$$\ldots,$$\beta_{n}(n\geq 0)$$\ldots$$\Gamma$$\vec{\beta}$$\mathcal{L}(S)$$\vec{\alpha}$$\Gamma$$\vec{\alpha},$$\Gammaarrow^{*}\tilde{\beta},$$!\Sigma$$!\Sigma$

Proposition 1 The following are equivalent,(1) is reachable from under ;(2)is provable in classical full linear logic;(3)
is provable in intuitionistic full linear logic.
(See $Girardl\theta f$ for the precise definition of classical and intuitionistic linear logic.)$\cdot$$\vec{\beta}$$\vec{\alpha},$$\vec{\alpha},$$\vec{\alpha}$$\Gamma$$\Gamma\vdash\otimes\vec{\beta}$$\Gamma\vdash\otimes\tilde{\beta}$

Proof. Consider the following subsystem $S’$ of linear logic;

Axiom:$\vec{\alpha}\vdash\otimes\vec{\alpha}$

Inference rules:$\underline{A,B,\Gamma\vdash\otimes\vec{\beta}}\otimes$$\frac{\vec{\alpha}\vdash\otimes\vec{\alpha}A,\mathrm{r}\vdash\otimes\tilde{\beta}}{\vec{\alpha},\otimes\vec{\alpha}-\mathrm{O}A,\mathrm{r}\vdash\otimes\vec{\beta}}-0$$A\otimes B,$ $\Gamma\vdash\otimes\tilde{\beta}$$\frac{A,\Gamma\vdash\otimes\vec{\beta}}{A\ B,\Gamma\vdash\otimes\vec{\beta}}$$\frac{\Gamma\vdash\otimes\vec{\beta}}{!A,\Gamma\vdash\otimes\vec{\beta}}!W$&$\frac{B,\Gamma\vdash\otimes\vec{\beta}}{A\ B,\Gamma\vdash\otimes\vec{\beta}}$&$\frac{!A,!A,\Gamma\vdash\otimes\vec{\beta}}{!A,\Gamma\vdash\otimes\vec{\beta}}!C$$\frac{\Gamma\vdash\otimes\vec{\beta}}{1,\Gamma\vdash\otimes\vec{\beta}}1$$\frac{A,\Gamma\vdash\otimes\vec{\beta}}{!A,\Gamma\vdash\otimes\vec{\beta}}!D$

ily shown, a sequent of the formAs, where is a process configuration of , is provable in $S’$ iff it is provable in classical full linear logic iff it is provable in intuitionistic full linear
logic. We can
ily transform a finite transition sequence of into a proof in $S’$ , and vice versa.
$\Gamma\vdash\otimes\vec{\beta}$$\mathrm{e}\mathrm{a}s$$S$$\Gamma$$S$$\mathrm{e}\mathrm{a}s$$\blacksquare$

The above Proposition shows that the logical notion of provability characterizes reachability.

\S 3

Naive Phase Semantics Characterizing Reachability\S 3.1Preliminary Remark on Intuitionistic Phase Semantics

This subsection is devoted to a brief introduction to intuitionistic phase semantics, as a preliminary
to the next subsection.
Phase semantics, originally introduced by, is a standard model-theoretic semantics
for (classical) linear logic. After the publication of [5], its intuitionistic versions are investigated byseveral authors, .
, with slight differences in their definitions.
Here we introduce a version of intuitionistic phase semantics, following. As proved in[22], the semantics completely characterizes provability in intuitionistic linear logic. In the lightof Proposition 1 in \S 2, which says that provability in intuitionistic linear logic characterizes reachability in , it is immediate that satisfiability in intuitionistic phase semantics also characterizereachability in S. However, intuitionistic phase semantics usually requires a certain closure operator to interprete formulas, which causes difficulty in understanding the intuitive meaning of
formulas via the semantics.
We shall introduce naive phase semantics, i.e., phase semantics without any closure condition,
in \S 3.2. That is obtained by modifying intuitionistic phase semantics defined below. A variant of$\mathrm{G}\mathrm{i}\mathrm{r}\mathrm{a}\mathrm{r}\mathrm{d}[5]$$\mathrm{A}\mathrm{b}\mathrm{r}\mathrm{u}\mathrm{s}\mathrm{c}\mathrm{i}[1],$$\mathrm{e}\mathrm{g}$$\mathrm{o}\mathrm{k}\mathrm{a}\mathrm{d}\mathrm{a}[22],$$\mathrm{s}_{\mathrm{a}}\mathrm{m}\mathrm{b}\mathrm{i}\mathrm{n}[27]$$\mathrm{O}\mathrm{k}\mathrm{a}\mathrm{d}\mathrm{a}[22]$$\mathrm{S}$153

intuitionistic phase semantics is also used for the canonical model construction for completenessof the trace models in \S 4.4.

Definition 2 An intuitionistic phase space $(M, D, \perp)$ consists of a commutative monoid $M$ , a
subset $D$ (called the facts) of the powersets ofthat satisfies$M\mathrm{a}\mathrm{n}\mathrm{d}\perp\in D$(P1) $D$ is closed under arbitrary$\cap$; in particular $M\in D$ ,(P2) If $X\subseteq M$ and $Y\in D$ , then $X-\mathrm{o}Y\in D$

is defined by $X-\triangleleft Y=\{y|\forall x\in Xxy\in Y\}$ for any $X,$ $Y\subseteq M$ . We also define $XY$ as
and(the smallest fact that includes $X$ ).
$1=\{1\}^{C}$
Then, we can define(1 stands for the unit element of $M$ ), $\mathrm{T}=M,$ $0=0^{C}$ , and forany facts $X,$ ,where$-arrow$$\{xy|x\in X, y\in Y\}$$X^{C}\mathrm{a}\mathrm{s}\cap\{Y\in D|X\subseteq Y\}$$Y$$\bullet X\otimes Y=(xY)^{C}$.

$\bullet$,$X\ Y=X\cap Y$,$X\oplus Y=(X\cup Y)^{c}$ ,$\bullet X^{\perp}=X-\circ\perp$.

Among the basic properties of intuitionistic phase spaces, we see the following;$\bullet$.

$\bullet$$\bullet$$\bullet$

For any facts $X,$
$X\otimes Y\subseteq Z$

iff

$Y$

and $Z,$ $X\otimes Y=Y\otimes X,$ $X\otimes(Y\otimes Z)=(X\otimes Y)\otimes Z,$ $1\otimes X=X$ ,$Y\subseteq X-\mathrm{o}Z$;$X-\circ(Y-\circ Z)=Y-\circ(X-\circ Z),$

$1-0X=X$ ;$X\otimes(Y\oplus Z)=(X\otimes Y)\oplus(X\otimes Z),$

$X-0$ $Y\ Z=$ ( $X-0$ Y)&(X-o $Z$ )$)$X\otimes (Y&Z)(X\otimes Y)&(X\otimes Z), but the reverse does not hold in general.

Associativity
nontrivial, but follows from the observation that $x^{c_{Y^{C}}}\subseteq(XY)c$ for any$X,$. Note that $(D, \ , \oplus, 0, -0, \otimes, 1)$ forms an IL-algebra in the sense of.
A classical phase space is a special intuitionic phase space in which $D$ consists of all
suchthat $X=X^{\perp\perp}$ .
The following definition is analogous to that of enriched (classical) phase spaces in(cf. also). If $M$ is an intuitionistic phase space, then $J(M)=\{x\in 1|x\in\{xx\}C\}$ is$M$
a submonoid of . An enriched intuitionistic phase space is an intuitionistic phase space $M$
endowed with a submonoid $K$ of $J(M)$ (not necessary to be a fact).
For any fact $X$ of enriched intuitionistic phase space, define$\mathrm{o}\mathrm{f}\otimes \mathrm{i}\mathrm{s}$$Y\subseteq M$$\mathrm{T}\mathrm{r}\mathrm{o}\mathrm{e}\mathrm{l}\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{a}[28]$$X’ \mathrm{s}$$\mathrm{L}\mathrm{a}\mathrm{f}_{\mathrm{o}\mathrm{n}}\mathrm{t}[13]$$\mathrm{G}\mathrm{i}\mathrm{r}\mathrm{a}\mathrm{r}\mathrm{d}[6]$$\bullet!X=(X\cap K)c$ .

..

The following are some basic properties of modality ! (cf.

$\mathrm{G}\mathrm{i}\mathrm{r}\mathrm{a}\mathrm{r}\mathrm{d}[5][6],$For any facts $X$ and $Y,$ $!X\subseteq X,$ $!X\otimes!X=!X,$ $!X\subset 1$ ; if$!Y\subseteq X$$\mathrm{L}\mathrm{a}\mathrm{f}_{\mathrm{o}\mathrm{n}}\mathrm{t}[13]$, then);$!Y\subseteq!X$;!(X&Y) $=!X\otimes!Y$ .

An intuitionistic phase model is given by an (enriched) intuitionistic phase space and an interpretation which maps each atom to a factof $M$ . Then any formula is interpreted by a fact
. We sayis interpreted byalong the above definitions, and$M$A^{*}$$1\in$M$that is satisfied in.
, and thatifis satisfied in
if$\Gamma\equiv A_{1},$

$A$

$A$

$\alpha^{*}$$\alpha$$A^{*}$$\ldots,$$A_{n}$$\Gamma^{*}=A_{1}^{*}\otimes\cdots\otimes A_{n}^{*}$$\Gamma\vdash C$$\Gamma^{*}\subseteq C^{*}$

is provable in
Theorem 1 Let
be a sequent in intuitionistic linear logic. Thenintuitionistic linear logic if and only if it is satisfied in every intuitionistic phase model.
$\Gamma\vdash C$$\Gamma\vdash C$

Proof. See$\mathrm{O}\mathrm{k}\mathrm{a}\mathrm{d}\mathrm{a}[22]$.

$\blacksquare$

Combined with Proposition 1 in \S 2, we obtain;
Corollary 1 Let be a process configuration of S. Then is reachable fromonly ifis satisfied in every intuitionistic phase model.
$\Gamma$$\vec{\alpha},$$\Gamma\vdash\otimes\vec{\beta}$$\vec{\beta}$$\vec{\alpha}$

under$\Gamma$

if and154

Naive Phase Semantics\S 3.2

As mentioned in the previous subsection, reachability in
is characterized by satisfiability in
intuitionistic phase semantics (Corollary 1). But it would be a shortcoming of phase semantics
that phase semantics heavily relies on some closure condition in order to be complete for its
corresoponding syntax; for example, $X\otimes Y$ should be interpreted by $(XY)\perp\perp$ in classical phasespaces and by $(XY)c$ in intuitionistic phase spaces. However, from the viewpoint of practicalapplications of linear logic such as logic programming, process calculus and formal linguistics, one
could hardly catch any intuitive meaning of these closure conditions. Hence it would be preferable
to dispense with any closure condition. Such a phase semantics without closure condition issometimes called a naive phase semantics.
Naive phase semantics is sound for full intuitionistic linear logic, but fails to be complete forthe following obvious reasons;$S$

1. The distributive law between&and\oplus holds for every naive phase model, but it cannot be
proved in linear logic.
2. Phase semantics requires that 1 be interpreted by the smallest fact including 1, the monoid
unit. In a naive phase model, however, such a fact would be {1}, that is too poor to be aninterpretation of 1; any formula of the form !A would collapse into 1 or , since !A must be
interpreted by a subset of the interpretation of 1.
$0$

Hence it is an interesting question to what extent of subsystems of linear logic one can obtainthe completeness with respect to naive phase semantics.
There are several completeness results on the naive phase semantics for certain very restrictedsubsystems of linear logic, especially for Lambek, which is essentially-fragmentof noncommutative intuitionistic linear logic, and its related systems.
proved that
Lambek Calculus and some systems related to it are complete with respect to the naive phasemodels (the generalized standard models or $GS$-models, in his terminology).
provedthat the naive phase models based on free semigroups, called the language, are sufficient tobe complete for Lambek Calculus. Okada&Terui[23] showed that the finite naive phase models are
sufficient to be complete for Lambek Calculus and some related systems, hence that these systems
have the finite model property with respect to the naive phase models.
In this subsection, we shall introduce the system
by restricting in such a way that 1 does
not occur and ! only occurs as an outermost connective. Then we prove that reachability inischaracterized by the completeness with respect to the naive phase models (Theorem 2 below).
has enough expressive power to represent a wide range of message-passing based communication
networks, hence our result in this Section would be useful in practical applications.
$(\otimes, -0)$$\mathrm{C}\mathrm{a}\mathrm{l}\mathrm{C}\mathrm{u}\mathrm{l}\mathrm{u}\mathrm{S}[14]$$\mathrm{B}\mathrm{u}\mathrm{s}\mathrm{Z}\mathrm{k}_{0}\mathrm{w}\mathrm{S}\mathrm{k}\mathrm{i}[4]$$\mathrm{P}\mathrm{e}\mathrm{n}\mathrm{t}_{\mathfrak{U}}\mathrm{s}[26]$$model_{\mathit{8}}$$S$$S_{1}$$S_{1}$$S_{1}$.

Definition 3 The language
If$A$$\mathcal{L}(S_{1})$is defined as follows;

is a formula in $L(S)$ that contains neither 1 nor !, then

The inference rules of$S_{1}$

is the same as$S$(but restricted to$A$$\mathcal{L}(S_{1})$In this Section, we write a process configuration in the formin the sequent are indicated by .

and !A are formulas in $L(S_{1})$ .

).

$!\Gamma,$$\Delta$, where all modal formulas$!\Gamma$

Definition 4 A naive phase model $M$ is an intuitionistic phase model (not enriched) in which thefacts $D$ consist of all subsets of $M$ .
A naive phase model does not need the closure operation $c_{;}X\otimes Y$ is simply interpreted byand each atomic formula is interpreted by any subset of $M$ . Since $D$ plays no role anddoes not have to be specified (because our language does not), we can say that a naive
phase model is simply a commutative monoid $M$ with anmaps each atomic
formula to a subset
of $M$ . Bangcannot be interpreted directly in a naive phase$XY$$\perp$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{n}\perp$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}*\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}$$\alpha$$\alpha^{*}$$!(\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{t}\mathrm{y})$155model for the reason discussed above. Thus we do not require a naive phase model to be enriched,rather, we interprete modal formulas as if they were axioms.
By a -model we mean a naive phase model in which $1\in A^{*}$ holds for eachoccuring in ,namely a naive phase model in which is true.
$\Gamma$$A$$\Gamma$$\Gamma$

Proposition 2 (Soundness) Let
under, then$\vec{\alpha}$$!\Gamma,$

Proof. If$\vec{\alpha},$$!\Gamma,$$\vec{\beta}$

is reachable from$\triangle\equiv!\Gamma,$$\Sigma_{0}arrow!\Gamma,$$\vec{\alpha}$

be a process configuration ofin every F-model.

$!\Gamma,$$(\vec{\alpha}, \Delta)^{*}\subseteq(\otimes\vec{\beta})^{*}$$\Delta$$\Delta$under$!\Gamma,$$\Delta$$S_{1}$. If$\vec{\beta}$

is reachable from, then there is a transition sequence$\Sigma_{1}arrow’\cdotsarrow!\Gamma,$ $\Sigma_{n}\equiv\vec{\beta},$$!\Gamma$.

(Note that the total amount of modal formulas does not change through transitions, by our restriction on
Then it is easily shown thatfor each $1\leq i\leq n$ in every$\mathcal{L}(S_{1}).)$\S 3.3$\Sigma_{i-1}^{*}\subseteq\Sigma_{i}^{*}$$\Gamma- \mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}.\blacksquare$Completeness of Naive Phase Semantics

To show the reverse of Proposition 2, namely, completeness, we exploit the completeness proof
method investigated by Okada&Terui[23].
First let us give some ideas informally. Given a process configuration, we havethe following transition sequence (derivation);$!\alpha-0\beta\otimes\gamma,$$\alpha$:$!\alpha-0\beta\otimes\gamma,$$\beta,$$\gamma\vdash$$\frac{\overline{!\alpha-\mathrm{O}\beta\otimes\gamma,\beta\otimes\gamma\vdash}}{\frac{!\alpha-0\beta\otimes\gamma,\alpha-0\beta\otimes\gamma,\alpha\vdash}{!\alpha-\circ\beta\otimes\gamma,\alpha\vdash}}$We would like to give a concrete model to this transition sequence and to give a concrete interpretation in the model to each formula occurring in the transition sequence. It is natural toconstruct a model based on preconditions of processes. What we mean by the term preconditionis illustrated in the following transition sequence, where each formula is labelled like $a:B$ withexpressing a precondition of ,
$B$

$B$

$a$

$\frac{\frac{\frac{!\alpha-0\beta\otimes\gamma,.\sqrt{\alpha}l.\beta,\sqrt[\Gamma]{\alpha}.\gamma\vdash}{!\alpha-0\beta\otimes.\gamma,\alpha\cdot\beta.\otimes\gamma\vdash}}{!\alpha-0\beta\otimes\gamma,1\alpha-\mathrm{O}\beta\otimes\gamma,\alpha\cdot\alpha\vdash}}{!\alpha-0\beta\otimes\gamma,\alpha\cdot\alpha\vdash}..\cdot.\cdot..$.
.
.
.
$\bullet$.

$\alpha$occurs in the initial process configuration, hence

itself is a precondition of .

$\alpha$$\alpha$We do not consider preconditions for modal formulas.

has the empty precondition denoted by 1 above because this can be produced
freely by Bang action.
$\alpha-\circ\beta\otimes\gamma$

emerges from two processes
and , which have preconditions 1 andrespectively. Henceis a precondition of.

$\beta\otimes\gamma$$\alpha-0\beta\otimes\gamma$$1\alpha\equiv\alpha$$\beta\otimes\gamma$

and$\alpha$$\alpha$,$\beta\otimes\gamma$

splits into and . Let us consider(the lefl-half of ) to be a precondition of ,(the right-half of ) to be a precondition of .

$\sqrt[\Gamma]{\alpha}$$\beta$$\sqrt[\iota]{\alpha}$$\gamma$$\alpha$$\alpha$$\beta$$\gamma$

The labels express the preconditions which have a natural monoid-structure, thus,and. We can construct a naive phase model from the labels occuring in the abovetransition sequence, in which$1\alpha\equiv\alpha$$\sqrt[\iota]{\alpha}\cdot\sqrt[r]{\alpha}=\alpha$156

if $a:B$ occurs in the transition sequence, then $a\in B^{*}$ .

Hence this model can be seen as a direct representation of the above transition sequence. This-model, because 1 :model is indeed aoccurs in the sequence, hence.
By a construction like the above, we can obtain a countermodel for the completeness proof.
. Then we can construct a naive phase model
Suppose that is not reachable from underin whichand. The resulting phase model is indeed a -model, hence weobtain the completeness.
Let us begin the proof by giving the precise definition of the labels. Our labels are obtained, which was used in his
by modifying the terms of the system ND introduced byproof of completeness for Lambek Calculus with respect to-models. See also
. We modify
for another use of the system-terms by adding the unit label 1 with convention$a1\equiv 1a\equiv a$ , and by imposing commutativity $ab\equiv ba$ on the labels.
$\alpha-0\beta\otimes\gamma$$(\alpha-0\beta \copyright \gamma)$$1\in(\alpha-0\beta\otimes\gamma)*$$\vec{\beta}$$\vec{\alpha}$$!\Gamma,$$\Delta$$\vec{\alpha}\Delta\not\in\otimes\vec{\beta}^{*}$$\vec{\alpha}\Delta\in(\vec{\alpha}, \Delta)^{*}$$\Gamma$$\mathrm{B}\mathrm{u}\mathrm{s}\mathrm{z}\mathrm{k}_{0}\mathrm{w}\mathrm{S}\mathrm{k}\mathrm{i}[4]$$\mathrm{G}\mathrm{S}$$\mathrm{N}\mathrm{D}$Definition 5 The labels$L$$\mathrm{P}\mathrm{a}\mathrm{n}\mathrm{k}\mathrm{r}\mathrm{a}\mathrm{t}’ \mathrm{e}\mathrm{V}[24]$$\mathrm{N}\mathrm{D}$and the simple labels$\overline{L}\subset L$

are defined as follows;

1. 1 is a simple label.

2. Each formula in$\mathcal{L}(S_{1})$

3. if

$a$

is a label and

4. if

$a$

and

is a simple label.

is a formula of the form $B\otimes C$ , then$A$$\sqrt[1]{a}A$and$\sqrt[\prime]{a}A$are simple labels.

are labels, then $ab$ is a label.

$b$

As a convention, we identify
with any of its permutations. Moreover, we assume
.
that
la
for any label . For example,
Now we define a reduction relation on the labels.
$a_{1}a_{2}\cdots a_{n}$$a1\equiv$$\equiv a$$b\sqrt[l]{a1}A\equiv b\sqrt[\iota]{a}A\equiv\sqrt[l]{a}Ab$

$a$

and
Definition 6 For any labels $a’,$ and any formula , if contains as sublabel
by , then we say that a reduces to ,results from by replacing one occurrence of.
denoted by. We denote the reflexive, transitive closure of the
$a’$

$A$

$b$

$a,$

$a$

$\sqrt[l]{b}A\sqrt[r]{b}A$$a$$\sqrt[\mathrm{i}]{b}A\sqrt[r]{b}A$

$a’$

$b$

$a-\prime a’$$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}-\succ \mathrm{b}\mathrm{y}\mapsto^{*}$

Lemma 1 The relation ト\rightarrow *on$L_{1}$

is confluent and terminating.

Proof. This was essentially due to$\mathrm{B}\mathrm{u}\mathrm{s}\mathrm{Z}\mathrm{k}_{0}\mathrm{w}\mathrm{S}\mathrm{k}\mathrm{i}[4]$.

. See also$\mathrm{P}\mathrm{a}\mathrm{n}\mathrm{k}\mathrm{r}\mathrm{a}\mathrm{t}’ \mathrm{e}\mathrm{V}[24]$.

$\blacksquare$to denote
As a corollary, each label has a unique normal form denoted by. Write(ab). Then we can easily derive as sociativity of from the above lemma.
A labelled formula is a formula equipped with a label in normal form (write $a:$ $A$ for a label,:,, $!B_{m},$ $a_{11}$and a formula ). A labelled process configuration is of the form
: $A,$
where each non-modal formula
is notis labelled by a label , whereas each modal formula: ,labelled. If, then: $A$ is sometimes abbreviated by:$a_{nn}$, if, thenandis abbreviated by $b:A,$ $B$ .
The inference rules ofare extended to those for labelled sequents, as follows;
$a$

$a$

$a\cdot b$

$a$

$A$

$!B_{1},$$A_{i}$$\Delta\equiv A_{1},$$\sqrt[l]{b}c:$$\mathrm{e}\mathrm{g}.$$\ldots,$$A_{n}$$\sqrt[r]{b}c:B$$A$$\ldots$$\ldots$$A_{1},$$a_{1}\cdots\cdot\cdot a_{n}$$\ldots,$$\sqrt[l]{b}C:A,$ $\sqrt[r]{b}c:B$$S_{1}$.
$\frac{!\Gamma,\sqrt[l]{a}A\otimes B\cdot.A,\sqrt[r]{a}A\otimes B\cdot B,C.\triangle\vdash}{!\Gamma,a.A\otimes B,C.\Delta\vdash}..\cdot$.

$.. \frac{!\Gamma.a_{1}\cdot.\cdots\cdot a_{n}\cdot b.B)C.\Delta\vdash}{!\Gamma,a_{1}\cdot\alpha_{1},..,an\cdot n\alpha,b\cdot\alpha_{1}\otimes\cdots\alpha_{n}-\mathrm{o}B,C.\Delta\vdash}.,\cdot$.

.
$\frac{!\Gamma,.a.A,c.\Delta..\vdash}{!\Gamma,a.A\ B,c\Delta\vdash}.$Note that if$!\Gamma,$$b:\Delta_{2}\vdash$$!\Gamma,$$a:\Delta_{1}\vdash$.

$\frac{!\Gamma,..a.B,c\cdot\Delta\vdash}{!\Gamma,aA\ B,C.\Delta\vdash}..$$A_{n}$$!B_{j}$$a_{i}$$a_{1}$$a_{n}$$\frac{!\Gamma,!A,1.A.’ c.\Delta\vdash}{!\Gamma,!A,c.\Delta\vdash}.$$\Delta$

157

is an instance of one of the above inference rules, then is identical with .
Letbe. A proof search tree
is a rooted tree where a labelled process
configuration of is as signed to each node, constructed as follows;$b$$\Delta$$A_{1},$$A_{n}$$\ldots,$$a$$\mathcal{T}(!\Gamma, \Delta)$$S_{1}$(1) Process configuration
root;(2) When$!\Gamma,$$a:\triangle$:$A_{1}$$!\Gamma,$$A_{1},$,$\ldots$$A_{n}$:($A_{n}$$A_{i}$is labelled by$A_{i}$

itself) is assigned to theis as signed to a node,’(i) if there is no$a:\Sigma$$!\Gamma,$

such that$!\Gamma,$$a:\Delta^{\prime_{arrow!}}\Gamma,$ $a:\Sigma$, then this node is a leaf of;(ii) otherwise, all sequents of the form
such that:assignments of the children nodes of this node (with assignment$a$$!\Gamma,$

Note thatthe assignments. Let$T(!\Gamma, \Delta)$$\mathcal{T}^{*}(!\mathrm{r}, \triangle)=${$\Sigma$$!\Gamma,$$b:\Sigma|!\Gamma,$ $b:\Sigma,$ $c$: II is a node of$\mathcal{T}(!\Gamma,$$\Delta)$$\Delta’arrow!\Gamma,$ $a:\Sigma$$a$includes all transition sequences starting from$\mathcal{T}(!\Gamma, \Delta)$$!\Gamma,$$a:\triangle^{J}$$!\Gamma,$$A_{1}$:$A_{1},$;, are the).

$\ldots$,$A_{n}$:$A_{n}$

asfor some $c:\Pi$ }.

occurs iniffor some .
The basic properties of labelled proof search trees are expressed in Lemma 2 and Corollary 2,
which play key roles in Lemma 3 and Lemma 4 below. To show Lemma 2, we need two Sublemmas(Sublemma 1 and Sublemma 2), which we state without proofs.
For each label , we define a sequence $O(a)$ of labelled formulas as follows;

We say that a label$b$$T^{*}(!\Gamma, \Delta)$$\Sigma$$b:\Sigma\in \mathcal{T}^{*}(!\Gamma, \Delta)$$a$1. $O(1)=\phi$ (the empty sequence);

2. $O(A)=A:$
3.

$A$

if

$A$

is a formula;$O(\sqrt[l]{b}B\otimes c)=\sqrt[l]{b}B\otimes c:B,$

4. $O(p1\ldots p_{n})=O(p_{1}),$

Sublemma 1 Let(i) $o(b_{1}),$(ii),$\ldots$$b_{n}$:$\Sigma_{1},$$\cdots,$$b_{n}$$b_{i}$:$\Sigma_{n}\in \mathcal{T}^{*}(!\Gamma, \Delta)$$b_{1},$:$p_{i}$;

is a simple label.

. Then;for each .
$i$$\Sigma_{i}$be labels occurring in, $O(b_{n})$ .

$b_{n}$$\ldots,$$O(b_{1}\cdots\cdot\cdot bn)arrow*!\mathrm{r},$ $O(b_{1}),$

Lemma 2 If::$b_{1}$$\Sigma_{1},$$O(b_{i})arrow^{*}!\Gamma,$ $b_{i}$Sublemma 2 Let$!\Gamma,$:, $O(p_{n})$ where each$\ldots$$\mathit{0}_{(b_{n}})\in \mathcal{T}^{*}(!\mathrm{r}, \Delta)$$\ldots,$$!\Gamma,$$b_{1}$$O(\sqrt[r]{b}B\otimes C)=\sqrt[\prime]{b}B\otimes c:c$$\Sigma_{i}\in \mathcal{T}^{*}(!\Gamma, \Delta)$$\Sigma_{n}\in T^{*}(!\mathrm{r}, \triangle)$$\mathcal{T}^{*}(!\Gamma, \Delta)$. If$O(b_{1^{\bullet}}\cdots\cdot b)n\in T^{*}(!\Gamma, \Delta)$.

for each $1\leq i\leq n$ and$b_{1}\bullet$.. .

$\bullet b_{n}$: II$\in \mathcal{T}^{*}(!\Gamma, \triangle)$, thenProof. By Sublemma, hence $O(b_{1}),$,$O(b_{i})arrow*bi:\Sigma_{i}$Sublemma 2. Since::
by Sublemma 1(ii), it easily follows that $b_{11)n}$.
$1(\mathrm{i}),$then$\ldots$$O(b_{1n}\ldots..b)\in \mathcal{T}^{*}(!\Gamma, \triangle)$$\ldots$$O(b_{n})\in \mathcal{T}^{*}(!\mathrm{r}, \Delta)$$\Sigma\cdots,$ $b$$\mathcal{T}^{*}(!\mathrm{r}, \Delta)$

Corollary 2 If each of a,
in
.

$b,$

$c$

and

$a\cdot b\cdot c$occur in$\mathcal{T}^{*}(!\mathrm{r}, \Delta)$, then$a\cdot b,$$b\cdot c$

and$a\cdot c$by$\Sigma_{n}\in$$\blacksquare$also occur$\mathcal{T}^{*}(!\mathrm{r}, \triangle)$

Proof. By definition
for some
and II. Hence by Lemma 2
Corollary 2 follows by definition.
$a:\Sigma_{1}\in \mathcal{T}^{*}(!\mathrm{r}, \Delta),$$\mathcal{T}^{*}(!\Gamma, \triangle)$$\Sigma_{1},$$\Sigma_{2},$$b:\Sigma_{2}\in \mathcal{T}^{*}(!\mathrm{r}, \Delta),$$\Sigma_{3}$$c:\Sigma_{3}\in T^{*}(!\Gamma, \triangle)$and$a\cdot b\cdot c:\Gamma \mathrm{I}\in$$a:\Sigma_{1},$ $b:\Sigma_{2},$ $c:\Sigma_{3}\in T^{*}(!\Gamma, \triangle)$. Then$\blacksquare$

Given a proof search tree
defined above, we construct a naive phase model. In the sequel, stands for.
andstands forconsists of a commutative monoid (also denoted by M) and an$\mathcal{T}(!\Gamma, \Delta)$$\mathcal{M}(!\Gamma, \Delta)$$\mathcal{M}$follows;$\mathcal{T}$$\mathcal{T}(!\Gamma, \Delta)$$\mathcal{T}^{*}$$\mathcal{M}\equiv$$\mathcal{T}^{*}(!\Gamma, \Delta)$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{e}\mathrm{r}_{\mathrm{P}^{\mathrm{r}}}\mathrm{e}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}*\mathrm{d}\mathrm{e}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{e}\mathrm{d}$

as

158

$\bullet \mathcal{M}=${ $a\in L|a$ occurs inoccuring in$\mathcal{T}^{*}$$\mathcal{T}^{*}$.

.

We assume that 1 is always in$\bullet$.

For$a\cdot b=\{$$a,$ $b\in \mathcal{M},$In particular,

For eachLemma 3$\cup\{\sqrt\}$$\mathcal{M}$, where$\sqrt \mathrm{i}\mathrm{s}$. Note that every

ifoccurs inotherwise.
$a\cdot b$$ab\sqrt$$a\cdot\sqrt=\sqrt \mathrm{f}\mathrm{o}\mathrm{r}$$\alpha,$}any

a distinguished propositional variable notis a label in normal form.

$a\in \mathcal{M}$$\mathcal{T}^{*};$.

$a\in \mathcal{M}$$\alpha^{*}=\{b|b:\alpha\in \mathcal{T}^{*}\}\cup\{\sqrt\}$$(\mathcal{M}, \cdot, 1)$

is actually a commutative monoid.

occurs in. If
Proof. Almost immediate. Only nontrivial is associativity, then by Corollary 2,
andoccur in . Hence $(a\cdot b)\cdot c=(a\cdot b)\mathrm{o}c=a\cdot(b\cdot c)=a\cdot(b\cdot c)$ .
, then $(a\cdot b)\cdot c=\sqrt=a\cdot(b\cdot c)$ .
does not occur inIf$\mathcal{T}^{*}$$a$.

$(a\cdot b)\cdot c=a\cdot(b\cdot c)$$a\cdot b$$b\cdot c$$b\cdot c$$\mathrm{o}b\cdot c$$a$$\mathcal{T}^{*}$$\tau*$$\blacksquare$

Lemma 4 For any formula $B,$ $(i)$ if$b:B\in \mathcal{T}^{*}$, then $b\in B^{*}$ , and $(ii)\sqrt\in B^{*}$ .

Proof. (ii) is obvious. Here we only prove (i) by induction on the complexity of$B$.

(Case 1)is an atomic formula. Immediate by definition.
(Case 2) $B\equiv C\otimes D$ .
: $D\in\tau*$ . By induction hypothesis,: $c,$
Assume : $C\otimes D\in\tau*$ . Then.
. Henceand, .
, where(Case 3)
. If $c\cdot b=\sqrt$ , then. It suffices to show that for any
Assume. By definition,
occurs in. Hence we may assume thatby induction hypothesis
for eachand :such that,means that there are labels
an assignment of a node of 7,:
. Hence by Lemma 2,:$c_{11}$. Hence,for some$B$$\sqrt[r]{b}C\otimes D$$\sqrt[\iota]{b}C\otimes D$$b$$\sqrt[r]{b}C\otimes D\in D^{*}$$\sqrt[\iota]{b}C\otimes D\in C^{*}$$\sqrt[r]{b}C\otimes D\in C^{*}\otimes D^{*}$$b=\sqrt[\mathrm{t}]{b}C\otimes D$$B\equiv\otimes\vec{\alpha}-\mathrm{o}D$$\vec{\alpha}=\alpha_{1},$$\alpha_{n}$$\ldots$$b:C-\triangleleft D\in \mathcal{T}^{*}$$c\cdot b$$(\mathrm{i}\mathrm{i})\sqrt\in D^{*}$$c\in\otimes\vec{\alpha}^{*}$$c_{1},$$!\Gamma_{0},$$c_{i}$$c\cdot b\in D^{*}$$c\in\otimes\vec{\alpha}^{*},$$\alpha,$$c_{n}$$\ldots$$c_{1}\cdots\cdot\cdot c_{n}\equiv c$$c_{n}$$\ldots$$\alpha_{n},$$\mathcal{T}^{*}$$b:\otimes\vec{\alpha}-\mathrm{o}D,$$c_{i}$$\alpha_{i}\in\tau*$$d:\Sigma\vdash \mathrm{i}\mathrm{s}$$d:\Sigma$.

$\frac{!\mathrm{r}_{0},c\bullet.b.D,d.\Sigma\vdash}{!\Gamma_{0,1\cdot 1\cdot\cdot,n}c\cdot\alpha,.C.\alpha,b.\Theta\vec{\alpha}-n\mathrm{o}D,d.\Sigma\vdash}..\cdot$, and by induction hypothesis, $c\cdot b\in D^{*}$ .
Therefore
C&D.
B\equiv
Obvious.
(Case 4)
$c\cdot b:D\in \mathcal{T}^{*}$$\blacksquare$

Finally we obtain;

Theorem 2 Let
if and only if$!\Gamma_{0},$$!\Gamma_{0},$$\Delta_{0}$$\Delta_{0}$be a process configuration of .
in every -model.
$S_{1}$$(\vec{\alpha}, \Delta_{0})^{*}\subseteq(\otimes\vec{\beta})^{*}$

Then$\vec{\beta}$

Proof. The only-if part is Proposition 2. To show the. reverse,
. Let
and
from under
By the above construction we get a proof search tree
. We claim the following;
model

)

$\mathrm{s}\mathrm{u}\mathrm{p}\mathrm{J}$$\vec{\alpha}$$!\Gamma_{0},$$\Delta_{0}$$!\Gamma_{0}\equiv!G_{1},$$\ldots,$

is reachable from$\vec{\alpha}$

under$\Gamma_{0}$$!G_{k},$$\Delta_{0}\equiv D_{1},$$\ldots,$$D_{l}$$\mathrm{O}\mathrm{S}\mathrm{e}$that$\beta\equiv\beta_{1},$$\ldots$$\mathcal{T}_{0}\equiv \mathcal{T}(!\Gamma_{0},\vec{\alpha}, \Delta 0)$

is not reachable,.
and a naive phase$\vec{\beta}$$\beta_{m}$$\mathcal{M}_{0}\equiv \mathcal{M}(!\Gamma_{0},\vec{\alpha}, \Delta 0)$(1)$\mathcal{M}_{0}$constructed above is a$\Gamma_{0}$-model.

(2) In$\mathcal{M}_{0}$, label$D_{1}D_{2}\cdots D_{l}$is in(3) In$\mathcal{M}_{0}$, label$D_{1}D_{2}\cdots D_{l}$is not$(\vec{\alpha}, \Delta_{0})^{*}$$\mathrm{i}\mathrm{n}\otimes\vec{\beta}^{*}$.
.

. (2) also follows. Hence by Lemma 4,
in
As for (1), 1 :for each
D_{1}\cdots
D_{l}$ .
$a\equiv
Hence, it,:wherefrom Lemma 4. As for (3), by as sumption
for each and,such thateasily follows by Lemma 2 that there are no labels.
$G_{i}\in \mathcal{T}^{*}0$$!G_{i}$$1\in G_{i}^{*}$$!\Gamma_{0}$$!\Gamma_{0},$$a$$\vec{\beta}\not\in T_{0}$$a_{1)}\ldots$$a_{1}\cdots\cdot\cdot a_{n}\equiv D_{1}D_{2}\cdots D_{l}$$a_{n}$$a_{i}\in\beta_{i}^{*}$$i$$\blacksquare$

159

\S 4

Algebraic Semantics Characterizing Trace Equivalence\S 4.1

Trace Equivalence

In this Section we introduce the notion of trace equivalencein our system of process
calculus, and give the characterization of the equivalence by means of model-theoretic semantics.
We introduce the system
in which implications are restrictied to the ones of the form
and two inference rules that express observable actions are added. These observable actions are
not inference rules of linear logic, but it enables us to estimate observable effects of processes in a
precise manner. Then we define the notion of trace and trace equivalence on processes (or process
configurations) in systemin terms of these observable actions.
We also introduce the system
which has the infinitary&expressions.
can express, forexample, value passing between processes (See Example 2 in \S 2).
Trace equivalence is a simple and intuitive notion, but has certain shortcomings. Among them,
it is often pointed out (cf. van Glabbeek [29],) that it identifies too many processes,
in particular it possibly identifies a deadlocking process with one that does not deadlock. We
shall briefly mention this point in Example 3(2). Nevertheless, trace equivalence deserves carefulanalysis, because it can be seen as the basis for other equivalences finer than this equivalence.
A relationship between the notion of trace and that of reachability is established in Proposition 3.
$(\mathrm{H}_{0}\mathrm{a}\mathrm{r}\mathrm{e}[7])$$\alpha-\mathrm{o}B$$S_{2}$$S_{2}$$\overline{S_{2}}$$\overline{S_{2}}$$\mathrm{M}\mathrm{i}\mathrm{l}\mathrm{n}\mathrm{e}\mathrm{r}[17]$Definition 7 The languageofis obtained by restricting
so that if a formula incontains
as subformula, then is a propositional variable a.
$S_{2}$$\mathcal{L}(s_{2})$$\mathcal{L}(S)$$A-\mathrm{o}B$$\mathcal{L}(s_{2})$$A$

has the following two actions in addition. These are called observable actions, while theactions described in \S 2 is called silent, since those actions are completely taken inside thesystem, and an external observer outside the system cannot observe them.
$S_{2}$$acti_{on}\mathit{8}$$\bullet$

Input Action$(\alpha)$$P\Gamma\vdash$–,$\alpha-\mathrm{o}P,$.

$\alpha$$\Gamma\vdash$(Input action gets a token from the outside of the system. This action is understood tobe always possible no matter what the environment is.)$\alpha$Output Action$\alpha$$(\overline{\alpha})$$\Gamma\vdash$$-\overline{\alpha}$$\Gamma\vdash$$\alpha,$(Output action$\overline{\alpha}$

throws away a token$\alpha$to the outside of the environment.)

Of course, observable actions are not logical inference rules at all. The point of introducing
these actions is that it enables us toprocess behavior from the outside of the system, andby means of these actions we can define the notion of trace eqivalence.
with infinitary&described in \S 2 Example 2.
We also introduce system , which extends$ob_{\mathit{8}}erve$$\overline{S_{2}}$Definition 8 The language
1. if$\alpha\in \mathcal{P}$

2. if
set,

, then$A_{i}\in \mathcal{L}(s_{2})$3. if$\overline{S_{2}}$$\mathcal{L}(\overline{S_{2}})$$S_{2}$

is defined as follows;$\alpha\in \mathcal{L}(\overline{S_{2}}))$, (i.e.,$A_{i}$

contains$\mathrm{n}\mathrm{o}\ _{j\in J}$) for each $i\in I$ , where$I$

denotes an arbitrary index;$\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{n}\ _{i\in I}A_{i}\in \mathcal{L}(\overline{S_{2}})$$\alpha\in \mathcal{P},$$A,$ $B\in \mathcal{L}(\overline{S_{2}})$, then$\alpha-\mathrm{o}A,$$A\otimes B$, A&B and !A are in

has the following inference rule in addition to those of$\frac{A_{j},\Gamma\vdash}{\ _{i\in I}Ai,\Gamma\vdash}$,$S_{2}$;$\mathcal{L}(\overline{S_{2}})$

.

160

where $j\in I$ .
It is clear that$\overline{s_{2}}$.

is a conservative extension of$S_{2}$. All results stated below hold both for$S_{2}$

and$\mathrm{f}_{\mathrm{o}\mathrm{r}}\overline{S_{2}}$Let Act beandbe the set of all finite sequences over Act. In
particular, the empty sequence is inand denoted by 1. For $t\equiv p_{1}\ldots p_{n}\in Act^{*}$ , we define$len(t)=n$ . In the sequel,range over Act*.
Now the transition relation $arrow$ , defined in \S 2, is reformulated for the labelled transition relation
as follows;$Act^{*}$$\{\alpha|\alpha\in \mathcal{P}\}\cup\{\overline{\alpha}|\alpha\in \mathcal{P}\}$$Act^{*}$$s,$ $t,$ $u,$$\ldots$

Definition 9
if$\Gammaarrow\triangle p$$\bullet$$\frac{\Delta\vdash}{\Gamma\vdash}p$is an instance of an inference rule ofthe inference.

.

$\Gammaarrow^{*}\Delta$

if

...

$\Gammaarrow p_{1}$$arrow\Delta p_{m}$$S_{2}$

with$p$

indicating the action name corresponding to(possibly $m=0$ ) where each

For each $t\in Act^{*}$ , we define a binary$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}\Rightarrow^{t}$$len(t))$ as follows;

If $len(t)=0$ then$\bullet$$t\equiv 1$. We define$\Gamma\Rightarrow^{1}\Delta$by

If is of the form $pt’$ , where $p\in Act,$ then.
$t$$\bullet$$p_{i}$

is a silent action.

on process configurations by induction on$\Gammaarrow^{*}\Delta$$\Gamma\Rightarrow^{t}\Delta$;

holds whenever there is a$\Gamma’$such that$\Gammaarrow^{*}arrowarrow^{*}\Gamma’pt’\Rightarrow\Delta$

Let be a process configuration ofof and write. Define$tr(\Gamma)=tr(\Delta)$ .
$\Gamma$$\Gamma\Rightarrow^{t}$$\Gamma$$S_{2}$. If

for some. Then and$\Gamma\Rightarrow^{t}\Gamma’$$tr(\Gamma)=\{t|\Gamma\Rightarrow^{t}\}$$\Gamma$$\Gamma’$$\Delta$, we say that $t\in Act^{*}$ is a trace
are said to be trace equivalent if

Example 3 Consider the processes below,$\Rightarrow\overline{\beta}$(1)$\alpha-0$\beta &\alpha -01$tr(\alpha-\circ$\beta &\alpha -01$\emptyset$$\Rightarrow\Rightarrow$$\beta 0$$)=\{1, \alpha, \alpha\overline{\beta}\}=tr(\alpha-0\beta)$$\Rightarrow\overline{\alpha}$(2) (!\alpha )&\alpha. Hence$\alpha-0$\beta &a-ol is trace equivalent to a-o .
$\beta$$!\alpha\Rightarrow\overline{\alpha}\ldots$$\overline{\Rightarrow}\Rightarrow\overline{\alpha}$$!\alpha\emptyset$

This process is trace equivalent to . This exemplifies a drawback of trace equivalence; (!a)&\alphamay deadlock whereas
never deadlock, but they are taken to be the same if we adopt trace
equivalence.
$!\alpha$$!\alpha$(3)tr(\alpha \otimes (\beta &7))

$=$

$=$

$\{1, \overline{\alpha},\overline{\alpha}\overline{\beta},\overline{\alpha\gamma},\overline{\beta},\overline{\beta}\overline{\alpha},\overline{\gamma})\overline{\gamma\alpha}\}$tr(\alpha \otimes \beta &\alpha \otimes 7).

Hence, \alpha \otimes (\beta &7) is trace equivalent to \alpha \otimes \beta &\alpha \otimes 7.

$\blacksquare$

Given $t\in Act^{*}$ , let $Inp(t)$ be the multiset {and a is an input action} and let Out $(t)$be the multiset {and is an output action}. The following Proposition shows the relationship between the notion of reachability and that of trace;$\alpha|\alpha\in t$$\alpha|\overline{\alpha}\in t$$\overline{\alpha}$

Proposition 3 If
whereconsists of modal formulas, then out $(t)$ is reachable from
$Inp(t)$ under . Conversely, if
is reachable from under , then there are $t\in Act^{*}$ and ,$Inp(t)=\vec{\alpha}$ andsuch that.
$\Gamma\Rightarrow^{i}!_{-}^{-}-$$!_{-}^{-}-$$\Gamma$$\Gamma\Rightarrow^{t}!_{-}^{-}-,$$\vec{\beta}$$\vec{\alpha}$$o_{u}t(t)=\vec{\beta}$$\Gamma$$!_{-}^{-}-$

161\S 4.2

Trace Models

Our next purpose is to characterize trace equivalence by means of model-theoretic semantics.
To this end, we introduce an algebraic model, called a trace model, and show soundness andcompleteness for trace equivalence with respect to the trace models.

..

Definition 10 A trace algebra $<D,$.
.

$1,$ $\otimes,$$-0,A>\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{S}\mathrm{i}\mathrm{s}\mathrm{t}\mathrm{s}$of the following;$A\subseteq D$

$<D,$

order

$\bullet<D,$$\bullet$$\wedge,$$\wedge,$$1>$ is a complete meet semilattice with maximal element 1.

$1>\mathrm{i}\mathrm{s}$$\otimes,$

We define a partial

by $p\leq q^{d}g_{p}^{e}\wedge q=p$ .

$\leq \mathrm{o}\mathrm{n}D$

a commutative monoid.

: $A\cross Darrow D$ . We writewhen we write).
$-0$$a-\mathrm{o}p$to$\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}-\mathrm{o}(a,p)$(in the sequel we assume that $a\in A$$a-\mathrm{o}p$$a\otimes(a-\mathrm{o}p)\leq p,$ $p\otimes(a-\circ q)\leq a-\mathrm{O}(p\otimes q)$$\bullet$$\otimes distributesover\wedge$$\bullet$$\infty$, i.e.,$\bigwedge_{i\in I}q\otimes p_{i}=q\otimes\bigwedge_{i\in I}p_{i}$distributes $over\wedge$ , i.e.,

The expansion law (cf.
$b-\triangleleft((a-\circ p)\otimes q)$.

.

$\bigwedge_{i\in I}a-\mathrm{o}p_{i}=a-0\bigwedge_{i\in I}p_{i}$) holds, i.e., $(a-\mathrm{o}p)\otimes(b-\mathrm{o}q)=a-\infty(p\otimes(b-\mathrm{o}q))$ A$\mathrm{M}\mathrm{i}\mathrm{l}\mathrm{n}\mathrm{e}\mathrm{r}[16][17]$.

In a trace algebra bang operator ! is defined bynumbers and denotes.

$!p= \bigwedge_{i\in N}p^{i}$, where $N$ is the set of natural$p^{i}$$-p\otimes\cdots\otimes p$

.

times

$i$

The following are easily derived in a trace algebra.

If $p\leq q$ then$\bullet p\otimes q\leq p$.

$\bullet!p\leq p,$$r\otimes p\leq r\otimes q$

and$a-\mathrm{o}p\leq a-\mathrm{o}q$.

.

$!p\otimes!p=!p$$!(p\wedge q)=!p\otimes!q$. If $!p\leq q$ then $!p\leq!q$ .

.

Definition 11 A trace model is a trace algebra with anmaps ainto. In a trace model, nonatomic formulas and process configurations are interpreted
as follows;$interpretation\mathrm{w}\mathrm{h}*\mathrm{i}_{\mathrm{C}\mathrm{h}}$$\in \mathcal{P}$$\alpha^{*}\in A(\subseteq D)$$\bullet(A\otimes B)^{*}=A^{*}\otimes B^{*};$.

$\bullet(\alpha-\circ B)^{*}=\alpha^{*}-\mathrm{o}B^{*})$$\bullet$.

(A&B)* $=A^{*}\wedge B^{*};$$\bullet(!A)^{*}=!(A^{*})$$( \ _{i\in I}A_{i})^{*}=\bigwedge_{i\in I}A_{i}^{*};$;$(A_{1}, \ldots, A_{n})^{*}=A_{1}\otimes\cdots\otimes A_{n}$, in particular the empty process configuration is interpretedby 1.

Remark that !A has the same interpretation. This reflects the syntactic observationthat $tr(!A)=tr(\ _{i\in N}A^{i})$ (cf. Lemma 6).
The trace models characterize trace equivalence, in the form of completeness theorem below;$\mathrm{a}s\ _{i\in N}A^{i}$

Theorem 3 $tr(A)=tr(B)$ if and only if $A^{*}=B^{*}$ in every trace model.
We prove the “only-if” part (soundness) in \S 4.3 (Corollary 3) and the “if” part (completeness)in \S 4.4 (Corollary 4).

162\S 4.3

Soundness of Trace Models

Through this subsection we fix a trace model $D=<D,$$-0,$ $A>$ . We cannot use the usual
induction on the length of proof to show the soundness of trace models, since we deal with possibly
infinite proof constructions that do not reach any axiom. Instead, the proof below proceeds asfollows;$\wedge,$$1,$ $\otimes,$

1. Assign $[t]\in D$ to each $t\in Act^{*};$
2. Define the observation value of

3. Show that $[A]=A^{*}$ for any

$A$

by

$\bigwedge_{A\Rightarrow}t[t]$$A\in \mathcal{L}(s_{2})$;.

Soundness easily follows from 3. It should be noted thatabove is the interpretation of
inductively defined along Definition 11, while $[A]$ is completely determined by the traces of ; todetermine $[A]$ , one does not have to know what exactly is. It is sufficient to know its observablebehavior, i.e., its traces.
First we inductively define a ternary
as follows;$A$$A^{*}$$A$$A$$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}_{-}}\triangleleft-^{\mathrm{O}}-\subseteq Act^{*}\mathrm{x}Act^{*}\mathrm{x}Act^{*}$.

$\bullet 1\triangleleft 101$

If.

$u\triangleleft s\circ t$, then$\alpha u\triangleleft s\circ\alpha t,$$\alpha u\triangleleft\alpha s\mathrm{o}t,$$u\triangleleft\alpha s\mathrm{o}\overline{\alpha}t$, and$u\triangleleft\overline{\alpha}s\mathrm{o}\alpha t$

for any$\alpha$.

Then we define $F(s, t)\subseteq Act^{*}$ by $F(s, t)=\{u\in Act^{*}|u\triangleleft s\mathrm{o}t\}$ .

Lemma 5
Proof.

$\Gamma,$($‘ \mathrm{I}\mathrm{f}$”$\Delta\Rightarrow u$

if and only if $u\in F(s, t),$$\Gamma\Rightarrow^{S}$

and

that

$s,$

$t$

.

$u\triangleleft s\mathrm{o}t$$\Delta\alpha t’\Rightarrow$$\Gamma’$$u’\triangleleft S^{;_{\mathrm{o}t}\prime},$$\Delta’\Rightarrow t’$$\Gamma’\Rightarrow S^{J}$$\Delta’$$\Deltaarrow^{*}\Gamma J,$$\Gamma,$for some

part: By induction on the generation of. We treat only the case whenis derived fromand
. Then there are some
and
such
and
holds, therefore
andhold. By induction hypothesis,
holds.
$\Delta*$part:means that there is a finite transition sequence$\Gamma\Rightarrow\overline{\alpha}s’$$u’\triangleleft\overline{\alpha}s’\mathrm{o}\alpha t^{J}$$\Delta\Rightarrow^{t}$$\Delta’$$\Delta’\Rightarrow u^{J}$$\mathrm{r}^{J},$$\Delta’\Rightarrow u’$$\Gamma,$$\Deltaarrow^{*}\Gamma’,$’$(‘ \mathrm{O}\mathrm{n}\mathrm{l}\mathrm{y}-\mathrm{i}\mathrm{f})$$\Gamma,$

and
(1)
(2)
(3)

$\Gamma_{0},$$\Gamma,$$\Delta\equiv \mathrm{r}_{0},$$\Delta \mathrm{p}_{1}1arrow p_{2}$$\Delta 0arrow\Gamma_{1},$$\Delta_{n}p_{n}$. $..arrow\Gamma_{n},$holds, where for each $1\leq i\leq n$ one of the following holds;
and
and
and
.

$\Delta$$\Delta_{0}*\Gamma_{nn},$$\Gamma_{i-1}arrow\Gamma_{i}p$$\Gamma_{i-1}\equiv\Gamma_{i}$$\Gamma_{i-1}\not\equiv\Gamma_{i}$$\triangle_{i-1}\equiv\Delta_{i;}$$\Delta_{i-1}arrow\Delta_{i;}p_{l}$$\triangle_{i-1}\not\equiv\Delta_{i}$We defineby induction on . If $i=0$ , thenand.
When (1) holds for $i\geq 1$ , then. Ifis an observable action, thenotherwise.
When (2) holds for $i\geq 1$ , similar to the previous case.
When (3) holds for $i\geq 1$ , then must be a receiving action, and either(3a)andholds for some , or(3b)
andholds for some .
If (3a) is the case, then
. If (3b) is the case, thenand$s_{i}\in Act^{*}$$t_{i}\in Act^{*}$$i$$t_{i}\equiv t_{i-1}$$s_{i}\equiv t_{i}\equiv 1$$p_{i}$$s_{i}\equiv S_{i-1p_{i};}$$s_{i}\equiv s_{i-1}$$p_{i}$$\Gamma_{i-1}arrow\Gamma_{i}\alpha$$\Delta_{i-1}arrow\triangle\overline{\alpha}$$\Gamma_{i-1}arrow\Gamma_{i}\overline{\alpha}$$\Delta_{i-1}arrow\triangle\alpha$$\alpha$$\alpha$$s_{i}\equiv s_{i-1}\alpha$$t_{i}\equiv t_{i-1}\alpha$$t_{i}\equiv t_{i-1}\overline{\alpha}$$s_{i}\equiv s_{i-1}\overline{\alpha}$and.

By the above construction, we see that $u\in F(s_{n}, t_{n}),$Lemma 6$!A\Rightarrow u$

if and only if$A^{n}\Rightarrow u$$\Gamma\Rightarrow s$

and$\Delta\Rightarrow t$.

$\blacksquare$for some $n\in N$ .

Proof. Obvious.
Remark: This lemma shows that, in$\blacksquare$$\overline{S_{2}}$, our bang !A is equivalent$\mathrm{t}\mathrm{o}\ _{i\in N}A^{n}$

up to traces.

163

Definition 12 For $t\in Act^{*}$ , we define $[t]\in D$ as follows;$\bullet[1]=1(\in D)$;$\bullet[\overline{\alpha}t]=\alpha^{*}\otimes[t]$;$\bullet[\alpha t]=\alpha^{*}-0[t]$.

.

The observation value of$[A]= \bigwedge_{A\Rightarrow}t[t]$$A$

is defined by.

Lemma 7 $\bigwedge_{u\in F()}s,t[u]=[s]\otimes[t]$ .
Proof. By induction on $len(s)+len(t)$ . Since other cases are similar, we only treat the casewhen is of the form
and is of the form.
$\alpha s’$$s$$\overline{\alpha}t’$

$t$

$=$
$u’ \in F(S’’\overline{\alpha}t)\wedge,[\alpha u^{J}]\wedge\wedge[\overline{\alpha}u’]\wedge\bigwedge_{uu^{l}\in F(\alpha s^{l},t)\in F(S^{l}t^{l})},[u’]J$$u \in F(\alpha S\bigwedge_{\prime J\overline{\alpha}t)},[u]$’$=$$\wedge,\alpha-\circ[u]’\wedge\bigwedge_{)S\overline{\alpha}tJJ)u\in;F(\alpha St\prime,\prime}\alpha\otimes[u’]$$u’\in F$$=$

A $u’\in F(S)\wedge[u’tJl$

(

$]$

)

$\alpha-\mathrm{O}$$\bigwedge_{\prime,u’\in F(s\overline{\alpha}t\prime)},[u]J\alpha\wedge\otimes\bigwedge_{)}[u]’\wedge$$\bigwedge_{\prime,u\prime\in F(\alpha S\prime t\prime)u’\in F(stl)},[u’]$$=$$\alpha-\mathrm{o}([S]’[\otimes\overline{\alpha}t]’)\wedge\alpha\otimes([\alpha s’]\otimes[t’])\wedge([s’]\otimes[tl])$$=$$\alpha\infty([_{S’}]\otimes(\alpha\otimes[t’]))\wedge\alpha\otimes((\alpha-0[S’])\otimes[t^{J}])\wedge([s’]\otimes[t’])$$=$$\alpha\otimes((\alpha-\mathrm{O}[s]’)\otimes[t’])$$=$$[\alpha s’]\otimes[\overline{\alpha}t^{J}]$.

The expansion law is needed in the case when$s$is of the form$\alpha s’$

and

$t$

is of the form$\beta t’$.

$\blacksquare$

Lemma 8 $[P^{n}]=[P]^{n}$ .

Proof. Obvious.

$\blacksquare$

Now we obtain the main proposition with the help of the above Lemmas.

Proposition 4 In every trace model, $[A]=A^{*}$ .

Proof. By induction on the complexity of .
Case 1) is a propositional variable. Obvious.
Case 2) is of the form $B\otimes C$ .
$A$

$A$
$A$

$[B\otimes C]$

Case 3)$A$

Case 4)$A$$=$$\bigwedge_{B\otimes c\Rightarrow}u[u]=\bigwedge_{B,C\Rightarrow}\mathrm{u}[u]=\bigwedge_{B\Rightarrow}s\bigwedge_{C\Rightarrow}t\bigwedge_{u\in F(,)}St[u]$$=$$\bigwedge_{B\Rightarrow^{\mathit{5}}}\bigwedge_{C\Rightarrow}2[\mathit{8}]\otimes[t]$$=$$\bigwedge_{B\Rightarrow^{S}}[s]\otimes\wedge c^{t}\Rightarrow[t]$$=$$[B]\otimes[C]=B^{*}\otimes C^{*}$(by Lemma 5)(by Lemma 7)(by induction hypothesis)

is of the form $!B$ . By Lemma 6 and Lemma 8.
is of the form B&r . Obvious.
$C$$\blacksquare$Soundness is almost immediate if we take into consideration that the observation value of aformula is completely determined by its traces.
Corollary 3 (Soundness) If $tr(A)=tr(B)$ then $A^{*}=B^{*}$ in every trace model.

164\S 4.4Completeness of Trace Models

The proof of completeness employs the usual canonical model construction for (phase semantic)
in whichcompleteness proof (cf.
). We construct a syntactic (canonical) model of
implies $tr(\Gamma)\supseteq tr(A)$ (Proposition 5). Then the completeness (Corollary 4) directly$tr(A)$ in systemfollows. It is trivial that for any formulas inis equivalent to $tr(A)$ in, hence we have the completeness forat the same time.
For each $t\in Act^{*}$ , we define
as follows;$\overline{S_{2}}$$\mathrm{O}\mathrm{k}\mathrm{a}\mathrm{d}\mathrm{a}[22]$$\Gamma\in A^{*}$$A$$S_{2}$$\mathcal{L}(S_{2}),$$\mathrm{s}\mathrm{y}_{\mathrm{S}\mathrm{t}\mathrm{e}\mathrm{m}}\overline{S_{2}}$$S_{2}$$t\in\sim \mathcal{L}(\overline{S_{2}})$$\bullet\sim 1=1(\in L(\overline{S_{2}}))$;,$\bullet\overline{\overline{\alpha}t}=\alpha\otimes t\sim.$.

$\bullet\overline{\alpha t}=\alpha-\mathrm{o}t\sim$.

We define a phase space-like structure$\bullet$$\bullet$Let$\mathcal{M}$be the free commutative monoid generated by all formulas in

For each $t\in Act^{*}$ , define$D$

as follows;$\mathcal{M}$, and for each$\mathrm{I}^{t}\mathrm{I}=\{\Gamma|\Gamma\Rightarrow\}t$$i\in\Lambda$$\bullet A=\{[\alpha \mathrm{J}|\alpha\in \mathcal{P}\}$.

$[A \mathrm{J}=\bigcap_{A\Rightarrow}2[t\mathrm{J}$is defined in such a way that $X\in D$ if and only if $X$ is of the form
for each. Then clearly [for any.

$t_{i}\in Act^{*}$

.
where

$\bigcap_{i\in\Lambda}\mathrm{I}t_{i}\mathrm{I}$$A\in \mathcal{L}(\overline{S_{2}})$$A\mathrm{I}\in D$.

It is easily seen that [$A\mathrm{J}=\{\Gamma|tr(\mathrm{r})\supseteq tr(A)\}$$(\#)$$A\in \mathcal{L}(\overline{S_{2}}),$$\mathcal{L}(\overline{S_{2}})$for any $X\in D$ , if$\Gamma\in X$

and

and

$\mathrm{M}t=[t\mathrm{J}$$tr(\Delta)\supseteq tr(\Gamma)$then. Moreover, we observe that$\triangle\in X$.

On this structure, we can define phase-semantic operations &and, then$\otimes \mathrm{a}\mathrm{s}$in \S 3.1; let$X\subseteq \mathcal{M}$,$Y\subseteq \mathcal{M}$$\bullet$$\bullet$$X \ Y=X\cap Y;\ _{i\in I}X_{i}= \bigcap_{i\in I}x_{i;}$$X\otimes Y=(XY)c=\cap\{[t\mathrm{I}|XY\subseteq \mathbb{I}^{t}\mathrm{I}\}$, where $XY=\{\Gamma, \triangle|\Gamma\in X, \Delta\in Y\}$ .

The interpretation of-o is modified; let $X\in A$ andis uniquely determined), and we define$\alpha$$!X$.

$[\alpha \mathrm{I}\infty Y=\cap\{[\alpha t\mathrm{I}|Y\subseteq[t\mathrm{I}\}$is defined by$X\subseteq \mathcal{M}$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{b}*\mathrm{y}\alpha*=[\alpha \mathrm{J}$Proposition 5 (i) $D\equiv<D,$(ii) For every formula$\cap,$$1,$ $\otimes,$$A\in \mathcal{L}(\overline{S_{2}}),$, then $X$ is of the form [$\alpha \mathrm{J}$(such an.

for eachfor each
Then we show the following;$\bigcap_{i\in N}X^{i}$$Y\subseteq \mathcal{M}$$a$$\in \mathcal{P}$. $1=[1\mathrm{J}=\{\Gamma|\Gamma\xi\}=$ M. Finally we define an. It is obvious that $A^{*}\in D$ for each$A\in \mathcal{L}(\overline{S_{2}})$.

$-0,A>and$ *defined above form a trace model.
.

$A\in A^{*}\subseteq \mathbb{I}^{A}\mathrm{I}$

From this, the completeness easily follows;
Corollary 4 (Completeness) If $A^{*}=B^{*}$ in every trace model, then $tr(A)=tr(B)$ .
$A^{*}=B^{*}$ holds in $D$ defined above. By ProposiProof of Completeness. By Proposition
A^{*}$$A\in
B^{*}$$A\in,, which in turn implies, that means
tion
hence
by Proposition$tr(A)\supseteq tr(B)$ . $tr(A)\subseteq tr(B)$ is shown similarly.
$5(\mathrm{i}),$$A\in[B\mathrm{J}$$5(\mathrm{i}\mathrm{i}),$$5(\mathrm{i}\mathrm{i})$$\blacksquare$

Proof of Proposition 5. First we show (ii) by induction on the complexity of(Case 1) is a propositional vairable. By definition.
$A$

$A$

.

165

is of the form a-o . First we prove that $a-\mathrm{o}B\in(\alpha-\circ B)^{*}=[a\mathrm{J}-\mathrm{o}B^{*}=$. It suffices to show thatfor each such that
Since
$B\in B^{*}$ by induction hypothesis,, that means. Hence a. Therefore(Case 2)$A$

$B$$\cap\{[\alpha t\mathrm{I}|B^{*}\subseteq[t\mathrm{I}\}$$\alpha \mathrm{r}B\in[\alpha t\mathrm{J}$$t$$B^{*}\subseteq[t\mathrm{I}\cdot$$B\Rightarrow t$$B\in \mathrm{I}^{t}\mathrm{I}$$-\mathrm{o}B\Rightarrow\alpha t$$\alpha-\mathrm{o}B\in[\alpha t\mathrm{I}\cdot$

To prove, assume $\Gamma\in(a-\mathrm{o}B)*$ . Thenfor any. In particular,
for any, sinceby induction hypothesis. Therefore,
for any. Then it follows that
because$(\alpha-\mathrm{o}B)^{*}\subseteq \mathbb{I}\alpha-\mathrm{o}B\mathrm{I}$$\Gamma\in[\alpha t\mathrm{J}$$\Gamma\in \mathbb{I}\alpha t\mathrm{J}$$\mathbb{I}t\mathrm{I}\supseteq \mathbb{I}B\mathrm{I}$$\mathbb{I}t\mathrm{I}\supseteq B^{*}$$B^{*}\subseteq \mathbb{I}B\mathrm{I}$$\Gamma\in \mathrm{I}at\mathrm{J}$$B\Rightarrow^{t}$$\Gamma\in[\alpha-\mathrm{o}B\mathrm{I}$(Case 3)is of the form $B\otimes C$ . By induction hypothesis, $B\in B^{*}$ and $C\in C^{*}$ . Hence. It is immediate that $B\otimes C\in(B^{*}C^{*})c=B^{*}\otimes C^{*}$ by $tr(B, C)=tr(B\otimes C)$ and$A$$B,$ $C\in B^{*}C^{*}$$(\#)$$\mathrm{I}\alpha-\mathrm{o}B\mathrm{I}=\mathrm{n}_{\alpha-\mathrm{o}B^{u}}\mathbb{I}\Rightarrow u\mathrm{I}=\bigcap_{B\Rightarrow}p[\alpha t\mathrm{I}\cdot$.

On the other hand,[CI, sinceandby induction hypothesis.
is shown by the observation that if $tr(\Gamma)\supseteq tr(B)$ and $tr(\Delta)\supseteq tr(C)$ , then$tr(\Gamma, \Delta)\supseteq tr(B, C)=tr(B\otimes C)$ . Finally we infer
from.
$B^{*}C^{*}\subseteq \mathbb{I}B\mathrm{J}$[$B^{*}\subseteq[B\mathrm{J}$$C^{*}\subseteq[C\mathrm{I}$$B\mathrm{I}[c\mathrm{I}\subseteq \mathrm{I}B\otimes C\mathrm{J}$$B^{*}C^{*}\subseteq[B\otimes C\mathrm{J}$$B^{*}\otimes C^{*}\subseteq \mathbb{I}^{B}\otimes C\mathrm{J}$(Case 4) is of the form B&C. This is a special case of (Case 6) below.
(Case 5) is of the form $!B$ . By induction hypothesis, $B\in B^{*}$ . Since $tr(!B)\supseteq tr(B),$ $!B\in B^{*}$ .
Hence we see that
$A$

$A$

$!B,$ $\ldots,$ $!B\in B^{*}\otimes\cdots\otimes B^{*}$$arrow$ –$n$for eachby$(\#),$

times$n\in N$times
. On the other hand, it can be easily shown that$n$$!B\in(B^{*})^{n}$$tr(!B)=tr$ . Therefore,$n$

for each , thus $!B\in!B^{*}$ .

times

$n$

To show, supposeand. Then, using
induction hypothesis, we can prove that
I for each . On the other hand, by Lemma 6,
if and only if
for some $n\in N$ . Henceand we conclude.
$\Gamma\in \mathbb{I}^{B^{n}}$$!B\Rightarrow^{t}$$!B\Rightarrow t$$\Gamma\in\bigcap_{n\epsilon N}B^{*n}$$!B^{*}= \bigcap_{n\in N}B^{*n}\subseteq[!B\mathrm{J}=\bigcap_{1B\Rightarrow}t[t\mathrm{J}$$n$$B^{n}\Rightarrow t$$!B^{*}\subseteq[!B\mathrm{J}$$\Gamma\in \mathrm{I}^{t}\mathrm{I}$(Case 6)$A$

is of the form
. By induction hypothesis,
for each $i\in I$ . Since, we see by
for each $i\in I$ . Therefore,.
is almost immediate from induction hypothesis.
$\ _{i\in I}B_{i}$$tr(\ _{i\in I}B_{i})\supseteq tr(B_{i})$$B_{i}\in B_{i}^{*}$$(\#)\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}\ _{i\in I}B_{i}\in B_{i}^{*}$$\ _{i\in I}B_{i}\in\bigcap_{i\in I}B_{i}*$$\ _{i\in I}B_{i}^{*}\subseteq \mathrm{I}\ _{i\in I}B_{i}\mathrm{I}$Now let us show (i). First note that we can obtain more strong result than (i);holdsfor each. Suppose, then $tr(\Gamma)\supseteq tr(A)$ . By (i) and
we obtain that.
Here we only show the expansion law and the distribution law. The otherlaws are shown similary. Note that each element in $A$ is of the form [ and each element in $D$ isof the form
The expansion law is proved as follows;$A^{*}=[A\mathrm{I}$$A\in \mathcal{L}(\overline{S_{2}})$$\Gamma\in A^{*}$$(\#)$$\Gamma\in[A\mathrm{J}$$\mathrm{b}\mathrm{e}\mathrm{t}\mathrm{w}\mathrm{e}\mathrm{e}\mathrm{n}\otimes \mathrm{a}\mathrm{n}\mathrm{d}\cap$$\alpha \mathrm{J}$$\bigcap_{i\in I}[t_{i}\mathrm{I}=\bigcap_{i\in I}[t_{i}\sim \mathrm{I}\cdot$$([ \alpha \mathrm{I}-\mathrm{o}\mathrm{n}i\in I[ti\mathrm{I})\otimes([\beta \mathrm{I}-\mathrm{O}\bigcap_{jj}\in \mathrm{I}Sj\mathrm{I})=[(a-0\ _{i} \in It\sim i)\otimes(\beta-\mathrm{O}\ i \in Jsj)\sim \mathrm{I}$$=[\alpha-\mathrm{o}(\ _{i\epsilon Ii}t\otimes(\sim\sim\beta\infty\ _{j}S)\in Ji\sim)\ \beta-\mathrm{o}((\alpha-\mathrm{O}\ _{i}t_{i}\epsilon I)\otimes\ _{j}Js\epsilon j)\sim \mathrm{I}$$(*)$$=\mathrm{I}\alpha \mathrm{J}-\circ(\cap i\in I\mathbb{I}ti\mathrm{I}\otimes([\beta \mathrm{J}-0\cap j\epsilon J[Sj\mathrm{I}))\cap[\beta \mathrm{I}-\mathrm{o}(([\alpha \mathrm{I}-\mathrm{o}\mathrm{n}i\in I\mathbb{I}^{t}i\mathrm{I})\otimes\cap j\in j[\mathit{8}j\mathrm{I})$In the above,$(^{*})$is due to the observation that$tr((\alpha-\circ B)\otimes(\beta-\circ C))=tr$($\alpha-\mathrm{o}(B\otimes(\beta-0$C))&\beta -o$((\alpha-\mathrm{o}B)\otimes C)$

The distribution law is shown as follows;$=$$\bigcap_{k\in K}(\bigcap_{\in iI}[ti\mathrm{J}\otimes\bigcap_{j\epsilon j}[Skj\mathrm{I})$$k\in K\mathrm{n}([\ i\epsilon Iti\otimes\ _{ij}\in J^{\overline{S_{k}}}\mathrm{I})\sim$$=$$[\ _{i\in I}t_{i}\otimes\ k,)\in K\mathrm{x}J\overline{s_{kj}}\sim(j$$=$$\bigcap_{i\in I}[t_{i}\mathrm{I}\otimes\cap k\in Kj\in\cap[sJkj$

For$(^{**})$, observe that

I

I$(**)$

).

166

.

$\bigcup_{k\in K}tr(\ i \in It_{i}\otimes\ j \in j\overline{S_{kj}}\sim)=tr(\ i \in It_{i}\otimes\ \sim(k,j)\in K\mathrm{x}J\overline{s_{kj}})$This completes the proof of Proposition 5.

\S 5$\blacksquare$

Conclusion and Future Works

So far we have seen how traditional logical analyses, especially model-theoretic semantics, contribute to characterize new notions from the discipline of process calculi.
We have obtained a simple semantics characterizing the reachability. One interesting point
can be found in the completeness proof of naive phase semantics in \S 3.3. Our naive phase model
construction for the completeness proof gives each process configuration a naive phase modelthat directly represents the precondition structure in the computation starting from ; in$a\in A^{*}$ holds wheneveris a precondition of . We also considered splitted preconditions, which represents a half of precondition of . It is the use of these splittedof the form
preconditions that allows us to drop the closure condition and obtain the completeness with respect
to the naive phase models. This model construction suggests that our naive phase models provide
solnewhat direct interpretation of processes. A further study is needed to clarify this point.
The second part of this paper is an attempt to apply the traditional model-theoretic technique to characterization of the new equivalence notions of processes that come from the theoryof process calculi. Trace equivalence, which we have characterized by trace models in \S 4, isso coarse that it would be of little use in practice. Nevertheless, it is important as the basis; the notion of trace equivalence wellfor further study on equivalences onshould be identified on the ground of theircaptures a primitive intuition thatobservable behavior. There is a wide range of equivalence notions naturally defined in terms
of process behavior, among which trace equivalence is not only the coarsest, but also the mostgeneral in the sense that each equivalence can be seen as a refinement of trace equivalence (cf.
. Therefore, it is expected, on the basis of our result in \S 4, tovanobtain model-theoretic characterizations for finer equivalences than trace equivalence, such as fail), simulation equivalence (cf.
) and bisimulation
ure equivalence (Brookes,
equivalence.
Our system is too restricted to develop a full theory of process calculus. An important mechanism which our system lacks is the guarding. By guarding a process (or a process configuration)with respect to some messages , we can inhibit communications of between the outside of thescope of guarding operator and the inside of the scope. This, roughly, corresponds to the existential quantifier in terms of logic. However, incorporation of guarding mechanism will undoubtedly
complicate the situation around the notion of observation and observable actions. Hence it still
remains uncertain whether our results hold for richer fragments that include a kind of guarding
operator in syntax.
Besides, the first author introduced in [20] the mobile linear logic to express mobile
passing in a linear logic-based process calculus, corresponding to Milner’s extension of CCS to, a mobile version and higher order mobile version of CCS. We leave these invesigation
on extended systems to future works.
$\Gamma$$\Gamma$$\mathcal{M}(\Gamma)$$\mathcal{M}(\Gamma),$

$A$

$a$

$\sqrt[l]{b}B$

$b$

$B$

$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}\mathrm{e}\mathrm{s}/\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}\mathrm{l}\mathrm{a}\mathrm{s}$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}\mathrm{e}\mathrm{s}/\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}\mathrm{l}\mathrm{a}s$$\mathrm{G}\mathrm{l}\mathrm{a}\mathrm{b}\mathrm{b}\mathrm{e}\mathrm{e}\mathrm{k}[29],$$\mathrm{M}\mathrm{i}\mathrm{l}\mathrm{n}\mathrm{e}\mathrm{r}[17])$$\mathrm{P}\mathrm{a}\mathrm{r}\mathrm{k}[\mathit{2}5]$$\mathrm{H}\mathrm{o}\mathrm{a}\Gamma \mathrm{e}\ \mathrm{R}\mathrm{o}\mathrm{S}\mathrm{c}\mathrm{o}\mathrm{e}[3]$$(\mathrm{M}\mathrm{i}\mathrm{l}\mathrm{n}\mathrm{e}\mathrm{r}[15])$$\vec{\alpha}$$\vec{\alpha}$$mes\mathit{8}age$$\pi-$$\mathrm{c}\mathrm{a}\mathrm{l}\mathrm{C}\mathrm{u}\mathrm{l}\mathrm{u}\mathrm{s}[19]$References[1] V. Michele Abrusci. Non-commutative intuitionistic linear propositional logic. Zeitschrift fuir
Mathematische Logik und Grundlagen der Mathematik, Vol. 36, pp. 297-318, 1990.

[2] Jean-Marc Andreoli and Remo Pareschi. Linear objects: Logical processes with built-in
inheritance. New Generation Computing, Vol. 9, pp. 445-473, 1991.
[3] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential
processes. JA CM, Vol. 31, No. 3, pp. 560-599, 1984.

167[4] W. Buszkowski. Completeness results for Lambek syntactic calculus. Zeitschrift f\"ur mathematische Logik und Grundlagen der Mathematik, Vol. 32, pp. 13-28, 1986.
[5] Jean-Yves Girard. Linear logic. Theoretical Computer Science, Vol. 50, pp. 1-102, 1987.

[6] Jean-Yves Girard. Linear logic: Its syntax and semantics. In J.-Y. Girard, Y. Lafont, and
L. Regnier, editors, Advances in Linear Logic, pp. 1-42. Cambridge University Press, 1995.
Proceedings of the Workshop on Linear Logic, Ithaca, New York, June 1993.
[7] C. A. R. Hoare. Communicating sequential processes. In R. M. McKeag and A. M. Macnaghten, editors, On the construction of programs–an advanced course, pp. 229-254. Cambridge University Press, 1980.

[8] C. A. R. Hoare. Communicating Sequential Processes. Prenti.ce-Hall, Englewood Cliffs, NJ,
1985.
[9] K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proceedingsof ECOOP’91, pp. 133-147. Springer-Verlag LNCS 512, 1991.
[10] Naoki Kobayashi. Asynchronous communication model based on linear logic. Master’s thesis,
Department of Information Science, University of Tokyo, March 1992.

[11] Naoki Kobayashi and Akinori Yonezawa. Logical, testing, and observation equivalence forfor processes in a linear logic programming. preprint (presented at Linear Logic Workshop,
Cornell University), 1993.
[12] Naoki Kobayashi and Akinori Yonezawa. Asynchronous communication model based on linear
logic. Formal Aspects of, Vol. 7, pp. 113-149, 1995. Short version appeared in
Joint International Conference and Symposium on Logic Programming, Washington, DC,
November 1992, Workshop on Linear Logic and Logic Programming.
$c_{\text{ノ}}omputing$[13] Yves Lafont. The finite model property for various fragments of linear logic.
Symbolic Logic, to appear. Available by ftp anonymous on iml.univ-mrs.fr,$J_{\mathit{0}u\gamma}nal$$\mathrm{i}\mathrm{n}/\mathrm{p}\mathrm{u}\mathrm{b}/\mathrm{l}\mathrm{a}\mathrm{f}\mathrm{o}\mathrm{n}\mathrm{t}$.

of[14] J. Lambek. The mathematics of sentence structure. American Mathematical Monthly, Vol. 65,
No. 3, pp. 154-170, 1958.
[15] R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, Vol. 25, pp.
267-310, 1983.

[16] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[17] R. Milner. Operational and algebraic semantics of concurrent processes. In J. van Leeuwen,
editor, Handbook of Theoretical Computer Science, pp. 1201-1242. Elsevier Science Publishers
B.V. (North-Holland), 1990.

[18] R. Milner. Functions as processes. Mathematical Structure in Computer Science, Vol. 2,
No. 2, pp. 119-146, 1992.

[19] R. Milner, J.G. Parrow, and D.J. Walker. A calculus of mobile processes. Information andComputation, Vol. 100, No. 1, pp. 1-77, 1992.
[20] Mitsuhiro Okada. Mobile linear logic as a framework for asynchronous and synchronous
mobile communication calculi. Technical Report, Concordia University, February 1993.
[21] Mitsuhiro Okada. A brief look at the linear logic from the proof search paradigm. In Introduction to Linear Logic (the lecture note of the introduction course at Linear96, Tokyo Meeting).

1996.

168

[22] Mitsuhiro Okada. Phase semantics for higher order completeness, cut-elimination and normalization proofs (extended abstract). In J.-Y. Girard, M. Okada, and A. Scedrov, editors,
ENTCS (Electronic Notes of Theoretical Computer Science) Vol.3: A Special Issue on the
Linear Logic 96, Tokyo Meeting. Elsevier-ENTCS, 1996. An earlier version is available by ftp
anonymous on iml.univ-mrs.fr, in.
$\mathrm{p}\mathrm{u}\mathrm{b}/\mathrm{o}\mathrm{k}\mathrm{a}\mathrm{d}\mathrm{a}$[23] Mitsuhiro Okada and Kazushige Terui. Naive phase semantics for some fragments of intuitionistic linear logic. Manuscript, available by ftp anonymous on abelard.flet.mita.keio.ac.jp,, 1996.
in$\mathrm{p}\mathrm{u}\mathrm{b}/\mathrm{P}\mathrm{a}\mathrm{p}\mathrm{e}\mathrm{r}\mathrm{S}/\mathrm{T}\mathrm{e}\mathrm{r}\mathrm{u}\mathrm{i}$[24] Nikolai Pankrat)ev. On the completeness of the Lambek calculus with respect to relativized
relational semantics. Journal of Logic, Language, and Information, Vol. 3, pp. 233-246, 1994.
[25] D. M. R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor,
Proceedings of 5th GI Conference, pp. 167-183. Springer-Verlag LNCS 104, 1981.

[26] M. Pentus. Language completeness of the Lambek calculus. In proc. of LICS 94, pp. 487-496.
IEEE, 1994.
[27] Giovanni Sambin. The semantics of pretopologies. In K. Do\v{s}en and P. Schr\"oder-Heister,
editors, Substructural logics, pp. 293-307. Oxford University Press, 1994.

[28] Anne S. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes 29, Center for the Studyof Language and Information, Stanford, California, 1992.

[29] R. J. van Gla.bbeek. The linear time- branching time spectrum. In J. C. M. Baeten andJ. W. Klop, editors, Proceedings CONCUR ’90, Amsterdam, pp. 278-297. Springer-Verlag
LNCS 458, 1990.
[30] R. J. van Glabbeek. The linear time
branching time spectrum II the semantics ofsequential processes with silent moves. In E. Best, editor, Proceedings CONCUR ’93,
Hildesheim, pp. 66-81. Springer-Verlag LNCS 715, 1993. Preliminary version available at-$\mathrm{f}\mathrm{t}\mathrm{p}://\mathrm{B}_{\mathrm{o}\mathrm{O}}1\mathrm{e}.\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{n}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{d}.\mathrm{e}\mathrm{d}\mathrm{u}/\mathrm{p}\mathrm{u}\mathrm{b}/\mathrm{s}\mathrm{p}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{m}.\mathrm{A}4.\mathrm{P}\mathrm{S}.\mathrm{g}\mathrm{z}$.