A Decidable Class of Asynchronous Distributed Controllers
P. Madhusudan and P.S. Thiagarajan
We study the problem of synthesizing controllers in a natural distributed asynchronous setting: a finite set of plants interact with their local environments and communicate with each other by synchronizing on common actions. The controller-synthesis problem is to come up with a local strategy for each plant such that the controlled behaviour of the network meets a specification. We consider linear time specifications and provide, in some sense, a minimal set of restrictions under which this problem is effectively solvable. We identify three restrictions: (R1) the specification should not discriminate between "causally equivalent" interleavings, (R2) the local strategy can only remember lengths of local histories and (R3) the local strategies enforce a fixed communication pattern. We show that the controller-synthesis problem is solvable if R1, R2 and R3 are met. Further, the problem becomes undecidable if one or more of these three restrictions are dropped. Our results also have a strong impact in the framework developed by Pnueli and Rosner [PR90].