析取参数化布尔方程组证明图的推广
An Extension of Proof Graphs for Disjunctive Parameterised Boolean Equation Systems
摘要：
参数化布尔方程系统（PBES）是一组方程，它将集合定义为满足方程的最小和/或最大不动点。这个系统被认为是一个声明性的程序，它定义了接受一个数据并返回一个布尔值的函数。PBES的成员问题是一个决定给定元素是否在定义集合中的问题，它对应于程序的一次执行。本文引入了约简证明图，研究了将一般不可判定的PBES成员问题转化为约简证明图来解决的方法。证明图中的顶点X（v）表示数据v在集合X中，如果该图满足从给定PBES导出的条件。然而，证明图一般是无限的。因此，我们引入顶点，每个顶点代表原始顶点的一组顶点，这可能导致有限图。对于析取PBES的一个子类，我们阐明了简化证明图应满足的一些条件。我们还展示了一些例子，没有有限的证明图，除了减少一个。我们进一步提出了一个减少的依赖空间，其中包含减少的证明图作为子图，如果一个证明图存在。我们提供了一个构造有限约化依赖空间的过程，并证明了该过程的合理性和完整性。
英文摘要：
A parameterised Boolean equation system (PBES) is a set of equations that defines sets as the least and/or greatest fixed-points that satisfy the equations. This system is regarded as a declarative program defining functions that take a datum and returns a Boolean value. The membership problem of PBESs is a problem to decide whether a given element is in the defined set or not, which corresponds to an execution of the program. This paper introduces reduced proof graphs, and studies a technique to solve the membership problem of PBESs, which is undecidable in general, by transforming it into a reduced proof graph. A vertex X(v) in a proof graph represents that the data v is in the set X, if the graph satisfies conditions induced from a given PBES. Proof graphs are, however, infinite in general. Thus we introduce vertices each of which stands for a set of vertices of the original ones, which possibly results in a finite graph. For a subclass of disjunctive PBESs, we clarify some conditions which reduced proof graphs should satisfy. We also show some examples having no finite proof graph except for reduced one. We further propose a reduced dependency space, which contains reduced proof graphs as sub-graphs if a proof graph exists. We provide a procedure to construct finite reduced dependency spaces, and show the soundness and completeness of the procedure.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
