Synthesis and equivalence of concurrent systems (Q1105355)

A framework for synthesis of synchronous concurrent systems with local memory is developed. Given an output specification of the system a cell action structure can be derived. This structure can be mapped into a communication structure, a model of the events in the target hardware with constraints on the communication possible between events, giving a schedule for the cell actions. Communication structures are interesting in their own right, and transformations defined on such can be used for showing equivalence between different computational networks. As an example, the equivalence between two specific communication structures is proved and it is shown that an FFT algorithm can be implemented on them.