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.
翻译:合成取决于对假设的发现,即对系统其余部分的行为进行限制,使系统某一组成部分能够实现规格。为了避免失去有效的解决方案,这些假设应当是实现真实性的必要条件。然而,由于通常有许多不同的行为,都具有相同的规格,因此通常不存在必要的行为限制。在本文件中,我们为合成合成引入了一种新的假设类别,我们称之为信息流动假设。这些假设反映了分布式计算的一个基本方面,因为各组成部分往往需要根据只有其他组成部分才能获得的信息采取行动。因此,某种信息流动往往是必要的要求,而确立信息流动的实际行为则不受控制。与行为假设(即单个计算轨迹的特性)形成对比的是,信息流动假设是过度的。我们介绍了一种从系统的时间逻辑规格中自动得出信息流假设的方法。我们随后为基于信息流动假设的组件实施自动合成提供了一种技术。这为构建信息流动假设提供了一种新的构成方法,同时对分布式系统进行了新的合成方法。我们先用新的组合法对分布式系统进行了实验,我们用一个鼓励工具合成。