On Reconfigurable Bisimulation, with an Application to the Distributed Synthesis Problem
Yehia Abd Alrahman, Nir Piterman
TL;DR
This work tackles the challenge of distributing a centralized deterministic automaton to asynchronous agents without incurring the prohibitive state explosion or fixed communication schemes of classical approaches. It introduces Reconfigurable Transition Systems and a Parametric Reconfigurable Bisimulation that identifies only the necessary participations per agent, enabling a joint system bisimilar to the original $T$ while dramatically reducing synchronization. A formal fixpoint algorithm computes the largest reconfigurable bisimulation, and a compression operator yields reduced, yet language-preserving, agent TSs that can be composed to reproduce the centralized behavior. The authors validate the approach with a Time-Sharing Service case study showing substantial state-space reductions and demonstrate a workflow for applying this method to distributed synthesis (teamwork synthesis), thereby bypassing undecidability arising from rigid fixed-communication architectures. Overall, the framework provides a practical path to scalable, loosely-coupled distributed implementations with dynamic, by-need coordination.
Abstract
We consider the problem of distributing a centralised transition system to a set of asynchronous agents recognising the same language. Existing solutions are either manual or involve a huge explosion in the number of states from the centralised system. The difficulty arises from the need to keep a rigid communication scheme, specifying a fixed mapping from events to those who can participate in them. Thus, individual agents need to memorise seen events and their order to dynamically compare their knowledge with others when communicating. To bypass this, we rely on reconfigurable communication: agents decide locally ``by-need'' when to participate or discard specific events during execution while not impacting the progress of the joint computation. Our distribution relies on a novel notion of Parametric Reconfigurable Bisimulation, that identifies the only required participations. We show how to compute this bisimulation and that such minimisation produces a joint system that is bisimilar to the original centralised one. We use a case study to show its effectiveness by producing agents that are much smaller than the centralised system and jointly perform the same computations. As a notable application, we use this distribution in order to allow for distributed synthesis from global specifications. In this case, rigid communication leads to undecidability, which is bypassed by our ability to dynamically prune communications.