存在性参数化布尔方程系统的约简依赖空间

参数化布尔方程系统（PBES）是一组方程，将满足这些方程的解集定义为最小和/或最大不动点。因此该系统被视为定义谓词的声明式程序，其中程序执行返回给定基原子公式是否成立。程序执行对应于 PBES 的成员性问题，但一般而言该问题是不可判定的。本文提出 PBES 的一个子类，其表达无全称量词约束的公式，并研究解决该子类中此问题的技术。我们利用成员性问题可归约为是否存在证明图的问题这一事实。为检查后者问题，我们引入所谓的依赖空间，它是包含所有极小证明图的图。然而依赖空间一般而言是无限的。因此，我们提出等价关系保持成员性问题结果的一些条件，进而在该关系下将两顶点识别为相同。在此意义上，依赖空间可能得到有限图。我们展示一些具有无限依赖空间但可通过等价关系约简为有限图的示例。我们提供一种构造有限依赖空间的过程并展示该过程的可靠性。我们还使用 SMT 求解器实现了该过程，并在包括缩小版 McCarthy 91 函数的一些示例上进行了实验。