论文标题
在有限的CTL中足够和必要的条件：遗忘方法
On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach
论文作者
论文摘要
计算树逻辑（CTL）是正式验证中的中心形式之一。作为一种规范语言，它用于表达预期系统所满足的属性。从验证和系统设计的角度来看，由于各种原因，此类属性的某些信息内容可能与系统无关，例如，由于实际困难，它可能会因时间而过时，或者可能是不可行的。然后，出现问题的问题是如何在不改变相关系统行为或违反给定签名的现有规格的情况下减去此类信息。此外，在这种情况下，两个至关重要的概念是有益的：最必要的条件（SNC）和给定特性的最弱的条件（WSC）。为了以原则性的方式解决这样的方案，我们在CTL中介绍了一种基于遗忘的方法，并表明它可以在给定模型和给定签名之上计算属性的SNC和WSC。我们研究其理论属性，还表明我们忘记的概念满足了现有的知识遗忘的基本假设。此外，我们分析了碎片CTL_AF的某些基本推理任务的计算复杂性。
Computation Tree Logic (CTL) is one of the central formalisms in formal verification. As a specification language, it is used to express a property that the system at hand is expected to satisfy. From both the verification and the system design points of view, some information content of such property might become irrelevant for the system due to various reasons, e.g., it might become obsolete by time, or perhaps infeasible due to practical difficulties. Then, the problem arises on how to subtract such piece of information without altering the relevant system behaviour or violating the existing specifications over a given signature. Moreover, in such a scenario, two crucial notions are informative: the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a given property. To address such a scenario in a principled way, we introduce a forgetting-based approach in CTL and show that it can be used to compute SNC and WSC of a property under a given model and over a given signature. We study its theoretical properties and also show that our notion of forgetting satisfies existing essential postulates of knowledge forgetting. Furthermore, we analyse the computational complexity of some basic reasoning tasks for the fragment CTL_AF in particular.
