Modular Primal-Dual Fixpoint Logic Solving for Temporal
Verification
HIROSHI UNNO, University of Tsukuba, Japan and RIKEN AIP, JapanTACHIO TERAUCHI, Waseda University, JapanYU GU, University of Tsukuba, Japan
ERIC KOSKINEN, Stevens Institute of Technology, USA
We present a novel approach to deciding the validity of formulas in first-order fixpoint logic with backgroundtheories 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 wefurther improve it to a novel modular primal-dual method. The key observations are (1) 𝜇CLP is closed undercomplement 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 paralleland exchanging each others’ partial solutions as sound bounds, the two processes mutually reduce eachothers’ solution spaces, thus enabling rapid convergence. The approach is also modular in that the bounds aresynthesized 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 theproperty 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.
CCS Concepts: • Theory of computation → Program verification; Logic and verification; Constraint
and logic programming; Automated reasoning.
Additional Key Words and Phrases: temporal verification, fixpoint logics, constraint logic programming
ACM Reference Format:
Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. 2023. Modular Primal-Dual Fixpoint Logic Solving
for Temporal Verification. Proc. ACM Program. Lang. 7, POPL, Article 72 (January 2023), 34 pages. https://doi.org/10.1145/3571265

Authors’ addresses: Hiroshi Unno, uhiro@cs.tsukuba.ac.jp, University of Tsukuba, Japan and RIKEN AIP, Japan; Tachio
Terauchi, terauchi@waseda.jp, Waseda University, Japan; Yu Gu, kou@logic.cs.tsukuba.ac.jp, University of Tsukuba, Japan;
Eric Koskinen, eric.koskinen@stevens.edu, Stevens Institute of Technology, USA.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/1-ART72
https://doi.org/10.1145/3571265

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72

72:2

1

Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

INTRODUCTION

One approach to temporal property verification of programs is to reduce the problem to that ofdeciding the validity of a formula in a fixpoint logic [Delzanno and Podelski 2001; Fioravanti et al.
2013; Fribourg 1999; Jaffar and Maher 1994; Kobayashi et al. 2019, 2018; Nanjo et al. 2018; Nilsson
and Lübcke 2000]. In such an approach, both the program and the property to be verified are
encoded together as a fixpoint logic formula so that the logic serves as a common intermediate
language for uniformly expressing various verification problems, separating the concern of reducing
verification problems to logical validity problems from that of solving the validity problems. The
verification community has historically embraced such a separation of concerns. For instance,
constrained Horn clauses (CHCs) [Bjørner et al. 2015] is a popular formal system for expressing
various verification problems, and it facilitated the rapid development of methods for problem
reduction and those for solving the reduced problems [Champion et al. 2018; Gurfinkel et al. 2015;
Hojjat and Rümmer 2018; Kahsai et al. 2016; Komuravelli et al. 2014; Unno and Kobayashi 2009].
In comparison to predicate constraint systems such as CHCs, an advantage of a fixpoint logic isthat it lends itself naturally to modular encoding of verification problems by representing both
finite (i.e., terminating) and infinite (i.e., diverging) behavior of program components as least andgreatest fixpoints [Kobayashi et al. 2019; Nanjo et al. 2018; Unno et al. 2017a].
In this paper, we present a novel approach to solving the validity checking problem for a firstorder fixpoint logic with background theories and arbitrarily nested inductive and co-inductive
predicates defining least and greatest fixpoints (formalized as a language called 𝜇CLP). Our approachis constraint-based, and reduces the validity checking problem of the given 𝜇CLP instance to a
constraint satisfaction problem for a predicate constraint language called pfwCSP, a generalizationof CHCs that was introduced in the work of Unno et al. [2021]. Coupled with an existing soundand-relatively-complete solver for pfwCSP from the same work, our novel reduction alone alreadygives a sound and relatively complete method for deciding 𝜇CLP validity, but we further improvethe method by extending it to a novel modular primal-dual method1 . The key observations are(1) 𝜇CLP is closed under complement where each inductive (resp. co-inductive) predicate in theoriginal primal instance has a corresponding co-inductive (resp. inductive) predicate representing
its complement in the dual instance obtained by taking the De Morgan’s dual of the primal, and(2) partial solutions (described below) for inductive (resp. co-inductive) predicates synthesized
during the constraint solving process of the primal side can be used as sound upper-bounds of thecorresponding co-inductive (resp. inductive) predicates in the dual side, and vice versa.
Based on the observations, our modular primal-dual approach translates both the primal 𝜇CLP
instance and its dual to their corresponding pfwCSP constraint sets, and solves both sets of constraints in parallel. Partial solutions are assignments to predicate variables that satisfy some but
not necessarily all clauses of the given constraint set2 . They are obtained as by-products of theconstraint solving process, and while generally insufficient for solving the given set of constraints,
they are guaranteed to be lower-bounds of the fixpoints corresponding to the (co-)inductive predicate defined by the clauses that they satisfy. Thus, they can be used as sound upper-bounds of thecorresponding fixpoints in the dual instance.
For example, in termination verification, an inductive predicate 𝑋 (e𝑥 ) in the primal problem
may represent the set of states from which some loop in the program always terminates, andthe corresponding co-inductive predicate in the dual problem represents the set of states from
1 Here, the terminology relative completeness is in the sense of Jhala and McMillan [2006]; Terauchi and Unno [2015]. Thatis, the solver is guaranteed to terminate relative to the assumption that there is a solution syntactically expressible aspredicates of the background theory.
2 Technically, we also allow partial solutions to only satisfy sound under-approximations of the clauses (cf. Section 5.2 fordetails).

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:3

which the same loop may diverge. Then, a partial solution to the co-inductive predicate in the
dual problem, say 𝜑, represents a lower-bound on the set of states from which the loop may
diverge. Therefore, its complement, ¬𝜑, is an upper-bound on the set of states from which the loop
always terminates and can be used as a sound upper-bound of the inductive predicate in the primal
problem. The bound is sound in the sense that asserting it does not rule out any actual solutions.
We assert the bound by adding the clause 𝑋 (e𝑥 ) ⇒ ¬𝜑 to the primal’s constraint set where 𝑋 is thepredicate variable corresponding to 𝑋 (cf. Section 5.1 for details). By solving the primal and dual
problems in parallel and exchanging each others’ partial solutions as sound bounds in this way,
the two processes mutually reduce each others’ solution spaces, thus enabling rapid convergence.
An analogy can be made to how clause-learning DPLL SAT solvers reduce the solution space byasserting learned clauses. The approach is also modular in that the bounds are synthesized andexchanged at granularity of individual (co-)inductive predicates. The approach synergizes well withthe aforementioned modularity present in fixpoint logic encodings of verification problems as it
lends itself to bounds synthesized and exchanged at granularity of individual program components,
as seen in the example above, as well as at the granularity of sub-properties of the properties to beverified (e.g., sub-formulas of a temporal logic formula expressing the property to be verified).
We have implemented the approach in a tool called MuVal and applied it to a diverse collectionof temporal verification problems including termination/non-termination, LTL, CTL, and eventhe full modal 𝜇-calculus model checking of infinite-state programs. For encoding the problems,
we adopt the approaches of Kobayashi et al. [2019]; Nanjo et al. [2018]; Unno et al. [2017a] to
exploit the modularity present in both the program and the property by expressing individual loops
and (recursive) functions in the program and sub-formulas of the property as individual (possibly
nested) (co-)inductive predicates. Thanks to our novel modular primal-dual solving method, MuVal
is able to go beyond the capabilities of existing related tools. Namely, MuVal beats AProVE [Giesl
et al. 2017], the winner of 2021 Termination Competition, on termination benchmarks in numberof solved instances. Additionally, MuVal was able to solve 4 challenging benchmarks from Dietsch
et al. [2015] that cannot be solved by their UltimateLTLAutomizer, a state-of-the-art tool for LTL
model checking of infinite state programs3 . We summarize the paper’s contributions below.
• The novel modular primal-dual approach to deciding the validity of a first-order fixpoint
logic with background theories by a reduction to parallel pfwCSP constraint solving.
• The implementation of the approach in the tool MuVal and experimental validation on adiverse collection of temporal verification problems.
The rest of the paper is organized as follows. Section 2 gives a brief overview with a running
example. Section 3 defines 𝜇CLP, a first-order fixpoint logic with background theories. Section 4
reviews pfwCSP and its solver PCSat. Section 5 formalizes the reduction of 𝜇CLP to pfwCSP
and the novel modular primal-dual solving method. Section 6 reports on the implementation andexperimental evaluation of our method. We discuss related work in Section 7 and conclude thepaper in Section 8. We note that pfwCSP and its solver PCSat reviewed in Section 4 are from Unno
et al. [2021] and are not new contributions of this paper. They are described there for the purpose of
making the paper self-contained (and also with the intent to later refer to the description of PCSat
to explain the modifications needed for our work in Section 5). As also remarked above, the mainnovel contributions of this paper are the primal-dual solving method described in detail in Section 5
and its implementation presented in Section 6. This includes the reduction from 𝜇CLP validity to
pfwCSP satisfiability described in detail in Section 5.1 which has only appeared previously in an
unrefereed arXiv paper [Unno et al. 2020].
3 Our experiments with MuVal even discovered that the benchmark files contained incorrect classifications, claiming “safe”

when they actually are not.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:4

2

Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

OVERVIEWThis section highlights the contributions of our work using a running example.
2.1

Modeling Verification Problems in First-Order Fixpoint Logic

Let us consider the termination verification problem of the following program taken from thebenchmark set of the FuncTion tool [Urban 2013; Urban and Miné 2014] slightly modified toilluminate the salient aspects of our approach:assume (x2 <= 3);
while (x1 >= 0 && x2 >= 0) {if (nondet()) { while (x2 != 3 && nondet()) { x2 = x2 + 1; }x1 = x1 - 1; } x2 = x2 - 1; }Here, nondet() returns a non-deterministic Boolean value. This program is always terminating forany external integer inputs x1,x2 and any internal Boolean non-deterministic choices. Note thatthe termination is witnessed by, for example, the lexicographic order of x1,x2.
As we shall show formally in Section 3.2, we systematically encode the termination verification
problem to a validity checking problem for a first-order fixpoint logic (formally, as a 𝜇CLP). Our
encoding adopts the approaches given in Kobayashi et al. [2019]; Nanjo et al. [2018]; Unno et al.
[2017a] to modularly encode the verification problem using both least and greatest fixpoints. Roughly,
the idea is to use least (resp. greatest) fixpoints to describe the terminating (resp. non-terminating)behavior of program components. For the running example, we obtain the following 𝜇CLP Pterm :∀𝑥 1, 𝑥 2 : int. 𝑥 2 > 3 ∨ 𝐼 (𝑥 1, 𝑥 2 ) where
I (𝑥 1, 𝑥 2 )J (𝑥 2 )NP (𝑥 2, 𝑥 2′ )=𝜇 ¬(𝑥 1 ≥ 0 ∧ 𝑥 2 ≥ 0) ∨I (𝑥 1, 𝑥 2 − 1) ∧ J (𝑥 2 ) ∧∀𝑥 2′ : int. NP (𝑥 2, 𝑥 2′ ) ∨ I (𝑥 1 − 1, 𝑥 2′ − 1)=𝜇 ¬(𝑥 2 ≠ 3) ∨ J (𝑥 2 + 1)=𝜈 ¬ 𝑥 2′ = 𝑥 2 ∨ 𝑥 2 ≠ 3 ∧ ¬NP (𝑥 2 + 1, 𝑥 2′ )Here, J is an inductive predicate defined as the least fixpoint (indicated by =𝜇 ) of the function
F (J) (𝑥 2 ) ≜ ¬(𝑥 2 ≠ 3) ∨ J (𝑥 2 + 1) over predicates. I is also an inductive predicate and is defined asa least fixpoint. By contrast, NP is a co-inductive predicate defined as the greatest fixpoint (indicatedby =𝜈 ) of the function G(NP) (𝑥 2, 𝑥 2′ ) ≜ ¬(𝑥 2′ = 𝑥 2 ∨ 𝑥 2 ≠ 3 ∧ ¬NP (𝑥 2 + 1, 𝑥 2′ )). Roughly, I (𝑥 1, 𝑥 2 )and J (𝑥 2 ) characterize the weakest pre-conditions for the termination of the outer and the inner
loops, respectively. Note that the inner loop terminates for all non-deterministic choices if andonly if ¬(𝑥 2 ≠ 3) eventually holds after a finite number of iterations of incrementing 𝑥 2 , which
is here enforced by the least-fixpoint definition of J. NP (𝑥 2, 𝑥 2′ ) denotes the complement of thefollowing inductive predicate P (𝑥 2, 𝑥 2′ ) which characterizes the transition relation of the inner loop:
P (𝑥 2, 𝑥 2′ ) =𝜇 𝑥 2′ = 𝑥 2 ∨ 𝑥 2 ≠ 3 ∧ P (𝑥 2 + 1, 𝑥 2′ ). In the definition of I , NP (𝑥 2, 𝑥 2′ ) is used to bind 𝑥 2′ toa possible value of the program variable x2 upon the termination of the inner loop, encapsulating
the internal behavior of the inner loop. Thus, the query formula is valid if and only if the program
terminates for all initial integer valuations of x1 and x2 and for all internal non-deterministic
choices. Though we could encode the termination verification problem using only least fixpoints byregarding the given program as a single monolithic transition system, this example demonstrates
an important property of first-order fixpoint logics such as 𝜇CLP: the verification problem can be
encoded modularly so that each program component (e.g., the inner and outer loop in the running
example) can be represented by separate (co-)inductive predicates.
The other important property of 𝜇CLP that we shall exploit in our approach is that it is closed
under complement. Namely, taking the De Morgan dual of a 𝜇CLP instance yields a complement
𝜇CLP instance that contains inductive (resp. co-inductive) predicate representing the dual of theProc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:5

each co-inductive (resp. inductive) predicate in the primal instance. As the dual of the running
example Pterm , we obtain the 𝜇CLP Pnterm shown below:∃𝑥 1, 𝑥 2 : int. 𝑥 2 ≤ 3 ∧ NI (𝑥 1, 𝑥 2 ) where
NI (𝑥 1, 𝑥 2 − 1) ∨ NJ (𝑥 2 ) ∨NI (𝑥 1, 𝑥 2 ) =𝜈 𝑥 1 ≥ 0 ∧ 𝑥 2 ≥ 0 ∧∃𝑥 2′ : int. P (𝑥 2, 𝑥 2′ ) ∧ NI (𝑥 1 − 1, 𝑥 2′ − 1)
NJ (𝑥 2 ) =𝜈 𝑥 2 ≠ 3 ∧ NJ (𝑥 2 + 1)
P (𝑥 2, 𝑥 2′ ) =𝜇 𝑥 2′ = 𝑥 2 ∨ 𝑥 2 ≠ 3 ∧ P (𝑥 2 + 1, 𝑥 2′ )Intuitively, NI (𝑥 1, 𝑥 2 ) and NJ (𝑥 2 ) respectively characterize the weakest pre-conditions for the
non-termination of the outer and the inner loops, generalizing the notion of recurrent sets [Gupta
et al. 2008] for modular verification: the non-emptiness of NI (𝑥 1, 𝑥 2 ) and NJ (𝑥 2 ) respectively implies
the non-termination of the inner and outer loops. Recall that P (𝑥 2, 𝑥 2′ ) characterizes the strongest
post-condition of the inner loop. Note that each inductive predicate in the primal instance Pterm(i.e., I and J) has a corresponding co-inductive predicate in the dual Pnterm (i.e., NI and NJ), and theco-inductive predicate in the primal (i.e., NP) has a corresponding inductive predicate in the dual
(i.e., P). Note that the encoding is modular in the sense that the terminating and non-terminating
behavior of each program components are encoded as separate (co-)inductive predicates, namely
by I and NI for the inner loop and by J and NJ for the outer loop. As we shall see next, MuVal tries
to prove the validity of the primal Pterm and the dual Pnterm simultaneously in parallel by sharing
learned information about each other’s (co-)inductive predicates.
2.2

Reduction to pfwCSP and Modular Primal-Dual Solving

Our main contribution is a novel primal-dual approach to deciding the validity of 𝜇CLP. The
approach works by (1) soundly and completely reducing both primal and dual 𝜇CLP instances
to satisfiability problems of the predicate constraint language pfwCSP, and (2) solving the twoconstraint satisfiability problems in parallel while trading learned information. pfwCSP was introduced in recent work by Unno et al. [2021] and generalizes CHCs [Bjørner et al. 2015] to arbitrary(i.e., possibly non-Horn) clauses, functionality constraints, and well-foundedness constraints overpredicate variables.
We overview the reduction to pfwCSP on the running example. The reduction is inspired by
the deduction technique in Nanjo et al. [2018] that eliminates least and greatest fixpoints by overand under-approximations via (co-)inductive invariants and well-founded relations, and eliminates
quantifiers by Skolemization. For the termination verification problem Pterm , our reduction gives
the following pfwCSP Cterm whose term variables are implicitly universally quantified:
(1)
(2)

(3)
(4)

𝑥 2 > 3 ∨ I (𝑥 1, 𝑥 2 )I (𝑥 1, 𝑥 2 ) ⇒ ¬(𝑥
 1 ≥ 0 ∧ 𝑥 2 ≥ 0) ∨I (𝑥 1, 𝑥 2 − 1) ∧ I⇓ (𝑥 1, 𝑥 2, 𝑥 1, 𝑥 2 − 1) ∧ J (𝑥 2 ) ∧(NP (𝑥 2, 𝑥 2′ ) ∨ I (𝑥 1 − 1, 𝑥 2′ − 1) ∧ I⇓ (𝑥 1, 𝑥 2, 𝑥 1 − 1, 𝑥 2′ − 1))
J (𝑥 2 ) ⇒ ¬(𝑥 2 ≠ 3) ∨ J (𝑥 2 + 1) ∧ J⇓ (𝑥 2, 𝑥 2 + 1)
NP (𝑥 2, 𝑥 2′ ) ⇒ ¬ 𝑥 2′ = 𝑥 2 ∨ 𝑥 2 ≠ 3 ∧ ¬NP (𝑥 2 + 1, 𝑥 2′ )I , J, and NP are predicate variables that respectively represent under-approximations of (co-)inductive
predicates I , J, and NP of Pterm . I⇓ and J⇓ are well-founded predicate variables that represent
well-founded relations and used to enforce bounded unfoldings of inductive predicates I and J,
respectively4 . Namely, J⇓ (𝑥 2, 𝑥 2 + 1) constrains the formal argument 𝑥 2 of 𝐽 and the actual argument
4 Here, we use the terminology bounded unfolding in a rather liberal sense. Namely, the unfolding need not be finite as its

bound may be witnessed by a (non-finitary) well-founded relation.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:6

Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

𝑥 2 + 1 of the recursive call to J to be related by a well-founded relation, and I⇓ (𝑥 1, 𝑥 2, 𝑥 1, 𝑥 2 − 1) andI⇓ (𝑥 1, 𝑥 2, 𝑥 1 − 1, 𝑥 2′ − 1) constrain the formal arguments (𝑥 1, 𝑥 2 ) and the actual arguments of thetwo recursive calls to be related by a well-founded relation. The transformation is inspired by ananalogous transformation done in binary reachability analysis [Cook et al. 2006; Grebenshchikov
et al. 2012; Kuwahara et al. 2014] that reduces termination verification problems to safety verification
problems.
Coupled with the sound-and-relatively-complete pfwCSP solver PCSat [Unno et al. 2021], ournovel reduction alone already gives a sound and relatively complete method for deciding 𝜇CLP
validity. As remarked before, we make a further innovation by extending the method to a modular
primal-dual method in which the dual 𝜇CLP problem is also reduced to a pfwCSP satisfiability
problem by applying the same reduction process. For the running example, we obtain from thedual problem Pnterm the following pfwCSP Cnterm :
(5)
(6)

(7)
(8)

𝑆𝜆 (𝑥 1 ) ∧ 𝑇𝜆 (𝑥 2 ) ⇒ 𝑥 2 ≤ 3 ∧ NI (𝑥 1, 𝑥 2 )NI (𝑥 1, 𝑥 2 ) ⇒ 𝑥 1 ≥ 0 ∧ 𝑥 2 ≥ 0 ∧
NI (𝑥 1, 𝑥 2 − 1) ∨ NJ (𝑥 2 ) ∨𝑈𝜆 (𝑥 1, 𝑥 2 ) ⇒ 𝑃 (𝑥 2, 𝑥 2′ ) ∧ NI (𝑥 1 − 1, 𝑥 2′ − 1)
NJ (𝑥 2 ) ⇒ 𝑥 2 ≠ 3 ∧ NJ (𝑥 2 + 1)
𝑃 (𝑥 2, 𝑥 2′ ) ⇒ 𝑥 2′ = 𝑥 2 ∨ 𝑥 2 ≠ 3 ∧ 𝑃 (𝑥 2 + 1, 𝑥 2′ ) ∧ 𝑃⇓ (𝑥 2, 𝑥 2′ , 𝑥 2 + 1, 𝑥 2′ )As above, NI , NJ, and 𝑃 represent under-approximations of (co-)inductive predicates NI , NJ, and 𝑃
of Pnterm , and 𝑃⇓ is a well-founded predicate variable used to enforce a bounded unfolding of 𝑃. 𝑆𝜆 ,𝑇𝜆 , and 𝑈𝜆 are functional predicate variables that characterize total functions to be synthesized andused to Skolemize the existential quantification of the term variables 𝑥 1, 𝑥 2 in clause (5) and 𝑥 2′ inclause (6), respectively.
Our modular primal-dual solver MuVal now tries to decide the satisfiability of both Cterm andCnterm by running two PCSat processes in parallel while synthesizing and exchanging soundbounds to reduce each others’ solution spaces. As remarked before, the bounds are synthesizedfrom partial solutions. For example, 𝜌𝑡 ≜ {J ↦→ 𝜆𝑥 2 .𝑥 2 = 3, J⇓ ↦→ _} is a partial solution for J in
Cterm as it satisfies the clauses that define J (i.e., clause (3)). While the partial solution is not an
actual solution of Cterm , from this information, we know that 𝜌𝑡 (J) is a lower-bound of the inductive
predicate 𝐽 of Pterm and therefore its complement is an upper-bound of the dual co-inductive
predicate 𝑁 𝐽 of Pnterm . We assert the upper-bound in the dual pfwCSP Cnterm by adding the clause
𝑁 𝐽 (𝑥 2 ) ⇒ 𝑥 2 ≠ 3. Roughly, the exchange says: the primal proved that the inner loop always
terminates when x2 = 3 and communicated the information to the dual so that it may limit its
search for states from which the inner loop may diverge to only those that satisfy x2 ≠ 3.
The communicated bound is still insufficient for the dual process to prove its satisfiability(inevitably because the program actually always terminates and therefore Cnterm is unsatisfiable).
But it may lead to a synthesis and exchange of another bound, this time from dual to primal:
J (𝑥 2 ) ⇒ 𝑥 2 ≤ 3, an upper-bound on the set of states from which the inner loop always terminate.
With such bounds, MuVal arrives at the following actual solution for Cterm , thus proving thevalidity of Pterm (and hence the termination of the program):
I (𝑥 1, 𝑥 2 )J (𝑥 2 )NP (𝑥 2, 𝑥 2′ )↦→ 3 ≥ 𝑥 2,↦→ 𝑥 2 ≥ 0 ∧ 𝑥 2 ≤ 3,↦→
𝑥 2 ≥ 0 ∧ 𝑥 2 ≤ 3 ∧ 𝑥 2′ ≥ 4

The assignments to the well-founded predicate variables I⇓ and J⇓ are deferred to Appendix A.
Note that our primal-dual solving method takes advantage of the modularity in the 𝜇CLP encoding
by synthesizing partial solutions and exchanging the bounds derived from them at the granularity
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:7

individual (co-)inductive predicates. Namely, in the example above, the information about the set ofstates from which the inner loop terminates (i.e., the information about the co-inductive predicate
NJ) was synthesized by the primal side and communicated to the dual side, and the the information
about the set of states from which the inner loop does not terminate (i.e., the information about theinductive predicate J) was synthesized by the dual side and communicated to the primal side. These
information are then asserted as clauses that upper-bound the possible solutions for the predicate
variables corresponding to the (co-)inductive predicates, thus reducing the solution spaces of theconstraint solver processes.
In the remainder of this section, we informally describe how partial solutions such as the ones in
the running example above are synthesized. We defer the formal details to Sections 4.1 and 5.2.
PCSat adopts the counterexample-guided inductive synthesis (CEGIS) approach to semi-decide
the satisfiability of the given pfwCSP instance. As standard for a CEGIS-based approach, it consistsof two sub-phases, a synthesis phase and a validation phase, and maintains a set of counterexamples.
A counterexample is a ground clause obtained by instantiating the term variables of a clause in the
input pfwCSP instance. In each iteration, the synthesis phase attempts to synthesize a candidate
solution that satisfies the current set of counterexamples, and then the validation phase checks
if the candidate solution is a genuine solution, i.e., one that actually satisfies the input pfwCSP
instance. If the validation phase detects that the candidate solution is not genuine, then it adds
to the set of counterexamples ground clauses that are unsatisfied by the candidate solution5 . The
semi-algorithm terminates with success when the validation phase detects that the latest candidate
solution is genuine, and terminates with failure when the synthesis phase detects the current set ofcounterexamples unsatisfiable (i.e., the input pfwCSP instance is actually unsatisfiable).
As described above, in an ordinary CEGIS-based approach, non-genuine candidate solutions are
only used to obtain additional counterexamples. Our novel modular primal-and-dual approach adds
an additional phase that follows the synthesis phase in which the non-genuine candidate solution
is analyzed to see if it is a partial solution. As discussed in the example above and in Section 1,
roughly, a candidate solution 𝜌 is detected to be a partial solution for an ordinary predicate variable
𝑋 if 𝜌 satisfies the clauses that define 𝑋 , that is, the clauses in which 𝑋 appears negatively andtransitively the clauses that define the ordinary predicate variables appearing positively in such
clauses. For instance, in the example above, only J itself appears as a positively occurring ordinary
predicate variable in the clause defining J (i.e., clause (3)), and so a candidate solution that satisfies
clause (3) (but may fail to satisfy the other clauses) is a partial solution for J.
As we shall describe in more detail in Section 5.2, the formal definition of partial solutions extends
the above by also allowing a partial solution to only satisfy under-approximations of the clauses
obtained by replacing some of the positively-occurring predicate variables by their lower-bounds,
where the lower-bounds are computed from (previously discovered) partial solutions themselves.
As we shall show in Section 5.2, the extension allows discovering more partial solutions, especiallyfor pfwCSP instances obtained from encoding methods that generates (co-)inductive predicate
definitions that mutually depend on each others.
3

𝜇CLP: A FIRST-ORDER FIXPOINT LOGIC WITH BACKGROUND THEORIESThis section defines 𝜇CLP, a first-order fixpoint logic with background theories. Its name is derived
from constraint logic programming (CLP) [Jaffar and Maher 1994] because it can be seen as anextension of CLP with arbitrarily-nested inductive and co-inductive predicate definitions andquantifiers.
5 Such ground clauses are obtained as by-products of checking the genuineness of the candidate solution (cf. Section 4.1).

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:8

Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

Let T be a (possibly many-sorted) first-order theory with the signature Σ. The syntax of T formulas 𝜙 and T -terms 𝑡 is:
𝜙 ::= 𝑋 (𝑡 1, . . . , 𝑡 ar(𝑋 ) ) | 𝑝 (𝑡 1, . . . , 𝑡 ar(𝑝) ) | ¬𝜙 | 𝜙 1 ∨ 𝜙 2 | ∀𝑥 : 𝑠.𝜙𝑡 ::= 𝑥 | 𝑓 (𝑡 1, . . . , 𝑡 ar(𝑓 ) )Here, the meta-variables 𝑋 and 𝑥 respectively range over predicate and term variables. The metavariables 𝑝 and 𝑓 respectively denote predicate and function symbols of the signature Σ. We use 𝑠
as a meta-variable ranging over sorts of the signature Σ. We write • for the sort of propositions
and 𝑠 1 → 𝑠 2 for the sort of functions from 𝑠 1 to 𝑠 2 . The return sort of a predicate variable is •. We
write ar(𝑜) and sort(𝑜) respectively for the arity and the sort of a syntactic element 𝑜. A function 𝑓
represents a constant if ar(𝑓 ) = 0. We write ftv(𝜙) and fpv(𝜙) respectively for the set of free termand predicate variables of 𝜙. We write 𝑥e for a sequence of term variables, |e
𝑥 | for the length of 𝑥e,and 𝜖 for the empty sequence. We assume the usual derived forms 𝜙 1 ∧ 𝜙 2 , 𝜙 1 ⇒ 𝜙 2 , and ∃𝑥 : 𝑠.𝜙.
A 𝜇CLP P over the theory T is a sequence of mutually (co-)recursive equations of the form:(𝑋 1 (e𝑥 1 ) =𝛼 1 𝜙 1 ); . . . ; (𝑋𝑚 (e𝑥𝑚 ) =𝛼𝑚 𝜙𝑚 ). Here, 𝛼𝑖 ∈ {𝜇, 𝜈 } and for any 𝑖, 𝑗 ∈ {1, . . . , 𝑚}, 𝑋𝑖 may
occur only positively in 𝜙 𝑗 . Informally, 𝑋 (e𝑥 ) =𝜇 𝜙 (resp. 𝑋 (e𝑥 ) =𝜈 𝜙) represents the inductive (resp.
co-inductive) predicate 𝜇𝑋 (e𝑥 ). 𝜙 (resp. 𝜈 𝑋 (e𝑥 ). 𝜙) defined as the least (resp. greatest) fixpoint of
the function F (𝑋 ) = 𝜆e𝑥 .𝜙. Note here that F is monotonic because the bound predicate variable 𝑋
occurs only positively in the body 𝜙.
The order of the equations is important. They express nestings of quantifiers 𝜇 and 𝜈 in ordinary
fixpoint logics. For example, a 𝜇CLP (𝑋 =𝜈 𝑋 ∧𝑌 ); (𝑌 =𝜇 𝑋 ∨𝑌 ) corresponds to 𝜈𝑋 .𝑋 ∧ (𝜇𝑌 .𝑋 ∨𝑌 )whereas its order reversed, that is, (𝑌 =𝜇 𝑋 ∨ 𝑌 ); (𝑋 =𝜈 𝑋 ∧ 𝑌 ),corresponds to 𝜇𝑌 .(𝜈𝑋 .𝑋 ∧ 𝑌 ) ∨ 𝑌 .
We define dom(P) = {𝑋 1, . . . , 𝑋𝑚 }. We say that P is closed if ftv(𝜙𝑖 ) ⊆ {e𝑥𝑖 }, fpv(𝜙𝑖 ) ⊆ dom(P)for each equation 𝑋𝑖 (e𝑥𝑖 ) =𝛼𝑖 𝜙𝑖 of P. A query for a 𝜇CLP P is defined as a T -formula 𝜙. We saythat the query is closed with respect to P if ftv(𝜙) = ∅ and fpv(𝜙) ⊆ dom(P). For a query 𝜙 andan interpretation 𝜌 of ftv(𝜙) ∪ fpv(𝜙), we write 𝜌 |= 𝜙 if 𝜙 is true under 𝜌. For a 𝜇CLP P, theinterpretation [[P]] (∅) maps dom(P) to their fixpoints (cf. Section 3.1 for the formal definition). A
𝜇CLP validity problem instance is pair (𝜙, P) of a closed 𝜇CLP P and a query 𝜙 closed with respect
to P. We say that (𝜙, P) is valid, written |= (𝜙, P), if [[P]] (∅) |= 𝜙.
𝑚 to be the
We define the De Morgan dual (or simply dual) of a closed 𝜇CLP P = (𝑋𝑖 (e𝑥𝑖 ) =𝛼 𝜙𝑖 )𝑖=1¬𝑚¬
𝜇CLP ¬P defined by (𝑋𝑖 (e𝑥𝑖 ) =¬𝛼 𝜎 (¬𝜙𝑖 ))𝑖=1 where 𝜎 ≜ {𝑋 1 ↦→ ¬𝑋 1 , . . . 𝑋𝑚 ↦→ ¬𝑋𝑚¬ }, ¬𝜇 ≜ 𝜈,and ¬𝜈 ≜ 𝜇. The dual of a 𝜇CLP validity problem instance (𝜙, P) is the 𝜇CLP validity problem
instance (𝜎 (¬𝜙), ¬P) where 𝜎 is the substitution used in the definition of ¬P as shown above.
We say that each predicate variable 𝑋𝑖 in the primal 𝜇CLP P corresponds to the predicate variable
𝜎 (𝑋𝑖 ) = 𝑋𝑖¬ in its dual ¬P, and vice versa.
𝜇CLP generalizes CLP and existing first-order fixpoint logics with background theories such as
Mu-Arithmetic [Bradfield 1999; Kobayashi et al. 2019; Lubarsky 1993; Nanjo et al. 2018], and cannaturally encode diverse classes of temporal program verification problems:• Termination and non-termination verification for imperative programs (Section 3.2).
• Model checking of labeled transition systems (LTSs) and recursive programs where specifications are given as non-deterministic Büchi word automata, which strictly subsume LTL. The
encodings for LTSs and recursive programs are explained in Section 3.3 and Kobayashi et al.
[2019], respectively.
• Modal-𝜇-calculus model checking of imperative programs. The encoding is given in Kobayashi
et al. [2019].
• Value-dependent temporal properties verification of higher-order effectful functional programs. The encoding is given in Nanjo et al. [2018].
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:9

As concrete examples of encodings, we present in Section 3.2 a modular encoding of terminationand non-termination verification for imperative programs, and in Section 3.3, a modular encodingof linear temporal property verification for LTSs. As we shall show, the former is modular in the
program side, that is, the 𝜇CLP encoding for a statement of a program is built from the predicatesdefined in the 𝜇CLP encodings for its sub-statements. By contrast, the latter is modular in theproperty side, that is, a temporal property is given by a Büchi automaton whereby the encoding
defines inductive and co-inductive predicates for each state of the automaton whose definitions arebuilt from the (co-)inductive predicates defined for the states one-step reachable from that state.
Section 3.1 presents the formal semantics of 𝜇CLP. Readers acquainted with first-order fixpoint
logics and their semantics may skip the section.
3.1

Semantics

We formalize the semantics of 𝜇CLP. Let A = (D, Σ, 𝐼 ) be the structure of the background firstorder theory T . Here, D is the universe, Σ is the signature, and 𝐼 is the interpretation function forthe predicate and function symbols in Σ. We write D𝑠 for the set of values in D of the sort 𝑠. In
particular, we define D• ≜ {⊤, ⊥} for the sort • of propositions. For a sequence e𝑠 = 𝑠 1, . . . , 𝑠𝑚 ofsorts with 𝑚 ≥ 0, we write De𝑠 for the sequence D𝑠1 , . . . , D𝑠𝑚 . We define D (e𝑠 →𝑠) ≜ De𝑠 → D𝑠 . We
assume that 𝐼 (𝑝) ∈ De𝑠 → D• if sort(𝑝) = e
𝑠 → •, and 𝐼 (𝑓 ) ∈ De𝑠 → D𝑠 if sort(𝑓 ) = e
𝑠 → 𝑠. We
introduce the partially ordered sets (D (e𝑠 →•) , ⊑ (e𝑠 →•) ) by defining⊑• ≜ {(⊤, ⊤), (⊥, ⊤), (⊥, ⊥)},⊑ (e𝑠 →•) ≜ {(𝑓 , 𝑔) | ∀e𝑣 ∈ De𝑠 .𝑓 (e𝑣 ) ⊑• 𝑔(e𝑣 )}.

Note that the least upper bound ⊔ (e𝑠 →•) and the greatest lower bound ⊓ (e𝑠 →•) operators with respectto ⊑ (e𝑠 →•) satisfy⊤ ⊓• ⊤⊤ ⊔• ⊤= ⊤,= ⊤,𝑓 ⊓ (e𝑠 →•) 𝑔⊤ ⊓• ⊥⊤ ⊔• ⊥⊥,⊤,==⊥ ⊓• ⊤⊥ ⊔• ⊤= 𝜆e𝑣 ∈ De𝑠 . 𝑓 (e𝑣 ) ⊓• 𝑔(e
𝑣 ),

= ⊥,
= ⊤,

𝑓 ⊔ (e𝑠 →•) 𝑔⊥ ⊓• ⊥⊥ ⊔• ⊥

=
=

⊥,
⊥

= 𝜆e
𝑣 ∈ De𝑠 . 𝑓 (e𝑣 ) ⊔• 𝑔(e𝑣)Note that (De𝑠 →•, ⊑e𝑠 →• ) is a complete lattice. The least (resp. greatest) element of De𝑠 →• is 𝜆e
𝑥. ⊥(resp. 𝜆e𝑥 . ⊤). The negation operator ¬ (e𝑠 →•) is defined by
¬• ⊤

=

⊥,

¬• ⊥

=

⊤,

¬ (e𝑠 →•) 𝑓= 𝜆e𝑣 ∈ De𝑠 . ¬• 𝑓 (e𝑣)

Given a T -formula 𝜙 and an interpretation 𝜌 of free term and predicate variables in 𝜙, we write
J𝜙K(𝜌) for the truth value of 𝜙 which is defined as follows:
J𝑋 (e𝑡 )K(𝜌)J𝜙 1 ∨ 𝜙 2 K(𝜌)J∃𝑥 : 𝑠.𝜙K(𝜌)J∀𝑥 : 𝑠.𝜙K(𝜌)J𝑥K(𝜌)≜≜≜≜≜

𝜌 (𝑋 ) (Je𝑡 K(𝜌)),
J𝜙 1 K(𝜌) ⊔• J𝜙 2 K(𝜌),Ãd • { J𝜙K(𝜌 {𝑥 ↦→ 𝑣 }) | 𝑣 ∈ D𝑠 },• { J𝜙K(𝜌 {𝑥 ↦→ 𝑣 }) | 𝑣 ∈ D𝑠 },𝜌 (𝑥),J𝑝 (e𝑡 )K(𝜌)J𝜙 1 ∧ 𝜙 2 K(𝜌)J¬𝜙K(𝜌)≜≜≜𝐼 (𝑝) (Je𝑡 K(𝜌)),
J𝜙 1 K(𝜌) ⊓• J𝜙 2 K(𝜌),¬• J𝜙K(𝜌)J𝑓 (e𝑡 )K(𝜌)≜𝐼 (𝑓 ) (Je𝑡 K(𝜌))

Here, we assume that 𝜌 (𝑥) ∈ Dsort(𝑥) and 𝜌 (𝑋 ) ∈ De𝑠 → D• if sort(𝑋 ) = e
𝑠 → •. We write 𝜌 |= 𝜙if and only if J𝜙K(𝜌 ′) = ⊤ holds for any extension 𝜌 ′ of the interpretation 𝜌 for the term andpredicate variables in (ftv(𝜙) ∪ fpv(𝜙)) \ dom(𝜌), where dom(𝜌) represents the domain of 𝜌. We
say the given formula 𝜙 is valid and write |= 𝜙 if and only if ∅ |= 𝜙 holds.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:10Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

Given a 𝜇CLP P and an interpretation 𝜌 of free term and predicate variables in P, we write[[P]] (𝜌) for the predicate interpretation for dom(P) induced by P which is defined byJ𝜖K(𝜌) ≜ ∅,J(𝑋 (e𝑥 ) =𝛼 𝜙); PK(𝜌) ≜ J𝑋 (e𝑥 ) =𝛼 𝜙K P (𝜌) ⊎ [[P]] (𝜌 ⊎ [[𝑋 (e𝑥 ) =𝛼 𝜙]] P (𝜌)),
n
o
J𝑋 (e
𝑥 ) =𝛼 𝜙K P (𝜌) ≜ 𝑋 ↦→ FP𝛼sort(𝑋 ) 𝜆𝑞.𝜆e
𝑣 .J𝜙K 𝜌 {𝑋 ↦→ 𝑞, 𝑥e ↦→ e𝑣 } ⊎ JPK (𝜌 {𝑋 ↦→ 𝑞})
where dom(𝜌) ∩ dom(P) = ∅ and the fixpoint operator FPe𝑠𝛼→• (•) is defined by:dFPe𝑠𝜇→• (𝐹 ) ≜ (e𝑠 →•) { 𝑞 ∈ De𝑠 →• | 𝐹 (𝑞) ⊑ (e𝑠 →•) 𝑞 },ÃFPe𝑠𝜈→• (𝐹 ) ≜ (e𝑠 →•) { 𝑞 ∈ De𝑠 →• | 𝑞 ⊑ (e𝑠 →•) 𝐹 (𝑞) }We note that the domain over which fixpoints are taken is De𝑠 →• , with the semantic ordering ⊑e𝑠 →• .
Example 3.1. Let us consider 𝜇CLP P𝜈𝜇 ≜ (𝑋 =𝜈 𝑋 ∧ 𝑌 ); (𝑌 =𝜇 𝑋 ∨ 𝑌 ) and 𝜇CLP P𝜇𝜈 ≜ (𝑌 =𝜇𝑋 ∨ 𝑌 ); (𝑋 =𝜈 𝑋 ∧ 𝑌 ). Note that the semantics of P𝜈𝜇 and P𝜇𝜈 are different as shown below,
though the definition of P𝜈𝜇 and P𝜇𝜈 only differ in the order of the equations:JP𝜈𝜇 K(∅) = 𝜌 𝜈𝜇 ⊎ J𝑌 =𝜇 𝑋 ∨ 𝑌 K𝜖 (𝜌 𝜈𝜇 ) = {𝑋 ↦→ ⊤, 𝑌 ↦→ ⊤}JP𝜇𝜈 K(∅) = 𝜌 𝜇𝜈 ⊎ J𝑋 =𝜈 𝑋 ∧ 𝑌 K𝜖 (𝜌 𝜇𝜈 ) = {𝑋 ↦→ ⊥, 𝑌 ↦→ ⊥}
where

𝜇 
𝜌 𝜈𝜇 = J𝑋 =𝜈 𝑋 ∧ 𝑌 K (𝑌 =𝜇 𝑋 ∨𝑌 ) (∅) = 𝑋 ↦→ FP•𝜈 𝜆𝑞.J𝑋 ∧ 𝑌 K({𝑋 ↦→ 𝑞} ⊎ 𝜌𝑞 )Ã
= 𝑋 ↦→ • { 𝑞 | 𝑞 ⊑• J𝑋 ∧ 𝑌 K({𝑋 ↦→ 𝑞, 𝑌 ↦→ 𝑞}) } = {𝑋 ↦→ ⊤}no𝜇𝜌𝑞 = J𝑌 =𝜇 𝑋 ∨ 𝑌 K({𝑋 ↦→ 𝑞}) = 𝑌 ↦→ FP•𝜇 𝜆𝑞 ′ .J𝑋 ∨ 𝑌 K({𝑋 ↦→ 𝑞, 𝑌 ↦→ 𝑞 ′ }) = {𝑌 ↦→ 𝑞}no𝜌 𝜇𝜈 = J𝑌 =𝜇 𝑋 ∨ 𝑌 K (𝑋 =𝜈 𝑋 ∧𝑌 ) (∅) = 𝑌 ↦→ FP•𝜇 𝜆𝑞.J𝑋 ∨ 𝑌 K({𝑌 ↦→ 𝑞} ⊎ 𝜌𝑞𝜈 )d= 𝑌 ↦→ • { 𝑞 | J𝑋 ∨ 𝑌 K({𝑋 ↦→ 𝑞, 𝑌 ↦→ 𝑞}) ⊑• 𝑞 } = {𝑌 ↦→ ⊥}𝜌𝑞𝜈 = J𝑋 =𝜈 𝑋 ∧ 𝑌 K({𝑌 ↦→ 𝑞}) = 𝑋 ↦→ FP•𝜈 𝜆𝑞 ′ .J𝑋 ∧ 𝑌 K({𝑋 ↦→ 𝑞 ′, 𝑌 ↦→ 𝑞}) = {𝑋 ↦→ 𝑞}■

Remark 1. Note that quantifiers over recursively enumerable (r.e.) domains (e.g., integers) can beeliminated in 𝜇CLP; We can encode ∃𝑥 : int.𝜙 and ∀𝑥 : int.𝜙 respectively as 𝐸 (0) and 𝐴(0) using thefollowing inductive and co-inductive predicates 𝐸 and 𝐴:
𝐸 (𝑥) =𝜇 𝜙 ∨ [−𝑥/𝑥]𝜙 ∨ 𝐸 (𝑥 + 1)
𝐴(𝑥) =𝜈 𝜙 ∧ [−𝑥/𝑥]𝜙 ∧ 𝐴(𝑥 + 1)
Intuitively, 𝐸 and 𝐴 are required to hold for some and for all integer 𝑥, respectively. This encoding
strategy, however, cannot apply to non r.e. domains like real numbers and is not useful in practiceeven for r.e. domains like rational numbers that have no simple way to enumerate all its elements.
This is the reason why our reduction given in Section 5 instead applies Skolemization with functional
predicate variables to handle quantifiers.
3.2

Encoding Termination and Non-Termination Verification for Imperative Programs

We consider a simple imperative language whose syntax of statements is given below.
𝑠::= skip | 𝑥 := 𝑒 | 𝑥 := ∗ | 𝑠 1 ; 𝑠 2 | if 𝑒 then 𝑠 1 else 𝑠 2 | while 𝑒 do 𝑠

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

encTerm( skip) ≜ (𝑊 ,𝑇 ,𝑊 (e𝑥 ) =𝜇 ⊤,𝑇 (e𝑥 , 𝑥e′) =𝜇

72:11

′
𝑥 ∈e
𝑥𝑥 =𝑥 )

Ó

encTerm(𝑥 := 𝑒) ≜ (𝑊 ,𝑇 , (𝑊 (e𝑥 ) =𝜇 ⊤); (𝑇 (e𝑥 , 𝑥e′) =𝜇 𝑥 ′ = 𝑒 ∧encTerm(𝑥 := ∗) ≜ (𝑊 ,𝑇 , (𝑊 (e𝑥 ) =𝜇 ⊤); (𝑇 (e𝑥 , 𝑥e′) =𝜇

Ó

Ó

𝑦 ∈e
𝑥 ,𝑦≠𝑥 𝑦𝑦 ∈e𝑥 ,𝑦≠𝑥 𝑦′ = 𝑦)})′ = 𝑦))(_,𝑇1¬, P1¬ ) = ¬(𝑊1,𝑇1, P1 )encTerm(𝑠 1 ; 𝑠 2 ) ≜ (𝑊 ,𝑇 ,𝑊 (e𝑥 ) =𝜇 𝑊1 (e𝑥 ) ∧ ∀e𝑥 ′ .𝑇1¬ (e𝑥 , 𝑥e′) ∨ 𝑊2 (𝑥e′);
′
′′
′′
′′
′
𝑇 (e
𝑥 , 𝑥e ) =𝜇 ∃e
𝑥 .𝑇1 (e𝑥 , 𝑥e ) ∧ 𝑇2 (e𝑥 , 𝑥e ); P1 ; P1¬ ; P2 )encTerm(𝑠 1 ) = (𝑊1,𝑇1, P1 )encTerm(𝑠 2 ) = (𝑊2,𝑇2, P2 )encTerm(𝑠 1 ) = (𝑊1,𝑇1, P1 ) encTerm(𝑠 2 ) = (𝑊2,𝑇2, P2 )encTerm( if 𝑏 then 𝑠 1 else 𝑠 2 ) ≜ (𝑊 ,𝑇 ,𝑊 (e𝑥 ) =𝜇 𝑏 ∧ 𝑊1 (e𝑥 ) ∨ ¬𝑏 ∧ 𝑊2 (e
𝑥 );
𝑇 (e
𝑥 , 𝑥e′) =𝜇 𝑏 ∧ 𝑇1 (e𝑥 , 𝑥e′) ∨ ¬𝑏 ∧ 𝑇2 (e𝑥 , 𝑥e′); P1 ; P2 )encTerm(𝑠 0 ) = (𝑊0,𝑇0, P0 )(_,𝑇0¬, P0¬ ) = ¬(𝑊0,𝑇0, P0 )encTerm( while 𝑏 do 𝑠 0 ) ≜ (𝑊 ,𝑇 ,Ó(𝑊 (e𝑥 ) =𝜇 ¬𝑏 ∨ 𝑏 ∧ ∀e𝑥 ′ .𝑇0¬ (e𝑥 , 𝑥e′) ∨ 𝑊 (e
𝑥 ′);
′
′
′′
′′
′′
𝑇 (e
𝑥 , 𝑥e ) =𝜇 ¬𝑏 ∧ 𝑠 ∈e
𝑥 .𝑇0 (e𝑥 , 𝑥e ) ∧ 𝑇 (e𝑥 , 𝑥e′); P0 ; P0¬ )𝑥 𝑥 = 𝑥 ∨ 𝑏 ∧ ∃eFig. 1. Modular encoding of termination/non-termination verification problems.

Here 𝑒 and 𝑏 respectively range over integer type expressions and boolean expressions. For (integertyped) variables of the language, we purposefully overload the term variables of 𝜇CLP and use
𝑥, 𝑦, 𝑧, etc. to range over them. The statement 𝑥 := ∗ denotes an assignment of a non-deterministic
integer value to the variable 𝑥.
The semantics of the language is standard. A state of the program 𝑠 is a sequence of integers e𝑣such that |e𝑣 | = |e𝑥 | where 𝑥e are the variables that appear in 𝑠. Roughly, a state represents the valuesof the variables. We write ⟨e𝑣 , 𝑠⟩ ⇓ e𝑣 ′ to mean that there is a terminating execution of 𝑠 from the′initial state e𝑣 to the final state e𝑣 , and write ⟨e𝑣 , 𝑠⟩ ⇑ to mean that there is a non-terminating executionof 𝑠 from the initial state e𝑣 . We say that a program 𝑠 always terminates (or, simply terminates) if not⟨e𝑣 , 𝑠⟩ ⇑ for any e𝑣 , and that 𝑠 may non-terminate (or, simply non-terminates) if ⟨e𝑣 , 𝑠⟩ ⇑ for some e𝑣.
That is, a program is said to be terminating if every execution of it is terminating, and otherwise
it is said to be non-terminating. The termination verification problem seeks to decide if the given
program is terminating or not. We reduce the problem soundly and completely to a 𝜇CLP validity
problem. Recall that 𝜇CLP is parameterized by a background first-order theory T . For the encoding
described in this section, we assume that the background theory is the theory of integers6 .
Let 𝑥e be the variables of the given program. We define the encoding procedure encTerm(𝑠) which
returns a triple (𝑊 ,𝑇 , P) where 𝑊 and 𝑇 are predicate variables defined in the 𝜇CLP P such thatar(𝑊 ) = |e
𝑥 | and ar(𝑇 ) = 2 · |e𝑥 |. As we shall show, 𝑊 encodes the weakest precondition for thetermination of 𝑠 and 𝑇 encodes the transition relation of 𝑠. The encoding is defined inductively
on the syntax of 𝑠 as shown in Figure 1. Here, we assume that 𝑊 and 𝑇 in the rules are fresh
predicate variables, and we write ¬(𝑊 ,𝑇 , P) for the De Morgan dual of (𝑊 ,𝑇 , P) defined by:¬(𝑊 ,𝑇 , P) = (𝑊 ¬,𝑇 ¬, P ¬ ) where P ¬ is the De Morgan dual of the 𝜇CLP P, and 𝑊 ¬ and 𝑇 ¬ are
the predicate variables defined in P ¬ that correspond to 𝑊 and 𝑇 , respectively.
The encoding ensures the following property.
6 More precisely, we assume that the background theory is one that can interpret the integer and boolean expressions of the

programming language.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:12Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

Lemma 3.2. Let (𝑊 ,𝑇 , P) = encTerm(𝑠). Then, [[P]] (∅) |= 𝑊 (e𝑣 ) iff not ⟨e𝑣 , 𝑠⟩ ⇑, and [[P]] (∅) |=
𝑇 (e
𝑣, e
𝑣 ′) iff ⟨e
𝑣 , 𝑠⟩ ⇓ e𝑣 ′.
That is, the 𝜇CLP P obtained by the encoding (𝑊 ,𝑇 , P) = encTerm(𝑠) precisely encodes theweakest precondition for termination of 𝑠 as the inductive predicate 𝑊 , and the transition relationof 𝑠 as the inductive predicate 𝑇 . Therefore, to verify (resp. refute) the termination of 𝑠, it suffices
to check the validity of the 𝜇CLP validity problem instance (∀e
𝑥 .𝑊 (e𝑥 ), P) where (𝑊 ,𝑇 , P) =encTerm(𝑠). More formally, we state the correctness of the encoding in the theorem below.
Theorem 3.3. Let (𝑊 ,𝑇 , P) = encTerm(𝑠). Then, 𝑠 terminates iff |= (∀e
𝑥 .𝑊 (e𝑥 ), P).
Note that the encoding contains nested (co-)inductive predicates. Namely, while the predicates 𝑊
and 𝑇 appearing in the conclusion of each rule is inductive, the complementation done in the rules
for sequences and loops introduce co-inductive predicate definitions. Also, note that the encoding
is modular. That is, the encoding for a statement 𝑠 contains the (co-)inductive predicates definedin the encodings for the sub-statements of 𝑠 as sub-formulas. Our encoding is inspired by similar
encodings for temporal property verification of functional programs given in Nanjo et al. [2018];
Unno et al. [2017a].
Example 3.4. Recall the program from Section 2.1. Applying encTerm to the inner while loop yields
the triple (J, P, Pin ) where Pin consists of the following recursive equations defining the inductive
predicates J and P (after some simplification, and by modeling nondet by a non-deterministic
assignment):
J (𝑥 2 ) =𝜇 ¬(𝑥 2 ≠ 3) ∨ J (𝑥 2 + 1)
P (𝑥 2, 𝑥 2′ ) =𝜇 𝑥 2′ = 𝑥 2 ∨ 𝑥 2 ≠ 3 ∧ P (𝑥 2 + 1, 𝑥 2′ )Note that the equation defining J is the same as the one in Pterm from Section 2.1, and the otherequation defining P is the same as the one in Pnterm . The order of the equations does not matter inthis case because the equations do not refer to each others’ predicates7 . It can be readily seen that J
and P respectively express the weakest precondition for the termination and the transition relationof the inner while loop. Then, using this encoding result for the inner while loop, the encoding
procedure yields for the outer while loop the triple (I, Q, Pout ) where Pout consists of the equationsin Pin and the equations defining I and NP from Pterm and the following equation defining Q:
Q(𝑥 1, 𝑥 2, 𝑥 1′ , 𝑥 2′ ) =𝜇 ¬(𝑥 1 ≥ 0 ∧ 𝑥 2 ≥ 0) ∧ 𝑥 2′ = 𝑥 2 ∧ 𝑥 1′ = 𝑥 1 ∨𝑥1 ≥ 0 ∧ 𝑥2 ≥ 0 ∧𝑥 2′ = 𝑥 2 − 1 ∧ (𝑥 1′ = 𝑥 1 ∨ ∃𝑥 2′′ .P (𝑥 2, 𝑥 2′′) ∧ 𝑥 2′ = 𝑥 2′′ − 1 ∧ 𝑥 1′ = 𝑥 1 − 1)
The equations in Pout are ordered appropriately so that an equation come before those that define
predicate variables occurring in the equation. Note that the equation defining I contains an occurrence of the co-inductive predicate NP whose definition is obtained by taking the dual of theequation defining P. Then, by modeling the assume with a conditional statement, for the whole
program, the encoding procedure returns (K, R, Pprog ) where Pprog consists of the equations in
Pout and the following equations (ordered appropriately as remarked above):
K (𝑥 1, 𝑥 2 ) =𝜇 ¬(𝑥 2 ≤ 3) ∨ I (𝑥 1, 𝑥 2 )R(𝑥 1, 𝑥 2, 𝑥 1′ , 𝑥 2′ ) =𝜇 ¬(𝑥 2 ≤ 3) ∧ 𝑥 1′ = 𝑥 1 ∧ 𝑥 2′ = 𝑥 2 ∨ 𝑥 2 ≤ 3 ∧ Q(𝑥 1, 𝑥 2, 𝑥 1′ , 𝑥 2′ )Finally, by simplifying Pprog by removing predicate definitions on which K does not depend (i.e., theequations defining Q and R) and moving the (non-recursive) equation defining K to the query part,
we obtain the 𝜇CLP validity problem instance (∀𝑥 1, 𝑥 2 .𝑥 2 > 3 ∨ I (𝑥 1, 𝑥 2 ), Pterm ) from Section 2.1.
7 Also, the order of equations does not matter when the equations are all of the same fixpoint modality (i.e., all 𝜇 or all 𝜈).

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:13

By construction, |= (∀𝑥 1, 𝑥 2 .K (𝑥 1, 𝑥 2 ), Pprog ) iff |= (∀𝑥 1, 𝑥 2 .𝑥 2 > 3 ∨ I (𝑥 1, 𝑥 2 ), Pterm ), and thus by
Theorem 3.3, we have obtained a sound-and-complete encoding of the termination verification
problem for the program as a 𝜇CLP validity problem. Taking the dual of the problem instance yields
the dual 𝜇CLP validity problem instance (∃𝑥 1, 𝑥 2 .𝑥 2 ≤ 3 ∧ NI (𝑥 1, 𝑥 2 )), Pnterm ) from Section 2.1 thatsoundly-and-completely encodes the non-termination verification problem for the same program.
3.3

Encoding Linear Temporal Verification for Labeled Transition Systems

A labeled transition system (LTS) is a triple (Z𝑛 , {𝜓 ℓ }ℓ ∈𝐿 , 𝐿) where Z𝑛 is the the set of states where
each state is a 𝑛-tuple of integers, 𝐿 is the finite set of labels, and {𝜓 ℓ }ℓ ∈𝐿 is an 𝐿-indexed set oftransition relations where |= 𝜓 ℓ (e𝑣, e𝑣 ′) for e𝑣, e𝑣 ′ ∈ Z𝑛 represents that the LTS may transition from the′state e𝑣 to the state e𝑣 with the label ℓ. Note that our LTS is an infinite-state system8 .
We review the notion of a Büchi automaton. A non-deterministic Büchi automaton 𝐴 is a tuple(𝑄, 𝐿, 𝛿, 𝑞 init , 𝐹 ) where 𝑄 is the finite set of states (unrelated to the states of the LTS), 𝛿 ⊆ 𝑄 × 𝐿 × 𝑄
is the transition relation, 𝑞 init ∈ 𝑄 is the starting state, and 𝐹 ⊆ 𝑄 is the set of final states. For 𝑞 ∈ 𝑄
and ℓ ∈ 𝐿, we write 𝛿 (𝑞, ℓ) for the set {𝑞 ′ ∈ 𝑄 | (𝑞, ℓ, 𝑞 ′) ∈ 𝛿 }. An infinite word ℓ0 ℓ1 · · · ∈ 𝐿𝜔 is
accepted by 𝐴 if and only if there exists an infinite sequence of states 𝑞 0, 𝑞 1, . . . such that 𝑞 0 = 𝑞 init ,𝑞𝑖+1 ∈ 𝛿 (𝑞𝑖 , ℓ) for all 𝑖 ≥ 0, and some state in 𝐹 occurs infinitely often.
We consider the temporal property verification problem in which we are given an LTS 𝑀 =𝑥 ) on states of 𝑀, and a Büchi automaton 𝐴 such that the label(Z𝑛 , {𝜓 ℓ }ℓ ∈𝐿 , 𝐿), a predicate 𝜙 init (eset of 𝐴 is 𝐿. The goal of the verification is to decide if for any (infinite) execution of 𝑀 from astate satisfying 𝜙 init (e𝑥 ), the infinite sequence of labels of the execution is accepted by 𝐴. That is,
the goal is to verify whether the given LTS satisfies the linear temporal property specified by thegiven Büchi automaton. We give an encoding of the verification problem in 𝜇CLP. Our encoding
is inspired by a similar encoding of temporal verification problems for recursive programs given
in [Kobayashi et al. 2019]. Let P𝑀,𝐴 be the 𝜇CLP comprising, for each 𝑞 ∈ 𝑄 and 𝛼 ∈ {𝜇, 𝜈 }, thefollowing equations defining mutually-recursive (co-)inductive predicates LV𝑞,𝛼 (e𝑥 ):ÓÔLV𝑞,𝛼 (e𝑥 ) =𝛼 ℓ ∈𝐿 ∀e𝑦 .𝜓 ℓ (e𝑥 , 𝑦e) ⇒ 𝑞′ ∈𝛿 (𝑞,ℓ) LV𝑞′,𝛼 (𝑞′ ) (e𝑦)where 𝛼 (𝑞) = 𝜈 if 𝑞 ∈ 𝐹 and 𝛼 (𝑞) = 𝜇 otherwise. The equations are ordered so that the co-inductive
equations come before the inductive equations. The correctness of the encoding is stated below.
Theorem 3.5. 𝑀 satisfies the temporal property given by 𝜙 init and 𝐴 iff the 𝜇CLP validity problem(∀e𝑥 .𝜙 init (e𝑥 ) ⇒ LV𝑞init ,𝜈 (e𝑥 ), P𝑀,𝐴 ) is valid.
The theorem follows from the fact that LV𝑞,_ (e𝑥 ) represents the set of states from which thelabels along the execution of the LTS is accepted by 𝐴 when 𝐴 is run from the state 𝑞. Note that theoccurrence of a predicate in the body of the recursive definition becomes the LV_,𝜇 variant whenno state in 𝐹 is visited in the corresponding execution step. This ensures that there must be a pathin which a state from 𝐹 is visited infinitely often.
4

PFWCSP

We review pfwCSP [Unno et al. 2021] that generalizes constrained Horn clauses (CHCs) and serves
as an intermediary in our modular primal-dual method for automatically deciding 𝜇CLP validity
problems. We use a meta-variable 𝜑 to range over T -formulas without quantifiers and predicate
Ôℓvariables.
First, a pCSP [Satake et al. 2020] C is a finite set of clauses of the form 𝜑 ∨ 𝑖=1
𝑋𝑖 (e𝑡𝑖 ) ∨
Ô𝑚
e
¬𝑋
(
𝑡
)
where
0
≤
ℓ
≤
𝑚.
We
defineftv(𝑐),
ftv(C)
andfpv(C)
intheobviousmanner.
𝑖𝑖𝑖=ℓ+1
We regard that the variables in ftv(C) are implicitly universally quantified. A pCSP is CHCs if
8 For concreteness we explain the encoding for LTSs over integers. However, our encoding method can be easily extended to

LTSs over any domain in the background theory of 𝜇CLP.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:14Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinenℓ ≤ 1 for all clauses, and co-CHCs if 𝑚 ≤ ℓ + 1 for all clauses. A predicate substitution 𝜎 is a map
from predicate variables 𝑋 to closed predicates of the form 𝜆𝑥 1, . . . , 𝑥 ar(𝑋 ) .𝜑. We write 𝜎 (C) for
the application of 𝜎 to C and dom(𝜎) for the domain of 𝜎. We call 𝜎 a syntactic solution for C ifÓfpv(C) ⊆ dom(𝜎) and |= 𝜎 (C). Similarly,
we call a predicate interpretation 𝜌 a semantic solution
Ófor C if fpv(C) ⊆ dom(𝜌) and 𝜌 |= C.
We next extend pCSP to pfwCSP by adding functionality and well-foundedness constraints. A
pfwCSP (C, K) consists of• a finite set C of pCSP clauses, and• a kinding map K that maps each 𝑋 ∈ fpv(C) to its kind: any one of •, ⇓, or 𝜆 which
respectively represent ordinary, well-founded, and functional predicate variable.
We write 𝜌 |= WF (𝑋 ) if the interpretation 𝜌 (𝑋 ) of the predicate variable 𝑋 is well-founded, thatis, sort(𝑋 ) = (e𝑠 ,e𝑠 ) → • for some sequence e𝑠 of sorts and there is no infinite sequence e
𝑣 1, e𝑣 2, . . . ofsequences e𝑣𝑖 of values of the sorts e𝑠 such that (e𝑣𝑖 , e𝑣𝑖+1 ) ∈ 𝜌 (𝑋 ) for all 𝑖 ≥ 1. We write 𝜌 |= FN (𝑋 )if sort(𝑋 ) = (e𝑠 , 𝑠) → • and 𝜌 |= ∀e𝑥:e𝑠 .(∃𝑦 : 𝑠.𝑋 (e𝑥 , 𝑦)) ∧ ∀𝑦1, 𝑦2 : 𝑠.(𝑋 (e𝑥 , 𝑦1 ) ∧ 𝑋 (e𝑥 , 𝑦2 ) ⇒ 𝑦1 = 𝑦2 )holds. We call a predicate interpretation 𝜌 a semantic solution for (C, K), written 𝜌 |= (C, K), if 𝜌
is a semantic solution of C, 𝜌 |= WF (𝑋 ) for all 𝑋 such that K (𝑋 ) = ⇓, and 𝜌 |= FN (𝑋 ) for all 𝑋
such that K (𝑋 ) = 𝜆. The notion of syntactic solution can be similarly generalized to pfwCSP.
Definition 4.1 (Satisfiability of pfwCSP). The predicate satisfiability problem of a pfwCSP (C, K)
is that of deciding whether it has a semantic solution.
It is known that the satisfiability of CHCs and the validity of CLP are inter-reducible (see e.g.,
Unno et al. [2017b]). Unno et al. [2021] presents a semi-algorithm called PCSat for semi-deciding thesatisfiability of pfwCSP. PCSat implements a counterexample-guide inductive synthesis (CEGIS)
based semi-algorithm that is sound and (relatively) complete that we will review in the next
subsection. In Section 5, we will show a sound and complete reduction from the 𝜇CLP validity
problem to the pfwCSP satisfiability problem.
4.1

CEGIS-based pfwCSP Solving

We review the CEGIS-based pfwCSP satisfiability checking semi-algorithm PCSat introducedin Unno et al. [2021]. As informally described in Section 2.2, PCSat consists of two phases, thesynthesis phase and the validation phase, that are iteratively executed until convergence (or up tosome time limit).
Algorithm 1 shows the pseudo-code of PCSat. PCSat takes as input a pfwCSP instance (C, K).
It first initializes the set of counterexamples 𝐸 to be an empty set (line 2)9 . Then, it iterates the
CEGIS iteration loop (lines 3–17) until convergence (or up to some time limit). In each iteration,
we call the sub-routine SynthesizeCandSol to synthesize a candidate solution that satisfies thecurrent set of counterexamples (line 4), that is, a substitution 𝜌 such that 𝜌 |= (𝐸, K). If there isno such a substitution, then SynthesizeCandSol returns UNSAT, indicating that (𝐸, K) is actuallyunsatisfiable. Since this implies that the input pfwCSP instance (C, K) is also unsatisfiable, the
CEGIS loop terminates by returning UNSAT (line 6). Otherwise, we obtain the substitution 𝜌 as a
candidate solution to the input pfwCSP instance, and we call the sub-routine ValidateCandSol
to check if the candidate solution also satisfies the input instance (C, K) (line 9). If so, then thecandidate solution is a genuine solution to the input instance and we terminate the CEGIS loop by
returning SAT (line 11). Otherwise, we obtain additional counterexamples 𝐸 ′ that witness the failureof 𝜌 to be a genuine solution. Formally, 𝐸 ′ is a set of ground clauses obtained by instantiating the
9 𝐸 can also be initialize with any set of ground clauses obtained by instantiating the term variables of the input clauses.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:15

Algorithm 1 PCSat
1: function PCSat((C, K))
2:
𝐸←∅
3:
while true do
4:ressyn ← SynthesizeCandSol(𝐸)5:if ressyn = UNSAT thenreturn UNSAT
else
let 𝜌 = ressyn inresval ← ValidateCandSol(𝜌, (C, K))
if resval = SAT then11:
return SAT
12:
else
13:
let 𝐸 ′ = resval in14:
𝐸 ← 𝐸 ∪ 𝐸′
15:
end if16:
end if17:
end while
18: end function
6:
7:
8:
9:
10:

term variables of the clauses of C such that 𝜌 ̸ |= (𝐸 ′, K). The new counterexamples are added tothe set of counterexamples 𝐸 and we repeat the CEGIS iteration.
We note that the SynthesizeCandSol always terminates, and returns UNSAT only when it finds
the given set of counterexamples semantically unsatisfiable (since a counterexample is a groundclause, there always exists a candidate solution conforming to a finite and semantically-consistent
set of counterexamples). Also, it only returns candidate solutions that satisfy functionality andwell-foundedness constraints by construction. The termination of ValidateCandSol depends on
the background theory (more precisely, whether the backend SMT solver terminates or not on the
background theory), and we assume that it terminates on theories with decidable satisfiability suchas LIA and NRA. We defer further details of the candidate solution synthesis and candidate solution
validation processes to [Unno et al. 2021]. PCSat is sound and complete, in the following sense.
Theorem 4.2 (Soundness and Completeness of PCSat [Unno et al. 2021]). PCSat((C, K))
returns SAT only if (C, K) is satisfiable, and returns UNSAT only if (C, K) is unsatisfiable.
As remarked before, PCSat is a semi-algorithm and is not guaranteed to always terminate. It
is necessarily so for most background theories including the theory of linear integer arithmetic,
because the satisfiability problem even for CHCs which is a subclass of pfwCSP as remarked before,
is already undecidable for such theories. However, PCSat is relatively complete in the sense that
if a syntactic solution exists and ValidateCandSol terminates on the background theory then it
is guaranteed to eventually converge. We defer the details of relative completeness to Unno et al.
[2021].
5

MODULAR PRIMAL-DUAL SOLVING

We now formally present the main contribution of this paper: MuVal, the novel modular primaldual approach to semi-deciding 𝜇CLP validity. Given a 𝜇CLP validity checking problem instance(𝜙 𝑝 , P𝑝 ), MuVal first constructs its De Morgan dual (𝜙𝑑 , P𝑑 ) as described in Section 3. Next, boththe primal instance (𝜙 𝑝 , P𝑝 ) and the dual instance (𝜙𝑑 , P𝑑 ) are each reduced to corresponding
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:16Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

pfwCSP constraint sets (C𝑝 , K𝑝 ) and (C𝑑 , K𝑑 ) by the process described in Section 5.1. Finally,
MuVal solves the two constraint sets in parallel. Each constraint solving process runs the PCSat
constraint solving semi-algorithm of Unno et al. [2021] except that with the modification to inferpartial solutions (cf. Section 5.2) so that whenever a partial solution for some predicate variable
is inferred by one process, a corresponding upper-bound is synthesized and passed to the otherprocess to reduce their search space. The partial solutions are also used to synthesize lower-bounds
of predicate variables for the process that inferred it. When one of the processes returns satisfiable(resp. unsatisfiable), we conclude by returning valid (resp. invalid) if it is the primal process that
returned, or invalid (resp. valid) if it is the dual process.
The following subsections describe the details of the sub-processes. Section 5.1 describes the
reduction of 𝜇CLP to pfwCSP and Section 5.2 describes the synthesis and exchange of sound bounds.
Section 5.3 gives a detailed description of the entire MuVal semi-algorithm.
5.1

Reduction of 𝜇CLP to pfwCSP

We now define the reduction of the given 𝜇CLP validity problem (𝜙, P) to a pfwCSP satisfiability
problem (C, K). We assume without loss of generality that predicates 𝑋 ∈ dom(P) occur only
positively in the query 𝜙: we can always transform the given query into this form by replacing
each negative occurrence of 𝑋 in 𝜙 with ¬𝑋 ¬ where the predicate 𝑋 ¬ is defined by the dual ¬P.
Our reduction consists of three steps: The first step, elim ∃ , Skolemizes positive occurrencesof existential quantifiers and negative occurrences of universal quantifiers by introducing fresh
functional predicate variables. The second step, elim𝜇 , replaces inductive predicates defined by𝜇-equations with co-inductive predicates defined by 𝜈-equations with guards (i.e., well-foundedness
constraints) for co-recursion added to preserve the semantics. The third step, elim𝜈 , further eliminates co-inductive predicates by replacing them with uninterpreted predicates represented as fresh
predicate variables. The reduction is defined asred(𝜙, P) ≜let (𝜙 𝜇 , P𝜇 , K𝜇 ) = elim ∃ (𝜙, P, ∅) inlet (𝜙 𝜈 , P𝜈 , K𝜈 ) = elim𝜇 (𝜙 𝜇 , P𝜇 , K𝜇 ) in elim𝜈 (𝜙 𝜈 , P𝜈 , K𝜈 )Here, the 𝜇CLP (𝜙 𝜇 , P𝜇 ) with free predicate variables K𝜇 is obtained from (𝜙, P) by eliminating
existential quantifiers with fresh functional predicate variables as stated above. The definition ofelim𝜈 (𝜙, P, K) is given as:elim𝜈 (𝜙, 𝜖, K) ≜ (cnf (𝜙), K)elim𝜈 (𝜙, P; (𝑋 (e𝑥 ) =𝜈 𝜙 ′), K) ≜ (C ∪ cnf (𝑋 (e𝑥 ) ⇒ 𝜙 ′), K ′ ∪ 𝑋 ↦→ • )where (C, K ′) = elim𝜈 (𝜙, P, K)
Here, 𝜙 is the formula obtained from 𝜙 by replacing each occurrence of a predicate 𝑋 ∈ dom(P)with the predicate variable 𝑋 that representsÓan under-approximation of 𝑋 . cnf (𝜙) converts 𝜙 into
its prenex and conjunctive normal form ∀e𝑥 . C and returns the set C of clauses. The trickiest partof the algorithm, namely, elim𝜇 (𝜙, P, K), is defined by:elim𝜇 (𝜙, P, K) ≜ (𝜙, P, K) where P is =𝜇 free.
𝑚 , K) ≜elim𝜇 (𝜙, P; (𝑋 (e𝑥 ) =𝜇 𝜙 ′); (𝑋𝑖 (e𝑥𝑖 ) =𝜈 𝜙𝑖 )𝑖=1
elim𝜇 (𝜎0 (𝜙), 𝜎0 (P); P ′, K ∪ 𝑋 ⇓ ↦→ ⇓ ) where𝑚P ′ = (𝑋 (e𝑥 ) =𝜈 𝜎𝑋 (𝜙 ′)); (𝑋𝑖 (𝑏𝑖 , 𝑥e, 𝑥e𝑖 ) =𝜈 𝜎𝑖 (𝜙𝑖 ))𝑖=1
𝜎0 = { 𝑋𝑖 ↦→ 𝜆e
𝑦 .𝑋𝑖 (⊥, e𝑣 , 𝑦e) | 𝑖 = 1, . . . , 𝑚 }𝜎𝑋 = 𝑋 ↦→ 𝜆e𝑦 .𝑋 (e𝑦 ) ∧ 𝑋 ⇓ (e𝑥 , 𝑦e) ∪ { 𝑋𝑖 ↦→ 𝜆e
𝑦 .𝑋𝑖 (⊤, 𝑥e, 𝑦e) | 𝑖 = 1, . . . , 𝑚 }𝜎𝑖 = 𝑋 ↦→ 𝜆e𝑦 .𝑋 (e𝑦 ) ∧ (𝑏𝑖 ⇒ 𝑋 ⇓ (e𝑥 , 𝑦e)) ∪ { 𝑋 𝑗 ↦→ 𝜆e𝑦 .𝑋 𝑗 (𝑏𝑖 , 𝑥e, 𝑦e) | 𝑗 = 1, . . . , 𝑚 }Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:17

As remarked before, elim𝜇 (𝜙, P, K) is inspired by an analogous reduction done in binary reachability analysis [Cook et al. 2006; Grebenshchikov et al. 2012; Kuwahara et al. 2014] for termination
verification. Next, we describe the main ideas of the reduction. The third argument of elim𝜇 accumulates generated fresh well-founded predicate variables. The base case of elim𝜇 (𝜙, P, K) justreturns the converted 𝜈-only 𝜇CLP (𝜙, P) with free predicate variables K. In the recursive step, forthe definition 𝑋 (e𝑥 ) =𝜇 𝜙 ′ of the right-most inductive (i.e., 𝜇) predicate 𝑋 in the input 𝜇CLP, we
generate a fresh well-founded predicate variable 𝑋 ⇓ and use it as the guard for each co-recursion in
the converted co-inductive definition 𝑋 (e𝑥 ) =𝜈 𝜎𝑋 (𝜙 ′): we use the substitution 𝜎𝑋 to replace each′call 𝑋 (e𝑡 ) in the body 𝜙 of 𝑋 with 𝑋 (e𝑡 ) ∧ 𝑋 ⇓ (e𝑥,e𝑡 ) that checks that the formal arguments 𝑥e of 𝑋
and the actual arguments e𝑡 of the co-recursion are related by the well-founded relation represented
by 𝑋 ⇓ .
At the same time, we extend the formal arguments of each co-inductive (i.e., 𝜈) predicate 𝑋𝑖 in theright-hand side of the equation for 𝑋 with arguments 𝑥e of the same sort as the formal arguments of
𝑋 and a Boolean argument 𝑏𝑖 , where we assume that the formal arguments 𝑥e𝑖 of 𝑋𝑖 are 𝛼-renamed
to avoid a name conflict between 𝑥e𝑖 and 𝑥e, 𝑏𝑖 . The extended formal arguments 𝑥e of 𝑋𝑖 are used
to receive the actual arguments previously passed to a call to the inductive predicate 𝑋 and are
related by 𝑋 ⇓ , in the converted definition of 𝑋𝑖 , with the actual arguments passed to each indirect
recursive call to 𝑋 in 𝑋𝑖 . Dummy values are passed as 𝑥e when no such previous call to 𝑋 exists
and the extended Boolean formal argument 𝑏𝑖 of 𝑋𝑖 indicates whether there indeed is such a callto 𝑋 and its actual arguments are passed as 𝑥e to 𝑋𝑖 (𝑏𝑖 = ⊤) or the dummy values are passed as 𝑥e
to 𝑋𝑖 (𝑏𝑖 = ⊥). In fact, we use the substitution 𝜎0 to replace each call 𝑋𝑖 (e𝑡 ) in the query 𝜙 and thedefinition of the predicates P in the left-hand side of the equation for 𝑋 with 𝑋𝑖 (⊥, e𝑣,e𝑡 ) for somesequence e𝑣 of dummy values of the same sorts as the formal arguments 𝑥e of 𝑋 . For the definition𝑋 (e𝑥 ) =𝜇 𝜙 ′, we use the substitution 𝜎𝑋 to replace each call 𝑋𝑖 (e𝑡 ) in 𝑋 with 𝑋𝑖 (⊤, 𝑥e, e𝑡 ).
Finally, for the definition 𝑋 𝑗 (e𝑥 𝑗 ) =𝜈 𝜙 𝑗 of each co-inductive predicate 𝑋 𝑗 in the right-hand sideof the equation for 𝑋 , we use 𝜎 𝑗 to replace each call 𝑋𝑖 (e𝑡 ) in 𝑋 𝑗 with 𝑋𝑖 (𝑏 𝑗 , 𝑥e, e𝑡 ) and each call 𝑋 (e𝑡)with 𝑋 (e𝑡 ) ∧ (𝑏 𝑗 ⇒ 𝑋 ⇓ (e𝑥,e𝑡 )) that checks that if 𝑥e are not dummy (i.e., 𝑏 𝑗 = ⊤), the actual argumentsof a previous call to 𝑋 passed around to 𝑋 𝑗 as its extended formal arguments 𝑥e are related by
𝑋 ⇓ with the actual arguments e𝑡 of the indirect recursive call to 𝑋 . In the resulting pfwCSP, thegenerated well-founded predicate variables occur only positively.
Example 5.1. Let us consider the 𝜇CLP (𝜙, P𝑋 ; P𝑌 ) where 𝜙 ≜ ∀𝑥 .𝑋 (𝑥) ∧ 𝑌 (𝑥), P𝑋 ≜ (𝑋 (𝑥) =𝜇
𝑌 (𝑥 − 1)), and P𝑌 ≜ (𝑌 (𝑦) =𝜇 𝑦 ≤ 0 ∨ 𝑋 (𝑦 − 1)). We obtain elim ∃ (𝜙, P𝑋 ; P𝑌 , ∅) = (𝜙, P𝑋 ; P𝑌 , ∅)andelim𝜇 (𝜙, P𝑋 ; P𝑌 , ∅) = elim𝜇(𝜙, P𝑋 ; (𝑌 (𝑦) =𝜈 𝑦 ≤ 0 ∨ 𝑋 (𝑦 − 1)), ∅) =(∀𝑥 .𝑋 (𝑥) ∧ 𝑌 (⊥, 0, 𝑥), P, 𝑋 ⇓ ↦→ ⇓ ) where P =𝑋 (𝑥) =𝜈 𝑌 (⊤, 𝑥, 𝑥 − 1)); 𝑌 (𝑏, 𝑥, 𝑦) =𝜈 𝑦 ≤ 0 ∨ 𝑋 (𝑦 − 1) ∧ (𝑏 ⇒ 𝑋 ⇓ (𝑥, 𝑦 − 1))
Here, in the first step of the transformation, the inductive definition of 𝑌 is simply replaced by the
co-inductive definition because the body of 𝑌 has no recursive call to 𝑌 . The indirect recursive callto 𝑋 in 𝑌 is properly handled in the second step by adding the formal arguments 𝑏 and 𝑥 to 𝑌 . Notealso that in the call 𝑌 (⊥, 0, 𝑥) in the query, 0 is used as a dummy value for the extended formal
argument 𝑥 of 𝑌 . We thus get the pfwCSP red(𝜙, P) = (C, K) where
𝑋 (𝑥), 𝑌 (⊥, 0, 𝑥), ¬𝑋 (𝑥) ∨ 𝑌 (⊤, 𝑥, 𝑥 − 1), ¬𝑌 (𝑏, 𝑥, 𝑦) ∨ 𝑦 ≤ 0 ∨ 𝑋 (𝑦 − 1),C≜¬𝑌 (𝑏, 𝑥, 𝑦) ∨ 𝑦 ≤ 0 ∨ ¬𝑏 ∨ 𝑋 ⇓ (𝑥, 𝑦 − 1))K ≜ 𝑋 ↦→ •, 𝑌 ↦→ •, 𝑋 ⇓ ↦→ ⇓The reduction presented here can be optimized removing unnecessary arguments (cf. Appendix C).
The soundness and the completeness of the reduction is stated below (cf. Appendix D for proof).
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:18Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

Theorem 5.2 (Soundness and Completeness of the Reduction from 𝜇CLP to pfwCSP).
(𝜙, P) is valid if and only if red(𝜙, P) is satisfiable.
Remark 2. Our reduction generates co-CHCs-style clauses that have only one negatively occurring
ordinary predicate variable. We have adopted this style because it the more natural direction from a
fixpoint logic point of view. Note that one can systematically convert back-and-forth from the co-CHCs
style to the CHCs style (i.e., only one positively occurring ordinary predicate variable in each clause)by replacing each literal of the form 𝑋 (e𝑡 ) with ¬𝑋 ¬ (e𝑡 ) and ¬𝑋 (e𝑡 ) with 𝑋 ¬ (e𝑡 ) for 𝑋 ∈ fpv(C), where¬
𝑋 is a fresh predicate variable that represents the negation of the ordinary predicate variable 𝑋 .
5.2

Synthesizing Sound Bounds from Partial Solutions

We now describe how the parallel pfwCSP constraint solving processes synthesize sound lowerand-upper-bounds from partial solutions to reduce each other’s solution spaces. As described in
Sections 2.2 and 4.1, the pfwCSP solver PCSat generates in each of its CEGIS iteration a candidate
solution to the given pfwCSP instance. In an ordinary CEGIS-based approach, such a candidate
solution, when it is found not to be a genuine solution, is only used to obtain additional counterexamples and then forgotten. However, in our novel modular primal-dual approach, we also check
whether the (non-genuine) candidate solution is a partial solution that satisfies some subset of theclauses. As we discussed in Sections 1 and 2.2, and shall describe in more detail next, such partial
solutions can be used to generate sound lower- and upper- bounds to reduce the solution spaces ofthe primal and the dual instances.
We next formalize when a candidate solution is a partial solution. For this, we define somepreliminary notions. In what follows, we assume that for any pfwCSP instance (C, K) and an
ordinary predicate variable 𝑋 of (C, K), there is a unique sequence of variables 𝑥e such that any
clause 𝑋 (e𝑦 ) ⇒ 𝜓 ∈ C satisfies 𝑦e = 𝑥e. Note that any pfwCSP instance generated by our reduction
method described in Section 5.1 can be converted to such a form because each clause has at mostone negatively occurring ordinary predicate variable. Also, for an ordinary predicate variable 𝑋 ,we define the definition of 𝑋 , denoted by Defs C (𝑋 ), to be the set of formulas {𝜓 | 𝑋 (e𝑥 ) ⇒ 𝜓 ∈ C}.
We omit C and simply write Defs (𝑋 ) when it is clear from the context. We say that a substitution
𝜌 is well-kinded for (C, K) if 𝜌 |= WF (𝑋 ) for all 𝑋 such that K (𝑋 ) = ⇓, and 𝜌 |= FN (𝑋 ) for all 𝑋
such that K (𝑋 ) = 𝜆. We write fpvord (𝜙) for the set of free ordinary predicate variables of 𝜙 (weassume that K is clear
Ð from the context). We extend the notation sets of clauses in the obvious
way: fpvord (C) = 𝜙 ∈ C fpvord (𝜙). We are now ready to formally define partial solutions.
Definition 5.3 (Partial Solution). For a candidate solution 𝜌 for a pfwCSP instance (C, K) and an
ordinary predicate variable 𝑋 ∈ fpvord (C), the property that 𝜌 is a partial solution for 𝑋 , written𝜌 ▷ ( C,K) 𝑋 , is defined co-inductively as the largest relation satisfying the following condition:𝜌 ▷ ( C,K) 𝑋 iff (1) 𝜌 is well-kinded and (2) there exists a set of ordinary predicate variables 𝑆 ⊆Ófpvord (𝜑) where 𝜑 = Defs C (𝑋 ) such that(2a) |= 𝜌 (𝑋 ) (e𝑥 ) ⇒ 𝜌𝑆 (𝜑) where 𝜌𝑆 = {𝑌 ↦→ LB(𝑌 ) | 𝑌 ∈ 𝑆 } ∪ {𝑌 ↦→ 𝜌 (𝑌 ) | 𝑌 ∉ 𝑆 }, and(2b) for each 𝑌 ∈ fpvord (𝜑) \ 𝑆, 𝜌 ▷ ( C,K) 𝑌 .
Here, LB(𝑌 ) is a lower-bound of the ordinary predicate variable 𝑌 that is initialized to be ⊥ andsoundly updated during the constraint solving process as we shall describe in Section 5.3. As we shallshow in Example 5.6, roughly, using a non-empty 𝑆 soundly cuts dependencies among predicate
variable definitions by under-approximating some predicate variables by concrete predicates that
denote their lower-bounds.
A partial solution for a predicate variable is generally not an actual solution of the given pfwCSP
because it needs not to satisfy clauses besides (under-approximations of) the ones that define that
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:19

Algorithm 2 PartialSolCheck
1: function PartialSolCheck((𝜌, (C, K)))2:
for each 𝑋 Ó∈ fpvord (C) do
3:
let 𝜑 = Defs C (𝑋 ) in4:
SAT2a(𝑋 ) ← {𝑆 | 𝑆 ⊆ fpvord (𝜑) ∧ 𝑆 satisfies condition (2a)}5:
end for

NotPsol ← ∅repeat𝑇 ← NotPsol
for each 𝑋 ∈ fpvord (C) \ NotPsol doÓ
let 𝜑 = Defs C (𝑋 ) in
if ∀𝑆 ∈ SAT2a(𝑋 ).(fpvord (𝜑) \ 𝑆) ∩ NotPsol ≠ ∅ then
12:
NotPsol ← NotPsol ∪ {𝑋 }13:
end if14:
end for15:
until 𝑇 = NotPsol
16:
return fpvord (C) \ NotPsol
17: end function
6:
7:
8:
9:
10:
11:

predicate variable. Namely, it need not to satisfy any goal clause which is (typically a unique) clausewith no negative occurrence of ordinary predicate variables (e.g., 𝑥 2 > 2 ∨ I (𝑥 1, 𝑥 2 ) in Cterm from
Section 2.2). However, a partial solution for a predicate variable is guaranteed to under-approximate
the least (resp. greatest) fixpoint of the corresponding inductive (resp. co-inductive) predicate,provided that LB also under-approximates the corresponding predicates in the same sense. We
state this property formally as the theorem below, which follows from the proof of Theorem 5.2.
Theorem 5.4. Suppose that (C, K) is reduced from a 𝜇CLP validity problem instance (𝜙, P), foreach 𝑌 ∈ fpvord (C), |= LB(𝑌 ) ⇒ [[P]] (∅) (𝑌 ) (e𝑥 ) where 𝑌 is the predicate variable in P corresponding
to 𝑌 , and 𝜌 is a partial solution for 𝑋 ∈ fpvord (C). Then, |= 𝜌 (𝑋 ) (e𝑥 ) ⇒ [[P]] (∅) (𝑋 ) (e𝑥 ) where 𝑋 is
the predicate variable in (𝜙, P) corresponding to 𝑋 .
Next, we describe an algorithm, PartialSolCheck, that computes, given a candidate solution 𝜌,
the set of ordinary predicate variables for which 𝜌 is a partial solution. We assume that condition (1),that is, well-kindedness of 𝜌, is satisfied10 . The pseudo-code of the algorithm is given in Algorithm 2.
Roughly, PartialSolCheck works by inductively marking ordinary predicate variables forwhich 𝜌 is not a partial solution. More formally, the algorithm takes a partial solution 𝜌 along witha pfwCSP instance (C, K) as input. It then builds the table SAT2a which stores for each ordinary
predicate variable 𝑋Ó, the set of sets of ordinary predicate variables that appear in the definition of 𝑋
such that if fpvord ( Defs C (𝑋 )) \𝑆 contains a predicate variable for which 𝜌 is not a partial solution
for every set of predicate variables 𝑆 in the set, then 𝜌 also cannot be a partial solution for 𝑋 . Moreconcretely, as shown in line 4, SAT2a(𝑋 ) is created by checking for each set of ordinary predicate
variables 𝑆 ⊆ fpvord (𝜑) whether 𝑆 satisfies condition (2a) mentioned above and letting such 𝑆 bea member of SAT2a(𝑋 ) 11 . Next, the algorithm initializes NotPsol to the empty set (line 6). NotPsol
is used to store the set of ordinary predicate variables for which 𝜌 is currently known not to be apartial solution. Then, the algorithm repeats the loop of lines 7–15 until no new predicate variables
for which 𝜌 is not a partial solution are discovered. Each iteration of the loop checks for each
10 This is ensured by construction for candidate solutions synthesized in PCSat (cf. Unno et al. [2021]).
11 As remarked in Remark 3, SAT2a can be optimized to only include maximal sets of ordinary predicate variables.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:20Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

ordinary predicate variable 𝑋 ∉ NotPsol, whether it should be put into NotPsol based on the table
SAT2a and the current NotPsol. Finally, the algorithm returns the set of ordinary predicate variables
that do not belong to NotPsol (line 16). It is easy to see that the algorithm works as intended, that is,
PartialSolCheck(𝜌, (C, K)) returns the set of predicate variables {𝑋 ∈ fpvord (C) | 𝜌 ▷ ( C,K) 𝑋 }.
From Theorem 5.4, it follows that if 𝜌 is a partial solution for a predicate variable 𝑋 in the
pfwCSP obtained from the primal (resp. dual) 𝜇CLP and 𝑋 is the (co-)inductive predicate in the
𝜇CLP corresponding to 𝑋 , then the complement of 𝜌 (𝑋 ) is an upper-bound of the (co-)inductive
predicate 𝑋 ¬ in the dual (resp. primal) 𝜇CLP. Therefore, adding the clause 𝑋 ¬ (e𝑥 ) ⇒ ¬𝜌 (𝑋 ) (e𝑥)to the pfwCSP reduced from the dual (resp. primal) 𝜇CLP where 𝑋 ¬ is the predicate variablecorresponding to 𝑋 ¬ does not rule out any actual solution of the dual (resp. primal) pfwCSP
because 𝑋 ¬ represents an under-approximation of 𝑋 ¬ . However, the addition of such a clausecan hasten the convergence of the constraint solving process as it (conservatively) reduces thespace of possible solutions. An analogy can be made to how clause-learning DPLL SAT solvers
conservatively reduce the solution space by asserting learned clauses.
Example 5.5. Recall Cterm from Section 2.2. Defs Cterm (J) = {¬(𝑥 2 ≠ 3) ∨ J (𝑥 2 + 1) ∧ J⇓ (𝑥 2, 𝑥 2 + 1)}.
ÓThen, for 𝑆 = ∅ ⊆ fpvord ( Defs Cterm (J)) = {J }, we have that |= 𝜌 (J) (𝑥 2 ) ⇒ 𝜌𝑆 (¬(𝑥 2 ≠ 3) ∨J (𝑥 2 + 1) ∧ J⇓ (𝑥 2, 𝑥 2 + 1)) for any substitution 𝜌 that satisfies clause (3) (note that 𝜌𝑆 = 𝜌 when𝑆 = ∅). Therefore, any such substitution that is well-kinded is a partial solution for J. For example,
𝜌𝑡 = {J ↦→ 𝜆𝑥 2 .𝑥 2 = 3, J⇓ ↦→ 𝜆𝑥 2, 𝑥 2′ .𝜑 } where 𝜆𝑥 2, 𝑥 2′ .𝜑 describes any well-founded relation overintegers is a partial solution for J. Note that, in this case, it suffices to let 𝑆 = ∅. The next example
shows a case where a non-empty 𝑆 is useful.
Example 5.6. Let C consist of the clauses below over ordinary predicate variables 𝑋 1, 𝑋 2, 𝑌1, 𝑌2
and a functional predicate variable 𝐹 :
(a)
(b)
(c)

𝑋 1 (𝑥, 𝑦) ⇒ 𝑋 2 (𝑥, 𝑦 + 1)
𝑋 2 (𝑥, 𝑦) ⇒ 𝑥 = 0 ∨ 𝑌1 (𝑥, 𝑦)
𝑋 2 (𝑥, 𝑦) ⇒ 𝑥 ≠ 0 ∨ 𝑌2 (𝑥, 𝑦)

(d)
(e)
(f)

𝑌1 (𝑥, 𝑦) ⇒ 𝑥 > 100 ∨ 𝑌1 (𝑥 + 1, 𝑦)
𝑌2 (𝑥, 𝑦) ⇒ ¬𝐹 (𝑥, 𝑦, 𝑧) ∨ 𝑧 > 0
𝑌2 (𝑥, 𝑦) ⇒ ¬𝐹 (𝑥, 𝑦, 𝑧) ∨ 𝑋 1 (𝑥 − 𝑧, 𝑦)Let 𝜌 be a substitution such that 𝜌 (𝑍 ) = 𝜆𝑥 .𝑥 > 0 for each 𝑍 ∈ {𝑋 1, 𝑋 2, 𝑌1, 𝑌2 } . We show that 𝜌 isa partial solution for 𝑋 2 and 𝑌1 with LB(𝑌2 ) = ⊥ (assuming that 𝜌 (𝐹 ) describes some total function
from pairs of integers to integers). First, 𝜌 is a partial solution for 𝑌1 because it directly satisfies
clause (d) that defines
Ó it and only 𝑌1 itself appearsÓin the definition. Secondly, with 𝑆 = {𝑌2 } ⊆{𝑌1, 𝑌2 } = fpvord ( Defs C (𝑋 2 )), we have that 𝜌𝑆 ( Defs C (𝑋 2 )) = (𝑥 = 0 ∨ 𝜌 (𝑌1 ) (𝑥, 𝑦)) ∧ (𝑥 ≠0∨LB(𝑌2 ) (𝑥, 𝑦))) = 𝑥 > 0. Therefore condition (2a) for 𝑋 2 is satisfied with that 𝑆. Then, because 𝜌 isa partial solution for 𝑌1 as described above, condition (2b) is also satisfied with the 𝑆 for 𝑋 2 . Thus, 𝜌is also a partial solution for 𝑋 2 . Note that 𝜌 cannot be a partial solution for 𝑋 2 if 𝑆 in Definition 5.3 isrestricted to be the empty set because 𝜌 does not satisfy clauses (e) and (f) that define 𝑌2 (regardlessof what 𝜌 (𝐹 ) is), which would be needed
if 𝑌2 in clause (c) was not under-approximated by its
Ó
concrete lower-bound LB(𝑌2 ) in 𝜌𝑆 ( Defs C (𝑋 2 )). Here, using the non-empty 𝑆 cut the dependency
on 𝑌2 (and 𝑋 1 ) from the definition of 𝑋 2 .
Remark 3. To compute the table SAT2a, for each ordinary predicate variable
𝑋 ∈ fpvord (C),ÓPartialSolCheck checks condition (2a) for each 𝑆 ⊆ fpvord (𝜑) where 𝜑 = Defs C (𝑋 ). As checking(2a) incurs a call to an SMT solver to decide |= 𝜌 (𝑋 ) (e𝑥 ) ⇒ 𝜌𝑆 (𝜑), the computation of SAT2a(𝑋 )makes a number of SMT calls exponential in |fpvord (𝜑)| and can be a performance bottleneck, The
cost can be alleviated by exploiting the observation that SAT2a(𝑋 ) only needs to contain “maximal”
sets of predicate variables. That is, it suffices to restrict SAT2a(𝑋 ) to contain 𝑆 ⊆ fpvord (𝜑) such that
𝑆 satisfies condition (2a) and there is no 𝑆 ⊂ 𝑆 ′ ⊆ fpvord (𝜑) with 𝑆 ′ satisfying condition (2a). Such
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:21

Input 𝝁CLP validity problem instance𝝓, 𝑷
Dualize

ToPfwCSP

ToPfwCSP
Primal Solver
SAT

𝑪 𝒑 , 𝒌𝒑

PCSAT

¬ 𝝓, 𝑷

Dual Solver
SAT

UNSAT

C. Sol.

𝑪 𝒅 , 𝒌𝒅
PCSAT

UNSAT

C. Sol.
UBUBPARTIALSOLCHECKPARTIALSOLCHECK

Valid

Invalid

Fig. 2. Overview of MuVal, the modular primal-dual 𝜇CLP validity solver

maximal sets can be efficiently computed by a greedy algorithm that starts from S = {fpvord (𝜑)},checks if all sets in S satisfies condition (2a) and if so lets SAT2a(𝑋 ) ← S and otherwise replaces thesets in S that do not satisfy the condition with sets obtained by removing one predicate variable fromeach such set, and repeat the process until we reach S whose elements all satisfy condition (2a).
5.3

A Detailed Description of the Modular Primal-Dual Semi-Algorithm

We now formalize MuVal, the modular primal-dual semi-algorithm for semi-deciding 𝜇CLP validity.
Figure 2 shows the overview of the semi-algorithm. Given an input 𝜇CLP validity problem instance(𝜙, P), MuVal makes its dual instance ¬(𝜙, P) (depicted by the box Dualize in Figure 2), andreduces both the primal (i.e. input) and the dual instances to pfwCSP constraint sets (C𝑝 , K𝑝 ) and(C𝑑 , K𝑑 ) via the method presented in Section 5.1, respectively (depicted by the boxes ToPfwCSP).
Then, the primal and the dual constraint sets are sent to the primal solver and the dual solver,
respectively. The two solvers are symmetric and run in parallel while exchanging sound upperbounds synthesized from partial solutions. Each solver uses a modified version of PCSat as a
sub-process, obtained by adding the following lines before line 12 in Algorithm 1:
i : 𝑆 ← PartialSolCheck(𝜌, (C, K))
ii : send ({𝑋 ¬ (e𝑥 ) ⇒ ¬𝜌 (𝑋 ) (e𝑥 ) | 𝑋 ∈ 𝑆 })iii : for each 𝑋 ∈ 𝑆 do LB(𝑋 ) ← LB(𝑋 ) ∨ 𝜌 (𝑋 ) (e𝑥 ) endfor
Additionally, the modified PCSat adds the line iv : C ← recv() ∪ C somewhere in the CEGIS
loop (lines 3–17) of Algorithm 1. Here, send (C ′) sends the set of clauses C ′ to the other solver
process, and recv() returns the set of clauses it received. The communication is non-blocking andbuffered so that recv() returns the union of the sets of clauses that have been received since the lasttime it was called. With the modification, PCSat, whenever it finds the given candidate solution
𝜌 to be non-genuine, computes the set of predicate variables 𝑆 for which 𝜌 is a partial solution
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:22Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

by calling the PartialSolCheck sub-routine (line i, and depicted by the arrows labeled C. Sol.
in Figure 2). Then, it communicates the learned information to the other process by sending theclauses {𝑋 ¬ (e𝑥 ) ⇒ ¬𝜌 (𝑋 ) (e𝑥 ) | 𝑋 ∈ 𝑆 } (line ii, and depicted by the arrows labeled UB). As explainedin Section 5.2, the clauses stipulate sound upper-bounds for the predicate variables of the otherprocess. Finally, it updates the lower-bound information LB by disjuncting LB(𝑋 ) with 𝜌 (𝑋 ) (e𝑥)for each 𝑋 ∈ 𝑆 (line iii). As explained in Section 5.2, LB is used by PartialSolCheck.
MuVal terminates by returning Valid if either the PCSat sub-process of the primal solver returns
SAT or that of the dual solver returns UNSAT, and terminates by returning Invalid if either the
PCSat sub-process of the primal solver returns UNSAT or that of the dual solver returns SAT.
The soundness and the completeness of MuVal immediately follows from the soundness andcompleteness of the reduction from 𝜇CLP validity to pfwCSP satisfiability (Theorem 5.2), thesoundness and completeness of PCSat (Theorem 4.2), and Theorem 5.4.
Theorem 5.7 (Soundness and Completness of MuVal). MuVal returns Valid only if the given
𝜇CLP validity problem instance is valid and returns Invalid only if it is invalid.
Example 5.8. Recall Cterm and its partial solution 𝜌𝑡 from Example 5.5 and Section 2.2. As explained there, 𝜌𝑡 is a partial solution for J. Additionally, J is the predicate in the input 𝜇CLP Pterm
corresponding to J, NJ is the dual predicate of J in the dual 𝜇CLP Pnterm , and NJ is the predicate variable in the pfwCSP Cnterm reduced from Pnterm corresponding to NJ. Thus, ¬𝜌𝑡 (J) (𝑥 2 ) = ¬(𝑥 2 ≠ 3)
is asserted as a sound upper-bound of NJ (𝑥 2 ) by adding the clause 𝑁 𝐽 (𝑥 2 ) ⇒ ¬(𝑥 2 = 3) to the
pfwCSP constraint set of the dual process. Likewise, 𝜌𝑡 (J) = 𝑥 2 ≠ 3 is a sound lower-bound of J,
and is used to update LB by LB(J) ← 𝑥 2 ≠ 3 ∨ LB(J).
As remarked in Section 2.2, used with a modular encoding of a verification problem, our primaldual solving method is able to synthesize information about individual program or specification
sub-component of the given program or specification. Namely, in this example, J and NJ represents
the terminating and non-terminating behavior of the inner loop of the program, respectively.
Correspondingly, the bounds synthesized for them give information about the states from which
the loop diverges and terminates, and therefore can be culled from the solution spaces of the dual
process and the primal process, respectively.
Remark 4. While we use partial solutions synthesized by one side to reduce the solution spaceof the other side, one may wonder if they can also be used to reduce the solution space of the sameside. That is, since a partial solution 𝜌 (𝑋 ) represents a lower-bound for the (co-)inductive predicate
𝑋 corresponding to 𝑋 , one may consider restricting the solution space of the same side by assertingthe clause 𝜌 (𝑋 ) (e𝑥 ) ⇒ 𝑋 (e𝑥 ). The clause asserts that any solution for 𝑋 is lower-bounded by 𝜌 (𝑋 ).
While this does not rule out the actual semantic fixpoint of 𝑋 from the solution space, it may rule out
sound syntactic solutions and can adversely affect the performance of the semi-algorithm. Namely, asolution for 𝑋 need not be the actual fixpoint of 𝑋 but only needs to be its under-approximation that is
sufficient to satisfy the given set of clauses.
Remark 5. As remarked before, PCSat synthesizes a candidate solution by finding a solutionthat is consistent with the current set of counterexamples, which are ground clauses obtained byinstantiating the term variables of the clauses in the given pfwCSP. While having more counterexamples
make the candidate solution more likely to be an actual solution, it can preclude synthesis of usefulpartial solutions, especially in the unsatisfiable side because there is no actual solution there. To
this end, MuVal implements a heuristic where partial solutions consistent with only some subsets ofthe counterexamples are synthesized. Specifically, in each iteration, MuVal synthesizes two kinds ofsubstitutions as candidates for partial solutions: those consistent with (1) all counterexamples, and(2) for each ordinary predicate variable 𝑋 , only the counterexamples obtained by instantiating theProc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:23

100

100

100

10

1

MuVal-parallel-exc

1000

Mu2CHC1000

AProVE

1000

10

1

1

10

100

MuVal-parallel

1000

10

1

1

10

100

MuVal-parallel

1000

1

10

100

MuVal-parallel

1000

Fig. 3. Comparison with AProVE and Mu2CHC on termination/non-termination benchmarks.

clauses that (transitively) define 𝑋 and some additional clauses of the form 𝑋 (e𝑡 ) where 𝑋 (e𝑡 ) appears
positively in a counterexample.
6

IMPLEMENTATION AND EVALUATION

We present the evaluation with MuVal. MuVal is implemented in Multicore OCaml and supports
the combined theory of Booleans, integer and rational arithmetic, and algebraic data types. We
report on two experimental evaluation. The supplementary material contains the benchmark set.
(Non-)Termination Verification. We experimented with MuVal on the 335 (non-)termination
verification problems from Termination Competition 2021 (C Integer track). For these benchmarks,
we encode the problems by first translating the given C program to a labeled transition system(LTS) in T2 format [Brockschmidt et al. 2016] using Clang and llvm2KITTeL [Falke et al. 2011] andsystematically encoding the termination verification problem for LTSs as 𝜇CLP validity checking
problems following the encoding approach described in Section 3.3 (by restricting the temporal
property to termination/non-termination). We compared MuVal with the state-of-the-art (non)termination verification tools AProVE [Giesl et al. 2017], iRankFinder [Ben-Amram and Genaim
2014], UltimateAutomizer [Heizmann et al. 2014], and Mu2CHC [Kobayashi et al. 2019].
Mu2CHC is a tool for semi-deciding the validity problem for Mu-Arithmetic, which is an instanceof 𝜇CLP with integer arithmetic as the background theory. Mu2CHC is based on an incomplete
reduction to CHCs and embarrassingly parallel solving of primal and dual problems (cf. Section 7
for more detail). For an ablation study, we ran MuVal with four configurations: primal (resp.
dual) only solves the primal (resp. dual) 𝜇CLP, parallel solves primal and dual problems inan embarrassingly parallel manner without exchanging sound upper-bounds, and parallel/exc
further enables the exchange of sound upper-bounds. The experiments were conducted on StarExec(CentOS Linux release 7.7.1908, Intel(R) Xeon(R) CPU E5-2609 @ 2.40GHz with 27 GiB RAM) with
1,200 seconds time limit.
The cactus plot shown in Figure 4 plots the number of solved instances (x-axis) against the time
taken to solve the instances (y-axis), non-cumulatively, for the above tools. MuVal’s parallel/exc
solved 210 terminating + 108 non-terminating instances while parallel solved 211 + 108, primalsolved 211 + 61, and dual solved 8 + 107. AProVE solved 216 terminating + 100 non-terminating
instances, iRankFinder solved 208 + 93, UltimateAutomizer solved 200 + 99, and Mu2CHC
solved 145 + 105. One problem instance was incorrectly reported non-terminating by iRankFinder.
Note that parallel (and parallel/exc) solved a similar number of instances as AProVE, the winnerof the C Integer track of the competition in 2018, 2020, and 2021. The left-most scatter plot in
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:24Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

Figure 3 compares them in detail. The scatter plot is in log-scale. Here the color of dots indicatesterminating (blue) and non-terminating (red) instances. We can see an advantage of parallel over
AProVE with respect to the elapsed time.
Note also that parallel significantly outperforms Mu2CHC 10
MuVal-parallelwith respect to the number of solved instances. As for the
AProVEiRankFinder
elapsed time, Mu2CHC often solved easy instances faster thanUltimateAutomizer
10
parallel as shown in the middle plot of Figure 3. This is partly
because Mu2CHC uses SPACER [Komuravelli et al. 2016] as
the backend CHCs solver. SPACER, being a highly-tuned 10
mature tool, is often substantially faster than PCSat that
MuVal uses as the backend pfwCSP solver (on CHCs subset
of pfwCSP). The right-most plot of Figure 3 compares the 10
configurations parallel and parallel/exc. There, we cannot
observe the advantage of parallel/exc over parallel. This
10
0
50
100
150
200
250
300
is partly because the encoded 𝜇CLP problems here tend to
Benchmarks passed (out of 335)
contain a small number of predicates with low modularity
which suppressed the exchange of learned upper-bounds.
Fig. 4. Cactus Plot for Termination VerTime in seconds (1,200 seconds time limit)

3

2

1

0

−1

ification.

Temporal Verification. We also experimented with MuVal
on 202 𝜇CLP validity checking problems that encode a diverse collection of temporal verification
problems: (1) 41 LTL verification problems from Dietsch et al. [2015], (2) 61 small and 56 industrial
CTL verification problems from Cook and Koskinen [2013], (3) 28 Mu-Arithmetic problems from
Kobayashi et al. [2019] encoding some properties of integer arithmetic (Problems 1–6), linear-time
temporal properties of first-order functional programs (Problems 7–22), branching-time temporal
properties (some only expressible in CTL* or modal-𝜇) of imperative programs (Problems 23–28),
and (4) 16 termination verification problems of FuncTion [Urban 2013; Urban and Miné 2014]. For(1) and (2), we automatically generated 𝜇CLP from the target C code using the reduction methodin Kobayashi et al. [2019] where we used LTL3BA [Babiak et al. 2012] to translate the given LTL
formula into a Büchi automaton. For (4), we applied encoding approach described in Section 3.2(manually, at the time of writing) to translate the problems to 𝜇CLP validity problems.
On the entire benchmark set (i.e., (1)-(4)), we compared with Mu2CHC which, to our knowledge,
is the only tool besides our MuVal that can handle all those classes of benchmarks. On the class(1) of LTL benchmarks, we compared MuVal with the state-of-the-art LTL verifier UltimateLTLAutomizer [Dietsch et al. 2015]. The experiments were conducted on Amazon Linux 2, Intel(R)Xeon(R) Platinum 8259CL CPU @ 2.50GHz CPU and 32 GiB RAM with 600 seconds time limit.
The cactus plot shown in Figure 6 compares the 4 configurations of MuVal with Mu2CHC.
MuVal’s parallel/exc solved 102 VALID + 92 INVALID instances while parallel solved 98 + 90,
primal solved 99 + 62, dual solved 41 + 86, and Mu2CHC solved 86 + 87. Note that parallel (andparallel/exc) significantly outperforms Mu2CHC: Mu2CHC failed to solve 23 instances that weresolved by MuVal and require synthesis of predicates with a complex shape and large coefficients(e.g., piecewise-defined and/or lexicographic affine ranking functions). This shows a limitationof Mu2CHC that relies on an incomplete reduction, separately synthesizes ranking functions
and inductive invariants, and cannot quickly feedback a failure of invariant synthesis to ranking
function synthesis and vice versa.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

100

MuVal-parallel

Mu2CHC

100

72:25

10

1

10

1

1

10

MuVal-parallel-exc

100

1

10

MuVal-parallel-exc

100Fig. 5. Comparison with Mu2CHC on temporal verification benchmarks.

Note also that parallel/exc further improves parallel: parallel/exc solved 4 hard instances thatwere not solved with parallel by exchanging sound upper-bounds12 . The scatter plots comparing
Mu2CHC, parallel and parallel/exc are shown in Figure 5.
Finally, we compare MuVal with UltimateLTLAuMuVal-parallel-exc
tomizer on the 41 LTL verification problems. MuVal parMuVal-parallel
Mu2CHC
allel/exc solved 18 VALID + 18 INVALID instances while 10
MuVal-primal
MuVal-dual
MuVal parallel solved 16 + 16, MuVal primal solved 16 +10
11, MuVal dual solved 4 + 13, and UltimateLTLAutomizer
solved 20 + 15. MuVal parallel/exc solved 4 instances thatwere not solved by UltimateLTLAutomizer. Among the 10
instances, MuVal even discovered that the LTL benchmark
files contained incorrect classifications, claiming “safe” when 10
they actually are not. On the other hand, MuVal failed
to solve 3 instances that were solved by UltimateLTLAu10
0
50
100
150
200
tomizer. A reason is that the instances are relatively large
Benchmarks passed (out of 202)
and the constraint preprocessor in the backend solver PCSat
is not efficient to handle them.
Fig. 6. Cactus Plot for Temporal VerifiTime in seconds (600 seconds time limit)

2

1

0

−1

−2

7

cation.

RELATED WORK

Our 𝜇CLP is a first-order fixpoint logic with backgroundtheories. As remarked before, 𝜇CLP can be seen as constraint logic programming (CLP) but extended
with arbitrarily nested (co-)inductive predicate definitions and quantifiers. CLP has been extensively
studied (see, e.g., Jaffar and Maher [1994]). It is well known that the validity problem of CLP and thesatisfiability problem of CHCs are inter-reducible. When the background theory is that of integer
arithmetic, by the results of Tsukada [2020], CHCs is Π 01 -complete (in the analytical hierarchy) but
𝜇CLP ∉ Π 01 , which imply that 𝜇CLP is strictly more expressive than CLP or CHCs and so there is
no sound and complete reduction from 𝜇CLP to CHCs. Unno et al. [2021] introduced pfwCSP as anextension of CHCs. The sound and complete reduction from 𝜇CLP to pfwCSP in this paper showsthat pfwCSP is at least as expressive as 𝜇CLP and therefore strictly more expressive than CHCs. In
12 Valid instances sas2010_mod_3 (the running example program from Section 2) and 05-toylinarith2.c are re-spectively solved by exchanging 7⇌

16 and 60⇌

68 bounds (primal⇌dual). Invalid instances

coolant_basis_4_1_unsafe_sftyliveness and coolant_basis_4_2_unsafe_sftyliveness are solved by 0 ⇌ 12 and0 ⇌ 13 bounds.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:26Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

fact, it can be shown that 𝜇CLP is in Δ12 while pfwCSP is Σ12 -complete. It is an open problem whether
there is a class of predicate constraint satisfaction problems that is computationally equivalent to
𝜇CLP. 𝜇CLP is also related to the Horn 𝜇-calculus of Charatonik et al. [1998] which is an extensionof ordinary (i.e., not constraint) logic programming by arbitrarily nested (co-)inductive predicate
definitions. That is, 𝜇CLP can be seen as an extension of the Horn 𝜇-calculus with constraints andquantifiers.
Unno et al. [2021] introduced pfwCSP for the purpose of verifying relational properties of
infinite state programs. They also presented the PCSat semi-algorithm for soundly-and-relativelycompletely solving pfwCSP that we also use within our MuVal (but with modifications for ournovel primal-dual solving method). Their approach directly uses pfwCSP to encode the verification
problems and is different from our approach that uses 𝜇CLP to encode verification problems andtranslate them to pfwCSP via our novel reduction. An advantage of our approach is that going
through 𝜇CLP allows modular encoding of verification problems in which program components
are expressed by separate (co-)inductive predicates whose modularity is preserved by our reduction.
Another important advantage of our approach is that, thanks to the fact that a 𝜇CLP instance can becomplemented by the standard De Morgan complement, it enables the novel primal-dual constraint
solving method that solves the pfwCSPs reduced from the given 𝜇CLP and its dual in parallel while
exchanging bounds to reduce each others’ solution spaces. By contrast, the approach of Unno et al.
[2021] is neither modular nor primal-dual. However, by using pfwCSP directly, Unno et al. [2021]
is able to verify difficult relational properties including 𝑘-safety properties requiring semanticschedulers and hyperliveness properties such as co-termination and generalized non-interference.
We leave for future work to investigate whether the ideas of this paper can be adopted to verificationof such relational properties.
There has been much work on temporal property verification of infinite state programs. These
include approaches for termination [Ben-Amram and Genaim 2014; Cook et al. 2006; Fedyukovich
et al. 2018; Giesl et al. 2017; Heizmann et al. 2014; Urban 2013; Urban et al. 2016; Urban and Miné2014], non-termination [Chen et al. 2014; Cook et al. 2014; Gupta et al. 2008], LTL [Cook andKoskinen 2011; Dietsch et al. 2015], ∀CTL [Cook et al. 2011], CTL [Beyene et al. 2013; Cook andKoskinen 2013; Urban et al. 2018], fair CTL [Cook et al. 2015a; Tellez and Brotherston 2020], andCTL∗ [Cook et al. 2015b, 2017]. However, few support the full class of modal 𝜇 calculus properties.
A notable exception is Kobayashi et al. [2019] that presents a method called Mu2CHC. Mu2CHC
modularly encodes modal 𝜇 model checking of infinite state programs to the problem of deciding
the validity of Mu-Arithmetic [Bradfield 1999; Lubarsky 1993] which is a first-order fixpoint logic
with the integer arithmetic as the background theory. We also use the same encoding to verify
modal 𝜇 calculus properties. However, Mu2CHC works by soundly-but-incompletely reducing thevalidity checking problem to (ordinary) CHCs which are then solved by an off-the-shelf CHCs
solver. By contrast, our MuVal soundly and completely reduces the problem to the extended class of
pfwCSP. As a consequence of the incomplete reduction, Mu2CHC cannot conclude anything when
the given set of constraints is found unsatisfiable, whereas our complete reduction allows MuVal toconclude invalidity (resp. validity) of the given 𝜇CLP instance when the primal (resp. dual) pfwCSP
is found unsatisfiable. Additionally, while Mu2CHC also solves the primal and the dual problems inparallel, it simply runs the two processes in an embarrassingly parallel manner without exchanging
information. By contrast, our novel modular primal-dual method allows the parallel constraint
solving processes to mutually improve each other by synthesizing and exchanging sound bounds
to reduce each others’ solution spaces.
The duality of verification and refutation has been observed and exploited in many prior works.
For example, IC3/PDR [Bradley 2011] is a method for safety property verification in which thesearch for an inductive invariant (called frames in that approach) is guided by the search forProc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:27

states that reach an error state. Recent works further investigate related forms of duality in safety
verification such as that casted as a backtracking interpreter for CLP [McMillan 2014] and thatbetween state space exploration and bounded-width induction [Padon et al. 2022]. Perhaps morecommonly, the duality is also implicit in the classic CEGAR (counterexample-guided abstraction
refinement) [Ball and Rajamani 2002; Clarke et al. 2000; Henzinger et al. 2004] and CEGIS based
approaches in which the search for a counterexample and that for a proof mutually guide each other.
In that sense, the CEGIS-based solver PCSat [Unno et al. 2021] that MuVal uses as a sub-process
can also been considered as a primal-dual approach, and therefore, MuVal can be considered topossess two levels of duality: the inner one inside of PCSat and the outer one in which the two
primal and dual PCSat processes execute in parallel while exchanging learned upper-bounds. A key
difference of our MuVal’s (outer) duality from those in prior approaches is that it is formulated as
the standard De Morgan duality of a first-order fixpoint logic. Thanks to the generality of the logic
and De Morgan duality, our approach extends the benefit of duality to many classes of verification
problems, including those beyond safety.
Another difference from many of the prior primal-dual approaches is that ours can exploit
modularity by modularly encoding verification problems in the first-order fixpoint logic. That is, as
we have shown, the logic allows can encode verification problems in which individual programand property components are expressed as different (but possibly nested) (co-)inductive predicates,
all of which will be subject to the under- and over-approximation of our primal-dual method. In
this respect, the primal-dual approaches of Godefroid et al. [2010] and Le et al. [2015] are also
modular, however, are specialized to (non-)safety verification and (non-)termination verification,
respectively13 . By contrast, our MuVal supports a wide range of temporal properties which is due
in no small part to the generality of the first-order fixpoint logic 𝜇CLP that underlies our approach.
8

CONCLUSION

We have presented a novel modular primal-dual approach to automatically checking validity ofa formula in a first-order logic with background theories and arbitrarily nested inductive andco-inductive predicate definitions. Our approach utilizes a novel reduction to the satisfiability of a
recently proposed class pfwCSP of predicate constraint satisfaction problems, and further extends
the existing constraint solving method by solving both the primal and the dual pfwCSP satisfaction
problems that are obtained from the given and its dual validity problems. Our method solves the two
problems in parallel while exchanging sound bounds synthesized from partial solutions to reduceeach others’ solution spaces. We have implemented the approach in the tool MuVal and obtained
promising experimental results on diverse benchmark sets of temporal verification problems.
ACKNOWLEDGMENTS
We thank anonymous reviewers for useful comments. This work was supported by JSPS KAKENHI
Grant Numbers JP20H04162, JP20K20625, JP22H03564, JP20H05703, and JP22H03570. Koskinen waspartially supported by Office of Naval Research under Grant Nos. N00014-17-1-2787 and N0001422-1-2643 and by NSF under Grant No. CCF-1618059.
REFERENCES
Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček. 2012. LTL to Büchi Automata Translation: Fast and More
Deterministic. In TACAS ’12. Springer, 95–109.
Thomas Ball and Sriram K. Rajamani. 2002. The SLAM project: debugging system software via static analysis. In POPL ’02(Portland, Oregon). ACM, 1–3.
13 Also, unlike our work, Godefroid et al. [2010] makes no use of modern liveness verification techniques like (non-finitary)well-founded relations.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:28Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

Amir M. Ben-Amram and Samir Genaim. 2014. Ranking Functions for Linear-Constraint Loops. J. ACM 61, 4, Article 26(July 2014), 55 pages.
Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses. In
CAV ’13 (LNCS, Vol. 8044). Springer, 869–882.
Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program
Verification. In Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday(LNCS, Vol. 9300). Springer, 24–51.
Julian C. Bradfield. 1999. Fixpoint Alternation and the Game Quantifier. In CSL ’99 (LNCS, Vol. 1683). Springer, 350–361.
Aaron R. Bradley. 2011. SAT-based Model Checking Without Unrolling. In VMCAI ’11 (Austin, TX, USA) (LNCS, Vol. 6538).
Springer, 70–87.
Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman. 2016. T2: Temporal Property Verification.
In TACAS ’16. Springer, 387–393.
Adrien Champion, Tomoya Chiba, Naoki Kobayashi, and Ryosuke Sato. 2018. ICE-Based Refinement Type Discovery forHigher-Order Functional Programs. In TACAS ’18 (LNCS, Vol. 10805). Springer, 365–384.
Witold Charatonik, David A. McAllester, Damian Niwinski, Andreas Podelski, and Igor Walukiewicz. 1998. The Horn
Mu-calculus. In LICS ’98. IEEE Computer Society, 58–69.
Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O’Hearn. 2014. Proving Nontermination via
Safety. In TACAS ’14 (LNCS, Vol. 8413). Springer, 156–171.
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-Guided Abstraction
Refinement. In CAV ’00 (LNCS, Vol. 1855). Springer, 154–169.
Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O’Hearn. 2014. Disproving termination with overapproximation.
In FMCAD ’14. IEEE, 67–74.
Byron Cook, Heidy Khlaaf, and Nir Piterman. 2015a. Fairness for Infinite-State Systems. In TACAS ’15. Springer, 384–398.
Byron Cook, Heidy Khlaaf, and Nir Piterman. 2015b. On Automation of CTL* Verification for Infinite-State Systems. In CAV’15. Springer, 13–29.
Byron Cook, Heidy Khlaaf, and Nir Piterman. 2017. Verifying Increasingly Expressive Temporal Logics for Infinite-State
Systems. J. ACM 64, 2, Article 15 (April 2017), 39 pages.
Byron Cook and Eric Koskinen. 2011. Making Prophecies with Decision Predicates. In POPL ’11 (Austin, Texas, USA). ACM,
399–410.
Byron Cook and Eric Koskinen. 2013. Reasoning About Nondeterminism in Programs. In PLDI ’13 (Seattle, Washington,USA). ACM, 219–230.
Byron Cook, Eric Koskinen, and Moshe Vardi. 2011. Temporal Property Verification As a Program Analysis Task. In CAV ’11(Snowbird, UT). Springer, 333–348.
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination proofs for systems code. In PLDI ’06. ACM,
415–426.
Giorgio Delzanno and Andreas Podelski. 2001. Constraint-based Deductive Model Checking. International Journal on
Software Tools for Technology Transfer 3, 3 (2001), 250–270.
Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, and Andreas Podelski. 2015. Fairness Modulo Theory: A New
Approach to LTL Software Model Checking. In CAV ’15. Springer, 49–66.
Stephan Falke, Deepak Kapur, and Carsten Sinz. 2011. Termination Analysis of C Programs Using Compiler Intermediate
Languages. In RTA ’11, Vol. 10. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 41–50.
Grigory Fedyukovich, Yueling Zhang, and Aarti Gupta. 2018. Syntax-Guided Termination Analysis. In CAV ’18 (LNCS,
Vol. 10981). Springer, 124–143.
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, and Valerio Senni. 2013. Generalization strategies for the verificationof infinite state systems. Theory and Practice of Logic Programming 13, 2 (2013), 175–199.
Laurent Fribourg. 1999. Constraint Logic Programming Applied to Model Checking. In LOPSTR ’99. Springer, 30–41.
Juergen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel,
Carsten Otto, Martin Pluecker, Peter Schneider-Kamp, Thomas Stroeder, Stephanie Swiderski, and Rene Thiemann. 2017.
Analyzing Program Termination and Complexity Automatically with AProVE. Journal of Automated Reasoning 58 (2017),
3–31.
Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and SaiDeep Tetali. 2010. Compositional may-must program analysis:
unleashing the power of alternation. In POPL ’10, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 43–56.
Erich Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, Moshe Y. Vardi, Y. Venema, and Scott Weinstein. 2005. Finite
Model Theory and Its Applications (Texts in Theoretical Computer Science. An EATCS Series). Springer.
Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. 2012. Synthesizing Software Verifiers
from Proof Rules. In PLDI ’12 (Beijing, China). ACM, 405–416.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:29

Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, and Ru-Gang Xu. 2008. Proving nontermination. In POPL ’08 (San Francisco, California, USA). ACM, 147–158.
Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework.
In CAV ’15. Springer, 343–361.
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination Analysis by Learning Terminating Programs.
In CAV ’14. Springer, 797–813.
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. 2004. Abstractions from proofs. In POPL
’04 (Venice, Italy). ACM, 232–244.
Hossein Hojjat and Philipp Rümmer. 2018. The Eldarica Horn Solver. In FMCAD ’18. IEEE, 1–7.
Joxan Jaffar and Michael J. Maher. 1994. Constraint logic programming: a survey. The Journal of Logic Programming 19(1994), 503 – 581.
Ranjit Jhala and Kenneth L. McMillan. 2006. A Practical and Complete Approach to Predicate Refinement. In TACAS ’06(LNCS, Vol. 3920). Springer, 459–473.
Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez, and Martin Schäf. 2016. JayHorn: A Framework for Verifying Java
programs. In CAV ’16, Vol. 9779. Springer, 352–358.
Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno. 2019. Temporal Verification of Programs via
First-Order Fixpoint Logic. In SAS ’19. Springer, 413–436.
Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. 2018. Higher-Order Program Verification via HFL Model Checking.
In ESOP ’18. Springer, 711–738.
Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014. SMT-Based Model Checking for Recursive Programs. In CAV’14 (LNCS, Vol. 8559). Springer, 17–34.
Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2016. SMT-Based Model Checking for Recursive Programs. Formal
Methods in System Design 48, 3 (June 2016), 175–205.
Stephan Kreutzer. 2004. Expressive equivalence of least and inflationary fixed-point logic. Annals of Pure and Applied Logic
130, 1 (2004), 61–78.
Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi. 2014. Automatic Termination Verification forHigher-Order Functional Programs. In ESOP ’14 (LNCS, Vol. 8410). Springer, 392–411.
Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin. 2015. Termination and Non-termination Specification Inference. In
PLDI ’15 (Portland, OR, USA). ACM, 489–498.
Leonid Libkin. 2004. Elements Of Finite Model Theory (Texts in Theoretical Computer Science. An Eatcs Series). Springer.
Robert S. Lubarsky. 1993. 𝜇-Definable Sets of Integers. Journal of Symbolic Logic 58, 1 (1993), 291–313.
Kenneth L. McMillan. 2014. Lazy Annotation Revisited. In CAV ’14 (Lecture Notes in Computer Science, Vol. 8559), Armin
Biere and Roderick Bloem (Eds.). Springer, 243–259.
Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi. 2018. A Fixpoint Logic and Dependent Effects for Temporal
Property Verification. In LICS ’18. ACM, 759–768.
Ulf Nilsson and Johan Lübcke. 2000. Constraint Logic Programming for Local and Symbolic Model-Checking. In CL ’00.
Springer, 384–398.
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken. 2022. Induction duality: primal-dual
search for invariants. 6, POPL (2022), 1–29.
Yuki Satake, Hiroshi Unno, and Hinata Yanagi. 2020. Probabilistic Inference for Predicate Constraint Satisfaction. AAAI ’20
34, 02 (Apr. 2020), 1644–1651.
Gadi Tellez and James Brotherston. 2020. Automatically Verifying Temporal Properties of Pointer Programs with Cyclic
Proof. Journal of Automated Reasoning 64, 3 (2020), 555–578.
Tachio Terauchi and Hiroshi Unno. 2015. Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement.
In ESOP ’15 (LNCS, Vol. 9032). Springer, 610–633.
Takeshi Tsukada. 2020. On Computability of Logical Approaches to Branching-Time Property Verification of Programs. In
LICS ’20 (Saarbrücken, Germany). ACM, 886–899.
Hiroshi Unno and Naoki Kobayashi. 2009. Dependent Type Inference with Interpolants. In PPDP ’09. ACM, 277–288.
Hiroshi Unno, Yuki Satake, and Tachio Terauchi. 2017a. Relatively Complete Refinement Type System for Verification ofHigher-order Non-deterministic Programs. Proceedings of the ACM on Programming Languages 2, POPL, Article 12 (Dec.
2017), 29 pages.
Hiroshi Unno, Yuki Satake, Tachio Terauchi, and Eric Koskinen. 2020. Program Verification via Predicate Constraint
Satisfiability Modulo Theories. CoRR abs/2007.03656 (2020). arXiv:2007.03656 https://arxiv.org/abs/2007.03656
Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021. Constraint-Based Relational Verification. In CAV ’21. Springer,
742–766.
Hiroshi Unno, Sho Torii, and Hiroki Sakamoto. 2017b. Automating Induction for Solving Horn Clauses. In CAV ’17. Springer,
571–591.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:30Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

Caterina Urban. 2013. The Abstract Domain of Segmented Ranking Functions. In SAS ’13 (LNCS, Vol. 7935). Springer, 43–62.
Caterina Urban, Arie Gurfinkel, and Temesghen Kahsai. 2016. Synthesizing Ranking Functions from Bits and Pieces. In
TACAS ’16. Springer, 54–70.
Caterina Urban and Antoine Miné. 2014. An Abstract Domain to Infer Ordinal-Valued Ranking Functions. In ESOP ’14.
Springer, 412–431.
Caterina Urban, Samuel Ueltschi, and Peter Müller. 2018. Abstract Interpretation of CTL Properties. In SAS ’18 (LNCS,
Vol. 11002). Springer, 402–422.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

A

72:31

SOLUTIONS TO THE WELL-FOUNDED PREDICATE VARIABLES IN THE EXAMPLE
OF SECTION 2.2

The solution for 𝐼 ⇓ (𝑥 1, 𝑥 2, 𝑥 1′ , 𝑥 2′ ) is as follows:
WF_I_(x1: int, x2: int, x1': int, x2': int) :=(f(x1,x2) >= 0 /\ f(x1,x2) > f(x1',x2') \/g(x1,x2) >= 0 /\ g(x1,x2) > g(x1',x2') /\(f(x1,x2) < 0 /\ f(x1',x2') < 0 \/ f(x1,x2) >= f(x1',x2'))) /\(D(x1',x2') => (f(x1,x2) >= 0 /\ f(x1,x2) > f(x1',x2') \/g(x1,x2) >= 0 /\ g(x1,x2) > h(x1',x2') /\(f(x1,x2) < 0 /\ f(x1',x2') < 0 \/ f(x1,x2) >= f(x1',x2')))) \/D(x1,x2) /\(f(x1,x2) >= 0 /\ f(x1,x2) > f(x1',x2') \/h(x1,x2) >= 0 /\ h(x1,x2) > g(x1',x2') /\(f(x1,x2) < 0 /\ f(x1',x2') < 0 \/ f(x1,x2) >= f(x1',x2'))) /\(D(x1',x2') => (f(x1,x2) >= 0 /\ f(x1,x2) > f(x1',x2') \/h(x1,x2) >= 0 /\ h(x1,x2) > h(x1',x2') /\ (f(x1,x2) < 0 /\f(x1',x2') < 0 \/ f(x1,x2) >= f(x1',x2'))))
wheref(x1,x2) = 2 * x1 + x2
g(x1,x2) = x1
h(x1,x2) = 2 * x1
D(x1,x2) = x1 >= 0 /\ 1 >= x1 /\ x2 < 0

The solution for 𝐽⇓ (𝑥 2, 𝑥 2′ ) is as follows:
WF_J_(x2: int, x2': int) :=f(x2) >= 0 /\ f(x2) > f(x2') /\(f(x2) >= 0 /\ f(x2) > g(x2') \/ g(x2) > h(x2') /\ f(x2) >= g(x2')) \/(g(x2) > f(x2') \/ h(x2) >= 0 /\ h(x2) > g(x2') /\ g(x2) >= f(x2')) /\h(x2) >= 0 /\ h(x2) > h(x2')
wheref(x) = 5 - x
g(x) = 0h(x) = -x

B

FRAGMENTS OF 𝝁CLP REDUCIBLE TO CHCS

This section discusses two fragments of 𝜇CLP whose validity is reducible to the satisfiability ofCHCs.
We first note that the validity of 𝜇CLP
(𝜙 0, ((𝑋 1 (e𝑥 1 ) =𝛼 1 𝜙 1 ); · · · ; (𝑋𝑚 (e𝑥𝑚 ) =𝛼𝑚 𝜙𝑚 )))has an equivalent CLP validity if all the following conditions are met: (1) 𝛼𝑖 = 𝜈 for all 𝑖 = 1, . . . , 𝑚,
(2) 𝑋 1, . . . , 𝑋𝑚 occur only positively in 𝜙 0 , and (3) universal (resp. existential) quantifiers occur only
positively (resp. negatively) in 𝜙𝑖 ’s. We henceforth call this fragment of 𝜇CLP, validity-reducible.
Similarly, the invalidity of 𝜇CLP has an equivalent CLP validity if: (1) 𝛼𝑖 = 𝜇 for all 𝑖 = 1, . . . , 𝑚, (2)𝑋 1, . . . , 𝑋𝑚 occur only positively in 𝜙 0 , (3a) 𝜙𝑖 ’s only free variables are 𝑥e𝑖 , and (3b) universal (resp.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:32Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen

existential) quantifiers occur only negatively (resp. positively) in 𝜙𝑖 ’s. We call this 𝜇CLP fragment,
invalidity-reducible.
We can then show that our reduction red(𝜙, P) satisfies the following property for the fragments.
Proposition 1. Let (𝜙, P) be a 𝜇CLP. If (𝜙, P) is validity-reducible, red(𝜙, P) always generates
co-CHCs. Similarly, if (𝜙, P) is invalidity-reducible, red(𝜙, ¬(P)) always generates co-CHCs.
Note also that the satisfiability of the co-CHCs C can be further reduced to that of the CHCs𝑡 ) with ¬𝑋 ¬ (e𝑡 ) and ¬𝑋 (e𝑡 ) with 𝑋 ¬ (e𝑡)C ¬ , obtained from C by replacing each literal of the form 𝑋 (e¬for 𝑋 ∈ fpv(C), where 𝑋 is a fresh predicate variable that represents the negation of 𝑋 . Thus
we can use off-the-shelf CHCs-solvers to discharge the validity-reducible and invalidity-reducible
fragments of 𝜇CLP.
C

OPTIMIZED red(𝜙, P)

Our 𝜇CLP validity checker MuVal optimizes red(𝜙, P) so that unnecessary arguments are suppressed. For example, from the 𝜇CLP (𝜙, P) where 𝜙 ≜ ∀𝑥 .𝑋 (𝑥) and P ≜ (𝑋 (𝑥) =𝜇 𝑌 (𝑥 −1)); (𝑌 (𝑦) =𝜇 𝑍 (𝑦 − 1)); (𝑍 (𝑧) =𝜇 𝑧 ≤ 0 ∨ 𝑋 (𝑧 − 1)), red(𝜙, P) generates the pfwCSP (C, K)
where


𝑋 (𝑥), 𝑋 (𝑥) ⇒ 𝑌 (⊤, 𝑥, 𝑥 − 1),








 𝑌 (𝑏 1, 𝑥, 𝑦) ⇒ 𝑍 (𝑏 1, 𝑥, ⊤, 𝑦, 𝑦 − 1),

C≜



 𝑍 (𝑏 1, 𝑥, 𝑏 2, 𝑦, 𝑧) ⇒ 𝑧 ≤ 0 ∨ 𝑋 (𝑧 − 1), 𝑍 (𝑏 1, 𝑥, 𝑏 2, 𝑦, 𝑧) ∧ 𝑏 1 ⇒ 𝑧 ≤ 0 ∨ 𝑋 ⇓ (𝑥, 𝑧 − 1)) K ≜ 𝑋 ↦→ •, 𝑌 ↦→ •, 𝑍 ↦→ •, 𝑋 ⇓ ↦→ ⇓By contrast, MuVal gets a simpler but equi-satisfiable pfwCSP (C ′, K) where
𝑋 (𝑥), 𝑋 (𝑥) ⇒ 𝑌 (𝑥, 𝑥 − 1), 𝑌 (𝑥, 𝑦) ⇒ 𝑍 (𝑥, 𝑦 − 1),C′ ≜𝑍 (𝑥, 𝑧) ⇒ 𝑧 ≤ 0 ∨ 𝑋 (𝑧 − 1), 𝑍 (𝑥, 𝑧) ⇒ 𝑧 ≤ 0 ∨ 𝑋 ⇓ (𝑥, 𝑧 − 1))Note that the query 𝜙 calls 𝑋 , 𝑋 calls 𝑌 , 𝑌 calls 𝑍 , and 𝑍 recursively calls 𝑋 . Thus, if we startfrom the query, 𝑍 is always passed the actual argument of the previous call to 𝑋 and, therefore, 𝑏 1
is always ⊤ and so unneeded. Moreover, 𝑏 2 and 𝑦 for 𝑍 are unneeded because 𝑍 does not call 𝑌
without going through 𝑋 that is defined prior to 𝑌 .
D

PROOF OF THEOREM 5.2

Theorem 5.2 follows from the soundness and the completeness lemmas for each steps of red(𝜙, P):
The following lemma for elim ∃ (𝜙, P, ∅), the first-step follows immediately from the well-known
soundness and completeness of Skolemization for first-order logic.
Lemma D.1. Suppose that elim ∃ (𝜙, P, ∅) = (𝜙 𝜇 , P𝜇 , K𝜇 ). Then, K𝜇 (𝑋 ) = 𝜆 holds for all 𝑋 ∈dom(K𝜇 ). We have |= (𝜙, P) if and only if there is an interpretation 𝜌 for dom(K𝜇 ) such that𝜌 |= FN (𝑋 ) for all 𝑋 ∈ dom(𝜌) and 𝜌 |= elim ∃ (𝜙 𝜇 , P𝜇 ).
The following lemma for elim𝜈 (𝜙, P), the third-step follows from the maximality of the greatest
fixpoints (i.e., co-induction principle) (see e.g., Corollary 1 in [Unno et al. 2017b] for a formal related
discussion of least fixpoints that occur in negative positions).
Lemma D.2. Suppose that elim𝜈 (𝜙 𝜈 , P𝜈 , K𝜈 ) = (C, K). For any interpretation 𝜌 for dom(K𝜈 ), thepfwCSP (C, K) has a semantic solution that extends 𝜌 if and only if 𝜌 |= (𝜙, P).
The following lemma follows from the proof of Lemma D.2 and implies Theorem 5.4.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

72:33

Lemma D.3. Suppose that elim𝜈 (𝜙 𝜈 , P𝜈 , K𝜈 ) = (C, K). For any interpretation 𝜌 for dom(K𝜈 ), if the
pfwCSP (C, K) has a semantic solution 𝜌 ′ that extends 𝜌, then for any 𝑋 ∈ dom(P), 𝜌 ′ ⊎ [[P]] (𝜌) |=𝑋 ⇒ 𝑋.
We finally show the soundness and the completeness of elim𝜇 (𝜙, P), the second-step.
Lemma D.4. Suppose that elim𝜇 (𝜙 𝜇 , P𝜇 , K𝜇 ) = (𝜙 𝜈 , P𝜈 , K𝜈 ). Then, K𝜈 (𝑋 ) = ⇓ holds for all
𝑋 ∈ dom(K𝜈 ) \ dom(K𝜇 ). For any interpretation 𝜌 for dom(K𝜇 ), 𝜌 |= (𝜙 𝜇 , P𝜇 ) if and only if there
is an interpretation 𝜌 ′ for dom(K𝜈 ) \ dom(K𝜇 ) such that 𝜌 ′ |= WF (𝑋 ) for all 𝑋 ∈ dom(𝜌 ′) and𝜌 ⊎ 𝜌 ′ |= (𝜙 𝜈 , P𝜈 ).
This can be shown as a corollary of the following lemma.
𝑚 ) if and only if there is an interpretation
Lemma D.5. 𝜌 |= (𝜙, P; (𝑋 (e𝑥 ) =𝜇 𝜙 ′); (𝑋𝑖 (e𝑥𝑖 ) =𝜈 𝜙𝑖 )𝑖=1′′
𝑥 ) =𝜈 𝜎𝑋 (𝜙 ′)); (𝑋𝑖 (𝑏𝑖 , 𝑥e, 𝑥e𝑖 ) =𝜈
⇓ such that 𝜌 |= WF (𝑋 ⇓ ) and 𝜌 ⊎ 𝜌 |= (𝜎0 (𝜙), 𝜎0 (P); (𝑋 (e𝑚𝜎𝑖 (𝜙𝑖 ))𝑖=1 ) where𝜌 ′ of 𝑋

𝜎0 ≜ { 𝑋𝑖 ↦→ 𝜆e
𝑦 .𝑋𝑖 (⊥, e𝑣 , 𝑦e) | 𝑖 = 1, . . . , 𝑚 }𝑦 .𝑋 (e𝑦 ) ∧ 𝑋 ⇓ (e𝑥 , 𝑦e) ∪ { 𝑋𝑖 ↦→ 𝜆e
𝑦 .𝑋𝑖 (⊤, 𝑥e, 𝑦e) | 𝑖 = 1, . . . , 𝑚 }𝜎𝑋 ≜ 𝑋 ↦→ 𝜆e

𝑦 .𝑋 (e𝑦 ) ∧ (𝑏𝑖 ⇒ 𝑋 ⇓ (e𝑥 , 𝑦e)) ∪ { 𝑋 𝑗 ↦→ 𝜆e𝑦 .𝑋 𝑗 (𝑏𝑖 , 𝑥e, 𝑦e) | 𝑗 = 1, . . . , 𝑚 } .
𝜎𝑖 ≜ 𝑋 ↦→ 𝜆e
Recall that the semantics of 𝜇CLP defined in Section 3.1 is compositional in the sense thatthe semantics of P2 in P1 ; P2 is defined independently with P1 and is parameterized by aninterpretation 𝜌 for the free predicate variables in P2 . Note also that the guard 𝑋 ⇓ (e𝑥 , 𝑦e) in Lemma D.5
for a call to 𝑋 is enabled only when the Boolean argument 𝑏𝑖 is ⊤ (i.e., only for co-recursive calls
caused (possibly indirectly) by 𝑋 ). Thus, by parameterizing 𝜙 and P away and focusing on the casewhere all 𝑏𝑖 ’s are ⊤ (the other cases are straightforward), the proof of Lemma D.5 boils down toshowing the following lemma.
𝑚 and P ′ ≜ (𝑋 (eLemma D.6. Let P ≜ (𝑋 (e𝑥 ) =𝜇 𝜙); (𝑋𝑖 (e𝑥𝑖 ) =𝜈 𝜙𝑖 )𝑖=1
𝑥 ) =𝜈 𝜎 (𝜙)); (𝑋𝑖 (e𝑥 , 𝑥e𝑖 ) =𝜈𝑚
𝜎 (𝜙𝑖 ))𝑖=1 where
𝑦 .𝑋 (e𝑦 ) ∧ 𝑋 ⇓ (e𝑥 , 𝑦e) ∪ { 𝑋𝑖 ↦→ 𝜆e
𝑦 .𝑋𝑖 (e𝑥 , 𝑦e) | 𝑖 = 1, . . . , 𝑚 } .
𝜎 ≜ 𝑋 ↦→ 𝜆e

We then have(1) JP ′K(𝜌 ⊎ 𝑋 ⇓ ↦→ 𝑅 ) ⊆ JPK(𝜌) for any well-founded relation 𝑅 and(2) JPK(𝜌) ⊆ JP ′K(𝜌 ⊎ 𝑋 ⇓ ↦→ 𝑅 ) for some well-founded relation 𝑅.

Proof:(1) The soundness is shown by well-founded induction with 𝑅. Let 𝐹 and 𝐺 be the defining
function of 𝑋 in P and P ′, respectively. In other words, 𝑋 in P and P ′ are respectively
expressed as 𝜇𝑋 .𝐹 (𝑋 ) and 𝜈𝑋 .𝐺 (𝑋 ). Let 𝐴 be a fixpoint of 𝐺. We then show ∀e𝑥 ∈ 𝐴. 𝑥e ∈𝜇𝑋 .𝐹 (𝑋 ) by well-founded induction with 𝑅. Since 𝐴 = 𝐺 (𝐴), we have 𝐴(e𝑥 ) = 𝐹 ({ 𝑦e ∈ 𝐴 |𝑅(e𝑥 , 𝑦e) }). Therefore, 𝑥e ∈ 𝐴 ⇒ 𝑥e ∈ 𝐹 ({ 𝑦e ∈ 𝐴 | 𝑅(e𝑥 , 𝑦e) }). By the induction hypothesis, wehave { 𝑦e ∈ 𝐴 | 𝑅(e𝑥 , 𝑦e) } ⊆ 𝜇𝑋 .𝐹 (𝑋 ). By the monotonicity of 𝐹 , 𝐹 ({ 𝑦e ∈ 𝐴 | 𝑅(e𝑥 , 𝑦e) }) ⊆𝐹 (𝜇𝑋 .𝐹 (𝑋 )) = 𝜇𝑋 .𝐹 (𝑋 ). We thus get 𝑥e ∈ 𝐴 ⇒ 𝑥e ∈ 𝜇𝑋 .𝐹 (𝑋 ).
(2) For proving the completeness, we construct such 𝑅 as the stage comparison relation studied in
finite model theory (see e.g., [Kreutzer 2004], [Grädel et al. 2005], or [Libkin 2004] for details).
The stage of e𝑣 for 𝑋 in P is defined as the smallest ordinal number 𝛼 such that e𝑣 ∈ 𝐹 𝛼 (⊥) holds
where 𝐹 is the defining function of 𝑋 in P. We then define 𝑅 by { (e𝑥 , 𝑦e) | stage(e𝑥 ) > stage(e𝑦 ) }.
𝛼 (⊥) = 𝐺 𝛼 (⊥) ⊆ 𝐺 𝛼 (⊤). Here,Let 𝐺 be the defining function of 𝑋 in P ′. We
then
get
𝐹

𝐹 𝛼 (⊥) = 𝐺 𝛼 (⊥) under the interpretation 𝜌 ⊎ 𝑋 ⇓ ↦→ 𝑅 is shown by transfinite induction
on 𝛼.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.

72:34Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen■
Received 2022-07-07; accepted 2022-11-07

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 72. Publication date: January 2023.