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].
|
concur02@fi.muni.cz |