Synthesizing distributed controllers for the safe operation of ConnectedSpaces

A collection of one or more devices, each described by its digital device manual and reachable over a network, is a ConnectedSpace. A set of safety policies may be enforced on a ConnectedSpace to ensure the safety of the environment in which the ConnectedSpace is deployed. The enforcement of these safety policies by one or more safely controllers governs the behavior of the devices within the ConnectedSpace. We propose a policy-based partitioning scheme for synthesizing k distributed safety controllers such that: (a) each device is guaranteed to be controlled by no more than two controllers, and (b) each policy is guaranteed to be enforced by exactly one controller. We present an experimental evaluation of our scheme. The experimental results show that the scheme is scalable with respect to the number of devices and the number of policies. We also show how safety controllers that are correct with respect to the policies, are synthesized using the theory of supervisory control.