通过分支互模拟证明线性化
Proving Linearizability via Branching Bisimulation
摘要：
线性化和进度属性是并发对象的关键正确性概念。然而，模型检验线性化遭受PSPACE-硬度的微量夹杂物问题。本文提出了利用分支互模拟，一个基本的语义等价关系的进程代数，可以有效地计算，在检查这些属性。一个商的建设提供了巨大的状态空间减少的结果。我们确认所提出的方法的优势，对十几个基准问题。
英文摘要：
Linearizability and progress properties are key correctness notions for concurrent objects. However, model checking linearizability has suffered from the PSPACE-hardness of the trace inclusion problem. This paper proposes to exploit branching bisimulation, a fundamental semantic equivalence relation developed for process algebras which can be computed efficiently, in checking these properties. A quotient construction is provided which results in huge state space reductions. We confirm the advantages of the proposed approach on more than a dozen benchmark problems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
