Assume–Guarantee Distributed Synthesis

Distributed reactive synthesis is the problem of algorithmically constructing controllers of distributed, communicating systems so that each closed-loop system satisfies a given temporal specification. We present an algorithm, called negotiation, for sound (but necessarily incomplete) distributed reactive synthesis based on assume-guarantee decompositions. The negotiation algorithm iteratively constructs assumptions and guarantees for each system. In each iteration, each system attempts to fulfill its specification and its guarantee (from the previous round), under the current assumption on the other systems, by solving a reactive synthesis problem. If the specification is not realizable, the algorithm computes a sufficient assumption on the other systems that ensures it can realize the specification and guarantee. This additional assumption further constrains the behavior of other systems and they might require an additional assumption, leading to the next round in the negotiation. The process terminates when a compatible assumption-guarantee pair is found for each system, which is sufficient to also satisfy the specification of each system. We have built a tool called Agnes that implements this algorithm. Using Agnes, we empirically demonstrate the effectiveness of our proposed algorithm on two case studies.