- Implement transducer T<sub>0</sub>, which adds a tau after every ∆ events - Implement transducer T<sub>1</sub>, which separates events and communications - Implement transducer T<sub>2</sub>, which propagates delay up to the clock tick - Implement transducer T<sub>3</sub>, which removes the clock tick and permutes the possible sends/receives between agents - Implement the pruning of the arena to ensure only valid paths exist