並行システムの検証と実装

並行システムの検証と実装
第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)
cA  
(! 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（イベント同期）
全体としてプロセスを表す式になる
eP
イベントになる式
プロセスになる式
演算子が2つを結合する
非形式的な意味: イベント e を発行した後，
プロセス P のように振る舞うプロセスを表す
©2015 PRINCIPIA Limited
7
Prefix の結合
Prefix は右結合
abP
=
a  b  P 
左結合とすると型が合わない: '' : Event  Process  Process
ab
a, b はイベントになる式
PQ
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
チャネル受信
cx:A  P
変数
変数の値域（省略可）
受信ガードに対応する
変数のスコープは P
©2015 PRINCIPIA Limited
11
チャネルとイベント
全体はイベントを表す
c.v
チャネル
©2015 PRINCIPIA Limited
アルファベット
チャネルを通して
受け渡される値
channelc.v = c
valuec.v = v

構成要素を取り出す
関数
12
チャネル送受信は糖衣構文
c!v  P
cx:A  P

c.v  P
E y/xは字句代入
 z:{c.x | xA}  P valuez/x
変数 z は他で使用されていない新しい変数
©2015 PRINCIPIA Limited
13
チャネル送受信は糖衣構文
cx:A  d!x  1  STOP
z:{ c.x | x  A } 
d.valuez  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

iI
 P0  P1  ...  Pn1
I =  0, 1, ...,  
SyncStitch での構文
(xalt i I (P i))
©2015 PRINCIPIA Limited
I はリスト
17
Prefix Choice と選択
x:  Px
A  a b c
a  Pa  b  Pb  c  Pc
x  Px

xA
©2015 PRINCIPIA Limited
18
非決定的選択（内部選択）
P
Q
プロセス間の演算子
非形式的な意味: プロセス P, Q いずれかを非決定的に選
択し，それ以降選択されたプロセスのように振る舞うプ
ロセスを表わす
P Q  Q P
非決定的選択演算子は
可換則・結合則を満たす
P  Q  R  P  Q  R
©2015 PRINCIPIA Limited
19
インデックス付き非決定的選択
P
iI
i

P0  P1  ...  Pn1
I = 
I =  0, 1, ...,  
SyncStitch での構文
(xndc i I (P i))
©2015 PRINCIPIA Limited
I はリスト
20
逐次合成
PQ
プロセス間の演算子
非形式的な意味: まずプロセス 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
iI

P0 || P1 || ... || Pn1
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
遷移関係の例
aP
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
aP
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

PbQ
Prefix
ExtCh2
©2015 PRINCIPIA Limited
bQ
b
PbQ
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
QR
ExtCh4


P  Q  R
IntCh2
ExtCh4
QR
P  Q  R
©2015 PRINCIPIA Limited
Q

PQ
R

PR
42
遷移規則: 逐次合成
P
Seq1
P Q
P
Seq2
P Q
©2015 PRINCIPIA Limited




P


a = 
PQ
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
?
aR
Para3
  P  b  Q || a  R


?

R
|| R

並行合成の左辺はイベント a を発行しなければならない
©2015 PRINCIPIA Limited
53
遷移導出の例
Prefix
ExtCh1
Para3
P

PbQ
P

Prefix
P
  P  b  Q || a  R

©2015 PRINCIPIA Limited

aR

R
P || R

54
問題
Q  cbQ
P  acP
?
?
c  P  || Q
?
?
c
©2015 PRINCIPIA Limited
55
解答
Q  cbQ
P  acP
Prefix
Prefix
Para3
cP
c
PName
P
c  P  || Q
c
©2015 PRINCIPIA Limited
cbQ
c
Q
c
c
bQ
bQ
P || b  Q
c
56
状態遷移図
●
●
プロセス式間の遷移関係がわかると状態遷移図
を求めることができる
–
状態（グラフのノード）はプロセス式
–
遷移にはイベント（観測可能な外部イベント，内部
イベント，終了イベント）が付随する
–
状態の同一性判定は構文の同一性を使う
状態遷移図はラベル付き遷移システムともいう
（Labelled Transition System, LTS）
©2015 PRINCIPIA Limited
57
状態遷移図の導出
初期プロセスからたどれる
すべての遷移を求める
P  acP
Prefix
PName
acP
P
Prefix
cP
©2015 PRINCIPIA Limited
a
c
a
cP
P からの遷移を
すべて求める
cP
遷移のないプロセス，または
P
既出のプロセスまで※
※ 無限に状態を持つ場合もある
58
状態遷移図の導出
P  acP
P
a
cP
状態遷移図
cP
P
a
P
c
©2015 PRINCIPIA Limited
c
cP
59
問題
プロセス ,  が次のように定義されているとします:
P  acP
Q  cbQ
プロセス P || Q の状態遷移図を求めてください
c
©2015 PRINCIPIA Limited
60
解答
Prefix
PName
acP
P
Para1
P || Q
a
a
c
©2015 PRINCIPIA Limited
cP
cP
★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
bQ
Para2
P || b  Q
c
©2015 PRINCIPIA Limited
cP
c  P  || b  Q
c
b
b
Q
P || Q
c
初期プロセス
62
解答
Prefix
bQ
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
bP
©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  aP
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 aQ
R  a  R  \ {a}
©2015 PRINCIPIA Limited
83
解答
P  Q \ {a},
Q aQ
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 QP
P と Q から非決定的に選択されるようなプロセスを作
ると，P と区別することができない
まず同値性があり，それから詳細化関係が導出される
と考えることができる
©2015 PRINCIPIA Limited
89
論理式・集合との類似性
論理式
pq  pqp
 pqq
集合
AB
 A BA
 A BB
プロセス
P Q
 P QP
©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
詳細化関係の反対称律
 pqqp
論理式
pq
集合
AB
 A BB A
プロセス
P Q
 P QQP
まず詳細化関係があり，それから同値性が導出される
と考えることもできる
©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 PP
-idem
規則（等式）
規則名
©2015 PRINCIPIA Limited
113
条件分岐演算子の導入
P Q
= if b then P else Q
もし条件 b が成り立つならばプロセス P のように振る舞い，
そうでなければプロセス Q のように振る舞うプロセスを表す
©2015 PRINCIPIA Limited
114
代数規則
P PP
-idem
P PP
-idem
P QQP
-sym
P QQ 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 P  P
<·>-idem
P  Q R  P R  Q R
<·>-dist-l
R P  Q  R P   R Q
<·>-dist-r
P <true> Q  P
P <false> Q  Q
P  Q R  P  Q 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
aAX
if A  X = {}
©2015 PRINCIPIA Limited
121

代数規則による書き換え例
P  acP
P || Q
= def
Q  cbQ
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 QP
プロセス 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  acP
P || b  Q
X
Q  cbQ
(X = c)
既出の式が出現するまで書き換えてください
ヒント: -stepを逆向きに使うと式が簡単になります
©2015 PRINCIPIA Limited
125
解答
P || b  Q
= def
X = c
a  c  P || b  Q
= ||-step  = cab  ac  bc = 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 =acF
F =abcF bE
並行プロセスを逐次プロセスに書き換えることができる
©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

Download Report