Quantifier Elimination and Craig Interpolation, Quantitatively
Kevin Batz, Joost-Pieter Katoen, Nora Orhan
TL;DR
The paper addresses the extension of quantifier elimination and Craig interpolation to the quantitative setting of piecewise linear quantities valued over extended rationals, using supremum and infimum quantifiers $\mathsf{S}$ and $\mathsf{J}$. It develops a three-stage QE algorithm (Guarded Normal Form, Disjunctive Normal Form, and valuation-dependent sup/inf computation) that yields quantifier-free, semantically equivalent representations even for unbounded/infinite values and discontinuities. It then proves a quantitative Craig interpolation theorem, showing that strongest and weakest interpolants between two quantities are quantifier-free and constructible, by projecting out non-common variables via QE. As an application, the paper demonstrates how QE can compute minimal and maximal expected outcomes for loop-free probabilistic programs with unbounded nondeterminism, integrating this with a weakest pre-expectation framework. The results provide a foundational toolset for automatic quantitative program verification and abstraction, with potential for broader use in probabilistic verification and static analysis.
Abstract
Quantifier elimination (QE) and Craig interpolation (CI) are central to various state-of-the-art automated approaches to hardware and software verification. They are rooted in the Boolean setting and are successful for, e.g., first-order theories such as linear rational arithmetic. What about their applicability in the quantitative setting where formulae evaluate to numbers and quantitative supremum/infimum quantifiers are the natural counterparts of Boolean quantifiers? Applications include establishing quantitative properties of programs, such as bounds on expected outcomes of probabilistic programs featuring nondeterminism, and analyzing the flow of information through programs. In this paper, we present, to the best of our knowledge, the first QE algorithm for possibly unbounded, $\infty$- or $-\infty$-valued, or discontinuous piecewise linear quantities. They are the quantitative counterpart to linear rational arithmetic, and they are a popular quantitative assertion language for probabilistic program verification. We provide rigorous soundness proofs as well as upper space complexity bounds. Moreover, we present two applications of our QE algorithm. First, our algorithm yields a quantitative CI theorem: given arbitrary piecewise linear quantities $f$ and $g$ with $f \models g$, both the strongest and the weakest Craig interpolant of $f$ and $g$ are quantifier-free and effectively constructible. Second, we apply our QE algorithm to compute minimal and maximal expected outcomes of loop-free probabilistic programs featuring unbounded nondeterminism.