顽固的事务减少（有证据）
Stubborn Transaction Reduction (with Proofs)
摘要：
并行交织的指数级增长仍然是并发程序模型检验的一个基本挑战。偏序约简（POR）和事务约简（TR）都能减少并发系统中的交织次数。与POR不同，事务还减少了中间状态的数量。另一方面，现代POR技术提供了更动态的识别交换行为的方法，这是获得良好约简的关键任务。我们表明，交易减少可以使用相同的动态交换性，发现在顽固集POR。我们还比较了减少POR和TR，证明与几个例子，这些技术相辅相成。通过在模型检测器LTSmin中实现动态事务，我们将其有效性与原始静态TR和两种POR方法进行了比较。一些输入，包括现实的案例研究，表明新的动态TR可以在实践中超过POR。
英文摘要：
The exponential explosion of parallel interleavings remains a fundamental challenge to model checking of concurrent programs. Both partial-order reduction (POR) and transaction reduction (TR) decrease the number of interleavings in a concurrent system. Unlike POR, transactions also reduce the number of intermediate states. Modern POR techniques, on the other hand, offer more dynamic ways of identifying commutative behavior, a crucial task for obtaining good reductions. We show that transaction reduction can use the same dynamic commutativity as found in stubborn set POR. We also compare reductions obtained by POR and TR, demonstrating with several examples that these techniques complement each other. With an implementation of the dynamic transactions in the model checker LTSmin, we compare its effectiveness with the original static TR and two POR approaches. Several inputs, including realistic case studies, demonstrate that the new dynamic TR can surpass POR in practice.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
