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.