数理解析研究所講究録 1442 巻 2005 年 76-82

76
並列合成の論理演算を持つ論理体系
竹内 泉 (Takeuti Izumi)
東邦大学理学部 (Faculty of Science, T\^oh\^o University)
要旨

ヘネシーミルナーの様相論理はプロセス代数などの遷移系に対して健全性と完全性を充たす。 この結果を、 並列合成を含む CCS に拡張するために、 論理体系に並列合成を表す論理演算を追加する。
重要語句: ヘネシー. ミルナーの様相論理, プロセス代数, CCS

1

序

ラベル付遷移系の性質を記述する論理体系としては、 ヘネシー. ミルナーの様相論理が有名である。 [S] これは、 公理によって規定される様相を持っ$\mathrm{K}$た多重様相命題論理である。 この論理はプロセス代数との間に充足関係が定義される。 プロセス代数の上の、 論理式に対する充足関係の等価性は、 公理的同等性、 双模倣関係と一致する。 また、 この充足関係の許でこの論理は健全かつ完全である。 即ち、 ある論理式が証明可能ならば全てのプロセスで充足され、 証明不能ならば反例がある。

プロセス代数に通信と並列合成を追加した理論模型としては、 ミルナーのCCS が知られている。 [M] プロセスの遷移を見るだけならば、 古典論理に様相を付加しただけの様相命題論理で十分であるが、 並列合成をもまた論理式によって把握することは興味深い問題である。 そこで、 従来の様相論理に並列合成を表す論理演算を追加した論理体系を提案する。 この論理は健全かつ完全であり、 更に、 証明探査と反例構成の手続を同時に行なうことが出来るであろことが予想される。

2プロセス代数
まず、 単純なラベル付遷移系の例としてプロセス代数を採り、 それに関して説明する。

定義 2.1(プロセス代数)
遷移要素$a\in A\text{、}$

有限集合

プロセス式 $P::=1|G$
ガード式 $G::=a.P|G+G$

これは後に現れる定義との比較の便宜の為にプロセス式とガード式とによって相互再帰的に定義しているが、$P:^{\sim}.=a.1|a.P|P+P$

77と定義したものと同等である。
1 は正常終了を表す。 他の文献で 0 と書かれているものと似ている。 しかし、 一般に 0 は単なる不活性を表すので、 その点は異なる。
プロセス式は今後単にプロセスと呼ぶ。
定義 22(遷移関係) プロセスの問の二項関係$arrow a$は、 以下の規則から生成される。
$a.Parrow Pa$$R+Parrow Qa$$Parrow Qa\Rightarrow P+Rarrow Qa,$3

同値関係
プロセスに対して三種の同値関係を導入する。

定義 3.1(公理的同等性) 以下の規則によって生成される同値関係的同等性と呼ぶ。 プロセス $P\text{、}Q\text{、}R$ 及び遷移 に対してを公理$\sim$$a$$P\sim P+P$ (二等則)$P+Q\sim Q+P$ (交換則)、$P\sim Q\Rightarrow a.P\sim a.Q,$、$P+R\sim Q+R$ (合同則)定義 32(双模倣) あるプロセス上の二項関係$\sim s$があって、 以下の条件を充たし、 $PSQ$ が成り立つならば、 $P$ と $Q$ は双模倣であるという。

任 5 のプロセス $P\text{、}Q$ に対して$-P\sim sQ\Rightarrow\forall a\in A$.
.
$\forall P’$$Parrow P’a\Rightarrow\exists Q^{/}$. $Qarrow aQ’\Lambda P’\sim Q’s$$-P\sim sQ\Rightarrow Q\sim Ps$

定義 33(論理式) $F::=1|\neg F|F\Lambda F|[a]F$

以下の略記法を用いる。
$F\supset G=\neg(F\Lambda\neg G)\text{、}F\vee G=(\neg G)\supset F\backslash F\supset\subset G=(F\supset G)\Lambda(G\supset F)$$\text{、}\langle a\}F=\neg[a]\neg F$

定義 34(充足関係)$-P\models 1<\Rightarrow P=1$$-P\models\neg F\Leftarrow\Rightarrow P\not\in F$$-P\models F\Lambda$$G\Leftrightarrow$$P\models F\ P$$-P\models[a]F\Leftrightarrow\forall Q$

定義 3,5 (恒真)$\models G$. $Parrow Qa\Rightarrow Q\models F$$\models F$$\Leftrightarrow\forall P$. $P\models F$

定義 36(充足等価) プロセス $P\text{、}Q$ が充足等価であるとは、$F\Leftrightarrow Q\models F$ となることを云う。

.

$\forall F$

定理 3.7 公理的同等、 双模倣、 充足等価の三者は互いに同値である。

$P\models$

$\tau\epsilon$

4

論理式の公理系
論理式に対して、$\mathrm{K}$公理による多重様相の公理系によって理論を定める。

論理式 $F$ がその理論の定理であることを
補題 4I$\dagger fF\Rightarrow\exists P$$\vdash F$と書く。

. $P\models F$

補題 4.2 $P\models F,$ $\vdash F\supset G\Rightarrow P\models G$.

.

. $P\models F\Leftrightarrow P\models G$

定理$43\mathit{1}$5並列合成のあるプロセス代数$\vdash F\Leftrightarrow\models F\mathit{2}$$\vdash F\supset\subset G\Leftrightarrow\forall P$定義 5.1(プロセス)
遷移名$n\in N\text{、}$

有限集合

遷移要素 $a\in A=\{\tau\}\cup N\cup\{\overline{n}|n\in N\}$

$P::=1|GP*P$
ガード式 $G::=a.P|G+G$
プロセス式$a=\overline{n}\in A$

記号

$*$

に対して

$\overline{a}=n$と定める。

$\overline{\tau}$という表現は無い。

は並列合成を表す演算記号である。 他の文献では 「 」 と書かれるこ$|$とも多い。
定義 52(遷移関係)$arrow a$は、 以下の規則から生成される。

$a.Parrow Pa$$Parrow Q\supset P+Rarrow Qaa,$ $R+Parrow Qa$$P\prec^{a}Q\Rightarrow P*Rarrow Q*Ra,$$R*Parrow R*Qa$$Parrow Qa,$

$P’arrow Q’a\Rightarrow P*Qarrow P’*Q’a$$Parrow Qa,$

$P’arrow Q’\overline{a}\supset P*Qarrow^{\mathcal{T}}P’*Q’,$$Q*Parrow^{\mathcal{T}}Q’*P’$

定義 53(公理的同等性) 3.1 の規則に以下を追加する。
プロセス $P\text{、}Q\text{、}R$ 及び遷移

$a$

に対して
$R*P\sim R*Q$ (合同則)$P\sim Q\Rightarrow P*R\sim Q*R,$$P\sim 1*P\sim P*1$ (単位元)$P=a_{1}.P_{1}+\ldots+a_{m}.P_{m}$.

$Q=b_{1}.Q_{1}+\ldots$ 十 $b_{n}.Q_{n}$に対して$P*Q\sim$$a_{1}.(P_{1}*Q)+$ $\ldots+a_{m}.(P_{m}*Q)+b_{1}.(P*Q_{1})+...$ $+b_{n}.(P*Q_{n})$$+\tau.(P_{i_{1}}*Q_{j_{1}})$$\langle$. ここで十... $+\tau.(P_{i_{f}}*Q_{j_{l}})$

分配則)$\{\langle \mathrm{i}_{1}, j_{1}\rangle, \ldots, \langle i_{l)}j_{l_{t}}\}\}=\{\langle i, j\rangle|a_{i}=\overline{b}_{j}\}$

この規則の許で以下が成り立つ。

$T9$

命題 5.4 $P*Q\sim Q*A$ (交換則)、 $P*(Q*R)\sim(P*Q)*R$ (結合則)

命題 55 任意のプロセス $P$ に対して、$*$を含まないプロセス$Q$があって$P\sim Q\mathrm{o}$定義 56(双摸倣、 充足関係、 充足等価)
は、プロセスの定義が拡張された以外と同一の定義による。

$3.2_{\text{、}}3.4_{\text{、}}3.6$

同様の定理が成り立つ。
定理 5.7 公理的同等、 双模倣、 充足等価の三者は互いに同値である。

6

並列合成を持った論理式

定義 6.1(論理式) $F::=1|\neg F|F\Lambda F|[a]F|F-\triangleleft F|F*F$

定義 62(充足関係)$-P\models 1\Leftrightarrow P=1$$-P\models\neg F\Leftrightarrow P*F$$-P\models F$

AG$\Leftrightarrow$$P\models F\ P$$\models G$$-P\models[a]F\Leftrightarrow\forall Q-Parrow Q\supset Q\models aF$$-P\models F-\triangleleft G\Leftrightarrow\forall Q$$-P\models F*G\Leftrightarrow\exists Q$. $Q\models F\supset P*Q\models G$, R. $P\sim Q*R,$ $Q\models F,$ $R|\vdash G$

定理 63 公理的同等、 双模倣と充足等価は互いに同値である。

充足関係の定義の中で公理的同等が参照されているので、 この定理は左程重要ではない。

7

論理体系

論理式が与えられたときに、 それが恒真であるかそれとも反例があるかを. $P\models F$ な判定することは有益である。 即ち、 論理式 $F$ に対して、 もしを答えがあるならばそのらば恒真であると答え、 もし $P\# F$ となるる計算手続を作ることが求められる。
ある適切な論理体系があって、 その論理体系で証明されるならばその論理式は恒真であり、 その証明探査手続が反例構成手続と一致しているということになれば、 先の要求は充たされる。 この要請を充たすような論理体系を定$\forall P$$P$$P$義する。

論理体系はゲンツェンの LK に倣って、 式を推論していく形を取る。

$\mathrm{L}\mathrm{K}$に於いては式は左辺と右辺より成っていたが、 ここで定義する論理体系は一80段以上の段より成る。 降段に左辺と右辺がある。 左辺、 右辺は論理式の有限集合である。 紙面での表記上は有限集合は列で表されるが、 その順序や重複には意味がない。
以降、$\Gamma\backslash \Gamma_{i}\text{、}\Delta/\text{、}$$\{F\}\mathrm{U}\Gamma\backslash \Gamma\cup\Gamma’$

等は論理式の有限集合を表す。 「 $F,$をそれぞれ表す。

$\Gamma$$\Gamma$」「$\Gamma,$$\backslash$$\Gamma’$」 はと $a\in A$ に対して押 $=\{F|[a]F\in\Gamma\}$

定義 7.1(式) 式とはこのような形をした図式である。

最下段とそれより上の段とは二重線で仕切られる。 二重線の上には 0 段以上の段がある。 二重線の下には必ず丁度 1 段ある。 二段は左辺と右辺の枡がある。 各論には論理式の有限集合がある。

表の形では書き辛いので、 一行の数式による表記法を与えておく。 先の表はこのように表記する。
$(\Gamma_{1}/\Delta_{1}/)(\Gamma_{2}/\Delta_{2})\ldots(\Gamma_{n}/\Delta_{n})\Rightarrow(\Gamma_{0}/\Delta_{0})$この式の直感的な意味はこのようなものである。 この式が証明できない場
合には、 以下を充たすプロセス $P_{1}*\ldots*P_{n}$ がある。
. $P_{1}*...$ $*P_{n}\models F$ )$\forall F\in\Gamma_{0}$$\forall \mathrm{i}\in 1,2,$$\ldots,$

特に$\Gamma 0,$$\ldots$,.

$(\forall F\in\Gamma_{i}.

$\Delta_{n}$$\Gamma_{n}\backslash \Delta_{1},$$\ldots,$

場合には、 式は$\forall P$$n$$\Rightarrow(/F)$

P_{i}\models F)\ \forall F\in\Gamma_{i}$が空であり、$\Delta_{0}$$(\Gamma_{1}/\Delta_{1})\ldots(\Gamma_{n}/\Delta_{n})\Rightarrow(\Gamma_{0}/\Delta_{0})$$\exists P$.

$P_{i}$

洋$F$

が唯一つの論理式 $F$ から成るとなる。 この場合には、. $P\models F\text{、}\Rightarrow(/F)$ が証明不能ならば

式. $P_{1}*\ldots*P_{n}\# F$$\ \forall F\in\Gamma_{i}$$\Rightarrow(/F)$

が証明可能ならば. $P*:F$ となる。に於いて、 小括弧で括られた$(\Gamma/\Delta)$$-r$ の段を表す。 以下では、 二重線より上の 0 段以上の段を纏めて等で表す。
$\tilde{\Gamma}=\{\Gamma_{1}/\Delta_{1}$)$\ldots(\Gamma_{n}/\Delta_{n}/)$に対して$\tilde{\Gamma}-(\Gamma_{i}/\Delta_{i})=(\Gamma_{1}/\Delta_{1})\ldots(\Gamma_{i-1}/\Delta_{i-1})(\Gamma_{i+1}/\Delta_{i+1})(\Gamma_{n}/\Delta_{n})$定義 72(推論規則)

構造規則
始式 :
$(F, \Gamma_{1}/F, \Delta_{1}))\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})$$\tilde{\Gamma}\Rightarrow(F, \Gamma_{0}/F, \Delta_{0})$増:,$, \cdot.\frac{(\Gamma_{1}/\Delta_{1})..\cdot(\Gamma_{n}/\Delta_{n})\Rightarrow(\Gamma_{0}/\Delta_{0})}{(\Gamma_{1}/\Delta_{1}’).(\Gamma_{n}’/\Delta_{n}’)\Rightarrow(\Gamma_{0}’/\Delta_{0})}$は$\tilde{\Gamma}\text{、}\tilde{\Gamma}’$$\delta 1$

但し$\forall \mathrm{i}\in\{0,1, \ldots,n\}$.

$\{\Gamma_{i}\}\subset$$\{\Gamma_{\acute{i}}\}\ \{\Delta_{i}\}\subset\{\Delta_{\acute{i}}\}$:$3\Phi$.
$\frac{(\Gamma_{1}//\Delta_{1})...(\Gamma_{n}/\Delta_{n})\Rightarrow(\Gamma_{0}/\Delta_{0})}{(\tau_{\sigma(1)}/\Delta_{\sigma(1\rangle})..(\tau_{\sigma(n\rangle}/\Delta_{\sigma(n)})\Rightarrow(\Gamma_{0}/\Delta_{0})}$

但しは$\sigma$$\{0,1,\ldots,\mathrm{n}\}$

上の置換。

:

$\Phi^{arrow}$$\frac{(\Gamma_{2},\Gamma_{1}/\Delta_{2)}\Delta_{1})\Rightarrow(\Gamma_{3},\Gamma_{0//}\Delta_{3},\Delta_{0})}{(\Gamma_{3},\Gamma_{1}/\Delta_{3},\Delta_{1})\Rightarrow(\tau_{arrow)},\tau_{0}/\Delta_{2},\Delta_{0})}.$

’

論理規則

1:
$\tilde{\Gamma}\Rightarrow(\Gamma/\Delta)$$\overline{(1/),\tilde{\Gamma}\Rightarrow(\Gamma/\Delta)}$$\overline{(1/[a]F),\tilde{\Gamma}\Rightarrow(\Gamma/\Delta)}$.
$\frac{(F,\Gamma_{1}/\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})}{(\Gamma_{1}/\neg F,\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}//\Delta_{0})}$$\frac{\tilde{\Gamma}\Rightarrow(F,\Gamma_{0}/\Delta_{0})}{\tilde{\Gamma}\Rightarrow(\Gamma_{0}/F,\Delta_{0})}$$\frac{\tilde{\Gamma}\Rightarrow(\Gamma_{0}/F,\Delta_{0})}{\tilde{\Gamma}\Rightarrow(\neg F,\Gamma_{0}/\Delta_{0})}$$\frac{(\Gamma_{1}/F,\Delta_{1}))\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})}{(\neg F,\Gamma_{1}/\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}//\Delta_{0})}$:$\Lambda$$(\Gamma_{1}/F, \Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})$$(\Gamma_{1}/G, \Delta_{1})2\tilde{\Gamma}\Rightarrow(\Gamma_{0}//\Delta_{0})$$(\Gamma_{1}/F\Lambda G, \Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})$$\frac{\tilde{\Gamma}\Rightarrow(\Gamma_{\dot{0}}/F,\Delta_{0})\tilde{\Gamma}\Rightarrow(\Gamma_{0}/G,\Delta_{0})}{\tilde{\Gamma}\Rightarrow(\Gamma_{0}/F\Lambda G,\Delta_{0})}$$\frac{(F,\Gamma_{1}/\Delta_{1}),\tilde{f}’\Rightarrow(\Gamma_{0}/\Delta_{0})}{(F\Lambda G,\Gamma_{1}/\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})}$$\frac{\tilde{\Gamma}\Rightarrow(F,\Gamma_{0}/\Delta_{0})}{\tilde{\Gamma}\Rightarrow(F,\Lambda G,\Gamma_{0}/\Delta_{0})}$$arrow$$\frac{\tilde{\Gamma}\Rightarrow(F_{)}\Gamma_{0}/\Delta_{0})}{\tilde{\Gamma}\Rightarrow(G\Lambda F,\Gamma_{0}/\Delta_{0})}$:$\frac{(F/),\tilde{\Gamma}\Rightarrow(/G)}{\tilde{\Gamma}\Rightarrow(/F-\circ G)}$$*$$\frac{(F,\Gamma_{1}//\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})}{(G\Lambda F_{\dot{J}}\Gamma_{1}/\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})}$,$\frac{\tilde{\Gamma}\Rightarrow(/F)(G/),\tilde{\Gamma}’\Rightarrow(\Gamma_{0}/\Delta_{0})}{(Farrow G/),\tilde{\Gamma},\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})}$:,$\frac{(F/)(G/),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})}{(F*G/),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})}$$\frac{\tilde{\Gamma}\Rightarrow(/F)\tilde{\Gamma}’\Rightarrow(/G)}{\tilde{\Gamma},\tilde{\Gamma}\Rightarrow(/F*G)}$[-] :$\frac{(\Gamma_{1}/F))\tilde{\Gamma}\Rightarrow(\Gamma_{0}/)}{([a]\Gamma_{1}/[a]F),\tilde{\Gamma}\Rightarrow([a]\Gamma_{0}/)}$$\frac{(\Gamma_{1}/F),(\Gamma_{2}/G),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/)}{([a]\Gamma_{1}/[a]F),([\overline{a}]\Gamma_{2}/[\overline{a}]G),\tilde{\Gamma}\Rightarrow([\tau]\Gamma_{0}/)}$に対して)$\overline{\tilde{\Gamma}\Rightarrow([a]\Gamma_{0}/[a]F)}$$(\Gamma_{i}^{a}/),\tilde{\Gamma}-(\Gamma_{i}/\Delta_{i})\Rightarrow(\Gamma_{0}/F)$(全ての $i\in\{1,2,$

但し$\ldots,$$n\}$$\tilde{\Gamma}=(\Gamma_{1}/\Delta_{1})\ldots(\Gamma_{n}/\Delta_{n})\backslash a\neq\tau$82$(\Gamma_{i}^{a}/)\mathrm{J}(\Gamma_{j}^{a}/))\tilde{\Gamma}-(\Gamma_{i}/\Delta_{i})-(\Gamma_{j}/\Delta_{j})\Rightarrow(\Gamma_{0}/F)$(全ての$\mathrm{i},$$(\Gamma_{i}^{\tau}/),\tilde{\Gamma}-(\Gamma_{i}/\Delta_{i})\Rightarrow(\Gamma_{0}/F)$$j\in\{1,2,$$\ldots,$$n\}(i\neq j)$(全ての $i\in\{1,2,$$n\}$$\ldots,$に対して)に対して)$\tilde{\Gamma}\Rightarrow([\tau]\Gamma_{0}/[\tau]F)$

但し$\tilde{\Gamma}=(\Gamma_{1}/\Delta_{1})\ldots(\Gamma_{n}/\Delta_{n})$切断$\frac{(F,\Gamma_{1}/\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})(\Gamma_{1}/F,\Delta_{1}))\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0\grave{J}}}{(\Gamma_{1}/\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/\Delta_{0})}$$\frac{(\Gamma_{1}/\Delta_{1}),\tilde{\Gamma}\Rightarrow(F,\Gamma_{0}/\Delta_{0})(\Gamma_{1}/\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}/F,\Delta_{0})}{(\Gamma_{1}/\Delta_{1}),\tilde{\Gamma}\Rightarrow(\Gamma_{0}//\Delta_{0})}$$\frac{\overline{\Gamma}\Rightarrow(F,\Gamma_{1}/\Delta_{1})(\Gamma_{1}/\Delta_{1}))\tilde{\Gamma}’\Rightarrow(\Gamma_{0}/F,\Delta_{0})}{\tilde{\Gamma},\tilde{\Gamma}’\Rightarrow(\Gamma_{0}/\Delta_{0})}$

この推論規則で式$\tilde{\Gamma}\Rightarrow(\Gamma/\Delta)$

論理式 $F$ に対して、が導出されることをを単に$\vdash\Rightarrow(/F)$$\vdash F$$\vdash\tilde{\Gamma}\Rightarrow(\Gamma/\Delta/)$と書く。と書く。

予想 73 ある式が証明可能ならば、 切断規則を使わないで証明可能である。

補題 74(健全性)$\vdash(\Gamma_{1}/\Delta_{1})(\Gamma_{2}/\Delta_{2})\ldots(\Gamma_{n}/\Delta_{n})\Rightarrow(\Gamma_{0}/\Delta_{0})$ならば、 以下を充たすプロセス$P_{n}$$P_{1},$$\ldots,$はない。

$\forall F\in\Gamma 0\cdot P_{1}*\ldots*P_{n}\models F)\ \forall F\in\Gamma_{i}$$\forall \mathrm{i}\in 1,2,$$\ldots,$

$n$

. (

$\forall F\in\Gamma_{i}$.

. $P_{1}*\ldots*P_{n}*F$\models F)&\forall F$\in\Gamma_{i}$. $P_{i}\# F$

定理 75(健全性) $\vdash F\supset\models F$
予想 76(完全性)$\models F\Rightarrow\vdash F$

更に、 この論理体系の証明探査手続によって証明不能であることが示された

場合には、 それと同時に反例構成が成されることが予想される。

参考文献
Modal and Temporal Logics’, in Abramsky, S. et.al.
:Handbook of Logic in Computer Science, vol. 2, pp477 563, Oxford
Science Pubiications, 1993.

[S]Stirling,$\mathrm{S}:\zeta$$\mathrm{e}\mathrm{d}\mathrm{s}$-[M]

Milner, R.: Communication and concurrency, Prentice-Hail Jnternational Computer Science Series archive, Prentice-Hall, Inc. 1989.