I Castellani, M Mukund and P S Thiagarajan
Proc. FSTTCS 19, Springer LNCS 1739 (1999) 219-231.
© Springer-Verlag Berlin Heidelberg
We study the problem of synthesizing distributed implementations from global specifications. In particular, we characterize when a global transition system can be implemented as a synchronized product of local transition systems. Our work extends a number of previous studies in this area which have tended to make strong assumptions about the specification - either in terms of determinacy or in terms of information concerning concurrency.
We also examine the more difficult problem where the correctness of the implementation in relation to the specification is stated in terms of bisimulation rather than isomorphism. As an important first step, we show how the synthesis problem can be solved in this setting when the implementation is required to be deterministic.