  Compositional synthesis relies on the discovery of assumptions, i.e.,
restrictions on the behavior of the remainder of the system that allow a
component to realize its specification. In order to avoid losing valid
solutions, these assumptions should be necessary conditions for realizability.
However, because there are typically many different behaviors that realize the
same specification, necessary behavioral restrictions often do not exist. In
this paper, we introduce a new class of assumptions for compositional
synthesis, which we call information flow assumptions. Such assumptions capture
an essential aspect of distributed computing, because components often need to
act upon information that is available only in other components. The presence
of a certain flow of information is therefore often a necessary requirement,
while the actual behavior that establishes the information flow is
unconstrained. In contrast to behavioral assumptions, which are properties of
individual computation traces, information flow assumptions are
hyperproperties, i.e., properties of sets of traces. We present a method for
the automatic derivation of information-flow assumptions from a temporal logic
specification of the system. We then provide a technique for the automatic
synthesis of component implementations based on information flow assumptions.
This provides a new compositional approach to the synthesis of distributed
systems. We report on encouraging first experiments with the approach, carried
out with the BoSyHyper synthesis tool.
