Quantifier Elimination and Craig Interpolation, Quantitatively

TL;DR

This paper introduces the first quantifier elimination algorithm for quantitative, possibly discontinuous piecewise linear quantities, enabling advanced analysis of probabilistic programs and establishing a quantitative Craig interpolation theorem.

Contribution

It presents a novel QE algorithm for unbounded, discontinuous piecewise linear quantities and demonstrates its applications in probabilistic program verification and quantitative Craig interpolation.

Findings

First QE algorithm for unbounded, discontinuous quantities

Effective construction of strongest and weakest Craig interpolants

Application to compute bounds on probabilistic program outcomes

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.