並行システム論 4/10

英語授業なのでわけがわからない。板書を追うくらいはなんとかなるかと思いきや、テキストファイルでは板書を忠実に書き写すこともできません。

教科書

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*)}