Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)

Abstract

We present a novel approach to deciding the validity of formulas in first-order fixpoint logic with background theories and arbitrarily nested inductive and co-inductive predicates defining least and greatest fixpoints. Our approach is constraint-based, and reduces the validity checking problem of the given first-order-fixpoint logic formula (formally, an instance in a language called μCLP) to a constraint satisfaction problem for a recently introduced predicate constraint language. Coupled with an existing sound-and-relatively-complete solver for the constraint language, this novel reduction alone already gives a sound and relatively complete method for deciding μCLP validity, but we further improve it to a novel modular primal-dual method. The key observations are (1) μCLP is closed under complement such that each (co-)inductive predicate in the original primal instance has a corresponding (co-)inductive predicate representing its complement in the dual instance obtained by taking the standard De Morgan's dual of the primal instance, and (2) partial solutions for (co-)inductive predicates synthesized during the constraint solving process of the primal side can be used as sound upper-bounds of the corresponding (co-)inductive predicates in the dual side, and vice versa. By solving the primal and dual problems in parallel and exchanging each others' partial solutions as sound bounds, the two processes mutually reduce each others' solution spaces, thus enabling rapid convergence. The approach is also modular in that the bounds are synthesized and exchanged at granularity of individual (co-)inductive predicates. We demonstrate the utility of our novel fixpoint logic solving by encoding a wide variety of temporal verification problems in μCLP, including termination/non-termination, LTL, CTL, and even the full modal μ-calculus model checking of infinite state programs. The encodings exploit the modularity in both the program and the property by expressing each loops and (recursive) functions in the program and sub-formulas of the property as individual (possibly nested) (co-)inductive predicates. Together with our novel modular primal-dual μCLP solving, we obtain a novel approach to efficiently solving a wide range of temporal verification problems.

Original languageEnglish
Pages (from-to)2111-2140
Number of pages30
JournalProceedings of the ACM on Programming Languages
Volume7
DOIs
Publication statusPublished - 2023 Jan 9

Keywords

  • constraint logic programming
  • fixpoint logics
  • temporal verification

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Fingerprint

Dive into the research topics of 'Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification'. Together they form a unique fingerprint.

Cite this