451 Let a and b be binary interactive variables. Define loop = ifbthenloopelseokfi
Add a time variable according to any reasonable measure, and then express b:= ⊥ || loop
as an equivalent program but without using || .
§ The left process owns b . Variable a could belong to either process; let’s give it to the right process. Let assignment take time 1 . Then the left process is
¬b(t+1) ∧ tʹ=t+1
Add recursive time to loop , and the right process is
loop
= if b t then t:= t+1. loop else ok fi
= if b t then t:= t+1. if b t then t:= t+1. loop else ok fi else ok fi
= if b t then if b(t+1) then t:= t+2. loop else t:= t+1 fi else ok fi
unroll Substitution Law
The left process gives us ¬b(t+1)
= if b t then if ⊥ then t:= t+2. loop else t:= t+1 fi else ok fi
= if b t then t:= t+1 else ok fi
= if b t then a tʹ = a t ∧ tʹ = t+1 else tʹ=t fi tʹ=t implies a tʹ = a t
= a tʹ = a t ∧ if b t then tʹ = t+1 else tʹ=t fi The independent composition is
∃tL, tR· ¬b(t+1) ∧ tL=t+1 ∧ a tR = a t ∧ if b t then tR = t+1 else tR=t fi
∧ tʹ = max tL tR The left process takes time 1 and the right process takes time 0 or 1 , so the maximum is 1
= ¬b(t+1) ∧ a(t+1) = a t ∧ tʹ = t+1 We no longer have an independent composition, so a and b are both variables
= b:= ⊥