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倍的加速比。