process algebra meeting minutes

2021/11/19



  • interaction

  • data process

  • can do

    • typed channel and process
    • verification (via SMT?)c
global i;

N = 
  c (c0, st_0) . 
  r <c0> . 
  r ( inl -> end
    ; inr (r0, st_r) -> 
        r <i, min st_0 st_r> .  N1)

N1 = 
  r (hs) . 
  c <hs> . 
  c ( inl j -> r <inl j> . N1 
    ; inr j -> r <inr j> . r (h_j-1, h_j) . F (h_j-1, h_j) . end)

-- multi-round = N | N | N ...
-- h_j-1 = the last agreed state hash
-- h_j = the fst disagreed state hash

F (h_j-1, h_j) -> 
  let result = eval op_j-1 h_j-1 in 
  if result = h_j 
  then WIN else LOSS

WIN = ..
LOSS = ..

C = c<c0, st0> . c (hashes) . c <f(...)> .
C2 = c(inl x -> ...
     ;inr y -> )

c : !int -> 

N = ...  c<inr w> .....

C = c (inl x -> ...
      ;inr y -> )
R = 


N | C | R

nu ()

N | (C | R1) | (C | R2) | ...

nu(c : ps<c>.pc<c> . AS)! | C1 | C2

AS = ps(c) . c(x). c(y) . c<x+y> . end  

C1 = pc(c) . c<3>.c<4>.c(r).end
C2 = pc(c) . c<5>.c<6>.c(r).end

operation semantics

(_--->_) = ...

 P | Q | R -> P' | Q' ....
 
 c<r>.P | c(x).Q ---> P | Q[x\r] --->
Select a repo