TY - JOUR
T1 - Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
AU - Unno, Hiroshi
AU - Terauchi, Tachio
AU - Gu, Yu
AU - Koskinen, Eric
N1 - Publisher Copyright:
© 2023 Owner/Author.
PY - 2023/1/9
Y1 - 2023/1/9
N2 - 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 novel modular primal-dual method. The key observations are (1) μCLP is closed under complement such that each (co-)inductive predicate in the original primal instance has a corresponding (co-)inductive predicate representing its complement in the dual instance obtained by taking the standard De Morgan's dual of the primal instance, and (2) partial solutions for (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 also modular in 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.
AB - 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 novel modular primal-dual method. The key observations are (1) μCLP is closed under complement such that each (co-)inductive predicate in the original primal instance has a corresponding (co-)inductive predicate representing its complement in the dual instance obtained by taking the standard De Morgan's dual of the primal instance, and (2) partial solutions for (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 also modular in 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.
KW - constraint logic programming
KW - fixpoint logics
KW - temporal verification
UR - http://www.scopus.com/inward/record.url?scp=85146419667&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85146419667&partnerID=8YFLogxK
U2 - 10.1145/3571265
DO - 10.1145/3571265
M3 - Article
AN - SCOPUS:85146419667
VL - 7
SP - 2111
EP - 2140
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
ER -