利用时间相关性信息增强LTL的不可满足核
Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance
摘要：
LTL经常被用来表达许多领域的规范，如嵌入式系统或业务流程。见证者可以帮助理解为什么LTL规范是可满足的，并且存在许多方法可以使理解见证者更容易。在不可满足的规范的情况下，不可满足的核心（UC），即，不可满足公式中本身不可满足的部分是一种已建立的调试方法。然而，很少的工作已经完成，以帮助理解UC的不可满足的LTL公式。在本文中，我们建议提高UC的不可满足的LTL公式的额外信息的时间点，在UC的子公式相关的不可满足性。例如，在“（G p）and（X not p）”中，第一次出现的“p”实际上仅与时间点1（时间从时间点0开始）的不可满足性“相关”。我们提出了一种方法来提取这样的信息，从分辨率图的时间分辨率证明LTL公式的不可满足性。我们在TRP++中实现了我们的方法，并进行了实验评估。
英文摘要：
LTL is frequently used to express specifications in many domains such as embedded systems or business processes. Witnesses can help to understand why an LTL specification is satisfiable, and a number of approaches exist to make understanding a witness easier. In the case of unsatisfiable specifications unsatisfiable cores (UCs), i.e., parts of an unsatisfiable formula that are themselves unsatisfiable, are a well established means for debugging. However, little work has been done to help understanding a UC of an unsatisfiable LTL formula. In this paper we suggest to enhance a UC of an unsatisfiable LTL formula with additional information about the time points at which the subformulas of the UC are relevant for unsatisfiability. For example, in "(G p) and (X not p)" the first occurrence of "p" is really only "relevant" for unsatisfiability at time point 1 (time starts at time point 0). We present a method to extract such information from the resolution graph of a temporal resolution proof of unsatisfiability of an LTL formula. We implement our method in TRP++, and we experimentally evaluate it. Source code of our tool is available.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
