数理解析研究所講究録902 巻 1995 年 80-10280lnductive Synthesis of Recursive Processes from Logical Properties *Shigetomo Kimura (木村曲面), Atsushi Togashi (富樫敦) and Norio Shiratori (白鳥則郎)
2-1-1 Katahira, Aoba-ku, Sendai, Japan.
Research Institute of Electrical Communication, Tohoku University.
〒 980-77 仙台市青葉区片平 2-1-1

東北大学電気通信研究所$\mathrm{e}$1-mail : {kimura,togashi,$\mathrm{n}\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{o}$}$\copyright \mathrm{s}\mathrm{h}\mathrm{i}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{o}\mathrm{r}\mathrm{i}.\mathrm{r}\mathrm{i}\mathrm{e}\mathrm{C}.\mathrm{t}_{0}\mathrm{h}\mathrm{o}\mathrm{k}\mathrm{u}.\mathrm{a}\mathrm{c}.\mathrm{j}\mathrm{p}$Introduction
The studies of process algebras started from the latter half of$1970’ \mathrm{s}$to give mathemat-

ical semantics for concurrent systems. Typical systems are CSP by Hoare $[5, 15]$ , CCS by
Milner [19] and ACP by Bergstra and Klop [2]. In Feb. 1990, ISO adopted LOTOS [4] as

the international standard for OSI specification description language. Algebraic formaliza-tion techniques are utilized as the descriptive languages for communicating processes andconcurrent programs. They are also applied to the verification problem, by virtue of themathematical formality. The processes, however, have the features such as non-determinacy
and concurrency, so their operational semantics are completely different from those of the

traditional automata and formal languages.
In the formal specification, modal or temporal logic are studied to express constrainsor to verify a specification. For example, [8] and [9] used temporal logics to verify thatspecifications had good properties like ‘safety’ or ‘liveness’, and did not have bad properties
such as ‘deadlock’.
From opposite point of view, we can regard these formulae as facts, which a specificationmust satisfy. And we seem to be able to infer a specification from facts by using learning

paradigms. Inductive inference is one of the learning paradigms and suitable for our purpose since an exact specification satisfying input facts can be inferred by means of inductive

inference. Therefore, the inductive inference of the processes forms a$\mathrm{b}\mathrm{a}s$

is for automaticsynthesis of highly reliable communicating protocols and concurrent programs from the ex-amples or the required properties. However, little has been investigated for the inductive

inference of collcurrent processes due to the difficulties arising from the process features suchas non-determinacy and concurrency.
We have already presented the algorithm that inductively synthesizes a basic process
in a subclass of CCS from concrete examples expressed in modal formulae which describe
A part of this study is supported by Grants from the Asahi Glass Foundation and Research Funds fromJapanese Ministry of Education. A preliminary version of this paper was published in the Proceedings of thefifth International Workqhop on Algorithmic Learning Tlleory. LNCS, 1994

81

the properties of the process and have demonstrated the validity and improvement of theapproach [16]. However, the expressive power of basic processes is weak. They cannot express

the recursive behaviors of a system. It remains to propose a synthesis algorithm for recursive
processes.
This paper presents an inductive synthesis algorithm for a recursive process. To synthesize
a process, facts, which must be satisfied by the target. process, is given to the algorithm

one by one since such facts are$\mathrm{i}\mathrm{n}\mathrm{f}\mathrm{i}_{1}\dot{\mathrm{u}}\mathrm{t}\mathrm{e}\mathrm{l}\mathrm{y}$many in general. Whenalgorithm, it outputs a process which satisfies the input

$n$

$n$

facts are input to thefacts. And this generation process

is repeated infinitely many times. To represent facts of a process, we adopt a subcalculusof -calculus [11, 17, 25], which can describe recursive behaviors. The correctness of the$\mu$algorithm can be stated that the output sequence of processes by the algorithm converges toa process, which cannot be distinguished from the intended one (if we could know it) by agiven enumeration of facts, in the limit.
In fact, the problem to synthesize a process is regarded as a satisfiability problem forlogical calculi. The satisfiability problem is a decision problem to determine whether or not agiven formula in the logic has a model. For example, Kozen [17] provided a tableau method
for the -calculus. We will compare our method with related works and discuss the reason$\mu$

why we employ inductive inference to synthesize a process in detail in Section 6.

The outline of the paper is as follows: Section 2 presents the algebraic formulation. ofprocesses, together with { -calculus. Section 3 discusses the discriminative power of a subcalculus of -calculus. Section 4 gives an algorithm that synthesizes a process satisfying a$\mathrm{t}$$\mu$given enumeration of facts. Section 5 introduces a prototype system SORP (Synthesizer of
Recursive Processes) based on the synthesis algorithm. The paper is concluded in Section 6,
where related works and future problems are briefly discussed.

Preliminaries

2

In this section, we briefly review the preliminary notions such as algebraic processes and$\mu$-calculus. See [11, 13, 15, 17, 19, 25] for more detailed discussions.

2.1

Algebraic Processes

Let $A$ be an alphabet, a finite set of symbols. Its element is called an action. This
corresponds to aevent of a process and this is assumed to be externally observable$\mathrm{p}_{\Gamma \mathrm{i}\mathrm{n}}1\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{V}\mathrm{e}$and controllable from$\mathrm{t}1_{1\mathrm{e}\mathrm{e}}\mathrm{n}\mathrm{V}\mathrm{i}\mathrm{r}\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{n}\mathrm{e}\mathrm{n}\mathrm{t}$denumerable set$C$Definition 2.1$Recu\Gamma_{\mathrm{L}}\sigma ive$

1. An inaction
2. If

3. If

$p$

$p_{1}$. Throughout this paper, it is assumed that we have aof process cons tants.

$0$terms are defined inductively as follows:

and a process constant $c\in C$ are$\mathrm{r}\mathrm{e}\dot{\mathrm{c}}$ursive terms.

is a recursive term, an action prefix . is a recursive term where $a\in A$ .
$a_{l^{y}}$and$p_{2}$

are recursive terlns, their summation$p_{1}+p_{2}$is a recursive term.

82

4. A process constant with a defining equation
term, where is a recursive term.

$c^{\mathrm{d}}=^{\mathrm{e}f}p$$c$, denoted as rec $c.p$ , is a recursive$\square$$p$

In a recursive term rec $c.p$ , every occurrence of in is called bound. We say is a scopeof rec . in rec $c.p$ . The occurrence of a process constant which is not within any scope ofrec . is called free. When every free occurrence of is within some subterm $a.q$ of , we call
$c$

$p$

$p$

$c$

$p$

$c$

$c$

is guarded in . When every constant in is guarded, is also called guarded. If every
occurrence of any process constant in is bound, is called closed. Otherwise it is called
denote the set of all processes.
open. Closed terms are called (recursive) processes. Let
By renaming process constants, every term is converted to a term such that if rec
$c$

$p$

$p$

$p$

$p$

$p$

$’\rho$$p’$$p$

and rec$c_{2}.p_{2}$are subterms in

$p’$

then

$c_{1}\neq c_{2}$$c_{1}.p_{1}$. This conversion is the same as -conversion in$\alpha$of-calculus [14]. Thus, a term can be represented as with a set
defining equations, where every subterm of the form rec $c.q$ in is replaced by .
with actions as labels.
transition
Semantics of a recursive term is given by a$\{c_{1}\mathrm{d}\mathrm{e}\mathrm{f}=p_{1\cdot\cdot n},., c=p\mathrm{d}\mathrm{e}\mathrm{r}n\}$$\lambda$

$p$

$p$

$c$

$p$

$label\epsilon d$$\mathit{8}ystem$

Definition 2.2 A labeled transition system is a triple $<S,A,$.
a transition relation definedand$arrow>$, where$S$

is a set of states$\square$$\mathrm{a}\mathrm{s}arrow\subset S\mathrm{x}A\cross S$$arrow \mathrm{i}\mathrm{s}$For $(s, a,s’)\inarrow$ , we normally write $sarrow s’a$ . Thus, the transition relation can be written as$arrow=\{aarrow|a\in A\}$ . $s\neg s’$ m ay be interpreted as “in the statean action can be performed
and after the action the state moves to ” . is called an a-succe8sor of 8. We use the usual
$a$

$a$

$s$

abbreviations as e.g.

$sarrow a$

for

$s’$

$s’$

.

$ss’\underline{a}$$\exists s’\in S\mathrm{s}.\mathrm{t}$and $s\#$ for$\neg\exists s’\in S\mathrm{s}.\mathrm{t}$. $sarrow s’a$ .

Definition 2.3 A transition relation on recursive ternls is given by the following transition
rules:$\frac{qarrow q’a}{\iota^{y}+qarrow qa/}$$\frac{parrow p’a}{p+qp’\underline{a}}$$\frac{p\{\mathrm{r}\mathrm{e}\mathrm{c}c.p/c\}arrow pa\prime}{\mathrm{r}\mathrm{e}\mathrm{c}c.parrow pa\prime}$$\overline{a.p\neg pa}$

where $p\{q/c\}$ is$p$except any free occurrences of$c$are replaced by .

$\square$$q$

Based on the operational semantics given by the transition system, several equivalences andpreorders have been proposed in order to capture various aspects of the observational behaviorof processes. One of those is the equivalence induced by the notion of a bisimulation $[19,20]$ .

Definition 2.4 A relation
for all $a\in A$ :over recursive terms is a strong bisimulation if $(p, q)\in R$ implies,

1. whenever $parrow p’a$ , then there exists$q’$such that $qarrow q’a$ and $(p^{J}, q)’\in R$ ,2. whenever $q\neg q’a$ , then there exists$p’$such that $parrow p’a$ and $(l^{J’}, q’)\in R$ .

Recursive terms

R.

$R$

$p\sim q$$p$$\square$and.q are strongly equivalent iff $(p,q)\in R$ for some strong bisimulation

denotes that

$p$

and

$q$

are strongly equivalent. Clearly,

bisimulation and an equivalence relation.

$\sim$

is the largest strong

83

Proposition 2.5

The following eqnotions are satisfied on processes.

$[12, 19]$

1. $p+q\sim q+p$ .

2. $p+(q+r)\sim(p+q)+r$ .
3. $p+p\sim p$ .

4. $p+0\sim p$ .

$\square$This proposition can be easily extended for recursive terms. It is known that the equivalence given by the above proposition is sound and complete over strong equivalence, when

only basic processes constructed by inaction, action prefix and summation, are considered [12].

Using this result. it is shown that any basic processes
process of the following fornl$p$can be equivalently transformed into a$\mathit{0}_{1}.p_{1}+\cdots+a_{n}.p_{n}(=^{\mathrm{e}}\sum_{i}nai\cdot p=1i)\mathrm{d}\mathrm{f}$. The order of$a_{i}.p_{i}$is immaterial

from equation 1 and 2. When $?l=0$ , it is understood that $\sum_{i=1}^{n}a_{i}.pi=0$ . In the following,recursive
based on that, we
assume both the commutative and associative law$\mathrm{o}\mathrm{f}+\mathrm{o}\mathrm{n}$$\mathrm{a}\mathrm{l}\backslash \mathrm{v}\mathrm{a}.\mathrm{V}\mathrm{s}$terms to avoid heavy use of brackets. Furthermore, by definition, a process constant without. Therefore, without loss of generality, to the rest of
this paper, we are concerned with only processes rather recursive terms.

its definition is strongly

2.2

$\mu$

$\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{i}\mathrm{v}\mathrm{a}\iota_{\mathrm{e}}\mathrm{n}\mathrm{t}$

to

$0$

-calculus

The alternative cllaracterization of equivalence on processes depends on the identificationof a process with the properties it enjoys. Then we can say that two processes are equivalent if

and only if they elljov exactly same properties. In other words, two processes are inequivalent
if one enjoys a property that the other does not enjoy. For this purpose, in this paper we-calculus [11, 17, 25], which includes a modality concerning actions, in order todescribe dynamic properties of processes. It is an extension of Hennessy-Milner logic [12] toadopt the$\mu$express recursive
synthesis algorithm.

)$\mathrm{e}\mathrm{r}\mathrm{t}\mathrm{i}\mathrm{e}\mathrm{s}$$1^{)\mathrm{r}\mathrm{o}}1$

Definition 2.6$for\uparrow m\prime lae$

. So we will introduce it to represent facts of a process for thein -calculus are defined inductively as follows:$l^{\iota}$

1. tt (true) is a formula.
2. A variable$x\in\iota 1’$

is a$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{n}\mathrm{l}\mathrm{U}\mathrm{l}\mathrm{a}$, where

3. If

$f$

and $f’$ are formulae, $f\vee f’$ and

4. If

$f$

is a formula. {$a\rangle f$

is a$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{n}\mathrm{u}\mathrm{u}\mathrm{l}\mathrm{a}$$\mathcal{X}$$\neg f$is a denumerable set of logica variables.
$l$

are formulae.

, where $a\in A$ .

5. If is a variable and is a formula with positive occurrence of $x-x$ occurs within
is a formula.
scopes of positive number of
$f$

$x$

$\square$$\mathrm{n}\mathrm{e}\mathrm{g}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{S}-l\iota.X.f$

The notion of freeness, boundness and scope for formulae in -calculus are defined similarly
to the one for recursive ternls or -calculus. A variable in a formula is guardecl, if every$l^{\iota}$$\lambda$

occurrence of$x$

is within some scope of

$f$

$x$

$\langle a\rangle$. A formula$f$

is guarded if every variable in

$f$

84

is guarded. A formula
$f$

$f$

is sometime written as $f(x)$ to express the free occurrence of. $f(g)$ denotes the resulting $f(x)$ , where every free occurrence of

replacement $f(g)$ , every free occurrence of a variable in

$g$

$x$

is replaced by$\mathcal{P}-$with$\mathcal{V}$, which is the valuation$\mathcal{V}’$$2^{\mathcal{P}}$be ais thethat agrees

except that $\mathcal{V}’(x)=S$ .

The set of all closed formulae is written as
valuation$f\equiv f’$$\mathcal{V}[S/x]$. In the$arrow 2^{\mathcal{P}}$$\mathcal{V}$adopt conventional notation$\backslash \eta r_{\mathrm{e}}$inis not bound in $f(g)$ by means ofrenaming bound variables. Recall that is the set of all processes. Let:Xvaluation, which assigns a set of processes to be satisfied to each variable, where
power set of P.

$g$

$x$

$\mathcal{V}$$L$. When a process, it is written as $p\models vf$ . The symbolmeans that $p|=vf$ iff

Definition 2.7 Let$\mathit{1}^{J}|=vf’$satisfies a formula$p$

and for all valuations$\mathcal{V}$.

be any process. Satisfaction relation of formulae in a valuation

$p$

in a

$f$

used to denote logical equivalence, i.e.

$\equiv \mathrm{i}\mathrm{s}$for all process$p$$\mathcal{V}$isdefined as follows:1.

$p|=v\mathrm{t}\mathrm{t}$.

2. $p|=vx$ if$p\in \mathcal{V}\langle_{X})$.

3. $p|=vf_{1}f_{2}$ if $p|=vf_{1}$ or $p|=vf_{2}$ .
4.

$p|=_{\mathcal{V}}\neg f$5.

$p|=v\langle a\rangle f$if $p\# vf$ , where $p\# vf$ means
if there exists some

6. $p|=v\mu x.f(x)$ if $p\in S$ for all$q$$\mathrm{t}1_{1}\mathrm{a}\mathrm{t}p$does not satisfy

iff$p|=_{\mathcal{V}’}f$for all$\mathcal{V}’$.

such that $parrow qa$ and $q|=vf$ .

$S\subseteq \mathcal{P}arrow \mathrm{S}\mathrm{u}\mathrm{c}\mathrm{h}$that$\forall q\in \mathcal{P}-.q\models_{\mathcal{V}[/x\mathrm{J}}Sf(X)$Note that a valuation is immaterial for close formulae$\mathcal{V}$

$f$

$f$

implies $q\in S$ .

$\square$in the sense that $p\models vf$ for some

. In the following, $|=v$ is abbreviated as$|=\mathrm{i}\mathrm{f}$there is no conflict about

its valuation.

Definition 2.8 The following logical notations are used for convenience:
1. ff$\mathrm{d}\mathrm{e}\mathrm{f}=\urcorner \mathrm{t}\mathrm{t}$.

2.

$f_{1}$

3.

$[a]f^{\mathrm{d}}=^{\mathrm{e}}\neg\langle a\rangle \mathrm{f}\neg f$

4.

$\nu x.f(X)^{\mathrm{d}}=\urcorner llX.\neg f\mathrm{e}f(\urcorner x)$A$f_{2}=\neg \mathrm{d}\mathrm{e}t(\urcorner f_{1}\mathrm{v}\urcorner f_{2})$.

.
.

For a set of closed formulae$\square$$L(L\subseteq \mathcal{L})$and a process $p,$ $L(p)$ is defined as follows:$L(p)^{\mathrm{d}\mathrm{e}}=\{\mathrm{f}f\in L|_{l})|=f\}$

Our definition of -calculus differs from that ofin [11]. Fortunately, each)system has same
power when is finite and only guarded formulae are concerned.
$\mathrm{S}\mathrm{T}\mathrm{A}(\mathcal{X}, A)$$\mu$$\Gamma \mathrm{e}\mathrm{S}\mathrm{S}\mathrm{i}\mathrm{v}\mathrm{e}$$\mathrm{e}\mathrm{x}_{1}$The set of all formulae in$f::=\mathrm{t}\mathrm{t}|$$\mathrm{S}\mathrm{T}\mathrm{A}(\mathcal{X}.A)$$A$

is defined in the following BNF:

Nil $|.\tau|Af|f+f|ff|\neg f|l^{\iota x.f}$ where$x\in \mathcal{X}$and$A\subseteq A$.

85Definition 2.9 Let be any process. Satisfaction relation of a formula invaluation is defined as follows:$p$$\mathrm{S}\mathrm{T}\mathrm{A}(\mathcal{X},A)$in a$\mathcal{V}$

1. $p|=v$ Nil if $p\sim 0$ .
2. $p|=vAf$

if$\exists p_{i}$3. $p|=vf_{1}+f_{2}$if$p_{i}$

and $a_{i}\in A(1\leq i\leq n)$ such thatand $p_{i}|=vf$ for each$p \sim\sum^{n}i=1ai\cdot pi$.
$\exists p_{1}$and$p_{2}$

such that $p_{1}|=vf_{1},$ ) $2|=vf_{2}$ and $p\sim p_{1}+p_{2}$ .
$l$

4. The satisfaction relation for other syntactical constructs is defined in the exactly same
way as in Definition 2.7.

$\square$Proposition 2.10 [11]1. $f+f\equiv f$ for

2.
3.

$f+\mathrm{N}\mathrm{i}1\equiv f$$\emptyset f\equiv \mathrm{f}\mathrm{f}$$f$of the form A $f’,$$\mathrm{t}\mathrm{t}$, Nil.

.

.

4. $(A_{1}\cup A_{2})f\equiv A1fA2f(A_{1}f+A_{2}f)$ .
5. $fi+(f2\vee f3)\equiv(fi+f2)\vee(f_{1}+f_{3})$ .

6$\urcorner(Af+\mathrm{t}\mathrm{t})\equiv(A-A)\mathrm{t}\mathrm{t}\vee A\neg f((A-A)\mathrm{t}\mathrm{t}+A_{\urcorner}f)$

7.

Nil.

$\neg(\sum_{i}A_{i}fi)\equiv\neg(\sum_{i}A_{i}fi+\mathrm{t}\mathrm{t})\vee[(\bigwedge_{i((}A-A_{i})\mathrm{t}\mathrm{t}A_{i^{\neg}}f_{i}))+\mathrm{t}\mathrm{t}]$.

8 $\mu xC_{1}[\{a\}c2[X+f]]\equiv\ell\iota Xc_{1}[\mathrm{t}a$} $C2[\mu y.(C_{1}\text{ノ}[\{a\}c2[y||+f)]]$ for any formulatexts$C_{1}$ $[]$

which are formulae with the hole$a\uparrow?dc_{2}[]$

$[]$

$f$

and con-.

proof We prove onlv 8 since it is not included in [11]. It roughly means a variable appearing

as a summand of some subterm can be eliminated. Since we are concerned with guarded
formulae, any equation of the form $x=f(x)$ has a unique least fixed point, i.e. $\mu x.f(x)$ .
Let $\hat{x}=\mu x.C_{1}[\{a\}C_{2}[x+f]]$ , the unique least fixed point of the equation $x=C_{1}[\{a\}C_{2}[x+$$f]]$ .
Thus we have
, wherefor $t=C$ (a context) or$\hat{x}=\hat{C}_{1}[\{a\}\hat{c}2[\hat{x}+\hat{f}]]$$t=f$ (a formula). Letof the equation$\hat{y}=\hat{x}+\hat{f}$. Then$y=\hat{C}_{1}[\{a\}\hat{c}_{2}[y]]+\hat{f}$$C_{1}[\{a\}c_{2}[lly.C_{1}\text{ノ}[\mathrm{t}a\}c2[y]]+f]]$.

$\hat{t}=t\{\hat{x}/x\}$$\hat{y}=\hat{C}_{1}[\{a\}\hat{c}2[\hat{y}]]+\hat{f}$$\mathrm{T}\mathrm{h}\mathrm{e}\Gamma \mathrm{e}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{e}.\hat{x}$. So$\hat{y}$is the fixed pointis the fixed point of the equation $x=$

. Hence we get the result.

$\square$For example,$\mu x.\{\mathrm{r}\iota\}(_{X}+\{b\}\mathrm{N}\mathrm{i}1)$$\mu x.\{a\}l\iota y.(\{b\}(X+y+\{_{C}\}\mathrm{N}\mathrm{i}1))$

It is easy to see that$\langle a\rangle$

in

$\mu$

-calculus is Itot

)

$1$

$\mu$

$\equiv$$\mu x.\{r\iota\}\mu y.(\{a\}y+\{b\}\mathrm{N}\mathrm{i}1)$$\equiv$$\{a\}’\iota y.(\{a\}y+\{b\}\mathrm{N}\mathrm{i}1)$$\equiv$$f^{\iota X.\{a\}l} \oint y.\{b\}\mu z.\mu w.(\{b\}w+\{a\}\{b\}_{Z}+\{C\}\mathrm{N}\mathrm{i}1)$$\equiv$$\{a\}\{b\}l\iota\approx\cdot l\iota w.\sim(\{b\}w+\{a\}\{b\}z+\mathrm{t}c\}\mathrm{N}\mathrm{i}1)$-calculus is elllbedded into$\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{i}\mathrm{d}\mathrm{e}\mathrm{d}$,in STA(\mbox{\boldmath $\lambda$}ノ,

$A$

).

$\mathrm{S}\mathrm{T}\mathrm{A}(,\mathrm{v},A)$.

. The diamond operator

However if we define$\langle a\rangle f^{\mathrm{d}\mathrm{e}}=^{\mathrm{f}}\{a\}f+\mathrm{t}\mathrm{t}$

as

86

in [11], the inclusion is obvious. The opposite direction is not so trivial. We can show theis finite and a formula is guarded. From Proposition 2.10, we canother inclusion whenis either of the form tt or $\{a\}f$ , where $a\in A$ , byassume any sumnuand (an )$A$$0_{1}$$\mathrm{e}\Gamma \mathrm{a}\mathrm{n}\mathrm{d}\mathrm{o}\mathrm{f}+)$the following algorithm since each formula is guarded
1. Remove any$\neg$

operators by logical connective rules and Proposition 2.10.6 and 7.

2. Eliminate any variables included in a summand by Proposition 2.10.8.

3. Convert any a.ction set of each prefix operator to a singleton set by Proposition 2.10.3
and 4.
4. Delete V and Nil operators within summand by Proposition 2.10.2 and 5.
Then we can show a translation function fromto -calculus.

$\mathrm{S}\mathrm{T}\mathrm{A}(\lambda’,A)$$\mu$

Definition 2.11 A translation function $H(f)$ from a formulain -calculus is defined in the following:

in

$f$

$\mathrm{S}\mathrm{T}\mathrm{A}(\mathcal{X}, A)$

into the one

$\mu$

.

1.

$H(\mathrm{t}\mathrm{t})=\mathrm{t}\mathrm{t}$2.

$H( \mathrm{N}\mathrm{i}1)=\bigwedge_{a}\in A[a]\mathrm{f}\mathrm{f}$.

3. $H(x)=X$ .
4. $H(\neg f)=\neg H\mathrm{t}f)$ .

5. $H(f_{1}\vee f2)=H(f_{1})\vee H(f_{2})$ .
6. $H(\mu x.f)=\mu x.H(f)$ .

.

7.

$H(\{a\}f)=\langle a\rangle H(f)\wedge[a]H(f)\wedge\wedge C\in A-\{a\}[_{C]}.\mathrm{f}\mathrm{f}$8.

$H(( \sum_{i\in I\{}ai\}fi)+\mathrm{t}\mathrm{t})=\bigwedge_{i\in I}\langle a_{i}\rangle H(f_{i})$9.

$H( \sum_{i\in I\{a_{i}}\}f_{i})=\mathrm{t}\bigwedge_{i\in I}\langle a_{i}.\rangle H(fi))$

A (

where

$I$

is a finite index set.

$\bigwedge_{i\in I}[a_{i}]\mathrm{V}_{a=a_{j}}ifi^{)}$

A$( \bigwedge_{a\in A-A}[a]\mathrm{f}\mathrm{f})$wherefinite index set and $A=\{a_{i}|i\in I\}$ .

Let$|=_{v,\mathrm{s}\mathrm{T}\mathrm{L}}\langle A,\lambda \text{ノ}$formulae of)($\mathcal{V}$$\mathrm{S}\mathrm{T}\mathrm{L}(A,$ $’\iota_{)}’$

Lemma 2.12 Let$l^{J}$

is sometimes$\mathrm{o}\mathrm{n}\tau \mathrm{i}\mathrm{t}\mathrm{t}\mathrm{e}\mathrm{C}\mathrm{l}$

$I$

is a

$\square$as$|=\mathrm{s}\mathrm{T}\mathrm{L}(A,x)$) be a satisfaction relation for. Then we have the following results.

be a process$a\uparrow?df$

a formu la in$\mathrm{S}\mathrm{T}\mathrm{L}(A, \prime \mathrm{Y})$. Then$p\models_{\mathcal{V}_{\mathrm{c}}^{\mathrm{q}\mathrm{T}\mathrm{L}}},\langle A,\chi$$p|=vH(f)$ .

Proposition 2.13 lThen

) $f$

iff

$\square$$A$

is finite and a guarded formulae are only concerned,$\mu$-calculus

has same $expressi\iota’ epou\prime er$ with $STA(\ell\iota’, A)$ .

$\square$

The following two propositions, the same results for$\mathrm{S}\mathrm{T}\mathrm{A}(\mathcal{X},A)$, can be proved by Propo-

sition 2.13.

Proposition 2.14 Let $f(x)$ be a guarded form

$nl\mathrm{r}\ell$. Then the $follou’ ing_{S}$ are satisfied:

87

1.

$l^{lX}\cdot f(X)\equiv \mathrm{v}k>0f^{k}(\mathrm{f}\mathrm{f})$.

2.

$\nu x.f(x)\equiv\wedge k>0f^{k}(\mathrm{t}\mathrm{t})$.

$\square$Proposition 2.15 Proce.

$a\uparrow?dq$$9.\underline{9}esp$

a

$re$

strongly equivalent, $i.e$ . $p\sim q$ , iff$\mathcal{L}(p)=\mathcal{L}(q)$.

$\square$

The next proposition shows that the negation can be removed from a formula.

Proposition 2.16 Any formula can be equivalently converted to a formula without negation,$i.e$. a formula built ?1) ivith$\mathrm{t}\mathrm{t},$ff,$\vee,$$\wedge,$$\langle a\rangle,$$[a],$$\mu$, and .

$\square$$\nu$

From now on. we will consider closed formulae without negation.

3

A subcalculus of ‘-calculus$f$

In section 4, an inductive synthesis algorithm for recursive processes is introduced. The

algorithm generates a process which satisfies given formulae. However, a formula of disjunctive
form, e.g.

$fg$ . or$l^{\iota?,f(x}.$)(

processes. Consider the formula
$a$

or

$b$

is ambiguous to our purpose, i.e. synthesis of$\equiv _{k>0}fk(\mathrm{f}\mathrm{f}\mathrm{I})$. It says the target process can execute either$\langle a\rangle \mathrm{t}\mathrm{t}\langle b\rangle \mathrm{t}\mathrm{t}$(or both). When it is input to the synthesis algorithm, the algorithm is unsure which

formula, i.e.

outputs a process

In such case,or$\langle a\rangle \mathrm{t}\mathrm{t}$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}$$\langle b\rangle \mathrm{t}\mathrm{t}$, is reall. needed. Suppose that the algorithm trusts

which satisfies it. But after some$\mathit{1}^{J}$$\langle a\rangle \mathrm{t}\mathrm{t}$$\mathrm{v}$$\mathrm{t}\mathrm{i}_{1}\mathrm{n}\mathrm{e}\mathrm{s},$$[a]\mathrm{f}\mathrm{f}(\equiv\neg\langle a\rangle \mathrm{t}\mathrm{t})$algorithm nlu,s backtrack at the point before$\mathrm{t}$the other formula (i.e.

$\langle b$)$\mathrm{t}\mathrm{t})$.

$\mathrm{E}\mathrm{s}_{1^{)\mathrm{e}\mathrm{C}}}\mathrm{i}\mathrm{a}$]$1_{\mathrm{V}}$, since a forlnula with

$\mu$

$p$

and

may be input.

was synthesized, and adopt

operator has infinite many${ }$operators (see Proposition2.14). it nlav cause backtracking infinite many times. To remedy

the difficulty, we focus on the forlluulae\vithout$\mathrm{V}$

and

$\mu$

operators. Let$\mathcal{L}_{d}$be the set of all

formulae defined in the following BNF:
ff $|x|\langle a\rangle f|[a]f|f$ A $f|\nu x.f$$f::=\mathrm{t}\mathrm{t}|$where$x\in \mathcal{X},$$a\in A$implies $q|=vf$ for$\dot{\mathrm{a}}11$$\leq_{d}$

iff

and

$p\leq_{d}\mathrm{r}_{\mathit{1}}$formulae$q\leq_{dI^{J}}$on recuresive process is defined by$\leq_{d}$$f\in \mathcal{L}_{d}$. Obviouslv,

suffice to define$p\sim_{d}q$. A relationand for all valuations$\mathcal{V}$$l^{\mathrm{J}}\leq_{d}q$. Note that onlv closed formulae

is a preorder and the resulting relation$\leq_{d}$, is an equivalence relation. So,

iff $p|=vf$$\leq_{d}$$\sim_{d}$, defined byturns out to be a partial orderon the equivalence classes of recursive process with respect to$\sim_{d}$, i.e.

$\mathfrak{y}_{J}$]$\leq_{d}[q]$iff $p\leq_{d}q$ ,where $[p]=\{l^{J’}|p\sim_{d}p’\}$ .
Lemma 3.1 For a$f_{ol/ou\prime}ing_{C}lai’??^{\sigma}.$$f_{\mathit{0}\Gamma\}?1}\mathrm{t}/laf\in \mathcal{L}_{d}$.

$recu\prime \mathit{8}i_{1},e$processes $p,q$ and a valuation$\mathcal{V},$$u\rangle$$e$have the:

1. $p|=vf$ and $q|=vf$ imply $p+q|=vf$ .

2. $a.p+a.q|=v[\mathrm{r}]f$ implies $Cl.(p+q)|=v[a]f$ .
Proposition 3.2 For any processes $p.p’,$$q.ra\uparrow?\mathrm{r}l$$\square$any action a, the followings are satisfied:

88

1.

$p\leq_{dq\Leftarrow\Rightarrow p}a.\leq_{d}$

a. .
$q$

2. $p\leq_{dq=\Rightarrow+r\leq_{dq+r}}p$ .
3. If $r\neq\succ then$ $c\iota.p+r\leq_{d}a.p’+\uparrow\cdot\Leftarrow\Rightarrow a.p+a.q+r\leq_{d}a.p’+a.q+r$ .

4. $a.p+a.q\leq_{d}$ $a_{l^{y+\iota.q(pq}}.’+a.+$ ).

$\square$Lemma 3.3 $p\sim q$ implies $p\sim_{d}q$ . Brrt $??ot$ vice versa.
As the discriminative power of this relation$\leq_{d}$$\square$, we have the following result on comparison

with the ready simulation preorder $\leq_{RS}[10]$ .

Definition 3.4 A ready simulation preorder is a binary relation$R$on processes such thatwhenever $(p, q)\in R$ and $a\in A$ then:

1. if $parrow p’$ thell$a$$\exists q’.qq^{\prime_{\mathrm{a}\mathrm{n}}}\mathrm{d}\underline{a}(p’,$$\mathrm{r}_{\mathit{1})}’\in R$

.

.

2. if

$qarrow a$

then

Let

$\leq_{RS}$be the union of all readv simulation preorders. Then we have the following result.

Lemma 3.5)$l$$p\underline{a}$$\leq_{d}q$$\square$implies $p\leq_{RS}q$ . $Bnt$ not vice versa.

We have also the following relation which has more

Definition 3.6 A binary relation
the followings. If

1. whenever$l^{J}\subseteq_{dq}$$pl)’\underline{o}$. for all$\subseteq_{d}$Lemma 3.7

power thanover processes is a maximum relation. then there exists$\backslash \mathrm{v}1_{1\mathrm{e}}\Gamma \mathrm{e}n\geq 1$$\mathrm{d}\mathrm{i}_{\mathrm{S}\mathrm{C}}\Gamma \mathrm{i}\mathrm{n}\mathrm{l}\mathrm{i}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}$$\leq_{d}$$\mathrm{w}1_{1}\mathrm{i}\mathrm{c}\mathrm{h}$.
satisfies$a\in Act,$

2. whenever $q\neg q’a$ , then there exist$p_{n}’\subseteq_{dq’},$$\square$$q’\mathrm{s}\mathrm{u}\mathrm{C}\mathrm{h}$$l^{J_{1}’},$

that $qarrow q’a$ and$\ldots,l^{)’}n$$p’\subseteq_{dq’}$,such that $parrow Ia)’i$ for each.

$l^{\mathrm{J}_{i}’}$, and $p_{1}’+\cdots+$$\square$$p\subseteq_{dq}in7l$) $liesp\leq_{dq}$. But$??ot$

vice versa.

$\square$After all, we have the following theorem. See Fig. 1. In the figure, the arrows indicate

proper inclusion relation between )$\mathrm{r}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{S}$

$1$

$R’$

( $R’$ has more discrinlinative power than. i.e.

$R$$Rarrow R’$

means

$R$

is properly included by). About traces [19], failures [5] and simulation

preorders [19] and thier relationsllip, see [10] for more detail.

Theorem$3.8\leq_{RS}arrow\supset\leq_{d}\supseteq\subseteq_{d}arrow\supset\sim$$\square$Synthesis algorithnl

4This section describes an inductive synthesis algorithm for recursive processes. Formulaein -calculus are regarded as specific properties of the intended process.
$\mu$

89

$\mathrm{E}\backslash 1$

4.1: The relationship of preorders.

Enumeration of facts

An algorithm we will propose now is an inductive one. It generates a process which
satisfies given facts, the properties of the intended target process, represented as formulae in-calculus. Thus, the input to the algorithm is an enumeration of formulae to be satisfied by$\mu$

the target process. Let$p_{\mathit{0}}$be the intended target process to be generated from its concrete

properties. It should be noted that

Definition 4.1 Let(or$\langle f,$$-\rangle$$\zeta T$$p_{\mathit{0}}$is neither known initially nor given in a precise manner.

be a set of pairs of) such that either$\langle f, +\rangle$or$\langle f, -\rangle$$S=\{f|\langle f, +\rangle\in U\}\cup\{\neg f|\langle f, -\rangle\in U\}$

deductlive system
If we used

$p_{\mathit{0}}$$\mathrm{S}\mathrm{T}\mathrm{L}(,\gamma,A)^{1}[11]$$\mathrm{f}_{0\Gamma}\mathrm{n}\mathrm{l}\mathrm{U}\mathrm{l}\mathrm{a}\mathrm{e}f\in \mathcal{L}$and a sign

always belongs to

$U$

$S$

(or -), i.e. $(f,$for every formula

is an enumeration of facts if. An element of

$+$

$S$

$+\rangle$$f\in \mathcal{L}$.

is consistent in theis called a fclct.

$\square$. the enumeration of facts might be defined as follows:$S=\{f\in \mathcal{L}|po|=f\}$

Unfortunately, this definition of an enumeration of facts is impossible. Sincea priori, we must consider

4.2

Synthesis

$S$

from

$U$

$p_{\mathit{0}}$is not known

in Definition 4.1 as an enumeration of facts.

$\mathrm{a}\mathrm{l}\mathrm{g}\mathrm{o}\Gamma \mathrm{i}\mathrm{t}\mathrm{h}_{11}\mathrm{u}$As we mentioned in section 3. our algorithm restricts input formulae to elements of the set$\mathcal{L}_{d}$in order to avoid llon-deternlinac.\’ arising from both

${ }$

and

$\mu$

operators. To take accountof this restriction, the definition of an enumeration of facts must be modified, i.e. define anenumeration of facts as it Definition 4.1 and remove formulae which do not belong toan enumeration of facts. Note that a fornlula with$\mathcal{L}_{d}$fromoperator also has non-determinacy, i.e.

$\nu$

how many times loops of process branches unfold.

Given an enumeration of facts. the algorithm synthesizes a process satisfying those facts.
Recall that a process can be represented as a term ) with a setof$\{c_{1}\mathrm{d}\mathrm{e}\mathrm{f}=p1, \ldots,cn\mathrm{d}\mathrm{e}\mathrm{f}=p_{n}\}$$l$defining equations. In the, a process is represented as a set of process definitions.
Each process definition rec $c.p$ is associated with a set of formulae-, denoted as $c:C$ , which$\mathrm{a}_{0}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{h}\mathrm{n}1$$C_{\text{ノ}}$must be satisfied ) theprocess constant.

can be omitted when it is not important. To describe the algorithm. we adopt a languag\^e like Prolog [6], wherepredicates$1$$\mathrm{c}\mathrm{o}\mathrm{r}\mathrm{r}\mathrm{e}\mathrm{s}\mathrm{P}^{\mathrm{o}}\mathrm{n}\mathrm{C}\mathrm{l}\mathrm{i}_{1}$$.\mathrm{v}$

$c$

$C$

$\mathrm{I}/\mathrm{O}$$1\mathrm{S}\mathrm{T}\mathrm{L}(.\iota^{y}, A)$

found yet.

is sound but$\mathrm{u}\mathrm{n}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{t}111\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{e}1_{\mathrm{V}}$llot complete. A complete deductive system for$\mu$-calculus is not

90

, let
denote process constants associating withcan backtrack as well. For brief
where
is a set of formulae. The initial stateor
the process definitionsof process definitionsof a process is always fixed to . Thus, a set
with its set of process definitions.
determines the process, it is important to take an identification of formulae $\nu x.f(X)$For a fact of the fornl l ノ x.
corresponds to , i.e. the formula(or bound variables ) with process constants . If$\nu x.f(x)$ , the variable
is renamed by . Since is a bound variable, the meaning of the$\mathrm{d}\mathrm{e}\mathrm{S}\mathrm{C}1\check \mathrm{i}_{1^{)}}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$c_{i}$$c_{i}:C_{i}\mathrm{d}\mathrm{e}\mathrm{f}=p_{i}$$c_{i}=^{t}p_{i}\mathrm{d}\mathrm{e}$$C_{i}$$\{c_{0}\mathrm{d}\mathrm{e}\mathrm{f}=p_{0,\ldots,n}c\mathrm{d}\mathrm{e}l=p_{n}\}$$c_{0}$$c_{0}$$f(x\rangle$

$c$

$x$

$x$

$x$

$c_{i}$$x$$x_{i}$

formula is not changed. We assunle further that we can recall the original formulafrom$x_{i}$$\nu x_{i}.f(x_{i})$. Also we adopt the following abbreviations:
A.. . A$\wedge\{f_{1}, \ldots, f_{n}\}=f_{1}$where$f_{n}$$\wedge\emptyset^{\mathrm{d}\mathrm{e}\mathrm{f}}=\mathrm{t}\mathrm{t}$.

: The resulting set of process definitions,
in are replaced by$S[c_{1}:C_{1}=^{\mathrm{e}t}p\mathrm{d}1, \cdots , c\iota.:Ck=\mathrm{d}\mathrm{e}tl^{y}k]$definitions of: The$\cdots,$$S$$c_{k}$

is added to$c_{i}:c_{i}\mathrm{d}\mathrm{e}=^{i}p_{i}$$S\{x/y\}$$c_{1},$$S$

which begin with the$\mathrm{s}\mathrm{i}_{\ln_{1}}$), respectively, or$y$is substituted for

$x$

in

$S$

.

comnlGnts are attached directly to the corresponding predicates$1\mathrm{e}$“($7_{()}$$\mathrm{m}\mathrm{a}\mathrm{r}\mathrm{l}\backslash ’$$c_{k}:C_{k}=^{f}pk\mathrm{d}\mathrm{e}$to state the synthesis algorithm. In order to help the understand-$\mathrm{o}\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$1$ing of the algorithm.

$\cdots$

where the process.

$c_{i}:C_{i}^{l},\mathrm{d}\mathrm{e}\mathrm{f}=p_{i}\not\in S$

where a free variable’$\mathrm{r}\mathrm{e}\mathrm{s}\iota 11\mathrm{t}\mathrm{i}_{1\mathrm{l}}\mathrm{g}l5$

Now, we are in a )if$c_{1}:C_{1}\mathrm{d}\mathrm{e}t=p_{1},$$S$”. The detail$\mathrm{e}\mathrm{x}\mathrm{p}\mathrm{l}\mathrm{a}11\mathrm{a}\mathrm{t}\mathrm{i}_{011}$

of the algorithm will be stated after

the completion of the algorithm.

Algorithm 4.2
Input:

algorithm]$[\mathrm{S}\mathrm{v}\mathrm{n}\mathrm{t}\mathrm{l}]\mathrm{e}\mathrm{s}\mathrm{i}\mathrm{s}$$\mathrm{E}\mathrm{n}\mathrm{u}\mathrm{m}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{i}_{0}11$

of facts$f_{1},$ $f_{2},$ $\cdots$. It is an enumeration of formulae be satisfied by theintellclecl target process. The order of them is arbitrary.

Output: Sequence of inferred processes $p1,l^{J}2,$to$f_{1}$

mpstart :-$f_{k}$$\cdots$. Each$p_{k}$

satisfies the whole input formulae.

$mp(\{c_{0}:\{\mathrm{t}\mathrm{t}\}\mathrm{d}\mathrm{e}\}=^{\mathrm{f}}0)$.

$r_{()}$

Tlle initial process is$0$.

$mp(S)$ :- % $S$ is a set of process definitions.

read- form$\mathrm{t}ll\mathrm{r}1(f),$$make_{\mathit{1}^{yr}(}ocC0,$ $t5’,$

write-proces.

$f,$$\underline{\backslash }(\mathrm{X}),$$mp(\mathrm{X})$.

$\%_{\mathrm{P}^{\Gamma \mathrm{O}}\mathrm{g}_{1\mathrm{a}\mathrm{m}}}$. %Input a formula.

$\mathit{7}_{\zeta 1}$$\mathrm{x}),$$\mathit{7}_{11}$$\mathrm{C}^{\tau_{\mathrm{O}}}11\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{u}\mathrm{e}$Modify the current process according to the new fact
% the result is set to X.
$\Psi_{(1}$the svnthesis process for$\mathrm{X}$)

2In the following procedures (clauses), we use
intellded

aie explained,

Output the result.

clauses of $rnakeproc\{c$ . S. $f,$$\mathrm{I}\mathrm{n}\mathrm{e}\mathrm{a}\mathrm{n}\mathrm{i}\mathrm{l}$$f$below:)$\mathrm{t}\mathrm{l}$$\mathrm{e}$next fact.

$2$$\mathrm{t}1_{1}\mathrm{e}$several meta variables alld Prolog-like variables whose

91%$\mathrm{t}\mathrm{t}\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\alpha\cdot$$makeproc(c_{i}, S, \mathrm{t}\mathrm{t},s)$

%

makep

$?\cdot oc(c_{i},$makeproc$S,$ $Xi,$ $g_{)}$$(C_{i}, s, x_{j}, \mathrm{X})$$S’arrow$:-

Where $i\neq j$ .

$\mathit{7}_{(1}$$\mathrm{d}\mathrm{e}pj=^{\mathrm{i}}pi\}$$(Cj\cdot s’, \wedge C_{i}, \mathrm{x})$$makeproC(C_{i}, S, x_{j}, \mathrm{X})$$\dot{?}\underline{.\mathrm{G}}-re\eta?t‘\iota\cdot \mathrm{C}$$\langle a\rangle f\ldots\ldots$

makeproc

, ,

.

,

makeproc. S.

.,. . . . . . . . . .. . . . ..... .. .....,.....................

. . . . . . . . . . . . .. . .. , . , .. . . . . . . . . . .. . .. .. . . . . .. . . , . . . .. ,$f,$$\mathrm{X}$). %snch that$\exists c_{?}.\cdot$$c_{i}\neg c_{j}\mathfrak{a}$and makeproc$(cj, ,5’, f, \mathrm{x})$.

.

$\uparrow??akeproC\langle ci\cdot s[ci:C_{ipi}\mathrm{d}=^{\mathrm{e}\mathrm{f}}+a.c_{j}, c.\uparrow:\{\mathrm{t}\mathrm{t}\}\mathrm{d}=^{\mathrm{e}t}0],$$f$

A $(\wedge\{f_{k}|[a]f_{k}\in c_{i}\}),\mathrm{x})$ .

% $[a]f\ldots\ldots.$ . . . .. . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. ... ..... ... ... . ....
$(C_{i}, ,5’, [a]f..5^{\cdot})$

is-valid...... (c):-$(C_{i}, S, \langle r\iota\rangle f.\mathrm{x})$$get_{-new}- l^{jl}oc’.\mathrm{s}.\mathrm{s}- col|..\underline{\sigma}t\prime Lf(cj)$makeproC$\Delta\cdots..(\mathrm{b}^{**})$:-$(ci, s, \langle a\rangle f, \mathrm{X})$$c_{i}$$*\cdots\ldots..(\mathrm{b}^{*})$:-. . . . .. . . . ..

exictss( $C.j,$) $\{X_{j}/x_{i}\}\{Cj/c_{i}\}$ ,. . . . . . . , ............... ........................

$make_{\mathit{1}^{Jro}}c(c_{i}.,5’.f\{x_{i}.).\mathrm{X})$%$\iota \text{ノ}x_{j}.f(x_{j})\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots(\mathrm{b})$.

( $S[c_{jj}:C=pi+\mathrm{d}\mathrm{e}r]-\{c_{i}$ :Ci?nakeproc$\mathrm{v}\cdots\ldots\ldots\ldots(\mathrm{a})$.

: a bound variable corresponding to the formula$x_{j}$. . . . . . .. . ... . . .. ... .

......

$(\mathrm{c}^{*})$..... .. .... .. .. (d)

$:-$

. %

$(\wedge C_{i}\supset[\mathrm{r}]f)$$|=\wedge C_{i}\supset[a]f$$n?akeproc(C|’ S,$ $[(l]f.S[C_{i}:(C_{i}\cup\{[cl]f\})^{\mathrm{d}}=^{\mathrm{e}t}pi])$ :$??ot- tra\iota?.8if(C_{i}, a)$makeproc. %$c_{i}\neq-$.

:-$(ci, s, [\mathrm{r}‘]f, \mathrm{X})$$f_{ora}ll(_{C_{\dot{7}},c_{i}}." 5’[ci:Ci^{\cup\{}[a]f\}=^{\mathrm{e}}IJj\mathrm{d}f], f, \mathrm{X})$%%$\forall c_{j}.Ci\underline{a}c_{j,?}.\mathrm{i}?\mathrm{f}/ke_{P}\uparrow.oc(c,\cdot, 5’[Ci:Ci\cup \mathrm{t}[c\iota]f\}^{\mathrm{d}\mathrm{e}}=pi]\mathrm{f}, f, \mathrm{x})$.

A $f_{2}\ldots\ldots\ldots\ldots\ldots..*\cdots$ $.,$

$f_{1}$.

(ci, S.

?nakeproct$Cj.\mathrm{Y},$$f_{1}.\mathrm{Y}$$f2,$$\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots.\mathrm{r}\cdots\cdots\cdots\cdots\cdots\cdot(\mathrm{e})$:-$makeproC(ci, s, f_{\mathrm{l}}\wedge f_{2}, \mathrm{X})$$\uparrow\eta akep_{\Gamma}oc$$\mathrm{x}$),).

(70 $\nu x.f(x)\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots\ldots$ .
$make_{l^{yro}}C$($c_{i},$

$s$

:

$S$

$f$

the currellt
the cllrrent set ofthe current
the inferred$\mathrm{p}_{\mathrm{l}\mathrm{O}\mathrm{C}}\mathrm{e}\mathrm{S}\mathrm{s}$

:
:

X:

.... .... ... .. ..... .............. ......... (f), l ノ x. $f(x).\mathrm{X}$ ) :-$???a\iota eproC(Ci\cdot S, f(Xi).\mathrm{X})$$\mathrm{c}$.

.

constant (meta valiable)$\mathrm{p}_{\mathrm{l}\mathrm{O}}\mathrm{c}\mathrm{e}\mathrm{s}\llcorner \mathrm{c}\backslash \iota \mathrm{e}\mathrm{f}_{1}1\mathrm{i}\mathrm{i}[\mathrm{i}\mathrm{o}\mathrm{I}\mathrm{l}\mathrm{s}$$\mathrm{f}_{\mathrm{o}11}\mathfrak{n}\mathrm{u}\iota_{\mathrm{a}}$$\square$(nleta)$\mathrm{v}\mathrm{a}\mathrm{J}^{\cdot}\mathrm{i}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}$)to be satisfied bv (metaa set of ptocess definitions (Prolog-like variable)$\mathrm{P}^{\mathrm{l}\mathrm{O}\mathrm{C}\mathrm{G}^{\mathrm{q}}\backslash }\mathrm{c}\cdot-$$\backslash ’\delta 1^{\cdot}\mathrm{i}\mathrm{a}\iota\supset 1\mathrm{e}$$\mathrm{c}$92Now, we)$1\mathrm{a}\mathrm{i}\mathrm{n}$$\mathrm{e}\mathrm{x}_{1}$the intuitive function of the clauses.

. simply return

since tt is satisfied by any processes.
Note that there are no clauses for the formula ff. Since ff indicates that the input formulae(a): If the current forlnula is$\mathrm{t}\mathrm{t}$$S$

are inconsistent, therefore it needs backtracking for this case. By means of backtracking
mechanism, the intended process
be eventually generated.
(b): If the current formula is , return since there already exists a recursive loop. If the(a process variable) which does not correspond to the current processcurrent fornlula is)(i.e.
constant
with needs modifications, since must satisfy the formulawhich must be satisfied bv . Therefore, in the clause identify and at first, then modify(See Fig. 2). The third clause incase of logicalagain to satisfy every condition in$\backslash \^{r}\mathrm{i}\mathrm{l}1$$S$$x_{j}$$x_{j}$$c_{i},$$S$$c_{i}$$c_{i}$$c_{i}$$c_{j}$$c_{j}$$C_{i}$$c_{j}$$\mathrm{v}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{a}\mathrm{l})\mathrm{l}\mathrm{e}$$\nu x_{j}.f(x_{j})$$x_{j}$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}$will ) invoked when identification of

and

$1$

$\mathrm{e}$$c_{i}$

makes contradiction. They may$c_{j}$

from the direct recursive loop. i.e. wrong connection of$c_{i}$

and$c_{j}$$\mathrm{a}\iota\cdot \mathrm{i}\mathrm{s}\mathrm{e}$. However, this is not always

the cases. Therefore. we need a controlling predicate. The predicate, -remake, judges
whether or not unfolding ofis necessarv in such a way that is-remake succeeds iff$i_{\mathit{8}}$$\nu x_{j}.f(x_{j})$the unfolding of the
explained after the$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{n}\tau\iota 1\mathrm{l}\mathrm{a}l\text{ノ}x_{j}.f(x_{j})$$\mathrm{e}\mathrm{x}_{1^{)}}’ 1\mathrm{a}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$(c): If the current

with

$a$

$\mathrm{f}_{0\Gamma \mathrm{n}1}\mathrm{u}\mathrm{l}\mathrm{a}$is necessary. Its intended function (meaning) will beof the algorithnl.

is of the fornu ($a\rangle f,$

and constructs a new process satisfying

already exists an -successor$a$$c_{j}$

ofsuch that$c_{i}$

tlle clause generally makes a branch labeled
as an -successor of

$f$

$a$

$c_{i}$. However, if there

can be modified to satisfy , then neither$f$$c_{j}$

new constants nor new processes are created. Otherwise, the clause creates a new branch
by getting a fresh process constant .
followed by a(d): For the current formula $[a]f$ every -successor must be checked and modified to satisfy
the subformula . This is done by the last clause of this case. This check can be easily verified
ifconditionholds. This is
we attach the condition to each process
definition, i.e. a process constant. If cannot
the action , it is sufficient to add $[a]f$$c_{j}$$\mathrm{n}\mathrm{e}\backslash \mathrm{v}_{1)}\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}$

$a$

$f$

$|=\wedge C_{i}\supset[a]f$$\mathrm{t}1_{1}\mathrm{e}$$\mathrm{w}1_{1}\mathrm{y}$to$C_{i}$$a$$\mathrm{p}\mathrm{e}\mathrm{r}\mathrm{f}\mathrm{o}\mathrm{r}\ln$$c_{i}$.

(e): If the currellt formula is a conjunction$f_{1}$

A$f_{2}$, apply$f_{1}$

and$f_{2}$(f): For the recursive formula l ノ ‘t. $f(!)$ , rename the bound variableto$c_{i}$

in this order.
$x$

into

$x_{i}$

to adjust it,

Whenever tllc
tries to make a$\mathrm{f}\mathrm{o}\mathrm{l}\cdot 1\eta 11\mathrm{l}\mathrm{a}\nu x.f(x)$at the nearest$1\mathrm{o}\mathrm{o}_{1^{)}}$

is$\mathrm{a}\mathrm{p}\mathrm{l}$)$\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{t}\mathrm{l}$$1^{)}1\mathrm{a}\mathrm{c}\mathrm{e}$to a process constant, the procedure makeproc

from the$\mathrm{a}\mathrm{p}\mathrm{l}$)$\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{d}$process constant. Especial, for the

first time, it tries to nlake direct lool) to the applied process constant. However, making aloop at the nearest place sometinles conflicts with the facts. Such situations are illustrated

in the Fig. 3 alld 4. In Fig. 3, the direct loop created at the first stage by the formula
conflicts with the third fact$\nu x_{0}.\langle a\rangle\langle b\rangle x_{0}$to avoid the conflict. In Fig. 4, the )$1$stage hasthis$\mathrm{p}_{\mathrm{o}\mathrm{t}\mathrm{e}11}\mathrm{t}\mathrm{i}\mathrm{a}\mathrm{l}1^{10}\backslash \mathrm{e}\mathrm{r}$.

$\mathrm{e}\mathrm{x}\mathrm{a}\mathrm{l}\mathrm{l}\tau \mathrm{p}\mathrm{l}\mathrm{e}$$\mathrm{T}1_{1\mathrm{e}11}$.

$\mathrm{f}\mathrm{l}\mathrm{l}\mathrm{e}$to make a$[a][b][b]\mathrm{f}\mathrm{f}$$\Gamma \mathrm{O}\mathrm{C}\mathrm{e}\mathrm{s}\mathrm{s}$. Thus, the direct loop must be unfolded

constant$1\mathrm{o}\mathrm{o}_{1^{)},1^{)}}\mathrm{o}\mathrm{s}\mathrm{S}\mathrm{i}\mathrm{b}1\mathrm{v}\backslash$$c_{1}$

with the condition

actuated by some facts, e.g.

created direct loop conflicts with the third fact

To avoid the unnecessary nfoldings$1\iota$)$\mathrm{o}\mathrm{f}1_{0}01$$\mathrm{S}$$[b]x_{0}$, the$\mathrm{I}$)$\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{e}\mathrm{d}\mathrm{u}\Gamma \mathrm{e}$$[c]\mathrm{f}\mathrm{f}$at the first$[a]\langle b\rangle\langle c\rangle \mathrm{t}\mathrm{t}$in.

, is-remake, checks whether or

93

not the current process is in the situations in Fig. 3 or 4 whenever invoked, that is the current

process does not satisfy the given facts. Then, is-remake forces backtracking if the current
process is not in the situations in Fig. 3 or 4. Otherwise, the procedure succeeds, i.e. direct
loops are unfolded once stated as above. In the case illustrated in Fig. 3, is-remake traces thepath which is passed by a formula occurring inconsistent, and backtracking is allowed if thepath has one or more loops and does not end on these loops. In the case of Fig. 4, is-remake

traces the path in the same way as the previous case, and backtracking is allowed if the pathis at the beginning of aloop, but does not go inside the loop, instead takes the different path.
In each case, the information about which formula made each branch is needed.

$\mathrm{E}\backslash 2$$\mathrm{E}3$

4.3: Some action$\sec_{1}\mathrm{u}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}\mathrm{S}$$(\mathrm{b}^{*})$.

are possible since a loop is constructed.

Results of the Algorithm

Lemma 4.3 Let$c:C\mathrm{d}\mathrm{e}\mathrm{I}=p\in S.$$\mathrm{X}\equiv S$: The function of the clause

If

except that$con\mathit{8}tants$. Also if$S$

be a set of$f$

is a formulo such thot $c|=f$ then.makeproc $(c, s, f,\mathrm{X})$ terminates with

$se\iota$$f$$l^{Jr\mathfrak{X}ess}$) $eralforn?ul\zeta rC\mathrm{t}1?ay$

has been

clefin itio

$ns$applied to the predicate makeproc andbe $ad_{C}led$ to some sets of $f_{orm}u\tau ae$ labeled at process$q\tau_{\Gamma ea}rl_{l}/r_{l^{J}\mathit{1})}‘ lied$

to $mr\iota keproC,$$S\equiv \mathrm{X}$.

$\square$94. 4: Some action sequences are possible since a branch modifies a loop.
satisfying initial segments
me that there exists a processof an enumemtion of facts, $u’ her\epsilon?1\geq 1$ . Assume Algorithm 4.2 outputs a set of process, we have the,also. For the n-th fact,
for the $n-1f_{C/C}ts,$definitions

Theorem 4.4$As_{\mathrm{c}}\sigma \mathrm{t}$$f_{1},$$p_{n}$$S_{n-1}$$f_{1},$$f_{n}$$f_{n-1}$$\cdots$$\cdots,f_{n}$followings:

terminates and returns an output, which(the initial state of ).
with the process

1. The algorithm ’$i\mathit{8}$$A^{/.\mathit{2}}$2. $c_{0}u’ iths_{n}$ satisfies
3.

$\mathrm{c}_{0}$$f_{n}$.

with $S_{n}sati.\sigma fiesf1,$

proof 1. When the )$definiti_{on\mathit{8}}$$S_{n}$$conSt\zeta|\uparrow?t_{C_{0}}$$S_{n}$

a set of process$\cdots$$\mathrm{r}\mathrm{e}\mathrm{d}\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{e}$$1$, $f_{n-1}$ .

makeproc calls itself recursively, let $f$ be a given formula to it,–the number of operators constructing
inandthe formula –can be greater than the size of , only in the clauses, the algorithm terminates.
andthe Algorithm 4.2. Without using the clauses
and

$g$

be a

$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{n}\mathrm{l}\mathrm{u}\mathrm{l}\mathrm{a}$to call itself. Then, the size of

$g$

$f$

$(\mathrm{b}^{*}),$

Therefore, it is sufficient to consider$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{m}$$(\mathrm{b}^{*}),$$(\mathrm{b}^{**})$$(\mathrm{b}^{**})$$(\mathrm{c}^{*})$$(\mathrm{c}^{*})$

only. Instinctively, the non-termination of thealgorithm means the following cases.
(i) Application of a set of formulae continues infinitely many times as if it is a chain reaction.
, the algorithm adds a new branch from the. In
This situation corresponds to$(\mathrm{c}^{*})$

current process definition. A )$1$$\langle$$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{S}$$\mathrm{c}^{*})$

after the brancll must satisfy every formula in thedefinition. However, another process definition may be added
again. If the above
as a new branch by the process, and the algorithm may arrive atlabeled set at$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}_{\mathrm{I}^{)}}\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{S}$$(\mathrm{c}^{*})$

situation contillues, the )$\mathrm{r}\mathrm{e}\mathrm{d}\mathrm{i}\mathrm{C}\mathrm{a}\mathrm{t}\mathrm{e}$$1$makeproc does not terminate.

(ii) Process reconstruction continues infinitely many times. This case corresponds to. The clause$(\mathrm{b}^{*})$

makes a loop as short as possible to satisfy a formula witha operator. However, in the cases of Fig. 3 and 4, the loop must be unfolded once
. Unfortunately unfolded loop may also be in the situation
by backtracking at

and$(\mathrm{b}^{**})$$(\mathrm{b}^{*})$$\nu$$(\mathrm{b}^{**})$

again. Repeating the above, process reconstruction
continues infinitely manv tilnes. Note tllat in this case, makeproc synthesizes one orwith infinite depth.
moreof Fig. 3 or 4 and arrive at$.\mathrm{n}$$\mathrm{b}\mathrm{r}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{c}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{S}$$(\mathrm{b}^{**})$

95

Suppose the given enumeration of facts has noarise, since both of definitions$\nu$

operator. Then the case (ii) dose notare not used. We consider only the case (i).
)
However, sincehasvariable, the size of a formula used for recursive
call inis less
one given to it. Consequently, the algorithm.
Next, we assulne thatexists a formula with in enumeration of facts. We have thefollowing cases.
and$(\mathrm{b}^{*})$$(\mathrm{b}^{**})$$\mathrm{e}\mathrm{a}\mathrm{c}1_{1}\mathrm{f}_{0}\Gamma 111111\mathrm{a}$$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}$$11\mathrm{O}\mathrm{I}$$\mathrm{t}1_{1}\mathrm{a}\mathrm{n}$$(\mathrm{c}^{*})$$\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{i}_{1}1\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{S}$$\mathrm{t}1_{1}\mathrm{e}\mathrm{r}\mathrm{e}$

$\nu$

.

Only the case (i) is arisen.
From the previous lemma, $n\hat{\{}akeproc$ neither makes new branches nor process definitions
from awhich are already given. Since the size of each element of a set of formulae$\mathrm{f}\mathrm{o}\mathrm{r}\iota\eta 11\mathrm{l}\mathrm{a}$for each )$1$$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{S}$definition is finite. the set of formulae can be applied within only finite

range of the process. Therefore.

$\mathrm{a}_{1^{)}\mathrm{p}\mathrm{o}\mathrm{n}}1\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{i}$of formulae is saturated in finite time, andmakeproc terminates.

$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{n}$Onlv the case (ii) is arisen.
The definition

given
is-re

$\mathrm{f}_{0\Gamma \mathrm{n}}1111\mathrm{a}\mathrm{e}\backslash ^{r}$$?nclk\epsilon$. A

unfolds a loop once. To arise the case (ii), there must exists some$(\mathrm{c}^{*})$

hich negate the loop infinitely nuany times and satisfy the condition of$\mathrm{f}_{0\Gamma \mathrm{n}1}\iota\iota 1\mathrm{a}\backslash \backslash ’ \mathrm{i}\mathrm{t}\mathrm{h}_{0}\mathrm{u}\mathrm{t}$operator cannot negate it infinitely. Even if there islノ

a formula with l ノ operator, the )which negates the loop, i.e. the formula ff, must$\mathrm{a}\mathrm{r}\mathrm{t}$$1$occur periodically. Therefore when a loop is unfolded fillitel.v many times, the formula
not only llegatcs points inside a.

$is- rel??ak\mathrm{r}$fails andbut also negate.s points outside the loop. Hence$1\mathrm{o}\mathrm{o}_{1^{)}}$

terminates.

$?7?\mathrm{r}k\epsilon proC$.

Both the cases (i) and (ii) are arisen.
$\mathrm{t}\backslash ^{\gamma}\mathrm{e}$can assume that both the cases (i) and (ii) arise alternatively. Then, firstly, someformulae negate the point of a loop, and thus the loop is unwound. Next, a set offornlulae, which is labeled at a process definition, are applied to the unwound loop

or certain branches. After all, the transmition of formulae arrives at the point of theloop, and$\mathrm{t}\mathrm{h}\mathrm{e}_{\mathrm{b}\mathrm{e}}$processes are

one formula$\backslash \backslash ’ 1\mathrm{l}\mathrm{i}\mathrm{C}\mathrm{h}$similar the )$\mathrm{r}\mathrm{c}\backslash \cdot \mathrm{i}\mathrm{o}\mathrm{u}\mathrm{s}$$1$have one or lnoreone.

2. By the following procedure.
procedure is-sati.

case

$f$

. To negate infinitely, there must exist at most$\mathrm{r}\mathrm{e}_{1^{)\mathrm{e}\mathrm{a}}}\mathrm{t}\mathrm{e}\mathrm{d}$$\mathrm{s}fied(f, i)$$\mathrm{a}11(1$$\nu$operators and negates the loop. This argument

thus the algorithm ternlinates.

$\uparrow.\underline{\sigma}- sati.\underline{\sigma}fi\xi_{-}d(f_{n}, i)$, we make sure that.

$c_{i}$

satisfy$f_{n}$.

:

oftt : Obviously $c_{i}|=f$ .
ff : It$\mathrm{n}\iota \mathrm{e}\mathrm{a}\mathrm{n}\mathrm{S}$case does$\langle a\rangle f’$that there does not exist a process which satisfies$1\iota \mathrm{o}\mathrm{t}$is$\mathrm{a}\mathrm{p}\mathrm{l}$)$\mathrm{u}\mathrm{t}$formulae. Thus, thisarise.

: From the algorithm, there exists$\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{d}$)$\mathrm{i}\mathrm{n}\mathrm{l}$. This . also satisfies$c_{j}$$c_{j}$$c_{i}\underline{\mathfrak{a}}c_{j}$such that makeproc selects it when the formula. Then make sure$is-.\underline{8}ati_{S}fied(f’,j)$is satisfied.

96$[a]f’$: If$c_{i}\neq-$. then obviously

is satisfied for any: Make sure$g\wedge h$$\nu x.g(x)$$x_{i}$$c_{j}$$c_{i}|=f$.

$\mathrm{I}\mathrm{l}1$

the case that$c_{i}\underline{a}c_{j}$, make sure is-satis fied$(f’,j)$.

$i_{-}.\backslash -.\underline{8}at_{S}‘ fied(g, i)$a‘lld is-satis fied $(h, i)$ are satisfied.

: Make sure is-satisfied $(g(X_{i}), i)$ is satisfied.

.

: Let its original formula behere,$c_{j}|=g^{n}\langle \mathrm{t}\mathrm{t}$. Suppose$x_{j}=x_{i}$. Since the procedure comes) where reconstructing loops for the original formula arise in $n-1$

times and $n\geq 1$ . As$c_{j}|= \bigwedge_{n\geq 0}g^{n}(\mathrm{t}\mathrm{t})$$\nu x_{j}.g(x_{j})$$J^{n}\mathrm{r}(X\dagger$. Therefore

is monotonicity for $n,$$\backslash ’ \mathrm{e}$$\mathrm{r}\mathrm{e}\mathrm{p}\mathrm{e}\mathrm{a}\mathrm{t}\mathrm{i}_{1\mathrm{l}}\mathrm{g}$this procedure leads toshow that $c_{j}|=\nu x_{j}.g(Xj)$ . Since length of each input

formula is finite and the synthesis algorithm terminates, the procedure terminates infinite st,eps.

3. Same as 2.

$\square$

The algorithm is a non terminating procedure. Therefore, we show its correctness byusing the concept, of convergence in the linlit, which has been a. key idea in inductive learning
paradigm [21].

Definition 4.5 Assume an algorithm reads in an enumeration of facts, and returns processes
sequentially. After sonle time, if the output )$1$by thisLemma 4.6
Algorithm 4.2
We

converges in$\mathrm{a}_{0}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{h}\mathrm{l}11$$As.\backslash \iota/’ nep$

$cotl?’ er\mathrm{c}Je\underline{.\sigma}$$\mathrm{c}\mathrm{o}11\mathrm{S}\mathrm{t}_{\Gamma \mathrm{U}\mathrm{c}}\mathrm{t}$is$\zeta(?l$$\mathrm{t}11\mathrm{C}$is always , then the inferred sequence$p$limit to ) over the enulneration of facts.

$\square$$l$inte nded process. and the inferred sequence ofin thea formula$\Gamma \mathrm{O}\mathrm{C}\mathrm{e}\mathrm{s}\mathrm{s}$$/i\uparrow?\iota$

it to a process$p’$. Then$p\leq_{dp’}$$p_{\Gamma OCes}seS$by the.

.

$\square$has suificient information to synthesize a process. For$\backslash \mathrm{v}\mathrm{h}\mathrm{i}\mathrm{c}\mathrm{h}$preliminary, we need the following definition.

Definition 4.7 If a set of )$1$$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}$dcfinitions

complete set of proccss rlefinition,.-q of a )$\mathrm{I}$

1.

$S$

has the initial process$\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{e}\mathrm{S}\mathrm{s}_{\mathrm{P}}$.

$cl_{i}\in A$$p\sim c_{0}$$c_{i}$a.

$c^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}}\mathit{0}1\cdot C1+\cdots+a_{n}.c_{n}$and each$S$:such that$\mathrm{d}\mathrm{e}\mathrm{f}\mathrm{i}1\dot{\mathrm{u}}\mathrm{t}\mathrm{i}_{0}\mathrm{n}C0=p\mathrm{d}\mathrm{e}t0$

2. Each process definition is of the form
$a_{1}.c_{1}+\cdots+\mathrm{r},.{}_{\mathrm{t}}C_{n}\mathrm{d}\mathrm{e}I=0)$

satisfies the following conditions, we call$S$

is a )$1$$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{S}$, where$\mathfrak{j}\geq 0$

constant whose )$1$(when $n=0$ ,$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{S}$definition

belongs to.5’.

3. For anv process definition$c\mathrm{d}\mathrm{e}\mathrm{f}=q$definitions is not equivalent toEvery guarded )$1$$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}_{l}J$

the following algorithm. We

$p$

in S.

. i.e.

in the deleted set$c_{0}$$c_{0} \oint p$)$\mathrm{r}\Theta \mathrm{S}\mathrm{e}11\mathrm{t}$this setof process

any more.

can be translated to a$\mathrm{r}\mathrm{e}_{1}$$S-\{c\mathrm{d}\mathrm{e}\mathrm{f}=q\}$$\mathcal{P}-(l’)$)$\mathrm{C}\mathrm{o}\mathrm{m}1^{1}$$\mathrm{e}\mathrm{t}\mathrm{e}$set of process definition of

$p$

by

.

Algorithm 4.8 Let be a guarded process and a set of process definitions associated with. At first, get a fresh process constant which is llot included in , then add
to .
.
Finally apply
rules to until is not modified any more.
$S$

$p$

$p$

$S$

$c_{0}$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{l}\mathrm{o}\backslash \mathrm{V}\mathrm{i}1\uparrow \mathrm{r}\mathrm{a}11\mathrm{S}\mathrm{r}_{\mathrm{o}\mathrm{f}}1\mathrm{l}\mathrm{u}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}11$$\ell\text{\c{a}}$$S$$c0^{\mathrm{d}\iota}=^{\mathrm{e}}p$

$S$

97

1. If

and

$c^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}}a_{l}.j\in S$

is not a )$l^{J}$$1$$Sarrow S[c^{\mathrm{d}\mathrm{e}}=^{\mathrm{f}}a.c’, c^{J^{\mathrm{d}}}=^{\mathrm{e}\mathrm{f}}p]$2. If$c^{\mathrm{d}}=^{\mathrm{e}\mathrm{f}}p+0\in S$

3. If$c^{\mathrm{d}\mathrm{e}}=^{t}p+p+r\in S$

4. If$c^{\mathrm{d}}=^{\mathrm{G}\mathrm{f}}p+a.q\in S$

and

5. If

6. If
7. If

then

and

$c^{\mathrm{d}}=^{\mathrm{e}l}c$

and’is a )$c’$$1$$b.c_{2},$is not a )

$q$

. if

and

$c$

$l^{\iota- \mathrm{c}\mathrm{a}}1\mathrm{C}111\iota 1\mathrm{S}$and completeness

$p$

for

full 1$p$$\square$. Observe that$c_{0}$$l^{J\Gamma O}ce.\underline{\sigma}s_{\mathit{1}^{J}}$

in

and

$S$

$c_{0}$

in$\mathcal{P}-(c\mathrm{o})$$q$cannot use. For processes$\mathrm{n}\tau \mathrm{e}\mathrm{a}\mathrm{n}\mathrm{s}$$\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{i}_{\mathrm{V}\mathrm{a}}\iota \mathrm{e}\mathrm{n}\mathrm{t}$.

, Algorithm 4.8 terminates and $P(p)$ is a complete set$‘- \mathrm{c}\mathrm{a}\mathrm{J}\mathrm{c}\iota 1\mathrm{l}\mathrm{U}\mathrm{S},$)$\mathrm{e}\mathrm{x}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{l}\mathrm{l}$$\mathrm{l}\mathrm{e}$$\mathrm{s}\mathrm{t}\mathrm{i}_{\Gamma 1\mathrm{i}_{1}}[24]$$\mathcal{F}(l^{)})$

sllollld beso$c_{\mathit{1}},$$\mathrm{t}/nClneSs$$lJ\leq_{d}c_{\mathit{1}}$means

the inductive$l’=a_{l^{J_{1}}}.+a_{l^{J_{2}}}.$$l^{)}1$)$\mathcal{F}(l))$

and$1\mathrm{o}\mathrm{o}_{\mathrm{I}^{)\mathrm{s}\mathrm{o}}1}1$$C$

w.r.t.

implies$q|=\mathcal{F}’(p)$, then we have

. Unfortunatelv our restricted calculus
for . So it seems that$p$$p_{2}\mathrm{n}\tau \mathrm{a}\mathrm{y}$$\leq_{d}$in our$q|=\mathcal{F}(p)$)$\mathcal{F}_{S}(C)[C]$$\mathrm{l}\mathrm{e}\mathrm{t}\mathrm{e}\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{n}\tau \mathrm{u}\mathrm{l}\mathrm{a}$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{I}$is a family of sets of )$1$$\Gamma \mathrm{O}\mathrm{C}\mathrm{e}\mathrm{s}\mathrm{s}$for all processes$\mathcal{F}’(p)=\langle a\rangle \mathcal{F}’(p_{1})\wedge$

no

${ }$

operators. We$\mathcal{F}(l))=\langle a\rangle \mathcal{F}’(p1)\wedge(a\rangle \mathcal{F}’(p_{2})$$\wedge\langle r‘\rangle \mathcal{F}’(l^{y}2)\wedge[a]\wedge(\mathcal{L}_{d}(\iota y1)\mathrm{n}\mathcal{L}_{d}(l^{J}2))$of a soul](1 and$1_{1}\mathrm{a}\mathrm{s}$have common properties, i.e.

is a formula which is logicallv equivaJellt toprocess constants and$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{a}\mathrm{t}_{\mathrm{P}}\leq_{d}q$$p$.

definition. The funclion $F(p)$ with the auxiliary function$\mathrm{f}_{0\Gamma \mathrm{n}\mathrm{l}\mathrm{a}}\mathrm{t}\mathrm{i}_{01\iota}$

for a process

the sense that $p\sim q$ iff, consider the process$\langle\zeta‘\rangle \mathcal{F}’\{l^{J}1$$\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{n}1}\mathrm{u}\mathrm{l}\mathrm{a}\mathcal{F}(p)$gave the formation of the sound and complete formula$\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{i}_{\mathrm{V}\mathrm{a}}1\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}\sim \mathrm{i}\mathrm{n}$operators to define

${ }$

alld

$p$

that $q\models F\{p$ ) inlplies

But this is not sufficient sincerecursive

are strongly$c_{1}\mathrm{d}\mathrm{e}\mathrm{f}=$$\square$$\langle a\rangle \mathcal{F}’(p_{2})\wedge[a](\mathcal{F}’(l^{J_{1}})\vee F’(p_{2}))$$\mathcal{F}_{S}(C)[c]$$\mathcal{P}-(c\mathrm{o})=\{c_{0}\mathrm{d}\mathrm{e}\mathrm{f}=a.c_{1},$of .

w.r.t. the strong

and . As an

Thus

is guarded.

$l^{J}$

restricted$\mathcal{F}’(p)$$p$dose not occur in any otller process definition then

, then$\zeta\tau_{efi’?1}\cdot ti_{or\mathit{1}_{\mathrm{c}}}\sigma$

$c’$

.

$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{n}Sarrow(S-\{c^{\mathrm{d}}=^{\mathrm{e}\mathrm{r}}c\}’)\{c/c’\}$Now, we can con struct a sound and complete

In

since

$c\neq c’$.

Lemma 4.9 For $a’ ?y$ gnarded$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}$. Note that$,5^{\cdot}=\{\mathrm{c}_{0}\mathrm{d}\mathrm{e}\mathrm{f}=\mathrm{r}.c_{1}, c_{1}\mathrm{d}\mathrm{e}\mathrm{f}=b.(c_{0}+c_{1})\}$$c_{2}=\mathrm{d}\mathrm{e}\mathrm{f}a.c1+b.c_{2}\}$of process$Sarrow S[c=^{\mathrm{e}}\mathrm{d}\mathrm{r}p+q]$

constant,)$\mathrm{r}\mathrm{o},\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}$

.

then

$\Gamma \mathrm{O}\mathrm{C}\mathrm{e}\mathrm{s}\mathrm{s}$.

constant then get a fresh process constant$1$$c^{\mathrm{d}}=^{\mathrm{e}t}q\in k5^{1}\backslash \iota\cdot \mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}c\neq c_{0}$$\mathrm{e}\mathrm{x}\mathrm{a}\mathrm{m}_{1^{1}}$ $\mathrm{e}$and.

$S-S[c^{\mathrm{d}\mathrm{e}}=^{\mathrm{f}}p+r]$$c^{J^{\mathrm{d}\mathrm{e}\mathrm{f}}}=q\in S$$Sarrow S-\{c^{\mathrm{d}\mathrm{e}\mathrm{f}}=q\}$

For

then

$Sarrow S[c^{\mathrm{d}\mathrm{e}}=^{t}p+a.c’, c^{\prime^{\mathrm{d}}}=^{\mathrm{e}}q]t$$c^{\mathrm{d}\mathrm{e}}=^{t}p+c’$

$c’$

.

$Sarrow S[c^{\mathrm{d}\mathrm{f}}=^{\mathrm{e}}p]$andconstant then get a fresh process constant$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}$)$\cap \mathcal{L}_{d}(p_{2})\neq\emptyset$.

though it is not inductivein the next definition gives

for a process$\wedge(\bigcap_{C\in}c, \mathcal{L}_{d}(c))$

constants.

$\mathcal{L}_{d(l^{J_{1}}}$

.

$p$

ill

$\mathcal{L}_{d}$. Instinctively,, where $C$ is a set ofis used technically to make$C$

forlnulae.

Definition 4.10 Let ,5’ be a
be a set of subsets of$C_{0}’$. For)$\mathrm{C}\mathrm{o}\mathrm{m}1^{1}$$\mathrm{e}\mathrm{t}\mathrm{e}$$Ci’\subseteq C_{0}’$set of process definitions,. a formula$F_{\backslash ^{\neg}}.(C’)[C^{2}]$$C_{0}=\{c|c^{\mathrm{d}\mathrm{e}\mathrm{f}}=p\in S\}$

and

$C$

is defined ill the following mutual

recursive equations:$[n]\mathrm{f}\mathrm{f}$$C_{JS}(C,a)[C’]$

$=$

$\{$

if $c\neq$ for anv $c\in C$ .
if there exist$[r‘](F_{3^{\neg(\bigcup_{C\in}.()}}c-\backslash C,a)[C])$

{

$c,$

$c’\in C$

such that$C\underline{a}$$\wedge C’.\in coml)\mathrm{t}\{S\langle C.,1)|C\in c\})\langle\zeta’\rangle(\tau S((^{-_{t}\prime})[C\tau]\mathrm{I})\wedge[a](F.5\backslash (\bigcup_{c\in}C, \cdot,\sigma(c, r\iota))[C’])$and $c’\neq’$ ,otherwise.

98.

if $C\in C$ ,$a_{C}$$=$$\mathcal{F}_{S}(C)[c]-$$\{$otherwise.

’ ノ xc’. $\bigwedge_{a\in A}(\mathcal{G}S(c, a)[c\cup\{C\}])$’
and $CO???b(\{c_{\text{ }}1, \ldots , C_{n}\})=\{\{c_{1}, \ldots , c_{n}\}|c_{1}\in c_{1},$ $\ldots,Cn\in$where $s(c, a)=\{c’.\in C|carrow C\}\mathit{0}$is thewhere
for $n\geq 0$ . For a guarded process , we defineノ$C_{n}\}$$F(p)\mathrm{d}\mathrm{e}\mathrm{f}=\mathcal{F}_{P(p)}(\{c\mathrm{o}\})[\emptyset]$$p$

initial process constant of
Let considerthen$\mathcal{F}(c_{0})$$c_{0}$.

$\mathcal{P}-(p)$$\square$and $A=\{a,b\}$ ,$S=\{c_{0}\mathrm{d}el=a.c_{1}, c_{1}\mathrm{d}\mathrm{e}\mathrm{f}=a.c_{2}, c_{2}\mathrm{d}\mathrm{e}\mathrm{f}=a.c_{0}+a.c_{1}+b.c_{1}\})$

is given by the following equations, where a family of sets of process constants isomitted.
A$\mathcal{F}(c_{0})=FS(\{C_{0}\})$$=$$l\text{ノ}x_{\mathrm{f}c\}}0^{\cdot}\langle\zeta l\rangle \mathcal{F},5^{\neg(}\{C.1\})\wedge[a]\mathcal{F}_{3}\backslash (\{c_{1}\})$$\mathcal{F}_{S\{}\{c1\})$$=$$l\text{ノ}X\{_{C}1\}\cdot\langle\prime l\rangle \mathcal{F}_{S(}\{c2\})\wedge[a]\tau_{s}(\{C2\})\wedge[b]\mathrm{f}\mathrm{f}$$\mathcal{F}_{S}(\{c_{2}\})$$=$$l\text{ノ}x_{\{c}2\}\cdot\langle cl\rangle.?.\{_{C}0\}\wedge\langle a\rangle x_{\{}\mathrm{c}1\}^{\wedge[}\mathit{0}]Fs(\{c0, c_{1}\})\Lambda\langle b\rangle x_{\{c\}^{\wedge}}1[b]X\{\mathrm{c}_{1}\}$$\mathcal{F}_{S}(\{c0, C_{1}\})$$=$$\iota \text{ノ}x_{\{\}}.\langle C0,C1\prime l\rangle F_{3}\neg(\{_{C_{1}}, C_{2}\})\wedge[a]F_{S}(\{C1, C2\}\mathrm{I}\wedge[b]\mathrm{f}\mathrm{f}$$\mathcal{F}_{5^{\neg}}(\{_{C,C_{2}}1\})$$=$$l\text{ノ}x_{\mathrm{f}\}}\mathrm{c}1,C2^{\cdot}\langle a\rangle \mathcal{F}.5(\{\neg c0, c2\})\wedge\langle a\rangle x_{\{cc_{2}\}}1$$\mathcal{F}_{S}(\{C_{0}, C_{2}\})$$=$$l\text{ノ}x_{\{cc_{2}\}}.\langle 0,\mathit{1}\zeta\rangle x_{\{c_{0},c_{1}}\}\wedge\langle a\rangle X\{C_{1}\}\wedge[a]x_{\{\mathrm{C}_{0}},c1\}\wedge[b]x\{C_{1}\}$$\mathcal{F}_{S}(\{c0,C_{1}.C2\})$$=$$l\text{ノ}x_{\{_{\mathrm{C}_{0}.C_{1^{C_{2}}}}.\}}.\langle \mathit{0}\rangle x_{\{_{C_{1\underline{9}}}},\}\wedge\langle cl(\rangle x_{\{_{C}0^{\mathrm{c}}1\cdot 2},\mathrm{C}\}\wedge[a]x\{c_{0}.c_{1},c’\}^{\wedge[b}\sim]x\{c1\}$We$\mathrm{s}\mathrm{l}_{1}\mathrm{o}\mathrm{w}\mathcal{F}\mathrm{t}p$$[b]\mathrm{f}\mathrm{f}$A,) is a sound and)$\mathrm{t}\mathrm{e}$$\mathrm{C}\mathrm{O}\ln_{1^{1\mathrm{e}}}.$

formula of$l^{J}$$[a]\mathcal{F}_{S(\{c_{0},c_{12}},$$C\})\wedge[b]x\{_{C\}}1$

in the following lemmas and propo-

sition.
Lemma 4.11

$L\epsilon tS$

a set of subsets of$C_{0}$

be a complete.

$-\sigma ct$. For cm

Definition 4.12 For two )$1$of$\mathcal{P}-(l))$

and$C_{q}$

and$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{e}\mathrm{s}_{l^{J}}$defined ill$\{c_{0}\}=_{p.q}\{c_{0}’\}$

3. For$C’\}$$\mathrm{r},$$C\subseteq C_{\rho}$$C_{p}$

andand$C_{q}$$c_{0}’\in C_{q}$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{f}\mathrm{o}\mathrm{l}1_{0}\backslash \iota’ \mathrm{i}\mathrm{n}\mathrm{g}$

.

$C$

be

$\square$be the sets of all process constants
be initial process constants of$C_{p}$

and$C_{q}$$C_{p}$

is a binary relation:$\{c_{i}’’\}c_{i}\underline{a}c_{\mathrm{i}}’’,$$C’\subseteq Ci_{q}’$alld $C’=\{c_{1}’, ..’. , c_{m}’\}\subseteq C_{q}$ , suppose $C=_{p,q}C’$ . Then for$1\leq i\leq n\}=_{p,q}\{c_{j}^{\prime\prime/}|c_{j}’arrow c_{j}’’’, 1a\leq j\leq???\}$.

$\mathrm{c}’a/’\in$C’,$, if $(’=_{l^{1}}.{}_{q}C’\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{l}\mathrm{l}\{c’’|cc’, c\underline{a}’\in C\}=_{p,q}\{c’’’|c’arrow

for any action .

and $P(q)$

and

.

and

$\square$$r$

Lemma 4.13 For

.

. let

$c|=\mathcal{F}_{S}(C)[C]$$5l$$C=\{c_{1}, \ldots, c_{n}\}\subseteq C_{p}|$$c’$$c_{\mathit{1}}$$C_{0}=\{c|c^{\mathrm{d}\mathrm{e}}=^{t}p\in S\}$

respectivelv. The corre. )$onded$ relation over subsets of

2. Forany action

Let

and

, and $c_{0}\in C_{p}$$=_{p,q}\subseteq 2^{C_{\rho}}\cross 2^{C_{q}}$$P(p)$$a\uparrow?yc\in C,$$\mathcal{P}-(’/)\Gamma \mathrm{e}\mathrm{s}_{1^{)\mathrm{e}\mathrm{c}\mathrm{t}}}\mathrm{i}_{\mathrm{V}\mathrm{e}\mathrm{l}\mathrm{y}}$’1.

$yC\subseteq C_{0}$of process definitions,and for.

,$\zeta|’?dC0\in C_{p}$$C\subseteq C_{p}a\uparrow?dC’\subseteq C_{q}$$|=\mathcal{F}_{\mathcal{P}(p)}(C)[c]$’ $a$$t_{1O}.p\Gamma oce.- 9.\underline{\sigma}e.\underline{\sigma}l$and,$\mathit{1}dq,$$c_{0}’\in C_{q}$$/\epsilon tC_{p}$

be

and

,

$C_{q}$$i\uparrow?ifiC\downarrow ll^{Jr\mathit{0}Ce.\mathrm{s}.\mathrm{q}}--$

be the set of all process constants ofrespectively.
andconstants of$C_{p}$$C_{q}’$and suppose $C=_{p,q}C’$ and for any $c’\in C’$ for some

. If $c|=f$ for$c\in C,$ $t/,e\uparrow?C’|=f$for $c’\in C’$ .

$C\subseteq 2_{-}^{C_{\mathrm{p}}}$,99

proof The )$\Gamma \mathrm{O}\mathrm{o}\mathrm{f}$$1$

has no$\nu$

is by structural induction on . First, we prove the lemlna for tlle case that$f$operator. It is$\mathrm{s}\mathrm{u}\mathrm{f}\mathrm{r}_{1}\mathrm{C}\mathrm{i}\mathrm{e}\mathrm{n}\mathrm{t}(0$consider only the cases

cases are ilnmecliate. In the following. we abbreviateWhen$c_{i}arrow a$$f=\langle \mathrm{r}$$[a]( \mathcal{F}_{S}(\bigcup_{c\in c^{S}}(C, a))[C\cup\{C\}])$.

.

Since $C”=_{p,q}C’’’$ and ) the

assumption, we can define $C”=\{c_{i}’’|c_{i}arrow a$ c\’i’,$\mathrm{F}_{\Gamma \mathrm{o}\mathrm{n}}\tau$for every $c’\in C’$ .
be$f=[\prime\prime]f^{;}$.

$\mathrm{i}11(1\mathrm{t}|\mathrm{C}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{l}\mathrm{l}$Frolll$\bigcup_{c\in C},.\prime s(c\zeta\prime\prime.).$$c”’|=F_{3},(C^{t\prime};)$we assume$\mathrm{f}\mathrm{i}\mathrm{l},\backslash \mathrm{t}$hypothesis,

for anv $c\in C.$$c-\tau\iota$$\mathrm{a}_{}^{\sigma},\mathrm{s}1\rceil \mathrm{J}111^{)}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$c_{j}^{\prime\prime J}|=f’$

. for

for

$\mathrm{T}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{n}$$\rfloor$

Proposition 4.14

3.

.

$c_{\mathit{1}}|=\mathcal{F}(_{l^{j}})i\uparrow l1/J/i\epsilon.\mathrm{b}lJ\leq_{dq}$.

$i\uparrow 17l$

The validity ofTheorem 4.15 [an?

$\epsilon??,u??l\epsilon’ roti_{\mathit{0}}l$$li\mathrm{t}^{\rceil},?it$

5

to a

. Therefore $c’|=f$let $C”$ be$\bigcup_{c\in c^{s}}(c, a)$, andAnd for any $c”’\in C’’’$ ,above.

.

$\square$$\square$is also shown by the following theorelll.

$\mathrm{A}\mathrm{l}\mathrm{g}\mathrm{o}1^{\cdot}\mathrm{i}\mathrm{t}]_{1}\iota 11- 1.2$

fion of$T_{\mathrm{t}l\mathrm{c}/t}\epsilon rl\iota\Gamma \mathrm{r}.\backslash .\sigma 1/’)7l^{)}$

of$\mathrm{f}_{0}\mathrm{r}\ln\iota 11\mathrm{a}f$$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}$1. $p|=F(l^{y)}\cdot$) $ljr.\mathrm{S}(/|=F1p)$]$l^{J}\leq_{d’}$.

. Since $C”=_{\rho.q}C’’’$ and bv the induction hypothesis. $c”’|=f’$ for any $c”’\in C’’’,$ .

Finally, from Proposition 2.1 . $C_{(j}|=f$ for any.

$C_{j}\prime\prime J\in C’’’’$$c”|=f’$ .

$\mathrm{a}\mathrm{n}.\backslash ’ c’’\in C’’,$

Therefore $c’|=f$ for every $c’\in C’$ . Another cases are same as$\sim \mathit{0}$$c_{i}’’|=$$(\mathrm{j}’’’’=\{c_{j}’’’|c_{j}’arrow ac_{j}’’’, c_{j}^{J}\prime\prime|=\mathcal{F}_{S}(C\text{ノ}\prime\prime)[C\cup\{C\}], 1\leq j\leq m\}$$\mathrm{y}$$C”’$

for easiness description.

$S$$\underline{\mathrm{t}}_{\mathrm{b}}^{\gamma},.(C’, a)=(\bigwedge_{C\mathrm{c}\circ m},,\in b(\{S\mathrm{t}C,a)|_{C}\in c\})\langle\zeta l\rangle(Fs(C’’)[C\cup\{C\}]))\wedge$

exists$\mathrm{T}1_{1\mathrm{C}\mathrm{l}1}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{l}\cdot \mathrm{e}$

$|$

When

as

and $f=[a]f’$ . Another) $f’$ , let C’ be $\{c_{j}|1\leq ? \leq?l\}$ alld $C’$ be $\{c_{j}’|1\leq j\leq??\mathrm{z}\}$ . Note thatfor $c_{i}\in C$ since $c_{j}|=f$ . So

$f’,$ $1\leq i\leq n\}$$\mathcal{P}(p)$$f=\langle a\rangle f’$$f$$f\mathrm{r}ct.\sigma$.

in$t/\mathrm{t}\epsilon$$\zeta ll\mathrm{r}/$orithm$f\mathrm{r}..rl\mathrm{r}\mathrm{r}/.\sigma\epsilon q\iota/e\uparrow 1C\epsilon$of$,/,.O\sim$’

if there exists a process$l^{J\Gamma \mathit{0}}ce.\sigma.\sigma e.\sigma$

by A$lc/orifht\uparrow l\mathit{4}\cdot\sim 2$$l^{J}$

satisfying

converges in the.

$proc\epsilon.\mathrm{s}.\backslash _{\mathit{1})’}.\backslash 1/\mathrm{r}hth\mathrm{r}/t_{l^{j}}\leq_{(;l}j’$$\square$

A Prototype for the Process Synthesis System
In this sectioll, we introduce a$\mathrm{I}^{)\Gamma \mathrm{o}\mathrm{t}\mathrm{t}}\mathrm{o}\mathrm{y}\mathrm{P}^{\mathrm{e}}$system SORP: Synthesizer of Recursive Processes

based on the Algorithm 4.2. This system adopts a graphical user interface to display thesynthesized )$1$$\Gamma \mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}‘\backslash \mathrm{C}$}$\mathrm{s}$(See Fig.

)$.\ulcorner$

$)$

. The

$\mathrm{s}_{\text{ノ}}.\mathrm{v}\mathrm{s}\mathrm{t}\mathrm{e}\ln$

X-window systel]].
As an example. wein Fig. .5.

$\mathrm{T}1_{1\mathrm{e}\mathrm{e}^{\mathrm{T}}}\wedge\backslash \mathrm{t}\mathrm{r}01\iota 1\mathrm{e}$formulae. i.e.
picture mcans

)

three

$\iota 1\mathrm{t}$left )$\mathrm{i}\mathrm{C}\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{r}\mathrm{e}$$1$$l\text{ノ}?\cdot.\langle/|\rangle\langle b\rangle.?\cdot,$‘$l^{\text{ノ}}.\mathrm{T}$$\langle b\rangle \mathrm{t}\mathrm{t}$. . Threein each input step.

6$\mathrm{i}_{11}1$$\mathrm{N}\dot{o}\mathrm{t}\mathrm{c}$$\mathrm{r}_{0\Gamma \mathrm{n}\mathrm{l}\mathrm{t}}\mathrm{l}\mathrm{l}\mathrm{a}\mathrm{e}$is implemented using SICStus Prolog and. in Fig. 3, to the prototype system. Its output

in Fig. 5 shows all

. and
)

$\mathrm{o}\mathrm{t}1_{1}\mathrm{e}\mathrm{r}1^{\mathrm{i}\mathrm{c}}$lhat each )$1$$[c/][b][b]\mathrm{f}\mathrm{f},$$\mathrm{t}$ures are$1^{\cdot}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{s}$$\mathrm{I}/\mathrm{O}$display,$\backslash \mathrm{v}1_{1\mathrm{e}\mathrm{r}}\mathrm{e}$we$\mathrm{i}1\iota \mathrm{p}\iota \mathrm{l}\mathrm{t}$the threealld quit the system. Note that ‘$x:’’ in the$0\iota\iota \mathrm{f}\mathrm{l}$))$\mathrm{U}\mathrm{t}1$$\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{e}\mathrm{S}\mathrm{S}\mathrm{e}\mathrm{s}$which the system synthesizes

corresponds to the one ill Fig. 3.

Concluding Relllarks and Related Works
enumera lgoritlllll for a recursive process based(led target ). Its validity was also
be salisfied by theThis paper presented theation of facts.
discussed.

$\backslash \backslash ’ 1_{1}\mathrm{i}_{\mathrm{C}\mathfrak{j}}|\mathrm{t}11\iota\iota.\backslash \mathrm{t}$$\mathrm{s}.\backslash ’ 1\mathrm{l}\mathrm{t}$]$011\mathrm{t}1_{1}\mathrm{e}$$\neg$$\mathrm{l}\mathrm{C}\mathrm{s}\mathrm{i}\backslash$$\mathrm{i}_{11\uparrow \mathrm{C}\mathrm{l}1}$$1$$\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{e}\mathrm{s}\mathrm{S}$

100

$?-$

$|$

$>>$

dise.

$x:

$<\mathrm{a}><\mathrm{b}>\mathrm{x}$$\mathrm{C}\mathrm{O}=\mathrm{a}.\mathrm{b}$

. CO
.

.

$>><\mathrm{b}>\mathrm{T}$$\mathrm{C}\mathrm{O}=_{\mathrm{a}.\mathrm{b}}.\mathrm{C}0+\mathrm{b}.0$$>>[\mathrm{a}][\mathrm{b}][\mathrm{b}]$F.

$\mathrm{C}0=\mathrm{a}.\mathrm{b}.\mathrm{C}1+\mathrm{b}.0$,$\mathrm{C}1=\mathrm{a}.\mathrm{b}$

$>>$

quit.

no
$\mathrm{E}.r_{):}$

Output exanlples of the prototype system.

As mentioned in the introduction, little had been investigated for inductive inference ofprocesses. IIowever, sollle deductive
satisfies a consistent formula.

consistency of a$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{l}\mathrm{t}\mathrm{l}\iota 1\mathrm{l}\mathrm{a}$in$\mathrm{a}_{\mathrm{P}1}$)$\mathrm{r}\mathrm{o}\mathrm{a}\mathrm{C}1_{1\mathrm{e}\mathrm{s}}$$\mathrm{a}_{1^{)}\mathrm{p}_{\Gamma \mathrm{o}\mathrm{a}}\mathrm{e}\mathrm{s}}\mathrm{c}\mathrm{h}$find a model which

provided an algorithm by tableau method to show$\mathrm{I}’\backslash \mathrm{o}\mathrm{z}\mathrm{e}\mathrm{n}[17]$$l^{1-}\mathrm{c}\mathrm{a}1_{\mathrm{C}}\iota 11\mathrm{t}\mathrm{l}\mathrm{S}$exist. These

. The

)

$\mathrm{a}_{\mathrm{o}\mathrm{r}}\mathrm{i}\mathrm{t}\mathrm{h}\mathrm{n}\mathrm{l}1$a finite tree-like model which a$\mathrm{u}\mathrm{i}\mathrm{l}\mathrm{d}\mathrm{S}$atisfies. Since the model is a tree. not a graph, the algorithm cannot
consistent
make a loop, i.e. a recursive ). Actuallv, hethat the depth of the model is$\mathrm{f}_{\mathrm{o}\mathrm{r}111}\iota\iota 1\mathrm{a}\int,\backslash$$\mathrm{s}\mathrm{l}_{\mathrm{l}\mathrm{o}\backslash }\mathrm{V}\mathrm{e}(1$$1$$\mathrm{e}\mathrm{x}_{1})\mathrm{o}\mathrm{n}\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{i}\mathrm{a}1$in$|f|^{3}$automaton modcl$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathfrak{l}\backslash \mathrm{s}$. Streett and$\backslash \backslash ’ 1\iota \mathrm{i}\mathrm{C}\mathrm{h}$$\Gamma_{\lrcorner}111\mathrm{e}\mathrm{r}\mathrm{S}\mathrm{o}\mathrm{n}[27]1)\mathrm{r}\mathrm{e}\mathrm{S}\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{e}\mathrm{d}$satisfies a given fornltla

tree with states in $O(2^{2}|p|)$ . Similarpresented a satisfiability$\mathrm{a}\mathrm{J}\mathrm{g}\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{h}\mathrm{n}\mathrm{l}$propositional temporal logic
operators. [3]

and

$\nu$

$1)\Gamma \mathrm{O}\mathrm{l})\mathrm{o}\mathrm{s}\mathrm{e}\mathrm{c}\mathrm{l}l\text{ノ}TL$

and provided$\partial 11$

Stirling’s work [22]

$|$

) $.$

)

$\mathrm{r}\mathrm{o}\mathrm{a}\mathrm{c}\mathrm{h}\mathrm{e}\mathrm{s}$$\mathrm{a}1^{)}1$$f$$q\vdash[a].f$)$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{r}\mathrm{e}$$1$

to build an. The built automaton model is a finite

for temporal logic are in [18] and [3]. [18]to create a model satisfied by a given formula in liner timeusing tablaue method,. which is liner tinle)$\mathrm{t}\mathrm{e}\mathrm{m}_{1}$$\mathrm{t}1_{1\mathrm{O}\mathrm{U}}\mathrm{g}\mathrm{h}$$\mathrm{o}\mathrm{r}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{o}\mathrm{g}\mathrm{i}_{\mathrm{C}}$its logic has no fixed pointwith fixed point operators$\mu$algorithm that constructed a graph model of given formula.
$\mathrm{s}\mathrm{e}\mathrm{e}\mathrm{n}\mathrm{l}\mathrm{s}$to be related with our work. Ill [22], he showed a sound andcomplete deductive system NL for finite processes. Using

does satisfy a certaina decision$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{l}\mathrm{l}\iota \mathrm{u}\mathrm{l}\mathrm{a}$. For$\mathrm{e}\mathrm{x}\mathrm{a}\mathrm{l}\gamma 11$)$\mathrm{l}\mathrm{e}$.

$p\vdash\langle a\rangle f$$\mathrm{N}\mathrm{L}$implies

implv $l^{J}+r/\vdash[cl]f$ . Fronl hese rules. a forlnula$\iota$, we can deduce that a process$p+q\vdash\langle a\rangle f$, and also $p\vdash[a]f$ ,$[a]\langle b\rangle\tau\wedge\langle a\rangle\langle c\rangle T$

can infer, for101example, a process $a.b.0+a.(b.0+c.0).$ Ill this sense, we can regard his system as a deductive
system for processextended to$\mathrm{s}\mathrm{y}\mathrm{n}\mathrm{t}1_{1\mathrm{e}}\mathrm{S}\mathrm{i}\mathrm{S}$. Of course. NL has no recursive expressions. NL is needed to berecursive )$\mathrm{s}\mathrm{y}\mathrm{n}\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{s}\mathrm{i}\mathrm{z}\mathrm{e}$$1$

The difference between our$\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{e}\mathrm{s}$$\mathrm{a}_{1^{)}1^{)\mathrm{r}}}\mathrm{o}\mathrm{a}\mathrm{c}\mathrm{h}$effectively.

and deductive ones is whether input formulae are

fixed or not. When
number of input formulae is finite and the sequence of formulae
is fixed, our algorithm gives similar result, as the deductive one. In practice, however, a$\mathrm{t}1_{1}\mathrm{e}$$\mathrm{s}$complete specification may not be given. After synthesizing, the user may want to input

more facts

to add lnore functions to an$\mathrm{a}\mathrm{n}\mathrm{d}/\mathrm{o}\mathrm{r}$over deductive ones in such a situation.
There is a restriction on )$\mathrm{i}\mathrm{n}_{1}$$\mathcal{L}_{d}$. However$\iota 1\mathrm{f}\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{m}1}11\mathrm{a}\mathrm{e}$)$\mathrm{o}\mathrm{u}\mathrm{t}_{1)}\mathrm{u}\mathrm{t}1$

in our$\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}\mathrm{S}$$\mathrm{a}\mathrm{J}\mathrm{g}_{\mathrm{o}\mathrm{r}\mathrm{i}}\mathrm{t},\mathrm{h}\mathrm{m}$. Our$\mathrm{a}_{1^{)}\mathrm{P}^{\mathrm{r}\mathrm{o}}}\mathrm{a}\mathrm{c}\mathrm{h}$. The formulae must be within

the problenl leads us to a process synthesis$\mathrm{o}\mathrm{v}\mathrm{c}\mathrm{r}\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{i}\mathrm{l}$has advantages$\mathrm{a}\mathrm{J}\mathrm{g}\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{h}\mathrm{m}$whose output

converges in the limit to a process equivalent to an intended target one.
The time or)$\mathrm{s}_{1^{)\mathrm{a}}}\mathrm{C}\mathrm{e}\mathrm{c}\mathrm{o}\mathrm{n}\eta^{]}$$\mathrm{e}\mathrm{X}\mathrm{i}\mathrm{t}\mathrm{y}$of the algorithm is not discussed and is left for a future

study.
参考文献[1] Angluin. D.:

Learning

Comput. 75. )$1$$[^{)}\cdot 87^{-}10\mathrm{t})(1.9\mathrm{s}^{-}l)$[2] Bergstra, .J.A.

Info. alld

[3] Banieqbal, 13.
$\mathrm{C}\mathrm{o}\mathrm{m}_{1^{)11}}\mathrm{t}$

[4]

$60,$

$\mathrm{r}\downarrow\prime 1\mathrm{l}\mathrm{d}$H.

. Sci. 398.

$\mathrm{B}\mathrm{r}\mathrm{i}\mathrm{n}\mathrm{k}_{\mathrm{S}}\mathrm{n}\mathrm{l}\mathrm{a}.$$\mathrm{P}1$) $109$$\mathrm{C}\mathrm{l}\mathrm{o}\mathrm{C}\mathrm{k}_{\mathrm{S}}\mathrm{i}\mathrm{l}1$$\mathrm{B}\mathrm{a}\mathrm{r}\mathrm{r}\mathrm{i}_{11}\mathrm{g}\mathrm{e}1^{\cdot}:$) $62-74$$1^{)}\mathrm{I}$$1^{r}\mathrm{Q}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{i}_{\mathrm{C}}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{I}1$.

“$\mathrm{F}_{d}.\Lambda.$:$\mathrm{S}_{1)\mathrm{l}}\cdot \mathrm{i}\mathrm{n}\mathrm{g}\mathrm{e}\mathrm{r}$“$\mathrm{T}\mathrm{e}111\mathrm{I}^{\mathrm{l}\mathrm{o}\mathrm{r}\mathrm{a}1}$[8] Fantechi. A., S. Gnesi$\mathrm{a}11$$\mathrm{A}.\mathrm{W}$$\mathrm{P}1^{)}\cdot 560$

.S. Melli

Science, Elsevier Science$\mathrm{I}\mathrm{n}\mathrm{f}$. andLogic with Fixed Points”, Lecture Notes in$\mathrm{T}\mathrm{e}\mathrm{n}\mathrm{l}\mathrm{p}_{\mathrm{o}\mathrm{r}\mathrm{a}}1$-Verlag(1989).

V. North-IIolland,, J. A CM., 31, 3.
$\mathrm{C}^{\mathrm{t}}$”,Algebra for Synchronous Communication”,$\mathrm{P}_{\Gamma \mathrm{o}\mathrm{c}\mathrm{e}}\mathrm{s}\mathrm{S}$$\mathrm{I}_{r}$, XV.F. and[7] Emerson,$\mathrm{C}^{\mathrm{I}}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{t}\mathrm{e}\Gamma \mathrm{e}\mathrm{x}\mathrm{a}\mathrm{J}\mathrm{n}\mathrm{p}\mathrm{l}\mathrm{e}\mathrm{s}$-137(1984).

[5] Brookes, S.D., C.A.R Hoare and[6]

Qll\‘eries andE.: A Tutorial on OTOS”, Proc. IFIP

Testing and$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{e}\mathrm{s}\mathrm{s}\mathrm{e}\mathrm{s}$$\mathrm{f}\mathrm{r}\mathrm{o}\ln$.

Klol):$\mathrm{a}\mathrm{l}’ \mathrm{d}\mathrm{J}.11^{-}.$$\mathrm{C}^{\tau_{\mathrm{o}\mathrm{n}}}\mathrm{t}.,$Sets$\mathrm{R}\mathrm{e}\mathrm{g}\backslash 1\mathrm{l}\mathrm{a}\mathrm{r}$$\mathrm{P}\mathrm{p}73-84(1986)$$\mathrm{c}\mathrm{o}11\mathrm{l}\mathrm{n}\mathrm{l}\mathrm{u}\mathrm{n}\mathrm{i}_{\mathrm{C}\mathrm{a}\mathrm{t}}\mathrm{i}\mathrm{n}\mathrm{g}$Sequential-599(1984).

$\mathrm{s}11:\cdot \mathrm{p}_{\mathrm{r}\mathrm{o}\mathrm{g}_{\Gamma \mathrm{a}111}}\min \mathrm{g}$in Prolog”, Springer-Verlag(1981).

and Modal Logic”, Handbook of Theoretical Computer$1^{)}1$$]$

on Protocol Specification,.

. Roscoe: “A Theory of$\mathrm{p}_{\mathrm{t}}|_{)}1\mathrm{i}\mathrm{s}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{S}\mathrm{B}.\mathrm{V}.,$($1\mathrm{V}_{0\Gamma}\mathrm{k}\mathrm{S}\mathrm{h}\mathrm{o}_{1^{)}}$

G. Il istori:‘) $..995$-1072(1990).

$\mathrm{C}\mathrm{o}\mathrm{l}\mathrm{n}\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{a}\mathrm{l}$Logic$\mathrm{s}_{\mathrm{e}\mathrm{n}\mathrm{l}\mathrm{a}\mathrm{n}}\mathrm{t}\mathrm{i}\mathrm{C}\mathrm{S}$and LOTOS”,

Protocol Speci fication. Testing and Verification, XL., IFIP, pp.365-378[9]$\mathrm{G}_{\mathrm{o}\mathrm{t}\mathrm{Z}}\mathrm{h}\mathrm{t}^{)}\mathrm{i}_{1}1$, R.:$\mathrm{s}_{1})\mathrm{e}\mathrm{c}\mathrm{i}\mathrm{f}\mathrm{i}_{\mathrm{C}\mathrm{a}}\mathrm{f}\mathrm{i}\mathrm{o}\mathrm{l}\mathrm{l}$.

$‘ \mathrm{S}_{1)}\mathrm{e}\mathrm{c}\mathrm{i}\mathrm{f}\backslash \cdot \mathrm{i}_{11}\mathrm{g}\subset_{0}^{\tau}11111\iota 111\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$\mathrm{T}\mathrm{c}\mathrm{S}\mathrm{t}\mathrm{i}\mathrm{l}\tau \mathrm{g}$[10] van Glabbeek,$\mathrm{c}_{0}^{\tau}\mathrm{m}_{1)1}1\mathrm{t}$and Verification,$\mathrm{R}.\mathrm{J}.:‘\cdot]^{\urcorner}11\mathrm{e}\mathrm{I}411\mathrm{l}\mathrm{c}\mathrm{a}\Gamma \mathrm{T}\mathrm{i}_{\ln}\mathrm{e}$. Sci. 458. Spri$1\iota_{\wedge}^{\sigma}\mathrm{e}\mathrm{r}$$\mathrm{X}\mathrm{L},$Services with$1^{)}1^{)}\cdot 295$)$\mathrm{o}\mathrm{r}\mathrm{a}\mathrm{l}$Logic”, Protocol-309(1990).

–Branching Time

-Verlag(1990).

$\mathrm{T}\mathrm{e}\mathrm{l}\mathrm{l}\mathrm{l}\mathrm{l}$”, Lecture Notes in$\mathrm{S}_{1)}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{r}\mathrm{t}\mathrm{l}\mathrm{n}1$102[11] Graf, S. and.J. Sifakis:

Their Properties”.

$\mathrm{I}\mathrm{n}\mathrm{f}$[12] Hennessv, M. and R.

J. ACM.. 32, 1.

$1^{)}\mathrm{I}$

Logic for the Description of Non-deterministic Programs and$‘.\mathrm{A}$. and collt)$\mathrm{h}\mathrm{I}\mathrm{i}\mathrm{l}\mathrm{n}\mathrm{e}\mathrm{r}:$) $.137$$\Gamma..68,$$\mathrm{p}\mathrm{p}.254-270(1986)$

Laws for$\Gamma \mathrm{a}\mathrm{i}\mathrm{c}$$\mathrm{A}\mathrm{l}\mathrm{g}\mathrm{e}\mathrm{l}$$\mathrm{N}\mathrm{o}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{m}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{s}\ln$

and Concurrency”,-161(1985).

[13] Hennessy, M.: “Algebraic Theory of Processes”, The MIT Press(1988).
[14] Hindley,alld$\mathrm{J}.\mathrm{R}.$$\mathrm{J}.\mathrm{P}$. Seldin: “Introduction to Combinators and$\lambda$-Calculus”, London

MatlleII\downarrow atical Societv Student Texts 1, Cambridge Univ. Press(1986).

[15] Hoare,$\mathrm{C}.\mathrm{A}$.R.:$::\mathrm{c}_{\mathrm{o}\mathrm{n}\tau \mathrm{n}11}111\mathrm{i}\mathrm{C}\mathrm{a}\uparrow \mathrm{i}_{1\mathrm{l}}\mathrm{g}$Sequential Process”, Prentice.

$\mathrm{H}\mathrm{a}\mathrm{l}\mathrm{l}(19\mathrm{s}5)$[16] Kinlura. S.. A. Togashi and S. Noguchi: “A Synthesis Algorithm of Basic Processes by

Modal Formulas” (in Japanese), Trans. IEICE, J75-D-I,[17] Kozen, D.:on$..\mathrm{I}\mathrm{t}\mathrm{e}\mathrm{s}\iota 1\mathrm{l}\mathrm{t}\mathrm{s}$$\mathrm{p}\mathrm{p}.3.33^{-}.35- 1119|\backslash ^{)}.3)$[18] Manna, Z. all P.

$\mathrm{t}\mathrm{l}\mathrm{l}\mathrm{c}\mathrm{P}\mathrm{r}\mathrm{o}_{1)}\mathrm{o}\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{i}_{0}\mathrm{n}\mathrm{a}1l^{\mathrm{t}}$$\mathrm{p}\mathrm{p}.1048^{-}1061(1992\mathrm{I}\cdot$-calculus”, Theoret.

$\mathrm{c}_{\mathrm{o}\mathrm{m}}^{\mathrm{t}}\mathrm{I}$)$11\mathrm{t}$. Sci., 27,.

$\mathrm{b}\mathrm{V}\mathrm{o}1_{1}$)$\mathrm{e}\mathrm{r}:‘ 4\mathrm{s}.\backslash ^{r}11\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{s}\mathrm{i}\mathrm{s}$Specifications”, ACM Trans.

of Connnunicating Processes$\mathrm{f}\mathrm{r}\mathrm{o}\ln$Temporal Logic

Languages and Systelns, 6-, 1, pp68-$0\mathrm{l}1\mathrm{p}_{\mathrm{r}\mathrm{o}\mathrm{g}\mathrm{r}\mathrm{a}}\mathrm{l}\mathrm{n}111\mathrm{i}\mathrm{n}\mathrm{g}$93(1984).

[19] Milner, R.:[20] Park, D.:

Sci. 104, 1)]). 167-183.

Yaleoretical

)

Modal

in
[26]

$\mathrm{p}\mathrm{p}.3\mathrm{J}1$, C.:$\mathrm{C}_{0}\mathrm{m}_{1^{)1\mathrm{i}\mathrm{t}}}$$\mathrm{S}\mathrm{t}\mathrm{i}\Gamma 1\mathrm{i}_{1}\mathrm{l}\mathrm{g}$$\mathrm{C}’ 1\iota$$(_{-}^{-\mathrm{t}}\mathrm{h}\mathrm{a}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{z}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$$1^{)}\mathrm{p}.27$

of Observationa3 Equivalence”, The-

-45(1985).

aractcrization of Observational Conguruence on Finite Terms$68,1^{)}\mathrm{p}.125$-145(1986).

‘-347(1987).

All Introduction to Modal and$‘ 4\backslash _{L}\mathrm{I}_{\mathrm{o}(}\mathfrak{j}C\gamma\iota$$\mathrm{s}_{1^{)\mathrm{r}\mathrm{i}\mathrm{n}\mathrm{g}}}\mathrm{e}1^{\cdot}$alld. Oxford Science$\mathrm{V}\mathrm{o}\mathrm{l}\iota \mathrm{l}\mathrm{n}1\mathrm{e}2$.S. alld
I
Proposit,[27] Streett,of Theories From Facts”, Technical Report 192,$\mathrm{I}_{1}1\mathrm{f}\mathrm{e}\mathrm{r}\mathrm{e}\mathrm{n}\mathrm{C}\mathrm{e}$$\mathrm{c}_{\mathrm{o}\mathrm{m}_{1^{)11}}}\mathrm{t}.,$. Sci. 491,

, C.:”, Lecture Notes in Comput.

Modal Logics For C’oinmunicating Systelns”, Theoretical C’omputer Sci-

[24] Stirling, C.:$\mathrm{S}\mathrm{t}\mathrm{i}\mathrm{r}\mathrm{l}\mathrm{i}\mathrm{l}\mathrm{l}\mathrm{g}$$\mathrm{s}\mathrm{e}\mathrm{q}_{\mathrm{U}}\mathrm{e}11\mathrm{c}\mathrm{e}\mathrm{S}$-Verlag(1981).

Science, 39.

of CCS”, Info. and[25]$\Gamma \mathrm{i}\mathrm{n}\mathrm{g}\mathrm{e}\mathrm{r}$on infinite).

$\mathrm{t}\mathrm{l}\uparrow \mathrm{e}\mathrm{r}$$\mathrm{C}^{\mathrm{t}}.:..\mathrm{A}$ence, 49,$\iota 1\mathrm{t}_{\grave{\mathrm{O}}}1\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{a}$A Proof-Theoretic$(_{}^{-}-,.:$$\mathrm{C}’ 01111$[23] Stirling,)$\mathrm{s}_{1}$: ‘Inductive$\mathrm{E}.\mathrm{Y}.$$\mathrm{U}\mathrm{n}\mathrm{i}\mathrm{v}\mathrm{t}\mathrm{l}9\mathrm{s}\mathrm{l}$[22] Stirling,

and a$::(^{-1},0\mathrm{l}\mathrm{l}\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{e}\mathrm{n}\mathrm{c}_{\mathrm{V}}$[21] Shapiro,and Concurrency”, Prentice-Ha11(1989).

$‘\cdot(^{-_{1}}0111\mathrm{l}11\mathrm{u}1\iota \mathrm{i}\mathrm{C}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{l}\mathrm{l}$$\mathrm{r}\iota$$\mathrm{i}\mathrm{o}\mathrm{l}\mathrm{r}\mathrm{l}\backslash \wedge$$\mathrm{F}_{\lrcorner}.\mathrm{A}$.

-Verlag,$\mathrm{T}\mathrm{e}111\mathrm{I}^{)\mathrm{O}}\mathrm{r}\mathrm{a}1$$\mathrm{P}\iota \mathrm{t}\mathrm{b}$]$\iota\iota-(^{-}-\mathrm{a}|1_{\mathrm{C}}\iota 111\mathrm{s}$.

$\mathrm{I}_{11}\mathrm{f}\mathrm{o}$‘) $.2$, pp.

Logics for CCS”, Lecture Notes-20(1991).

Logics”,$\mathrm{i}_{\mathrm{C}}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{S}$$\mathrm{E}\mathrm{l}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{r},\backslash \mathrm{o}\mathrm{t}1:$$\mathrm{P}1$$\mathrm{T}\mathrm{e}\mathrm{m}\mathrm{p}_{\mathrm{o}\mathrm{r}}\mathrm{a}\mathrm{J}$)$\mathrm{I}\mathrm{I}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{d}\iota$$‘ \mathrm{J}77$$\mathrm{O}\mathrm{o}\mathrm{k}$of Logic in Computer Science-563(1992).

An Automata Theoretic Decision Procedure for the. and$\mathrm{t}_{-}^{-(}\mathrm{o}1111^{1}\mathrm{u}\mathrm{t}$. $81$ , Academic Press,$\mathrm{p}\mathrm{p}249^{-}264(1989)$.