计算最小可区分的Hennessy-Milner公式是NP难问题，但其变种是可处理的。
摘要：计算非双模相似状态的最小可区别公式的问题。如果公式的大小必须是最小的，我们证明这是NP难的。类似地，存在一个短的可区别追踪的问题是NP完全的。然而，如果最小化被定义为最小嵌套形态数量，我们可以提供多项式算法，甚至可以通过递归要求最小嵌套否定数量来扩展。原型实现显示，生成的公式比Cleaveland引入的方法生成的公式要小得多。
作者：Jan Martens, Jan Friso Groote
论文ID：2307.05265
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-12