计算极小区分 Hennessy-Milner 公式是 NP 难的，但若干变体可高效求解
计算机科学中的逻辑
2023-07-12 v1
摘要
我们研究有限标记转移系统（LTS）中非互模拟状态的极小区分公式计算问题。我们证明，若公式大小必须极小，则该问题是 NP 难的。类似地，存在短区分迹的问题为 NP 完全。然而，若将极小性表述为嵌套模态符的最少数量，我们可提供多项式算法，并且甚至可通过递归要求嵌套否定的最少数量来扩展。一个原型实现表明，所生成公式比 Cleaveland 引入的方法生成的公式小得多。
引用
@article{arxiv.2307.05265,
title = {Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable},
author = {Jan Martens and Jan Friso Groote},
journal= {arXiv preprint arXiv:2307.05265},
year = {2023}
}
备注
Accepted at CONCUR 2023