Abstract:
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.