Information Flow Guided Synthesis with Unbounded Communication
Bernd Finkbeiner, Niklas Metzger, Yoram Moses
TL;DR
This work tackles the problem of synthesizing distributed reactive systems when information must flow unboundedly between components. It introduces a prefix-based, safety-aware information-flow framework that uses finite information classes to capture the essential information at each time step, enabling scalable compositional synthesis via HyperLTL-style assumptions and guarantees. The authors present a practical instantiation, FlowSy, which implements the approach and demonstrates superior performance over previous bounded-information methods on several benchmarks. The key contributions are the prefix distinguishability construction, the finite information-class mechanism, safety hyper implementations, and a compositional synthesis pipeline that yields local components with guaranteed information flow. The approach significantly expands the applicability of automated distributed synthesis to protocols with streaming, potentially infinite communication, and offers practical tooling for real-world designs.
Abstract
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.