Comparison of Algorithms for Checking Emptiness on Büchi Automata
Comparison of Algorithms for Checking Emptiness on Büchi Automata
复制标题
DOI：
10.4230/drops.memics.2009.2349
复制
发表时间：
2009-10
期刊：
影响因子：
--
通讯作者：
Andreas Gaiser;Stefan Schwoon
中科院分区：
文献类型：
--
作者：
Andreas Gaiser;Stefan Schwoon
我们重新研究有限状态系统的LTL模型检测问题。典型的解决方案，如Spin，在飞行中工作，将问题简化为Buchi空虚。这可以在线性时间内完成，并且存在具有此属性的各种算法。尽管如此，细微的设计决策可以在实践中对其实际性能产生很大的影响，特别是在动态使用时。我们比较了大量的算法实验上的一个大的基准套件，测量其实际运行时的性能，并提出改进。与Spin中实现的算法相比，我们的最佳算法平均快约33%。因此，我们建议，对于动态显式状态模型检查，嵌套DFS应该被更好的解决方案所取代。
We re-investigate the problem of LTL model-checking for finite-state systems. Typical solutions, like in Spin, work on the fly, reducing the problem to Buchi emptiness. This can be done in linear time, and a variety of algorithms with this property exist. Nonetheless, subtle design decisions can make a great difference to their actual performance in practice, especially when used on-the-fly. We compare a number of algorithms experimentally on a large benchmark suite, measure their actual run-time performance, and propose improvements. Compared with the algorithm implemented in Spin, our best algorithm is faster by about 33 % on average. We therefore recommend that, for on-the-fly explicit-state model checking, nested DFS should be replaced by better solutions.