Information flow guided synthesis is a compositional approach to the automated construction of distributed systems where the assumptions between the components are captured as information-flow requirements. Information-flow requirements are hyperproperties that ensure that if a component needs to act on certain information that is only available in other components, then this information will be passed to the component. We present a new method for the automatic construction of information flow assumptions from specifications given as temporal safety properties. The new method is the first approach to handle situations where the required amount of information is unbounded. For example, we can analyze communication protocols that transmit a stream of messages in a potentially infinite loop. We show that component implementations can then, in principle, be constructed from the information flow requirements using a synthesis tool for hyperproperties. We additionally present a more practical synthesis technique that constructs the components using efficient methods for standard synthesis from trace properties. We have implemented the technique in the prototype tool FlowSy, which outperforms previous approaches to distributed synthesis on several benchmarks.

翻译：信息流引导的综合是一种构建分布式系统的组合式自动化方法，其组件间的假设通过信息流需求进行刻画。信息流需求属于超属性，确保当某个组件需要基于仅存于其他组件的特定信息执行操作时，该信息将被传递至该组件。我们提出了一种从时序安全属性规约自动构建信息流假设的新方法。该方法首次能够处理所需信息量无界的情形，例如可分析在潜在无限循环中传输消息流的通信协议。我们证明，原则上可通过超属性综合工具从信息流需求构建组件实现。此外，我们提出了一种更实用的综合技术，该技术利用基于轨迹属性的标准综合高效方法构建组件。我们已在原型工具FlowSy中实现该技术，其在多项基准测试中优于先前的分布式综合方法。