重组：一种用于高效组合验证的新技术
Recomposition: A New Technique for Efficient Compositional Verification
AI总结：
针对组合验证中组件选择研究不足的问题，提出以重组映射为核心的组合验证框架，通过启发式方法筛选少量重组映射并行验证，在TLA+模型检测器中实现后，性能与TLC相当。
摘要：
组合验证算法在模型检测领域已得到深入研究。合理选择待验证组件对提升效率至关重要，但该问题受到的关注相对较少。本文针对这一空白，提出了一种新颖的组合验证框架，将组件选择作为明确的核心概念。该框架先将系统分解为多个组件，再将这些组件重组成新组件以实现高效验证。本技术的核心是重组映射，它决定了重组的执行方式；因此组件选择问题可归结为寻找优质的重组映射。但可能的重组映射空间可能十分庞大，为此我们提出启发式方法来寻找少量的重组映射组合，再并行运行这些映射。我们在TLA+语言的模型检测器中实现了相关技术。实验表明，在一组分布式协议基准测试集上，我们的工具性能与知名TLA+模型检测器TLC相当。
英文摘要：
Compositional verification algorithms are well-studied in the context of model checking. Properly selecting components for verification is important for efficiency, yet has received comparatively less attention. In this paper, we address this gap with a novel compositional verification framework that focuses on component selection as an explicit, first-class concept. The framework decomposes a system into components, which we then recompose into new components for efficient verification. At the heart of our technique is the recomposition map that determines how recomposition is performed; the component selection problem thus reduces to finding a good recomposition map. However, the space of possible recomposition maps can be large. We therefore propose heuristics to find a small portfolio of recomposition maps, which we then run in parallel. We implemented our techniques in a model checker for the TLA+ language. In our experiments, we show that our tool achieves competitive performance with TLC-a well-known model checker for TLA+-on a benchmark suite of distributed protocols.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
