数理解析研究所講究録902 巻 1995 年 156-178156

プロセス計算の統合支援環境の構築*

東北大通研 吉田仙(Sen Yoshida)

東北大通研 富樫敦

(Atsushi Togashi)

東北大通研 白鳥則郎 (Norio Shiratori) \dag er

1

はじめに

近年, 情報処理システムの分散化・並列化に伴い, 並行システ

ムの仕様記述を形式的に行ない計算機による仕様の検証や自動合成を可能にするための手段として, 形式記述技法に対する重要性が高まっている. その中で, 並行に動作するプロセスの振舞いを

代数的な形式体系として扱うプロセス計算 [13] が注目され,までに多数開発されてきた.

これ

CCS [7], CSP [5], ACP [1] などはプロセス計算の代表的な例である.
また, それらプロセス計算において, その構文規則にしたがって表現されたプロセスの操作的意味を調べることを目的とする処理系が, いくつかのプロセス計算に対し作成されている [12].
*本研究は–部, 旭硝子財団, 文部省科学研究補助金による援助を受けている.
$\uparrow${$\mathrm{y}\mathrm{o}\mathrm{s}\mathrm{h}\mathrm{i}\mathrm{d}\mathrm{a}$, 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}$. riec. tohoku.

$\mathrm{a}\mathrm{c}$. jp$\text{し}$157

かしながら,

そのような処理系を作成するには–般に多大な労力を必要とし, 個々のプロセス計算に対しそれぞれ処理系を作成す

るのは非効率的である. そこで, プロセス計算の開発・利用を統合的に支援し, 汎用の処理機能を提供できるようなシステムを構築することが望まれる. プロセス計算の統合支援環境の実現により期待される点を挙げると, 以下のようになる.
$\bullet$

既存のプロセス計算の処理系が容易に作成できる.

$\bullet$

新たなプロセス計算を設計する場合に, 設計されるプロセス

計算上でのプロセスの遷移関係を表示したり, プロセス問の等価性を判定したりすることによって設計を支援できる.
$\bullet$

多様なプロセス計算をまとめて扱う形式的手法を与えることができる.

以上の理由から本論文では, まず第 2 章でプロセス計算を形式的に扱うためのモデルとして抽象プロセス計算を定義する.

また第 3 章では抽象プロセス計算をモデルに持つプロセス計算記述言語 LCC を提唱し,さらにこの言語のインタプリタとしての機能を持つプロセス計算支援システム$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{S}$の実装例を第 4 章

で紹介する. 最後に第 5 章でまとめと今後の課題について述べる.

158

2

抽象プロセス計算
前章で触れたように, これまで多くの研究者が多数のプロセス計算を提唱しその性質を解明してきた. 本論文では, プロセス計

算を抽象的なレベルでとらえそれらの–般的な性質を調べるための土台として, 抽象プロセス計算を定義する. 抽象プロセス計算
は, プロセス計算の操作的意味を SOS [8] 的アプローチによって与える手法であり, 個々のプロセス計算特有の表現からプロセス計算の持つ意味を独立させることができる.
はじめに,

抽象プロセス計算の構文を定める遷移式言語を定義する. 遷移式言語は, 抽象データ型の構文である等式言語 [9] に似た構文を持つ. 等式言語では等式の左辺と右辺が多ソートの項で表されるが, . 遷移式言語ではプロセ$\nearrow.\backslash$やアクションが多ソートの項として表される.
定義 2.1 (シグニチャ)
シグニチャはソートの集合 $S$ と演算記号領域
ある.

ここで

$\Sigma$は集合族$\langle\Sigma_{1l,S})\rangle_{u})\in s*,\in Ss$$\Sigma$

との対

であり,

$S^{*}$$\langle S, \Sigma\rangle$

は$S$からなるすべての有限系列の集合である.

で

の元
口

定義 2.2 (遷移式言語)
遷移式言語は 4 項組$\langle S, \Sigma, X, \sim*\rangle$

である.

ここで $S$ とがシグニチャとなる集合と集合族である.

$X$であるような記号の加算無限集合

の族

$s’)$

$X_{s}$$\Sigma$は$\langle S, \Sigma\rangle$

は $X_{s}\cap X_{S}’=\emptyset(s\neq$$\langle X_{S}\rangle_{-}.\mathrm{q}\in s$

であり,

159

X、の元をソート$S$の変数という.

$’\sim$は遷移を表す論理記号である.

口

定義 2.3 (項)$\langle S, \Sigma, X, \sim*\rangle$

を遷移式言語,の変数集合族$\langle Y_{S}.\rangle_{\text{、}\in}S$$T[\Sigma(Y)]_{s}$

$Y$

とする.

を

$Y_{s}\subseteq X_{\text{、}}$であるような任意

このとき各ソート

$s$

に対して,

を次の条件を満たす最小の集合とする.

1.

$\sum_{\epsilon,s}\cup Y_{s^{\neg}}\subseteq T[\sum(Y)]_{S}$2.

$f\in\Sigma_{s_{1}\cdots s_{n},s}$

かつ $\xi_{i}.\in T[\Sigma(Y)]_{s}i(i=1, \cdots, n)$ ならば$f( \xi_{1)}\cdots)\xi_{l},)\in T[\sum(Y)]_{S}$$T[\Sigma(\mathrm{Y})]_{s}$の元をソート

元をソート
について,

$s$

$s$

の

$\Sigma(Y)$項という. 特に$T[\simeq(\nabla x)]_{s^{-}}\text{の}$の項ということがある. また, シグニチヤ$T[\Sigma]$

は各$T[\Sigma]_{\mathrm{q}}.$,であるような集合族である.

が変数を含まない項の集合

T[\Sigma ]、の元をソート$s$$\langle S, \Sigma\rangle$$T[\Sigma(\emptyset)]_{\text{、}}$の閉じた項と口$’\backslash$い ).

遷移式言語における式は, 遷移の前後の状態を表す項と, 遷移時に行なわれるアクションを表す項からなる. 遷移は同– のソートの台の中で起こるものとする.
定義 2.4 (遷移式)

遷移式言語
る.

ここで

$\langle S, \Sigma, X, \sim\rangle$

$\xi$

と

$\eta$

における遷移式は記号列は同じソートの $\Sigma(X)$ 項である.

$\xi’\sim\alpha\eta$

であ
口

.

160

既存のプロセス計算において各プロセスの動作は遷移規則によって規定される場合が多い. 抽象プロセス計算では遷移規則が条件.
付き遷移式として与えられる.
定義 2.5 (遷移規則)

遷移式言語$\mathcal{L}=\langle s, \Sigma, x,’\vee\rangle$

における遷移規則は次のような形の推論規則である.
$\{\varphi_{i}|i\in I\}$$\varphi$

ここで $I$はインデックスの集合であり, 各 $\varphi_{i}(i\in I)$ . との遷移式である.
.

$\vee^{\backslash }?$$\varphi_{?}.‘(i\in I)$を遷移規則の仮定,$\varphi$$\varphi$は$\mathcal{L}$

を結論とい

.

口

定義 2.6 (抽象プロセス計算)$\mathcal{L}=\langle S. ’\Sigma, X, \sim’\rangle$

移式言語
る.

$\mathcal{L}$$\langle \mathcal{L}, \Gamma\rangle$とを$\mathcal{L}$を遷移式言語とする. 抽象プロセス計算は遷における遷移規則の集合$\langle S, \Sigma, X, \Gamma\rangle$$\Gamma$との対$\langle \mathcal{L}, \Gamma\rangle$と略記することがある.

であ口

抽象プロセス計算上での遷移の導出は形式論理体系における定理の証明と同様にして行なわれる. すなわち, ある遷移式を導出

することは仮定がなく結論がその遷移式であるような遷移規則の証明を与えることに相当する.
定義 2.7 (代入)$.\langle S, .\Sigma, X, \sim\rangle$$\langle\sigma_{\text{、}}$:

を遷移式言語とする. このとき, 代入$X_{S} arrow T[\sum(X)]S\rangle_{S}\in s$である.

$\sigma$

は写像族

161

$\sigma$を項から項への写像族$\langle\sigma_{s}$:$T[ \sum(X)]\text{、}arrow T[\sum(X)]_{S}\rangle_{\text{、}}\in S$に拡張する. すなわち, 任意の \xi \in T[\Sigma (X)]、に対して,

1. $\xi=x\in X_{s}$ ならば

2.

$\xi=f\in\Sigma_{\epsilon,s}$3.

$\xi=f(\xi_{1}, \cdots, \xi_{n}),$ならば$\sigma_{\text{、}}(\xi)=\sigma_{S}(x)$$\sigma_{\text{、}}(\xi)=f$$f\in\Sigma_{\text{、}}1\ldots sn’\text{、ならば}$$\sigma_{\text{、}}(\xi)=f(\sigma_{s_{1}}(\xi_{1}))\ldots)\sigma_{s_{n}}(\xi_{n}))$さらに,\mbox{\boldmath $\sigma$}

を遷移式および遷移規則にも拡張する.

口

定義 2.8 (証明)を遷移規則の集合,$\Gamma$$\{\varphi_{i}|i\in I\}$$\varphi$

を遷移規則とする. この遷移規則の$\Gamma$における証明とは, 上向

きの枝を持ち, すべての上向きの道が有限であり, 以下の性質を持つ木である. すなわち, 各ノードが遷移式によってラベル付けされており, 根がラベル$\varphi$を持ち, かつ各ノードについて, 以

下のいずれかが成り立つ.
$\bullet$

ノードがラベル $\varphi_{i}(i\in I)$ を持ち,ドが存在しない.

そのノードの上にはノー162$\bullet$

ノードがラベル$\psi$を持ち, その真上のノードのラベルの集合

が $\{\psi_{j}|j\in J\}$ であり,在し$\sigma(-\gamma)$

かつ遷移規則$\gamma\in\Gamma$と代入$\sigma$が存が$\frac{\{\psi_{j}|j\in J\}}{\psi}$となる.
口

定義 2.9 (証明可能性)$\Gamma$を遷移規則の集合,能であるとは,$\Gamma$$\gamma$を遷移規則とする.

における$\gamma$が$\Gamma$から証明可の証明が存在することである. ま$\gamma$

た, 仮定のない遷移規則$\emptyset$$\varphi$がから証明可能であるとき, 遷移式$\circ$$\Gamma$

いい,$\Gamma\vdash\varphi$と書$\langle$$\varphi$

は$\Gamma$から導出されると.

ロ

次に抽象プロセス計算の操作的意味を与える方法を示す. プロ
セス計算におけるプロセスの操作的意味は, そのプロセスを初期状態に持つラベル付き遷移システムで与えられる. 抽象プロセス
計算では, 状態やアクションがシグニチヤ

うなラベル付き遷移システムを特に$\Sigma$$\langle S, \Sigma\rangle$の項であるよ.

ラベル付き遷移システムと呼び, その上でプロセスの意味が与えられる. この方法は LO-

TOS における構造的ラベル付き遷移システムを用いた操作的意
味論 [6] を拡張したものといえる.

163

定義 2.10 (ラベル付き遷移システム)

ラベル付き遷移システムは 4 項組

は状態の非空集合,

$A$

である.

はアクションの集合である.

は遷移関係乳$a\in A\}$$\langle^{\mathrm{p},A\mathcal{T}},,$ $p0^{\rangle}$$\prime \mathcal{P}\cross P$の族である.

ここで$\mathcal{I}=\cdot \mathrm{t}-^{a}|$$P^{0}\in P$

は初期状

態である.

口

定義 2.11 ($\langle S, \Sigma\rangle$$\Sigma$

ラベル付き遷移システム)をシグニチャとする.

はラベル付き遷移システム
ソート$\mathrm{p}$$s_{\text{、}tat^{e}}\in S$

に対し,$\Sigma$$\langle$

ラベル付き遷移システム $LTS[\Sigma]$$P,$ $A,$,$\mathcal{I}_{P\mathrm{o}^{\rangle}}$である.

$7^{\supset}\subseteq T[\Sigma]_{sta}ste$

である.

ここで,

ある

また,

$A\subseteq$

である.

$\bigcup_{S\in S}T[\sum]_{s}$口

定義 2.12 (導出)
$C=\langle^{g\nabla},rightarrow,$

$(S$

.

$\in S)$$X,$$\Gamma^{\rangle}$

を抽象プロセス計算とする. 項 $\xi\in T[\Sigma(X)]S$の導出 Derc$(\xi)$

は以下の条件を満たす最小の集合である.

1. $\xi\in Der_{C}(\xi)$

2. $\zeta\in Derc(\xi)$ かつある$\alpha$について $\Gamma\vdash\zeta’\sim\alpha\eta$

ならば,$\eta\in Der_{\mathrm{C}}’(\xi)$口

定義 2.13 (プロセス)

抽象プロセス計算$C=\langle S, \Sigma, X, \Gamma\rangle$

におけるプロセスとはある

164

ソート

$S_{p}\in$.

$\xi\in T[\Sigma]_{\text{、}}p$$S$の閉じた項の集合の操作的意味はによって与えられる.
る.

また$\mathcal{T}$$\Sigma$$T[\Sigma]_{\text{、}p}$

ラベル付き遷移システム

3$\langle^{\mathrm{p}A\tau},,, \xi\rangle$

ここで $\prime \mathcal{P}=Der_{C(\xi),A}=\bigcup_{S\in S}\tau[\Sigma]_{S}$ であは各 $\alpha\in A$ に対し名となるような遷移関係の集合族$\eta\}$の要素である. プロセス$=$$\{(\zeta, \eta)|\zeta,$$\langlearrow\rangle_{\alpha\in A}\alpha$$\eta\in \mathrm{p},$$\Gamma\vdash\zeta\sim^{\alpha}\succ$

である.

口

プロセス計算記述言語
この章では, 抽象プロセス計算をモデルに持つプログラミング語として, 、プロセス計算記述言語 LCC (Language for Concur-$–\overline{\mathrm{I}}-\ovalbox{\tt\small REJECT}$

rent process Calculi) を提唱する.
.

$3\cdot 1$$\mathrm{L}\mathrm{C}\mathrm{C}$LCC は, プロセス計算の構文規則と遷移規則を抽象的に記述することによって汎用処理系でその意味解釈を行なえるようにするためのプログラミング言語である. この—–語は抽象プロセス計$\square$

算をモデルとして持ち, 実際の構文もモデルとしての遷移式言語に強く依存している. ただし実装上の問題として, 演算記号や変数, 遷移規則などの集合はすべて要素数が有限に制限される.

また, 記述の容易性を増すために LCC ではモデルにはない機能も付加されている.

165

3.2

LCC の説明LCC は,

header,部分に大別される.
$\text{し}$,$\mathrm{s}\mathrm{i}^{\mathrm{g}\mathrm{n}}\mathrm{a}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{e}$,$\mathrm{b}^{0}\mathrm{d}^{\mathrm{y}}$,$\mathrm{f}^{\mathrm{o}\mathrm{O}}\mathrm{t}\mathrm{e}\mathrm{r}$の 4 つのheader はプロセス計算の記述の開始を表

またプロセス計算の名前を定義する.

signature ではシグ

ニチャ, すなわちソートと演算記号などが宣言される.

body は遷移規則を記述する部分である. 最後の footer はプロセス計算の記述の終了を示す. 以下で LCC の 4 つの部分をそれぞれ説明
する.

3.2.1

headerheader は次のように記述される.
calculus$\langle$$\mathrm{C}\mathrm{a},1\mathrm{c}\mathrm{N}\mathrm{a}1\iota 1\mathrm{e}^{\rangle}$is

イタリック体で書かれた calculus とり,calculus が記述の開始を示す.

$is$$\mathrm{s}$gnaturesignature は以下のように構成される.
$\langle \mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{P}\mathrm{a}\mathrm{r}\mathrm{t}\rangle$$\{\{\langle \mathrm{S}\mathrm{u}\mathrm{b}\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{p}\mathrm{a}\mathrm{r}^{\rangle}\mathrm{t}\}\}$LCC の予約語であ$\langle \mathrm{C}\mathrm{a}\mathrm{l}\mathrm{C}\mathrm{N}\mathrm{a}\iota \mathrm{n}\mathrm{e}\rangle$に付けられた名前である.

3.2.2

は

はプロセス計算

166$\langle \mathrm{O}\mathrm{p}\mathrm{P}\mathrm{a}\mathrm{r}\mathrm{t}\rangle$$\{\{\langle_{\mathrm{S}\mathrm{e}\mathrm{t}\mathrm{p}\mathrm{a}}\mathrm{r}\mathrm{t}\rangle\}\}$.

$\langle \mathrm{S}^{\mathrm{o}\mathrm{r}\mathrm{t}}\mathrm{p}\mathrm{a}\Gamma \mathrm{t}\rangle$

LCC ではあるソートのはソートの宣言部である.

台の部分集合に名前をつけることができ, その . うな名前をサブ$\text{よ}$ソートと呼ぶ. ソートとサブソートの問の包含関係はで定義される. 各ソートの演算記号はれる.

$\langle$$\mathrm{O}_{1^{\mathrm{J}}}\mathrm{P}\mathrm{a}\mathrm{r}\mathrm{t}^{\rangle})$$\langle \mathrm{S}\mathrm{u}\mathrm{b}\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{P}\mathrm{a}\mathrm{r}\mathrm{t}\rangle$

において列挙さ

LCC ではいくつかの項を集めて集合を作ることができ,その名前を SetPa-rt で定義する.
$\rangle$$\langle$$\langle \mathrm{S}^{\mathrm{o}\mathrm{r}}\mathrm{t})\mathrm{p}\mathrm{a}\mathrm{r}\mathrm{f},\rangle$

sorts

は, 次のような形をしている.

$\langle \mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{I}’\backslash \mathrm{e}\mathrm{y}\rangle$... .

予約語 SOrt の後に, そのプロセス計算で扱われるソート$\langle \mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{K}\mathrm{e}\mathrm{y}\rangle$が宣言される.

LCC は組み込みソー

ここで宣言される通常のソートの他に,トとして internal を持っている.

このソートは意味解釈の段階においてそれぞれ特別な意味を持つ.

internal の台はプロセスが行なうアクションのうち外部からは観測不可能な内部アクショ
ンとみなされる.
$\langle$

SortPa-rt で宣言されたソートの問に包含関係がある場合は,$\rangle$

その関係がsubsorts$\mathrm{S}\mathrm{u}\mathrm{b}\mathrm{S}\mathrm{o}\Gamma \mathrm{t}\mathrm{p}.\mathrm{a}$$\langle$-l’t の中で次のように定義される.
$\rangle$$(\langle \mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{I}’’\backslash \mathrm{e}.\mathrm{v}\rangle< )$...

$\langle \mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{I}<\mathrm{e}\mathrm{y}\rangle$

.

167

記号 $<$ は, その右側にある$\langle$の台が左側のものを包$\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\iota\backslash \nearrow \mathrm{e}^{\mathrm{y}\rangle}$

含するということを意味する. 組み込みソート internal の項は意味解釈の段階で内部アクションとみなされる.

演算記号の定義は下のようなものである.
$op_{S}\langle \mathrm{o}_{1^{\supset}}\mathrm{F}\mathrm{o}1^{\backslash }\ln\rangle$... :$\{\{\langle \mathrm{S}_{\mathrm{o}\mathrm{r}}\mathrm{t}\mathrm{I}’\backslash \mathrm{e}.\mathrm{y}\rangle\ldots\}\}$$\langle \mathrm{O}_{1}\supset \mathrm{F}\mathrm{o}\mathrm{r}1\prime 1’1\rangle.\cdots$$->\langle \mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{I}\backslash \mathrm{e}\mathrm{y}\nearrow\rangle$.

が定義される演算記号のリストであり, 演算記

号のソートと被演算記号のソートがすべて同じ演算記号が-度に定義される. :. と$\cdot$$->$にはさまれた部分は被演算記号のソートのリストである. $->$ に続$\langle$$\langle$$\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{I}\langle \mathrm{e}^{\mathrm{y}}\rangle$

は演算記号により構成される項がどのソートの台となるかを指定する.

$3\cdot 2\cdot 3$$\mathrm{b}^{0}\mathrm{d}^{\mathrm{y}}$プロセス計算の遷移規則は body 部で以下のように記述される.
$\{\{\langle\backslash [\mathrm{a}1\sim \mathrm{P}\mathrm{a}\mathrm{r}\mathrm{t}\rangle\}\}$$\langle \mathrm{R}\mathrm{u}\mathrm{l}\mathrm{e}\mathrm{P}\mathrm{a}|1^{\cdot}\mathrm{G}\rangle$$\langle \mathrm{R}\mathrm{u}\mathrm{l}\mathrm{e}\mathrm{p}\mathrm{a}\}\mathrm{r}\mathrm{t}t\rangle$

る変数がは遷移規則の記述であり, その規則の中で用いられ$\langle\iota^{\gamma}\mathrm{a}1\sim \mathrm{p}.\mathrm{a}-\mathrm{r}\mathrm{f})\rangle$

において宣言される.

遷移規則の記述の中に現れる全ての変数は$\langle \mathrm{V}\mathrm{a}\mathrm{r}\mathrm{P}\mathrm{a}T\mathrm{t}\rangle$

において宣言され, ソートが割り当てられる. その記法は以下のようなも

168

のである.

vars
$\langle$$\langle$$\mathrm{V}\mathrm{a}|\mathrm{r}\mathrm{N}\mathrm{a}\downarrow \mathrm{m}\mathrm{e}^{\rangle}\cdots$$\mathrm{V}\mathrm{a}1^{\wedge}\mathrm{N}\mathrm{a}\mathrm{l}\mathrm{n}\mathrm{e}^{\rangle}\cdots$:.

$\langle \mathrm{V}\mathrm{a}1^{\sim}\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}\rangle\ldots$が宣言される変数のリストであり,はそれらがどのソートの変数であるのかを指定する.
としては,$\langle \mathrm{s}^{0\Gamma \mathrm{t}}\mathrm{p}\mathrm{a}\mathrm{r}\mathrm{t}\rangle$$\langle \mathrm{v}^{\mathrm{a}1}\sim \mathrm{s}^{0}\mathrm{r}\mathrm{t}\rangle$$\langle \mathrm{V}\mathrm{a}1^{\sim}\mathrm{S}^{\mathrm{o}\mathrm{r}}\mathrm{t}\rangle$

で定義される通常のソートのほかに, 組み

込みソートを指定することもできる. 組み込みソート Set が割り当てられた変数は, 解釈時においてタの名前 Set$\langle$$\mathrm{N}\mathfrak{c}1‘ 1\mathrm{u}l\mathrm{e}^{\rangle}$に束縛され,$\langle$$\langle$$\mathrm{s}^{\mathrm{e}}\mathrm{t}\mathrm{P}\mathrm{a}\mathrm{r}\mathrm{t}^{\rangle}$$\mathrm{S}\mathrm{e}\mathrm{t}\mathrm{N}\mathrm{a}\mathrm{m}\mathrm{e}^{\rangle}$で定義されたデーが表す集合が代入されたとみなされる.

遷移規則は以下のように記述される.

rule$\{\{\langle \mathrm{T}1^{\backslash }\mathrm{a}11\mathrm{S}\rangle\cdot\cdot\cdot\}\}$

予約語 rule と$=>$$=>\langle \mathrm{T}1^{\sim}\mathrm{a}\mathrm{n}\mathrm{S}\rangle$.

に挟まれた部分は遷移規則の仮定となる遷移式のリストであり, 矢印の後に遷移規則の結論が書かれる. 遷

移規則の仮定と結論は全て遷移式であり, その記法は下のようなものである.
$\langle \mathrm{T}\mathrm{e}\mathrm{r}\mathrm{m}\rangle$–$\langle \mathrm{T}\mathrm{e}\mathrm{r}\mathrm{l}\mathrm{l}\mathrm{l}\rangle->\langle \mathrm{T}\mathrm{e}\mathrm{r}1l\mathrm{T}\rangle$

1 つの遷移式は 3 つの項とその間の矢印から構成される. -番
左の項は遷移前のプロセス, 真中の項がプロセスが遷移する時に行なうアクション, そして-番右の項が遷移後のプロセスを意味
している.

169

3.2.4

footer

プロセス計算の記述は下の 1 行によって終了する.

endcalc
LCC による記述例$3\cdot 3$

簡単な例として, アクションプレフィックスと選択に関する演

算記号だけを持つプロセス計算 BPAtau を LCC で記述すると,
以下のようになる.

calculus BPAtau
sorts act

$1\supset \mathrm{r}\mathrm{o}\mathrm{c}$.

subsorts internal
a

$ops$
$op$

$\mathrm{b}\mathrm{c}$

$is$

$<$

act .

: $->$ aact .

tau : $->$ internal .

$o^{p}0:->1)\mathrm{r}\mathrm{o}\mathrm{C}$$.op^{*}$

: act

.

$1\supset \mathrm{r}\mathrm{o}\mathrm{c}->1^{3\mathrm{r}\mathrm{o}\mathrm{c}}$$o^{p+\mathrm{r}}:$.

$1^{3\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{p}\mathrm{c}-}0>1^{0}\mathrm{r}\mathrm{o}\mathrm{C}$

$var$

.

A : act .

vars$\mathrm{E}$EI E1I E12 Er Erl Er2 : proc .

$ru\iota^{e}=>(*\mathrm{A},\mathrm{E})-\mathrm{A}->\mathrm{E}$rule Ell–

A $->$ E12.

$=>+(\mathrm{E}\mathrm{l}1,\mathrm{E}\mathrm{r}^{)-}$

A $->$ E12 .

170$rule/\mathrm{r}1-\mathrm{A}->\mathrm{E}\mathrm{r}2=>+(\mathrm{E}1,/_{\mathrm{r}}1)-\mathrm{A}->/\mathrm{r}2$.

endcalc
最初の行は header であり, このプロセス計算が BPAtau と名付けられていることを示している.
次に Signature が記述されている.

という 2 種類のソートを扱う.

BPAtau では aCt と prOC

ソート aCt の台には$\mathrm{b},$$\mathrm{a},$びサブソート internal の台である tau という定数項が属し,
ソート proc の定数項である.

$*$は act と$\mathrm{C}$

およ
$0$

は

proc の 2 つの引数をとるオペレータであり, それにより作られる項は. prOC となる. 次の行は選択を表すオペレ一タめ定義である.
2 つの引数をとり続いて$\mathrm{b}\mathrm{o}\mathrm{d}\mathrm{y}$prOC の変数は$\mathrm{E}$$\mathrm{P}^{\Gamma \mathrm{O}\mathrm{C}}$$+$は proc の台からの項を構成する.

が記述される.|‘ノ – トact の変数は A であり,

, El, Ell などである. 最初の rule 文はアクション

プレフィックスに関する遷移規則の記述であり,アクションプレフィックスによって構成される項からは, いつでもアクションを行なうことが出来るという意味の規則が書かれている. 次の 2 つは選択に関する規則の記述であり,

2 つの引数のプロセスのうちどちらかがアクションを行なうことが出来る場合, そのアクシンが選択実行されると解釈される.
最後の行が footer で, 以上で BPAtau の記述が完了する.
$\cdot$$\text{ョ}$

171

4

プロセス計算支援システム
本章では, 第 3 章で提唱した LCC のインタプリタとして設計されたプロセス計算支援システム$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{s}$

について,

その概

要を説明する.
$\mathrm{p}_{\Gamma \mathrm{O}}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{S}$

算記述言語(PROcess Calculus SUport System) は, プロセス計,$\mathrm{L}\mathrm{C}^{\mathit{1}}\{\mathrm{C}1$

を解釈し,プロセス計算の構文規則に従って表現されたプロセスの操作的意味を解析するシステムである.
$\mathrm{S}\mathrm{u}\mathrm{S}$は現在,$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{c}-$プロセスのラベル付き遷移システムのグラフ表示とプロセス問の等価性判定の 2 つの機能を持っている. これらの機能を用いることによって, ユーザはこのシステムをプロセス計

算の開発及び利用支援系として活用することが出来る.
$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{s}$の構成は図 1 の様に表される.

ンパイラ, データベース, 計算器,$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{S}$は,コ

ツール, ユーザインタフェー

スの 5 つのモジュールから構成される. コンパイラは, プロセス計算を記述した LCC ファイルを読み込み, シグニチャや遷移規則に関する情報を計算器が参照できるような形に変換してデータベースに蓄積する. データベースはプロセス計算に関する様々なデータを蓄積し, 必要に応じて計算器に情報を提供する. 計算器
は,

‘ノ ‘

$-[]\mathrm{s}$の要求に応じてデータベース内の情報を参照しながら$<$プロセスの遷移関係を導出する推論エンジンである. ツールは,計算器に導出関係を導出させることによってプロセスの操作的意

172

味としてのラベル付き遷移システムを作成したり, 等価性を判定したりする. ユーザインタフエ一スはコマンド入力を受け付けた

リアプリケーションの出力を画面に表示したりする.

図 1:$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{S}$は$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{s}\mathrm{u}\mathrm{S}$の構戒

SICStus Prolog 1 を用いて実装されており, X

Window Systein 上で動作する.
$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{S}$には LCC で記述されたプロセス計算上でのあるプロセスを初期状態とするラベル付き遷移システムを作成してグラフ表示するツールが用意されている. このツールは,記述によって与えられたプロセス計算に対し,–LCC でのつのプロセスが入力されるとそのプロセスから任意のアクションによって到達可能な全てのプロセスを計算器を用いて枚挙する.

さらにそれら遷移後のプロセスから到達可能なプロセスを調べるということを繰
lSICStus Prolog は Swedish Institute of Computer Science の登録商標である.

173

り返すことによって, 与えられたプロセスを初期状態とするラベ

ル付き遷移システムを作り上げる. これをラベル付き有向グラフの形でウィンドウに表示する.

プロセスの問の等価性を判断する基準には様々なものがあるが,$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{S}$のツールは双模倣等価と観測等価という 2 つの等価性を有限のプロセスについて調べることが出来る.

ここで,

プロセ

ス問の等価性のレベルを以下の 4 つに分けて定義する.

identical 恒等関係 $pIdq$

strong 双模倣等価 $p\sim q$
weak 観測等価であるが強等価でない$p\approx q,$$p^{r} \oint.q$

different 異なる$p\not\simeq q$

2 つのプロセスを入力すると,.

$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{s}$はそれらの問の等価性が上の 4 つのレベルのうちどのレベルにあるかを調べ, 答える.
例として, 次に示す 2 つのプロセスの問の等価性を判定してみる.
$P_{1}=*(\mathrm{a},$ $+(*(\mathrm{b}, 0),$ $*(\mathrm{t}\mathrm{a}\mathrm{u},$ $*(_{\mathrm{C}\mathrm{o})))},)$$P^{\underline{q}}=+(*(\mathrm{a}, *(\mathrm{c}, \mathrm{o})), *(\mathrm{a}, +(*(\mathrm{b}, 0), *(\mathrm{t}\mathrm{a}\mathrm{u}, *(\mathrm{C}, \mathrm{o})))))$

まずそれぞれのプロセスのラベル付き遷移システムを表示させると, 図 2 のような出力が得られる.

さらに,2 っのプロセスの174

間の等価性を自動判定させた結果を図 3 に示す. 結果が weak となっているのは 2 つのプロセスが双模倣等価ではないが観測等価であるという解析結果を示している.
$\mathrm{r}\mathit{1}\Rightarrow*\mathit{1}^{\mathrm{A}}\mathit{1}\mathrm{b}$寡)$*\mathrm{f}*=1\mathrm{I}$

図 2-a:*l 架$P_{1}$$- \mathrm{n}\rangle$}}$\rangle$

図 2-b:.

$P_{2}$

図 2: 観測等価なプロセス

5

おわりに

第 2 章において, プロセス計算を形式的に記述する方法として

抽象プロセス計算を定義した. 抽象プロセス計算と同様にプロセス計算を SOS スタイルで記述する手法として TSS [4] と GSOS [2]がある.

これらと抽象プロセス計算を比較すると, TSS や GSOS

ではプロセスは単- ソートの項であり, またアクションは構造を持たないラベルであった. これに対し抽象プロセス計算ではプロ

175

$|?-$

equivalence ($,$$’*(\mathrm{a},+(*(\mathrm{b}, 0), *(\mathrm{t}\mathrm{a}\mathrm{u}, *(\mathrm{c}, 0))))$’,$+(*(\mathrm{a}, *(\mathrm{c}, 0)), *(\mathrm{a}, +(*(\mathrm{b}, 0), *(\mathrm{t}\mathrm{a}\mathrm{u}, *(\mathrm{c}, 0)))))’$

Equiv).

Equiv

$=$

weak ?

$\mathrm{y}\ominus \mathrm{S}$

$|$

$?-$

図 3. 等価性の判定結果

セスもアクションも多ソートの項で表される. このことは多 \langle の点でプロセス計算の記述を容易で明確なものにしている. 特にアクションに構造が伴う$\mathrm{C}^{\mathrm{t}},\mathrm{H}\mathrm{O}\mathrm{C}\mathrm{S}$や$\pi- \mathrm{c}\mathrm{a}|\mathrm{l}\mathrm{c}\mathrm{u}\mathrm{l}\mathrm{u}\mathrm{s}$などのプロセス計算を自然に記述できるのが抽象プロセス計算の特徴である.
ところで,

TSS や GSOS ではそのクラスにおける合同性など

に関する -般的性質の解明が進んでいる [4, 3, 2]. 抽象プロセス

計算のクラスにおいて同様な -般的性質の解明をすることは興味深い内容である. また,GSOS では遷移規則にあるアクションによって遷移することができないという負の仮定を記述することができるが, 抽象プロセス計算にもこれを導入することが考えられ
る.

第 4 章でプロセス計算の支援環境を提供するシステムを紹介し

,

176

た.

このシステムの機能として, 有限のプロセスの問の等価性判定を行なえるのであるが, 同値類分割の手法を用いることによって再帰を含むプロセス問でも等価性を判定でき, そのアルゴリズ

ムをインプリメントすることは早急に達成しなければならない課
題である.

をさらに実用的なシステムにしていくためには, プ$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{C}\mathrm{S}\mathrm{u}\mathrm{S}$

ロセス計算をモジュール化して記述できるような枠組を LCC に付加することが考えられる. その場合 2 つの抽象プロセス計算を結合するような \mp デルと結合したときの性質の変化の解明を行なう必要がある.

参考文献[1] J. A. Bergst,ra and J.
ing process,
Lenstra,$J$.

. Klop.

A lgebra of communicat-

of de Bakker, J. W., $H$a $zew$ in$\backslash f_{\mathrm{O}}1.1$$K$$1\lambda;$, M.,$ke\mathit{1}$. $eds$ . $CWIMonographs$ . North-Holland, 1986.

[2] B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can’t be
traced: Preliminary report. In 15th Annual A CM SIGA CT-

SIGPLAN Symposium on Principles

of Programming

Languages, pp. 229-239 1988.
[3] WJ Fokkink The
M. Hagiya and J.

$\mathrm{C}^{\mathrm{t}}$$\mathrm{T}_{\mathrm{c}^{\text{ノ}}}\backslash \gamma \mathrm{f}\mathrm{t}/\mathrm{T}\mathrm{y}_{d}\searrow \mathrm{t}$.

$\backslash _{\sim}|/\mathrm{I}\mathrm{i}\mathrm{t}\mathrm{c}\mathrm{h}\mathrm{e}\mathrm{l}1$fronlat reduces to tree rules In, editors, Proc. of the 2nd Inter-177

national Symposium on Theoretical Aspects of Computer

Software, Lecture Notes in Computer Science, pp. 440-453.

Tohoku University, Springer-Verlag, 1994.
[4] J. F. Groote and F.

. Structured operational se-$\backslash f\mathrm{a}\mathrm{a}11’\mathrm{d}_{\Gamma}\mathrm{a}\mathrm{g}\mathrm{e}\mathrm{r}$mantics and bisimulation as a congruence. Information andComputation, Vol. 100, No. 2, pp. 202-260, 1992.
[5] C. A. R.

. Communicating Sequential Process. Prentice$\mathrm{H}\mathrm{o}\mathrm{a}\mathrm{r}\mathrm{e}|$Hall, 1985.

[6] ISO. Information processing systems$\cdot$terconnection--

Open Systems In-

LOTOS- A formal description techniquebased on the temporal ordering of observational behaviour,chapter 7, pp. 25-70. ISO, 1989. ISO 8807.

[7] R. Milner. A$\mathrm{c}\mathrm{a}1_{\mathrm{C}\mathrm{u}}11l\mathrm{s}$of communicating systenls. Lecture

Notes in Conputer Science$\backslash f_{\mathrm{O}}1.92,$$,$, 1980.

[8] G. D. Plotkin. A structural approach to operational semantics. Technical report, Computer Science Department, Aarhus$1981\text{ノ}$$\mathrm{U}\mathrm{n}\mathrm{i}\mathrm{v}\mathrm{e}\Gamma \mathrm{s}\mathrm{i}\mathrm{t}_{\mathrm{c}}\backslash \Gamma,$. DAIMI FN-19$\cdot$[9] 稲垣康善, 坂部俊樹. 抽象データタイプの代数的仕様記述法の基礎 (1) 多ソート代数と等式論理. 情報処理, Vol. 25, No. 1,

1984.

178

[10] 吉田仙, 富樫敦白鳥則郎. 並行プロセス計算の開発・利用支
援環境. 電子情報通信学会技術報告, Vol. 93, No. 496,$\mathrm{P}\mathrm{P}\cdot 65-$

72,1994. COMP93-85.

[11] 吉田仙, 木村成伴, 富樫敦, 白鳥則郎. 汎用並行プロセス計算システムの設計開発. 電子情報通信学会技術報告, Vol. 93, No.

123, pp. 27-36 1993. COMP93-23.
$\ovalbox{\tt\small REJECT}$[12] 情報処理学会. 特集 : 通信システムの形式記述技法の標準化.
情報処理, Vol. 31, No. 1, pp. 2-81,1990.

[13] 富樫敦. 代数的プロセスの計算モデル. 日本ソフトウェア科学会チュートリアルテキスト, 1992.