並行システムの検証と実装 第10章 CSP 理論 PRINCIPIA Limited 初谷 久史 ©2015 PRINCIPIA Limited CSP とは ● ● Communicating Sequential Processes 並行システムの振る舞いを記述し,その性質を論証する ための数学的理論 – プロセス代数と呼ばれる理論の1つ(他にπ計算など) ● 1978年 C. A. R. Hoare によって提案された ● 特徴 – 詳細化関係の定義 – 豊富な意味論 ©2015 PRINCIPIA Limited 2 Photograph by Rama, Wikimedia Commons, Cc-by-sa-2.0-fr CSP 理論 ● 構文論 ● 意味論 – 操作的意味論 – 表示的意味論 – ● ● トレース意味論 ● 安定失敗意味論 ● 失敗発散意味論 代数的意味論 各意味論間の関係 ©2015 PRINCIPIA Limited 3 構文 ::=| | | | | | | | | | SyncStitch での記法 STOP SKIP e A c!v STOP SKIP 停止プロセス 終了プロセス (! e P) 同期(prefix) (xalt x A (! x P)) prefix choice チャネル送信 Q Q Q || Q (alt P Q) cA (! c (v) P) (? c (x) (member x A) P) チャネル受信 (ndc P Q) 選択 非決定的選択 (seq P Q) (par X P Q) 逐次合成 並行合成 (par '() P Q) (hide X P) インターリーブ X | ||| Q ©2015 PRINCIPIA Limited | \X 隠蔽 4 構文例 CSP での記法 a b c STOP SyncStitch での記法 (! a (! b (! c STOP))) a STOP b STOP P || Q \ C X ©2015 PRINCIPIA Limited (alt (! a STOP) (! b STOP)) (hide C (par X P Q)) 5 プロセスを表す式 (a P b Q) \ {b} x (a x) (A x) B プロセスを表す式 数を表す式 集合を表す式 ベクトルを表す式 ©2015 PRINCIPIA Limited 6 Prefix(イベント同期) 全体としてプロセスを表す式になる eP イベントになる式 プロセスになる式 演算子が2つを結合する 非形式的な意味: イベント e を発行した後, プロセス P のように振る舞うプロセスを表す ©2015 PRINCIPIA Limited 7 Prefix の結合 Prefix は右結合 abP = a b P 左結合とすると型が合わない: '' : Event Process Process ab a, b はイベントになる式 PQ P, Q はプロセスになる式 ©2015 PRINCIPIA Limited 誤った式 ill-formed 8 Prefix Choice 変数のスコープは P x:A P 変数 イベントの集合 になる式 プロセスになる式 Prefix Choice であることを示す記号(つけない流儀もある) 非形式的な意味: イベントの集合 A に含まれるいずれ かのイベントを発行した後,変数の値が発行したイベ ントである環境でプロセス P のように振る舞うプロセ スを表す ©2015 PRINCIPIA Limited 9 Prefix Choice の例 x:a b c x STOP a b a b c c ©2015 PRINCIPIA Limited この範囲では x=c 10 チャネル送受信 チャネルになる式 送信する値になる式 チャネル送信 c!v P チャネル受信 cx:A P 変数 変数の値域(省略可) 受信ガードに対応する 変数のスコープは P ©2015 PRINCIPIA Limited 11 チャネルとイベント 全体はイベントを表す c.v チャネル ©2015 PRINCIPIA Limited アルファベット チャネルを通して 受け渡される値 channelc.v = c valuec.v = v 構成要素を取り出す 関数 12 チャネル送受信は糖衣構文 c!v P cx:A P c.v P E y/xは字句代入 z:{c.x | xA} P valuez/x 変数 z は他で使用されていない新しい変数 ©2015 PRINCIPIA Limited 13 チャネル送受信は糖衣構文 cx:A d!x 1 STOP z:{ c.x | x A } d.valuez 1 STOP ©2015 PRINCIPIA Limited 14 選択(外部選択) P Q プロセス間の演算子 非形式的な意味: プロセス P, Q それぞれが最初に提示す るイベントをすべて提示し,P が提示したイベントが発 生したらそれ以降 P のように振る舞い,Q が提示したイ ベントが発生したらそれ以降は Q のように振る舞うプロ セスを表す ©2015 PRINCIPIA Limited 15 選択演算子の可換性・結合性 選択演算子は可換則と結合則を満たす P Q Q P P Q R P Q R 3つ以上のプロセスからの選択は 括弧を使わず任意の順序で書ける ©2015 PRINCIPIA Limited P Q R 16 インデックス付き選択 Pi iI P0 P1 ... Pn1 I = 0, 1, ..., SyncStitch での構文 (xalt i I (P i)) ©2015 PRINCIPIA Limited I はリスト 17 Prefix Choice と選択 x: Px A a b c a Pa b Pb c Pc x Px xA ©2015 PRINCIPIA Limited 18 非決定的選択(内部選択) P Q プロセス間の演算子 非形式的な意味: プロセス P, Q いずれかを非決定的に選 択し,それ以降選択されたプロセスのように振る舞うプ ロセスを表わす P Q Q P 非決定的選択演算子は 可換則・結合則を満たす P Q R P Q R ©2015 PRINCIPIA Limited 19 インデックス付き非決定的選択 P iI i P0 P1 ... Pn1 I = I = 0, 1, ..., SyncStitch での構文 (xndc i I (P i)) ©2015 PRINCIPIA Limited I はリスト 20 逐次合成 PQ プロセス間の演算子 非形式的な意味: まずプロセス P のように振る舞い,P が正常終了した場合は,その後プロセス Q のように振る 舞うプロセスを表す ©2015 PRINCIPIA Limited 21 逐次合成の例 a SKIP b SKIP a b SKIP a STOP b SKIP a STOP "同じ"の意味は後で定義 ©2015 PRINCIPIA Limited 22 並行合成 P || Q X 2つのプロセスとイベント集合の 3項間演算子 非形式的な意味: プロセス P, Q が並行に動作した場合の 振る舞いを表すプロセス.プロセス P, Q 間でイベントの 集合 X に属するイベントは同期し,属していないイベン トは同期しない ©2015 PRINCIPIA Limited 23 並行合成演算子の可換性・結合性 並行合成演算子は可換則と結合則を満たす P || Q Q || P X P X || Q || R P || Q || R X ©2015 PRINCIPIA Limited X X X 24 インデックス付き並行合成 || Pi X iI P0 || P1 || ... || Pn1 X I = X X I = 0, 1, ..., SyncStitch での構文 (xpar i I X (P i)) ©2015 PRINCIPIA Limited I はリスト 25 インターリーブ P ||| Q P || Q {} ©2015 PRINCIPIA Limited プロセス間の演算子 イベントの集合として空集合を 指定した並行合成と同じ 26 隠蔽 P \C プロセスとイベントの集合の 間の演算子 非形式的な意味: プロセス P が発生するイベントのう ち,イベントの集合 C に属するものを内部イベント tau に変換したプロセスを表す ©2015 PRINCIPIA Limited 27 プロセス定義 P (x x1 x) プロセスパラメータ プロセスパラメータのスコープは プロセス式 E プロセス名 Px,y プロセス式 プロセスパラメータは添字で書く場合もある ©2015 PRINCIPIA Limited 28 プロセス定義の例 P s in?x P s x out!s P 0 SyncStitch での表現 (define-process (P s) (alt (? in (x) (P (+ s x))) (! out (s) (P 0)))) ©2015 PRINCIPIA Limited 29 CSP の意味論 CSP の3つの意味論 ● 操作的意味論 ● 表示的意味論 ● 代数的意味論 ©2015 PRINCIPIA Limited 31 プロセスの操作的意味論 ● ● プロセスが実行できる遷移を定めることが意味を定めるこ とになるという考え方 プロセスを表す well-formed なすべての式について,どの ようなイベントを発行し,どのような式に遷移するかとい う遷移関係を定める 観測可能イベント 内部イベント 終了イベント P P プロセスを表す式 ©2015 PRINCIPIA Limited 遷移関係を表す矢印 32 遷移関係の例 aP P Q SKIP ©2015 PRINCIPIA Limited a P P 正常終了後のプロセス 33 推論規則による遷移関係の定義 推論規則の形式 0個以上の前提 (条件) 規則名 導出される結論 前提がすべて満たされ,かつ付帯条件が成り立つならば 結論が成り立つ ©2015 PRINCIPIA Limited 34 遷移規則: プロセス名 PName P N a a P P プロセス定義 プロセス名 N がプロセス式 P で定義されていて, かつ P がイベント a を発行して P' に遷移するならば, N はイベント a を発行して P' に遷移することができる ©2015 PRINCIPIA Limited 35 遷移規則: Prefix, SKIP 前提はない Prefix aP Skip SKIP ©2015 PRINCIPIA Limited a P a アルファベット 正常終了後のプロセス 36 遷移規則: 選択 1/2 P a ExtCh1 ExtCh2 P Q ©2015 PRINCIPIA Limited P a = P Q Q a P の場合を含む Q a = Q 37 遷移規則: 選択 2/2 P ExtCh3 P Q Q ExtCh4 P Q ©2015 PRINCIPIA Limited P P Q Q P Q 38 遷移導出: 選択 導出木 Prefix P ExtCh1 PbQ Prefix ExtCh2 ©2015 PRINCIPIA Limited bQ b PbQ P P Q b Q 39 遷移導出: SKIP との選択 Prefix P ExtCh1 P SKIP Skip ExtCh2 SKIP P SKIP ©2015 PRINCIPIA Limited P P 40 遷移規則: 非決定的選択 IntCh1 P Q IntCh2 P Q ©2015 PRINCIPIA Limited P Q 41 遷移導出: 非決定的選択と選択 IntCh1 QR ExtCh4 P Q R IntCh2 ExtCh4 QR P Q R ©2015 PRINCIPIA Limited Q PQ R PR 42 遷移規則: 逐次合成 P Seq1 P Q P Seq2 P Q ©2015 PRINCIPIA Limited P a = PQ P Q 43 遷移規則: 並行合成 1/4 P Para1 P || Q P P || Q a A {} インターリーブ Q Para2 P || Q ©2015 PRINCIPIA Limited Q P || Q a A {} 44 遷移規則: 並行合成 2/4 イベント同期 P Para3 P || Q ©2015 PRINCIPIA Limited P Q Q P || Q a 45 遷移規則: 並行合成 3/4 P Para4 P || Q Q Para5 P || Q ©2015 PRINCIPIA Limited P || Q Q 各コンポーネントは 独立して終了できる P || 外部からは見えない 46 遷移規則: 並行合成 4/4 Para6 || すべてのコンポーネントが終了すると 並行合成したプロセスが終了する ©2015 PRINCIPIA Limited 47 遷移規則: 隠蔽 1/2 P Hide1 P \X P Hide2 P \X ©2015 PRINCIPIA Limited P P \X P a A {} P \X a 48 遷移規則: 隠蔽 2/2 P Hide3 P \X P 終了イベントは隠蔽されない ©2015 PRINCIPIA Limited 49 遷移導出の考え方 ? ? P b Q || a R ? ? ©2015 PRINCIPIA Limited 50 遷移導出の考え方: 抽象構文木 最上位の演算子は 並行合成 P b Q || a R || 並行合成の遷移規則は6個 順に適用可能か調べる ©2015 PRINCIPIA Limited P {} b R Q 51 遷移導出の考え方 ? Para3 P b Q || a R ? || R 並行合成の右辺はイベント a のみ発行可能 イベント a は同期する ©2015 PRINCIPIA Limited 52 遷移導出の考え方 Prefix ? aR Para3 P b Q || a R ? R || R 並行合成の左辺はイベント a を発行しなければならない ©2015 PRINCIPIA Limited 53 遷移導出の例 Prefix ExtCh1 Para3 P PbQ P Prefix P P b Q || a R ©2015 PRINCIPIA Limited aR R P || R 54 問題 Q cbQ P acP ? ? c P || Q ? ? c ©2015 PRINCIPIA Limited 55 解答 Q cbQ P acP Prefix Prefix Para3 cP c PName P c P || Q c ©2015 PRINCIPIA Limited cbQ c Q c c bQ bQ P || b Q c 56 状態遷移図 ● ● プロセス式間の遷移関係がわかると状態遷移図 を求めることができる – 状態(グラフのノード)はプロセス式 – 遷移にはイベント(観測可能な外部イベント,内部 イベント,終了イベント)が付随する – 状態の同一性判定は構文の同一性を使う 状態遷移図はラベル付き遷移システムともいう (Labelled Transition System, LTS) ©2015 PRINCIPIA Limited 57 状態遷移図の導出 初期プロセスからたどれる すべての遷移を求める P acP Prefix PName acP P Prefix cP ©2015 PRINCIPIA Limited a c a cP P からの遷移を すべて求める cP 遷移のないプロセス,または P 既出のプロセスまで※ ※ 無限に状態を持つ場合もある 58 状態遷移図の導出 P acP P a cP 状態遷移図 cP P a P c ©2015 PRINCIPIA Limited c cP 59 問題 プロセス , が次のように定義されているとします: P acP Q cbQ プロセス P || Q の状態遷移図を求めてください c ©2015 PRINCIPIA Limited 60 解答 Prefix PName acP P Para1 P || Q a a c ©2015 PRINCIPIA Limited cP cP ★A 後で再利用 c P || Q c c P || Q a c c P || b Q c 練習問題の結果 61 解答 ★A P Para1 P || b Q a a c Prefix bQ Para2 P || b Q c ©2015 PRINCIPIA Limited cP c P || b Q c b b Q P || Q c 初期プロセス 62 解答 Prefix bQ Para2 c P || b Q c b b Q c P || Q c 既出 ©2015 PRINCIPIA Limited 63 解答 P || Q c b a c P || Q c c P || b Q c b a ©2015 PRINCIPIA Limited c P || b Q c 64 操作的意味論: まとめ ● ● 操作的意味論ではプロセスが実行できる遷移を遷移規則に よって定めることで意味を定める 遷移関係から状態遷移図を求めることができる ©2015 PRINCIPIA Limited 65 操作的意味論: 課題 ● プロセスの振る舞いについては厳密に定めることができた が,プロセス間の同値性や詳細化関係については何もいえ ない – 同値性については,計算木の同一性を採用する,あるいは 双模倣(Bisimulation)という概念を導入すると定めること ができる – 内部イベントを考慮した同値性を定義することは難しい ©2015 PRINCIPIA Limited 66 CSP の3つの意味論 ● 操作的意味論 ● 表示的意味論 ● 代数的意味論 ©2015 PRINCIPIA Limited 67 表示的意味論 ● ● 構文が表す意味を数学的に構築して,構文に対応付け る(意味を与える)という考え方 構文が表す意味のことを表示(denotation)という 構文の集合 P || Q bP ©2015 PRINCIPIA Limited 意味の集合 P Q SKIP 対応付ける 68 CSP の3つの表示的意味論 ● トレース意味論 ● 安定失敗意味論 ● 失敗発散意味論 ©2015 PRINCIPIA Limited 69 トレース意味論 ● プロセスの意味は,プロセスが発生する可能性のある すべてのトレースの集合であるとする考え方 [ ] traces(P ) 意味関数 構文に意味を対応付ける関数 ©2015 PRINCIPIA Limited 70 トレース集合の定義 traces(STOP) = } traces(SKIP) = } traces(a P ) = } a^s | s traces(P )} traces(P Q) = traces(P ) traces(Q) traces(P Q) = traces(P ) traces(Q) ©2015 PRINCIPIA Limited 選択と非決定的選択は区別できない 71 トレース集合の定義: 逐次合成 逐次合成 traces(P Q ) = s | s traces(P ) A (s)} s^t | s^ traces(P ) t traces(Q )} (s) はイベント列 s に含まれるイベントの集合 ©2015 PRINCIPIA Limited 72 トレース集合の定義: 並行合成 並行合成 traces(P || Q ) = u | s t. s traces(P ) X t traces(Q ) u synchX(s t) } ©2015 PRINCIPIA Limited 73 トレース集合の定義: synchX 関数 synchX(s t) の定義 x x X x = x y y A X とするとき synchX(s t) synchX(t s) synchX( ) } synchX( x) } synchX( y) y} ©2015 PRINCIPIA Limited 74 トレース集合の定義: synchX 関数 synchX(s t) の定義(つづき) synchX(x^s y^t) y^u | u synchX(x^s t)} synchX(x^s x^t) x^u | u synchX(s t)} synchX(x^s x^t) } synchX(y^s y ^t) y^u | u synchX(s y ^t)} y ^u | u synchX(y^s t)} ©2015 PRINCIPIA Limited 75 トレース集合の定義: synchX 関数 synchX(s t) の定義(つづき) synchX(s t^) } synchX(s^ t^) u^ | u synchX(s t)} ©2015 PRINCIPIA Limited 76 トレース集合の定義: 隠蔽 隠蔽 traces(P \ X ) = s \ X | s traces(P ) } イベント列の隠蔽 \ X x^s \ X s \ X y^s \ X y^s \ X s^ \ X s \ X^ ©2015 PRINCIPIA Limited x X y A X 77 トレース集合の定義: 再帰的定義 再帰的に定義されたプロセスの場合 P aP traces(P ) = traces(a P ) traces(P ) = } a^s | s traces(P )} これは traces(P ) を未知数とする方程式になっている X = } a^s | s X} ©2015 PRINCIPIA Limited 78 トレース集合の定義: 再帰的定義 X = } a^s | s X} X s X a^s X X = s | s a}} は集合 の要素からなるすべて有限な列の集合 = a a a a a a } ©2015 PRINCIPIA Limited 79 トレース集合の定義: 再帰的定義 P P a STOP traces(P ) = traces(P a STOP) traces(P ) = traces(P ) } a^s | s traces(STOP)} X = X a} 解が複数存在する と a が含まれる任意の集合が解になる ©2015 PRINCIPIA Limited ※ トレース集合として健全であるために条件がつく 80 ガードされたプロセス ● ● 再帰的に定義されたプロセスにおいて,どの選択を 通っても少なくとも1つのイベントを発生させてから 再帰する場合,プロセスはガードされているという ガードされているプロセスのトレース集合は唯一に定 まる ● ガードされていないプロセスは発散する ● 発散したプロセスのトレース集合は不定になる P P a STOP ©2015 PRINCIPIA Limited ガードされていない プロセスの例 81 トレース集合の定義: 再帰的定義 P a P \ {a} traces(P ) = } a^s | s traces(P \ {a})} = } a^s | s s \ {a} | s traces(P )}} = } a^(s \ {a}) | s traces(P )} X = } a^(s \ {a}) | s X} a で始まり,それ以降 a を含まない任意のトレースが含まれ得る ©2015 PRINCIPIA Limited ※ トレース集合として健全であるために条件がつく 82 問題 ● 次のように定義されたプロセスのトレース集合 を求めてください P Q \ {a}, Q aQ R a R \ {a} ©2015 PRINCIPIA Limited 83 解答 P Q \ {a}, Q aQ traces(P ) = s \ {a} | s traces(Q) } = s \ {a} | s s | s {a}*} = s \ {a} | s {a}*} = } ©2015 PRINCIPIA Limited 84 解答 R a R \ {a} traces(R ) = s \ {a} | s traces(a R ) } = s \ {a} | s } a^s | s traces(R )}} = } s \ {a} | s traces(R )} X = } s \ {a} | s X} a を含まないトレースからなる集合が解になる ©2015 PRINCIPIA Limited ※ トレース集合として健全であるために条件がつく 85 表示的意味論の利点 ● ● プロセスの同値性,詳細化関係を定義できる 同値性,詳細化関係が Congruence であること を証明できる ©2015 PRINCIPIA Limited 86 プロセスの同値性 2つのプロセスが同値である(同じ振る舞いを持つ)というこ とを意味が同じであるとして定義することができる P Q [ ] [Q] トレース意味論の場合 P Q traces(P ) traces(Q) ©2015 PRINCIPIA Limited 87 詳細化関係 CSP の表示的意味論では,集合の包含関係によって詳細化関 係を定義することができる トレース意味論の場合 P Q traces(P ) traces(Q) ©2015 PRINCIPIA Limited 88 詳細化関係の直観的説明 プロセス P と Q の間に詳細化関係 P Q が成り立つとは プロセス Q の振る舞いがプロセス P の振る舞いの中に含まれ ている(許容されている)ということである P Q P QP P と Q から非決定的に選択されるようなプロセスを作 ると,P と区別することができない まず同値性があり,それから詳細化関係が導出される と考えることができる ©2015 PRINCIPIA Limited 89 論理式・集合との類似性 論理式 pq pqp pqq 集合 AB A BA A BB プロセス P Q P QP ©2015 PRINCIPIA Limited B A 90 詳細化関係の導出 トレース意味論の場合 P Q P Q P traces(P Q) traces(P ) traces(P ) traces(Q) traces(P ) traces(P ) traces(Q) ©2015 PRINCIPIA Limited 91 詳細化関係の反対称律 pqqp 論理式 pq 集合 AB A BB A プロセス P Q P QQP まず詳細化関係があり,それから同値性が導出される と考えることもできる ©2015 PRINCIPIA Limited 92 段階的詳細化 ● ● プログラムの開発は仕様 Spec からはじめて段階的に 詳細化を行い,最終的に実行可能な実装 Imp を得る 過程だと考えられる.これを段階的詳細化(Stepwise Refinement)という 開発を段階に分けることで,各段階での問題を小さく 簡単にすることができる Spec P P2 P Imp ©2015 PRINCIPIA Limited 93 Congruence 関係 ● システムのコンポーネントを詳細化関係の成り立つコン ポーネントに入れ替えたとき,入れ替え前後のシステムの 間で詳細化関係が成り立つことが保証されている.これを Congruent であるという P S P' S' P ©2015 PRINCIPIA Limited Q P' Q 94 Congruence 関係 Prefix の場合 合成性 構成要素のトレース集合を元に 全体のトレース集合が定義されている traces(a P ) = } a^s | s traces(P )} P P traces(P ) traces(P ) a^s | s traces(P )} a^s | s traces(P )} traces(a P ) traces(a P ) a P a P ©2015 PRINCIPIA Limited 単調性 P P C[P ] C[P ] 95 CSP の3つの表示的意味論 ● トレース意味論 ● 安定失敗意味論 ● 失敗発散意味論 ©2015 PRINCIPIA Limited 96 安定失敗意味論 ● プロセスの意味はトレース集合と安定失敗集合のペア であるとする考え方 [ ] (traces(P ) failures(P )) failures(P ) = (s X) | s traces(P ) X refusals(P/s )} 拒否 ©2015 PRINCIPIA Limited 後 97 安定失敗集合の定義 failures(STOP) = ( X) | X } failures(SKIP) = ( X) | X } ( X) | X } failures(a P ) = ( X) | a A X} (a^s X) | (s X) failures(P )} ©2015 PRINCIPIA Limited 98 安定失敗集合の定義 安定失敗意味論では非決定的選択と選択を区別できる failures(P Q) = failures(P ) failures(Q) failures(P Q) = ( X) | ( X) failures(P ) failures(Q)} (s X) | s = (s X) failures(P ) failures(Q)} ( X) | X traces(P ) traces(Q)} ©2015 PRINCIPIA Limited 99 安定失敗集合の定義 failures(P Q) = (s X) | (s X }) failures(P )} (s^t X) | s^ traces(P ) (t X ) failures(Q)} failures(P || Q) = (u Y Z ) | X Y (X }) = Z (X }) s t (s Y ) failures(P ) (t Z ) failures(Q) ©2015 PRINCIPIA Limited u synchX(s t) 100 安定失敗集合の定義 failures(P \ X) = (s \ X Y ) | (s X Y ) failures(P )} ©2015 PRINCIPIA Limited 101 プロセスの同値性と詳細化関係 P F Q traces(P ) traces(Q) failures(P ) failures(Q) P F Q traces(P ) traces(Q) failures(P ) failures(Q) failures(P Q) = failures(P ) failures(Q) P F Q P Q F P ©2015 PRINCIPIA Limited 102 安定失敗集合: 非決定的選択 failures(a P b Q) = failures(a P ) failures(b Q) = ( X) | a A X} (a^s X) | (s X) failures(P )} ( X) | b A X} (b^s X) | (s X) failures(Q)} ©2015 PRINCIPIA Limited 103 安定失敗集合: 選択 failures(a P b Q) ( X) | ( X) failures(a P ) failures(b Q)} (s X) | s = (s X) failures(a P ) failures(b Q)} ( X) | a A X b A X} (a^s X) | (s X) failures(P )} (b^s X) | (s X) failures(Q)} ©2015 PRINCIPIA Limited 104 安定失敗集合: 非決定的選択と選択 failures(a P b Q) ( X) | a A X} ( X) | b A X} (a^s X) | (s X) failures(P )} (b^s X) | (s X) failures(Q)} failures(a P b Q) ( X) | a A X b A X} (a^s X) | (s X) failures(P )} (b^s X) | (s X) failures(Q)} ©2015 PRINCIPIA Limited 105 発散の安定失敗集合 P Q \ {a} where Q a Q failures(Q) = ( X) | a A X} (a^s X) | (s X) failures(Q)} = (s X) | s a} a A X} failures(P ) = (s \ {a} Y ) | (s {a} Y ) failures(Q)} = (s \ {a} Y ) | s a} a A {a} Y } = } ©2015 PRINCIPIA Limited 106 CSP の3つの表示的意味論 ● トレース意味論 ● 安定失敗意味論 ● 失敗発散意味論 ©2015 PRINCIPIA Limited 107 失敗発散意味論 ● ● ● プロセスの意味は拡張された失敗集合と発散トレース集合 のペアであるとする考え方 発散トレース集合 divergences(P ) は発散に至るすべての トレースからなる集合.発散後の任意のトレースも含む 拡張された失敗集合 failures(P ) は安定失敗に加えて発散 に至るトレース s と任意のイベント集合 X のペア (s, X) を含む [ ] (failures(P ) divergences(P )) ©2015 PRINCIPIA Limited 108 失敗発散意味論における詳細化関係の解釈 ● ● ● 実装は仕様が発生させてもよいとするトレースだけ発生し てよい 実装は各トレース後に仕様が拒否してもよいとするイベン ト集合だけを拒否してよい 実装は仕様が発散してもよいとするトレース後だけ発散し てもよい P FD Q failures(P ) failures(Q) divergences(P ) divergences(Q) ©2015 PRINCIPIA Limited 109 安定失敗と失敗発散の違い ● ● 安定失敗意味論 – 発散しているプロセスについては何もいえない – 発散したプロセスが発散から脱出できたと仮定した場 合に,それ以降の挙動を調べることができる 失敗発散意味論 – 発散するプロセスに対しても詳細化関係を調べること ができる – プロセスが発散した後の挙動を調べることはできない ©2015 PRINCIPIA Limited 110 表示的意味論: まとめ ● 表示的意味論では数学的に構築した意味を構文に対応付ける ● CSP ではプロセスを識別する能力の異なる複数の意味を定義できる – トレース意味論: トレース集合 ● – 安定失敗意味論: トレース集合と安定失敗集合 ● – ● ● 安全性 活性 失敗発散意味論: 失敗集合と発散トレース集合 プロセスの同値性と詳細化関係を定義できる 同値性と詳細化関係が CSP の各演算子に対して Congruence であるこ とを確認できる.特に並行合成に対する Congruence は段階的詳細化を 支援する ©2015 PRINCIPIA Limited 111 CSP の3つの意味論 ● 操作的意味論 ● 表示的意味論 ● 代数的意味論 ©2015 PRINCIPIA Limited 112 代数的意味論 ● プロセスの同値性を規則の集合によって定義す ることで意味を定めるとする考え方 選択の冪等性 P PP -idem 規則(等式) 規則名 ©2015 PRINCIPIA Limited 113 条件分岐演算子の導入 P <b> Q = if b then P else Q もし条件 b が成り立つならばプロセス P のように振る舞い, そうでなければプロセス Q のように振る舞うプロセスを表す ©2015 PRINCIPIA Limited 114 代数規則 P PP -idem P PP -idem P QQP -sym P QQ P -sym P Q R P Q R -assoc P Q R P Q R -assoc ©2015 PRINCIPIA Limited 115 代数規則 P Q R P Q P R -dist a P Q a P a Q prefix-dist ?x A P Q ?x A P ?x A Q input-dist P Q R P Q P R a P [a/x] ?x a P STOP ?x P STOP P P ©2015 PRINCIPIA Limited --dist prefix-step STOP-step -unit 116 代数規則 -step ?x A P ?x B Q ?x A B P Q <x A B> P <x A> Q P <b> P P <·>-idem P Q <b> R P <b> R Q <b> R <·>-dist-l R <b> P Q R <b> P R <b> Q <·>-dist-r P <true> Q P P <false> Q Q P Q <b> R P Q <b> P R ©2015 PRINCIPIA Limited <true>-id <false>-id <·>--dist 117 代数規則 P || Q Q || P ||-sym P || (Q R) (P || Q) (P || R) ||-dist P || (Q || R) (P || Q) || R ||-assoc X X X X X X X ©2015 PRINCIPIA Limited X X X X X 118 代数規則 P ?x A P , Q ?x B Q ||-step P || Q ?x C P || Q <x X> X X X P || Q P || Q <x A B> X X P || Q <x A> P || Q)) X X C = X A B A X B X ©2015 PRINCIPIA Limited 119 代数規則 P Q \ X P \ X Q \ X P \ X \ Y P \ X Y hide-combine null hiding P \ {} P a P \ X ©2015 PRINCIPIA Limited hide-dist P \X a P \ X if a X if a A X hide-step1 120 代数規則 hide-step (?x A P ) \ X ?x A (P \ X) if A X {} ((?x (A X) (P \ X)) STOP) P [a/x] \ X aAX if A X = {} ©2015 PRINCIPIA Limited 121 代数規則による書き換え例 P acP P || Q = def Q cbQ X = c a c P || c b Q = ||-step = c a c a c c c = a a c P || c b Q = ||-step = c c c c c c c = c a c P || b Q 並行プロセスの振る舞いを前から切り出してくことができる ©2015 PRINCIPIA Limited 122 代数的意味論における詳細化関係 P Q P QP プロセス Q がプロセス P の詳細化であることを示すために は,代数的規則を使って P Q P を証明すればよい ©2015 PRINCIPIA Limited 123 詳細化関係の証明例 a P b Q a P = def a P b Q a P = a P b Q = -sym a P a P b Q = a P b Q = -assoc a P a P b Q = a P b Q = -idem a P b Q = a P b Q = reflexivity true ©2015 PRINCIPIA Limited 124 問題 P acP P || b Q X Q cbQ (X = c) 既出の式が出現するまで書き換えてください ヒント: -stepを逆向きに使うと式が簡単になります ©2015 PRINCIPIA Limited 125 解答 P || b Q = def X = c a c P || b Q = ||-step = cab ac bc = a, b ?x:{a, b} c P || b Q <x=a> a c P || Q = -step, def, prefix-step a c P || b Q b P || Q = ||-step a b c P || Q b P || Q = ||-step, def a b c P || b Q b P || Q ©2015 PRINCIPIA Limited 126 並行プロセスから逐次プロセスへの変換 P || Q = a c P || b Q P || b Q = a b c P || b Q b P || Q E P || Q F P || b Q E =acF F =abcF bE 並行プロセスを逐次プロセスに書き換えることができる ©2015 PRINCIPIA Limited 127 代数的意味論まとめ ● ● ● 代数的意味論ではプロセスの同値性を規則の集 合によって定義することで意味を定める 規則を使った式の変形によって並行プロセスを 逐次プロセスに変換することができる 式変形によって詳細化関係を証明できる ©2015 PRINCIPIA Limited 128 各意味論間の関係 ● 操作的意味論と表示的意味論の関係 ● 表示的意味論と代数的意味論の関係 ©2015 PRINCIPIA Limited 129 操作的意味論と表示的意味論の関係 表示的意味論 操作的意味論 遷移規則 導出 トレース集合 失敗集合 発散トレース集合 比較 トレース集合op 失敗集合op 発散トレース集合op 表示的意味論の意味概念を ラベル付き遷移システム上で定義する ©2015 PRINCIPIA Limited 130 イベント列に対する遷移関係 遷移関係 a これを元にイベント列に対する遷移を定義する -遷移 -遷移 ©2015 PRINCIPIA Limited s は を含んでいてもよい 末尾に があってもよい s は を含まない 末尾に があってもよい 131 イベント列に対する遷移関係 -遷移 0 ... のとき P0 P P P ... P P ak k が成り立つ が存在して,すべての k について k -遷移 s ある が存在して \ {} かつ ©2015 PRINCIPIA Limited 132 操作的意味論上での意味概念定義 安定性 Q. Q Q 拒否 ref Q. Q Q a X. R. Q ©2015 PRINCIPIA Limited a R 133 操作的意味論上での意味概念定義 発散 ある P0 P P P ... が存在して すべての k について k ©2015 PRINCIPIA Limited k が成り立つ 134 操作的意味論上での意味概念定義 トレース集合 s racesop( ) = {s | Q. Q } 安定失敗集合 failuresop( ) = {(s, X) | Q. s (s^, X) | Q. ©2015 PRINCIPIA Limited Q r X s^ Q} 135 操作的意味論上での意味概念定義 発散トレース集合 divergencesop( ) = {s^t | Q. ©2015 PRINCIPIA Limited s Q Q 136 操作的意味論と表示的意味論の関係 表示的意味論 操作的意味論 races( ) = racesop( ) failures( ) = failuresop( ) divergences( ) = divergencesop( ) ©2015 PRINCIPIA Limited 137 各意味論間の関係 ● 操作的意味論と表示的意味論の関係 ● 表示的意味論と代数的意味論の関係 ©2015 PRINCIPIA Limited 138 代数的意味論と表示的意味論の関係 代数的意味論 表示的意味論 比較 =Q = Q =F Q =FD Q ©2015 PRINCIPIA Limited 139 CSP 理論まとめ ● 構文論 ● 意味論 – 操作的意味論 – 表示的意味論 – ● ● トレース意味論 ● 安定失敗意味論 ● 失敗発散意味論 代数的意味論 各意味論間の関係 ©2015 PRINCIPIA Limited 140 CSP 理論まとめ ● 操作的意味論 – ● 表示的意味論 – ● 操作的意味論ではプロセスが実行できる遷移を遷移規則 によって定めることで意味を定める 表示的意味論では数学的に構築した意味を構文に対 応付ける 代数的意味論 – 代数的意味論ではプロセスの同値性を規則の集合に よって定義することで意味を定める ©2015 PRINCIPIA Limited 141 CSP 理論まとめ ● ● ● トレース意味論 – トレース集合を意味とする – 安全性 安定失敗意味論 – トレース集合と安定失敗集合を意味とする – 活性 失敗発散意味論 – 失敗集合と発散トレース集合を意味とする – 発散フリー性 ©2015 PRINCIPIA Limited 142 CSP 理論まとめ ● プロセス間の同値関係と詳細化関係が定義されている ● 詳細化関係は段階的詳細化を支援する ● ● 同値関係と詳細化関係は CSP の各演算子に対して Congruent である Congruence は段階的詳細化を支援する Spec P P2 P Imp P P C[P ] C[P ] ©2015 PRINCIPIA Limited 143
© Copyright 2025 ExpyDoc