英語授業なのでわけがわからない。板書を追うくらいはなんとかなるかと思いきや、テキストファイルでは板書を忠実に書き写すこともできません。
教科書
1. C.A.R Hoare
Communicating Sequential Processes
Prentice - Hall
2. Y.A.Ryan and S.A.Schneider
The Modelling and Analysis of Security Protocols: The CSP Approach
Addison - Wesley
ref. D.SANGIOGI and D.Walker
The π-calculus: A Theory of Mobile Prosesses
Cambridge University press
Concurrent System theory
Formalism 形式化
Expression | Semantics ─ Compution ─ Logic
\ Set theory × Algorithm
Event
This is an atomic process
__「 ̄ ̄ ̄State
↑event
│ ̄ ̄ ̄│
←───→
↑ ↑ ↑
Process
1. Event(actions): a, b, c,...
(Event variables x, y, z,...)
2. Processes: MS, MC,...
(Process variables: X, Y, Z,...)
(Process Meta variables: P, Q, R,...)
3. Set of Events: A, B, C,...
αP ≗ Set of Events used in prosess P
↑イコールの上に三角
i) STOP_A ≠ STOP_B A≠B
ii) (x -> P) x (a -> STOP_A)
↑ │ (a -> (a -> STOP_A))
gard │ :
prefix construction :
A = {top height}
t r
M = (r -> (t -> (r -> (r -> STOP_A))))
→→
↑r r
→t
r
iii) X = F(X)
↑start with gard
solution of X = F(X)
uX: F(X)
uX: A.F(X)
↑set of event
ex. P = (a -> P)
(a -> (a -> (a -> ...
iv) (a -> P | b -> Q) Selection construction
a ≠ b
α(a -> P | b -> Q) = αP = αQ
α(a -> P | b -> Q) = αP∪αQ∪{a, b}
n)
VM = (coin -> (coffee ->
VM | tea ->
VM))
(P coffee B -> -c-o-f-f-e-e- ->
VM|
ex) VM2 = (coin -> (coin -> VM3 | coffee -> VM2 | tea -> VM2))
VM3 = (coffee ->
VM○ | tea ->
VM○)
Mutual Recursive definition.
VM2 = (coin -> VM3)
VM3 = (coin -> VM4 | coffee -> VM2 | tea -> VM2)
VM4 = (coffee -> VM3 | tea -> VM3)
Algebraic lows
i) (x -> P | y -> Q) = (y -> Q | x -> P)
ii) STOP_A ≠ (x -> P)
iii) (x -> P) ≠ (y -> Q) q x≠y
iv) uX.F(X) = F(uX:F(X))
─── ─────
× ×
Traces (軌跡)
operators
<> 1) s^t cf.
^=
L1: s^<> = <>^s = s
L2: s^(t^u) = (s^t)^u
f:{traces}->{traces}
f is strict iff f(<>)=<>
f is distribution iff f(s^t)=f(s)^f(t)
Theorem 1.
f is distribution -> f is strict
ii) tn
t0 =<>
tn+1 = t^tn
Q2 Theorem 2
L3: tn+1 = tn^t
L4: (s^t)n+1 = s^(t^s)n^t
iii) Restriction
tPA Q3: Define tPA
ex) P{a,c} =
Q4: tPA is distribution
strict
L1: <>PA = <>
L2: PA = sPA^tPA
L3: sP{} = <>
L4: (sPA)PB = sP(A∩B)
iv) head tail
0 = x
' =
v) *
A* = {s|sPA = s}
L1: <> ∈ A*
∈ A* if x ∈ A
∈ A* if s ∈ A* and t ∈ A*
A* = {t|t: <> or (t0 ∈ A and t' ∈ A*)}