Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
复制标题
用于时间验证的模块化原对偶定点逻辑求解
DOI：
10.1145/3571265
复制
发表时间：
2023
影响因子：
--
通讯作者：
Koskinen, Eric
中科院分区：
文献类型：
--
作者：
Unno, Hiroshi;Terauchi, Tachio;Gu, Yu;Koskinen, Eric
我们提出了一种新的方法来决定一阶不动点逻辑的公式的有效性与背景理论和任意嵌套的归纳和共归纳谓词定义最小和最大的不动点。我们的方法是基于约束的，减少了一阶不动点逻辑公式的有效性检验问题（形式上，一种名为µCLP的语言中的实例）到最近引入的谓词约束语言的约束满足问题。再加上约束语言的现有合理且相对完整的求解器，这种新颖的约简本身已经给出了一个合理的、相对完整的方法来确定µCLP的有效性，但我们进一步将其改进为一种新颖的模块化原始-对偶方法。关键的观察结果是：（1）μCLP在补集下是封闭的，这样原始实例中的每个（共）归纳谓词都有一个对应的（共）归纳谓词表示它在通过原始实例的标准De Morgan对偶获得的对偶实例中的补集，（2）在原边约束求解过程中合成的（共）归纳谓词的部分解可以作为可靠的上在对偶边中对应的（共）归纳谓词的边界，反之亦然。通过并行求解原始问题和对偶问题，并交换彼此的部分解作为合理的边界，这两个过程相互减少彼此的解空间，从而实现快速收敛。该方法是alsomodularin的边界合成和交换的粒度的个人（共）归纳predicate.We证明了我们的新的不动点逻辑解决的效用，通过编码的各种各样的时间验证问题，在μCLP，包括终止/非终止，LTL，CTL，甚至是全模态μ演算模型检查的无限状态程序。编码通过将程序中的每个循环和（递归）函数以及属性的子公式表示为单独的（可能嵌套的）（共）归纳谓词来利用程序和属性中的模块性。结合我们新颖的模块化原始-对偶µCLP求解，我们获得了一种有效解决各种时间验证问题的新方法。
We present a novel approach to deciding the validity of formulas in first-order fixpoint logic with background theories and arbitrarily nested inductive and co-inductive predicates defining least and greatest fixpoints. Our approach is constraint-based, and reduces the validity checking problem of the given first-order-fixpoint logic formula (formally, an instance in a language called µCLP) to a constraint satisfaction problem for a recently introduced predicate constraint language.Coupled with an existing sound-and-relatively-complete solver for the constraint language, this novel reduction alone already gives a sound and relatively complete method for deciding µCLP validity, but we further improve it to a novelmodular primal-dualmethod. The key observations are (1) µCLP is closed under complement such that each (co-)inductive predicate in the originalprimalinstance has a corresponding (co-)inductive predicate representing its complement in thedualinstance obtained by taking the standard De Morgan’s dual of the primal instance, and (2)partial solutionsfor (co-)inductive predicates synthesized during the constraint solving process of the primal side can be used as sound upper-bounds of the corresponding (co-)inductive predicates in the dual side, and vice versa. By solving the primal and dual problems in parallel and exchanging each others’ partial solutions as sound bounds, the two processes mutually reduce each others’ solution spaces, thus enabling rapid convergence. The approach is alsomodularin that the bounds are synthesized and exchanged at granularity of individual (co-)inductive predicates.We demonstrate the utility of our novel fixpoint logic solving by encoding a wide variety of temporal verification problems in µCLP, including termination/non-termination, LTL, CTL, and even the full modal µ-calculus model checking of infinite state programs. The encodings exploit the modularity in both the program and the property by expressing each loops and (recursive) functions in the program and sub-formulas of the property as individual (possibly nested) (co-)inductive predicates. Together with our novel modular primal-dual µCLP solving, we obtain a novel approach to efficiently solving a wide range of temporal verification problems.
登录
查看更多内容
DOI：
--
发表时间：
1999
期刊：
Annual Conference for Computer Science Logic
影响因子：
--
作者：
Julian Bradfield
通讯作者：
Julian Bradfield
验证无限状态系统的日益富有表现力的时态逻辑
DOI：
--
发表时间：
2017
期刊：
Journal of the the ACM
影响因子：
--
作者：
Byron Cook
通讯作者：
Byron Cook
基于 CEGIS 的终止分析中的决策树学习
DOI：
10.1007/978-3-030-81688-9_4
发表时间：
2021
期刊：
Proceedings of CAV 2021, Springer LNCS
影响因子：
--
作者：
Kura Satoshi;Unno Hiroshi;Hasuo Ichiro
通讯作者：
Hasuo Ichiro
DOI：
10.1007/978-3-642-54833-8_21
发表时间：
2014-04
期刊：
--
影响因子：
--
作者：
Takuya Kuwahara;Tachio Terauchi;Hiroshi Unno;N. Kobayashi
通讯作者：
Takuya Kuwahara;Tachio Terauchi;Hiroshi Unno;N. Kobayashi
DOI：
10.1109/fmcad.2014.6987597
发表时间：
2014-10
期刊：
2014 Formal Methods in Computer-Aided Design (FMCAD)
影响因子：
--
作者：
B. Cook;Carsten Fuhs;K. Nimkar;P. O'Hearn
通讯作者：
B. Cook;Carsten Fuhs;K. Nimkar;P. O'Hearn