Abstract
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. In this talk, I will 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 synthesis is not successful, the algorithm computes an additional sufficient assumption on the other systems that will ensure satisfaction of the specification and the 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 also sufficient to 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 several examples.