Think Stitch
PRINCIPIA  最近の更新


インターフェイス指定による並行合成の failures

CSP の教科書によると,インターフェイス指定による並行合成の failures は次のように定義されています.(今回も終了のことは無視しておきます)

\[ \begin{split} \textit{failures}(P\ \underset{X}{||}\ Q) = & \{ (u, Y \cup Z) \ |\ & Y - X &= Z - X \land \\ & & (\exists s, t. & (s, Y) \in \textit{failures}(P) \land \\ & & & (t, Z) \in \textit{failures}(Q) \land \\ & & & u \in s\ \underset{X}{||}\ t) \} \end{split} \]

この定義をはじめて見たとき,Y - X = Z - X という条件はどういう意味だろう,なぜ拒否が Y ∪ Z になるのだろう,と考え込んでしまいました. 今日は,この式の意味の説明に挑戦してみたいと思います.

Y - X = Z - X ということは,X からはみ出している Y の部分と,同じくはみ出している Z の部分が同じということです. そのままですね(^^;).図示するとこんな感じです.

X の外側にはみ出しているところは一致していて,中は別々でもかまわないということです.

なぜこんなふうになるかというと,それは次のとおりです.

X の外側にあるイベントは同期しませんから,プロセス P, Q どちらも自由に発生させることができます. したがって,どちらかが拒否しないとすると並行合成したプロセスも拒否しないことになります. したがって,両方が拒否するものだけが拒否になります.

一方 X の内側では同期しなければなりませんから,P, Q いずれか一方が拒否すれば,並行合成したプロセスも拒否することになるわけです.だから,必ずしも重なってなくてもいいわけです.

failures の別表現

この考え方を使うと,failures の別表現を導くことができます. 一般的に考えることにして,イベントの集合 W が並行合成したプロセスの拒否である必要十分条件を求めます. 先ほどのように W を X の中と外に分けます. 中は W ∩ X,外は W - X です.

中は同期しますから,どちらか一方の拒否に含まれていればいいということになります. したがって次の条件を満たすプロセス P の拒否 Y と Q の拒否 Z があればいいことになります.

\[ W \cap X \subseteq Y \cup Z \]

一方,X の外側では同期しませんから,W - X はプロセス P, Q のある拒否に同時に含まれていなければなりません.

\[ W - X \subseteq Y \cap Z \]

両者を合わせると次のような定義が得られます.

\[ \begin{split} \textit{failures}(P\ \underset{X}{||}\ Q) = \{ (u, W) \ |\ \exists & s, t, Y, Z. \\ & (s, Y) \in \textit{failures}(P) \land \\ & (t, Z) \in \textit{failures}(Q) \land \\ & u \in s\ \underset{X}{||}\ t \land \\ & W \cap X \subseteq Y \cup Z \land \\ & W - X \subseteq Y \cap Z \} \end{split} \]

2つの定義が同値であることの確認

2つの定義が同値であることを Isabelle で確認してみました.

トレースの部分は同じなので,拒否の部分だけを比較します. イベントの集合がプロセス P, Q の拒否であることを,同じ文字の述語 P, Q で表すことにします. 前提として,拒否の部分集合がまた拒否であることを置いてあります.これはだいじな健全性条件の1つです.

かなり自動証明に頼ってますけど :P ごらんのとおり同値であることが証明できます.

lemma "[|
  ALL X X1. P X & X1 <= X --> P X1;
  ALL X X1. Q X & X1 <= X --> Q X1
  |] ==>
  {W. EX Y Z. W = Y Un Z & Y - X = Z - X & P Y & Q Z} =
  {W. EX Y Z. W Int X <= Y Un Z & W - X <= Y Int Z & P Y & Q Z}"
apply(rule subset_antisym)
apply(clarsimp)
apply(rule_tac x="Y" in exI)
apply(rule_tac x="Z" in exI)
apply(clarsimp)
apply (metis Diff_subset Un_Diff sup_idem)

apply(clarsimp)
apply(rename_tac W Y Z)

apply(rule_tac x="W Int Y" in exI)
apply(rule_tac x="W Int Z" in exI)
apply(rule conjI)
apply (metis Un_Diff_Int inf_absorb1 inf_sup_distrib1 le_supI2 le_sup_iff)
apply(auto)
apply(drule_tac x="Y" in spec)
apply(rotate_tac -1)
apply(drule_tac x="W Int Y" in spec)
apply(blast)
apply(rotate_tac 1)
apply(drule_tac x="Z" in spec)
apply(rotate_tac -1)
apply(drule_tac x="W Int Z" in spec)
apply(blast)
done

プロセスの一般形で考える

別のアプローチをやってみます.一般にプロセスは次のように表すことができるでしょう. (大きい sqcap が出ないので,小さい方でがまんしてください.) ただし,非決定性がないとき,つまり添字集合 I が1個だけしか要素を持たない場合は単なる prefix choice であるとします.

\[ P = \sqcap_{i \in I} ?x:A_i \rightarrow P' \]

プロセス Q も同様に表します.

\[ Q = \sqcap_{j \in J} ?x:B_j \rightarrow Q' \]

並行合成の代数的規則によると,この2つのプロセスを並行合成した結果は次のようになります.

\[ P\ \underset{X}{||}\ Q = \sqcap_{i \in I, j \in J} ?x:C_{ij} \rightarrow R \]

ここで

\[ C_{ij} = (X \cap A_i \cap B_j) \cup (A_i - X) \cup (B_j - X) \]

です.初期状態での拒否を問題にしたいので,R のことは放っておきます.

さて,イベントの集合 W がこのプロセスの拒否になるのは,非決定性のある分岐 i, j において,Cijと W が共通部分を持たないときです.この条件を変形していくと次のようになります.

\[ \begin{split} & W \cap C_{ij} = \{\} \\ = & \\ & W \cap ((X \cap A_i \cap B_j) \cup (A_i - X) \cup (B_j - X)) = \{\} \\ = & \\ & (W \cap X \cap A_i \cap B_j) \cup (W \cap (A_i - X)) \cup (W \cap (B_j - X)) = \{\} \\ = & \\ & (W \cap X \cap A_i \cap B_j) = \{\} \land (W \cap (A_i - X)) = \{\} \land (W \cap (B_j - X)) = \{\} \\ \end{split} \]

後ろの2項は次のようにできます.

\[ \begin{split} W \cap (A_i - X) = (W - X) \cap A_i \\ W \cap (B_j - X) = (W - X) \cap B_j \end{split} \]

第1項はさらに次のように変形できます.

\[ \begin{eqnarray*} & W \cap X \cap A_i \cap B_j = \{\} \\ =& \\ & (W \cap X) \setminus (A_i \cap B_j)^\complement = \{\} \\ =&\\ & W \cap X \subseteq (A_i \cap B_j)^\complement \\ =&\\ & W \cap X \subseteq {A_i}^\complement \cup {B_j}^\complement \\ =&\\ & W \cap X = W \cap X \cap ({A_i}^\complement \cup {B_j}^\complement) \\ =&\\ & W \cap X = (W \cap X \cap {A_i}^\complement) \cup (W \cap X \cap {B_j}^\complement) \end{eqnarray*} \]

そこで次のように Y と Z を定義します.

\[ \begin{split} Y &= (W - X) \cup (W \cap X \cap {A_i}^\complement) \\ Z &= (W - X) \cup (W \cap X \cap {B_j}^\complement) \end{split} \]

すると

\[ \begin{split} & Y - X = Z - X = W - X \\ & Y \cup Z = W \end{split} \]

というわけで,Y, Z はこんなふうになってるわけです.

2013/11/28
© 2013,2014,2015 PRINCIPIA Limited