Building finite automata from DI specifications

Numerous formalisms exist to specify delay-insensitive computations and their implementations. It is not always straightforward to compare specifications in the different formalisms. One way of comparing specifications is transforming them to automata in which nodes are annotated with progress requirement. In this paper we present an alogorithm that transforms DI-algebra recursive process expressions into finite automata. In doing so we develop an operational semantics for DI-algebra. The algorithm has been proven correct, and we highlight the most interesting aspects of that proof. The algorithm has been implemented and turns out to be very valuable in the process of getting a specification right.