一句话：指出现有反链精化检查算法的可靠性与性能缺陷，提出正确高效的新算法，实验证明其运行时间和内存更优。
精化是逐步开发方法的基础，可用于证明或计算系统是否满足其规约。Wang 等人提出了基于反链的算法，用于判定 trace refinement、stable failures refinement 与 failures-divergences refinement。我们指出现有算法在可靠性（soundness）和性能方面存在问题，并提出新的、正确的反链算法。大量实验表明，新算法在运行时间和内存占用上均优于原算法；此外，应用保发散的分支互模拟最小化还能进一步缩短运行时间。
The notion of refinement plays an important role in software engineering. It is the basis of a stepwise development methodology in which the correctness of a system can be established by proving, or computing, that a system refines its specification. Wang et al. describe algorithms based on antichains for efficiently deciding trace refinement, stable failures refinement and failures-divergences refinement. We identify several issues pertaining to the soundness and performance in these algorithms and propose new, correct, antichain-based algorithms. Using a number of experiments we show that our algorithms outperform the original ones in terms of running time and memory usage. Furthermore, we show that additional run time improvements can be obtained by applying divergence-preserving branching bisimulation minimisation.
@article{paperbot1343,
title = {Correct and Efficient Antichain Algorithms for Refinement Checking},
author = {Maurice Laveaux and Jan Friso Groote and Tim A. C. Willemse},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:8)2021}
}