Quantifier Elimination and Craig Interpolation: The Quantitative Way

Lecture notes in computer science, pp. 176–197

Abstract

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 pendant to traditional Boolean quantifiers? Applications include establishing quantitative properties of programs such as bounds on expected outcomes of probabilistic programs featuring unbounded non-determinism and analyzing the flow of information through programs. In this paper, we present the - to the best of our knowledge - 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 are a popular quantitative assertion language for probabilistic program verification. We provide rigorous soundness proofs as well as upper space complexity bounds. Moreover, our algorithm yields a quantitative CI theorem: Given arbitrary piecewise linear quantities $$f,g$$ with $$f\models g$$ , both the strongest and the weakest Craig interpolant of $$f$$ and $$g$$ are quantifier-free and effectively constructible.

Authors 3

1. Kevin Batz corresponding Aachen

   RWTH Aachen University · University College London

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   University College London, London, UK

2. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

3. Nora Orhan Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany