Synthesis of distributed protocols is a hard, often undecidable, problem. Completion techniques provide partial remedy by turning the problem into a search problem. However, the space of candidate completions is still massive. In this paper, we propose optimization techniques to reduce the size of the search space by a factorial factor by exploiting symmetries (isomorphisms) in functionally equivalent solutions. We present both a theoretical analysis of this optimization as well as empirical results that demonstrate its effectiveness in synthesizing both the Alternating Bit Protocol and Two Phase Commit. Our experiments show that the optimized tool achieves a speedup of approximately 2 to 10 times compared to its unoptimized counterpart.

翻译：分布式协议的综合是一个困难且通常不可判定的问题。补全技术通过将问题转化为搜索问题提供了部分解决方案。然而，候选补全空间仍然非常庞大。本文提出优化技术，通过利用功能等价解中的对称性（同构）将搜索空间规模减少一个阶乘因子。我们给出了该优化的理论分析以及实证结果，展示了其在综合交替比特协议和两阶段提交协议中的有效性。实验表明，与未优化的工具相比，优化后的工具实现了约2到10倍的加速比。