同余同构枚举下的分布式协议合成

摘要:分布式协议的综合是一个困难的问题,常常是不可决问题。完成技术通过将问题转化为搜索问题来提供部分解决方法。然而,候选完成的空间仍然非常庞大。在本文中,我们提出了优化技术,通过利用功能上等同解决方案中的对称性(同构)来减小搜索空间的大小,将其缩小了一个阶乘因子。我们对这种优化进行了理论分析,并通过实证结果证明了其在综合交替位协议和两阶段提交协议方面的有效性。我们的实验表明,优化工具的速度比未优化的工具提高了大约2到10倍。

作者:Derek Egolf, Stavros Tripakis

论文ID:2306.02967

分类:Logic in Computer Science

分类简称:cs.LO

提交时间:2023-07-31

PDF 下载: 英文版 中文版pdf翻译中