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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Quantifier Elimination and Craig Interpolation: The Quantitative Way

  • Kevin Batz,
  • Joost-Pieter Katoen,
  • Nora Orhan

摘要

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.