利用时间相关性信息增强 LTL 不可满足核心
计算机科学中的逻辑
2013-06-13 v1 软件工程
摘要
LTL 常用于表达嵌入式系统或业务流程等众多领域的规范。见证（Witnesses）有助于理解为何 LTL 规范是可满足的，且已有多种方法使理解见证变得更容易。对于不可满足的规范，不可满足核心（UCs），即不可满足公式中本身不可满足的部分，是一种成熟的调试手段。然而，鲜有工作致力于帮助理解不可满足 LTL 公式的 UC。在本文中，我们建议通过补充关于 UC 子公式在哪些时间点与不可满足性相关的额外信息，来增强不可满足 LTL 公式的 UC。例如，在"(G p) and (X not p)"中，"p"的第一次出现实际上仅在时间点 1（时间从时间点 0 开始）与不可满足性“相关”。我们提出了一种从 LTL 公式不可满足性的时间归结证明的归结图中提取此类信息的方法。我们在 TRP++ 中实现了该方法，并进行了实验评估。我们工具源代码可用。
引用
@article{arxiv.1306.2694,
title = {Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance},
author = {Viktor Schuppan},
journal= {arXiv preprint arXiv:1306.2694},
year = {2013}
}
备注
In Proceedings QAPL 2013, arXiv:1306.2413