  This paper presents a method for synthesizing a reactive program which
coordinates the actions of a group of other reactive programs, so that the
combined system satisfies a temporal specification of its desired long-term
behavior. Traditionally, reactive synthesis has been applied to the
construction of a stateful hardware circuit. This work is motivated by
applications to other domains, such as the IoT (the Internet of Things) and
robotics, where it is necessary to coordinate the actions of multiple sensors,
devices, and robots. The mathematical model represents such entities as
individual processes in Hoare's CSP model. Given a network of interacting
entities, called an \emph{environment}, and a temporal specification of
long-term behavior, the synthesis method constructs a \emph{coordinator}
process (if one exists) that guides the actions of the environment entities so
that the combined system is deadlock-free and satisfies the given
specification. The main technical challenge is that a coordinator may have only
\emph{partial knowledge} of the environment state, due to non-determinism
within the environment, and environment actions that are hidden from the
coordinator. This is the first method to handle both sources of partial
knowledge, and to do so for arbitrary linear temporal logic specifications. It
is shown that the coordination synthesis problem is \PSPACE-hard in the size of
the environment. A prototype implementation is able to synthesize compact
solutions for a number of coordination problems.
