On Reconfigurable Bisimulation, with an Application to the Distributed Synthesis Problem

Abstract

We address the problem of distributing a sequential system across asynchronous agents that jointly recognize the same language. Existing approaches incur state-space blow-up due to fixed communication structures. We propose a solution based on reconfigurable communication, where the communication structure is not fixed but instead computed and subsequently minimized. We rely on a novel notion of Parametric Reconfigurable Bisimulation, which beyond classical state-space minimization, identifies the necessary communications for each agent while pruning the rest. We show how to compute this bisimulation, how to minimize communications per agent, and prove that the composition of the resulting agents remains bisimilar to the original sequential system. As a key application, we enable teamwork synthesis, a variant of distributed synthesis, from global specifications. While distributed synthesis is undecidable, we show that teamwork synthesis is decidable. We further validate our results with a detailed experimental evaluation.