Oink：现代奇偶博弈求解器的实现与评估

奇偶博弈在形式化验证与综合中有重要的实际应用，特别是用于解决模态μ演算的模型检测问题。从理论角度看它们也很有趣，因为人们广泛认为它们存在多项式时间解法，但迄今未知此类算法。近年来，许多新算法及对已有算法的改进被提出。我们实现了一个新颖且易于扩展的工具Oink，它是现代奇偶博弈算法的高性能实现。我们进一步对现代奇偶博弈算法与求解器在真实基准和随机生成博弈上进行了全面的实证评估。我们的实验表明，我们的新工具Oink优于当前最先进的水平。