符号模型检测的保留反例归约
计算机科学中的逻辑
2013-01-16 v1
摘要
LTL 模型检测的代价对所验证公式的长度高度敏感。我们观察到，在某些特定条件下，输入的 LTL 公式可以在模型检测之前被归约为一个更易处理的公式。在我们的归约中，这两个公式不必逻辑等价，但它们相对于模型共享相同的反例集。在模型以符号方式表示的情况下，启用此类归约的条件可以通过轻量级的努力（例如使用 SAT 求解）来检测。在本文中，我们暂将这种技术命名为“保留反例归约”（简称 CePRe），并最终通过适配 NuSMV 对所提出的技术进行了实验评估。
引用
@article{arxiv.1301.3299,
title = {Counterexample-Preserving Reduction for Symbolic Model Checking},
author = {Wanwei Liu and Rui Wang and Xianjin Fu and Ji Wang and Wei Dong and Xiaoguang Mao},
journal= {arXiv preprint arXiv:1301.3299},
year = {2013}
}