Fri 20 Jan 2023 13:30 - 13:55 at Square - Logic Programming Chair(s): Marco Patrignani

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 $\mu$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 $\mu$CLP validity, but we further improve it to a novel {\em modular primal-dual} method. The key observations are (1) $\mu$CLP is closed under complement such that each (co-)inductive predicate in the original {\em primal} instance has a corresponding (co-)inductive predicate representing its complement in the {\em dual} instance obtained by taking the standard De Morgan's dual of the primal instance, and (2) {\em 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 {\em 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 $\mu$CLP, including termination/non-termination, LTL, CTL, and even the full modal $\mu$-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 $\mu$CLP solving, we obtain a novel approach to efficiently solving a wide range of temporal verification problems.

#### Fri 20 JanDisplayed time zone: Eastern Time (US & Canada) change

 13:30 - 14:45 Logic ProgrammingPOPL at Square Chair(s): Marco Patrignani University of Trento 13:3025mTalk Modular Primal-Dual Fixpoint Logic Solving for Temporal VerificationDistinguished PaperPOPLHiroshi Unno University of Tsukuba; RIKEN AIP, Tachio Terauchi Waseda University, Yu Gu University of Tsukuba, Eric Koskinen Stevens Institute of Technology DOI 13:5525mTalk Optimal CHC Solving via Termination ProofsPOPLYu Gu University of Tsukuba, Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP DOI 14:2025mTalk From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection ProblemsPOPLAaron Bembenek Harvard University, Michael Greenberg Stevens Institute of Technology, Stephen Chong Harvard University DOI Pre-print