Dieses Kapitel untersucht die entscheidende Rolle der Eliminierung von Quantifizierern und Craig-Interpolation im Bereich der quantitativen Programmverifikation. Es beginnt mit der Einführung von Quantifizierungs-Eliminierungs-Algorithmen, die Formeln erster Ordnung in quantifiziererfreie Äquivalente verwandeln, und deren Anwendung in automatischen Verifikationstechniken. Das Kapitel vertieft sich dann in Craig-Interpolation, ein wichtiges Werkzeug, um prägnante Erklärungen für Erreichbarkeitsinformationen bei der Programmüberprüfung abzuleiten. Ein wesentlicher Schwerpunkt liegt auf stückweise linearen Größen, die für das Nachdenken über probabilistische Programme unverzichtbar sind. Das Kapitel stellt den ersten quantitativen Eliminierungsalgorithmus für diese Mengen vor, der rigorose Soliditätsnachweise und Komplexitätsanalysen liefert. Darüber hinaus wird ein neuartiges Craig-Interpolationstheorem für stückweise lineare Größen eingeführt, das die Existenz und Konstruierbarkeit quantitativer Craig-Interpolanten demonstriert. Das Kapitel schließt mit potenziellen Anwendungen und zukünftigen Forschungsrichtungen, was es zu einer wertvollen Ressource für diejenigen macht, die daran interessiert sind, den Bereich der quantitativen Programmverifizierung voranzutreiben.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
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.
Hinweise
This research was supported by the ERC AdG project 787914 FRAPPANT.
1 Introduction
Quantifier elimination algorithms take as input a first-order formula \(\varphi \) over some background theory \(\mathcal {T}\) and output a quantifier-free formula \(\textsf{QE}(\varphi )\) equivalent to \(\varphi \) modulo \(\mathcal {T}\). Prime examples include Fourier-Motzkin variable elimination [25, 45] and virtual substitution [40] for linear rational arithmetic, Cooper’s method [18] for linear integer arithmetic, and Cylindrical Algebraic Decomposition [16] for non-linear real arithmetic. Quantifier elimination is extensively leveraged by automatic hard- and software verification techniques for, e.g., computing images of state sets [35, 36], or for synthesizing loop invariants either from templates [17, 27, 31] or by solving abduction problems [22].
Craig interpolation [19] is vital to various automatic hard- and software verification techniques. A first-order theory \(\mathcal {T}\) is called (quantifier-free) interpolating [32], if for all formulae \(\varphi ,\psi \) with \(\varphi \models _\mathcal {T}\psi \), there is an effectively constructible (quantifier-free) formula \(\vartheta \) — called Craig interpolant of \((\varphi ,\psi )\) — with \(\varphi \models _\mathcal {T}\vartheta \models _\mathcal {T}\psi \) and such that all free variables occurring free in \(\vartheta \) also occur free in both\(\varphi \) and \(\psi \). Intuitively, \(\varphi \models _\mathcal {T}\psi \) encodes some (desirable or undesirable) reachability information and \(\vartheta \) is a concise explanation of this fact, abstracting away irrelevant details. The computation of (quantifier-free) Craig interpolants is a vivid area of research [1, 13, 15, 26, 57] with applications ranging from symbolic finite-state model checking [39, 43, 56] over computing transition power abstractions [12] to automatic infinite-state software verification [2, 11, 28, 29, 44, 52, 53].
Anzeige
Quantitative program verification includes reasoning about expected outcomes of probabilistic programs via weakest pre-expectations [30, 37, 38, 42], reasoning about the quantitative flow of information via quantitative strongest post [59], and reasoning about competitive ratios of online algorithms via weighted programming [7]. Quantitative reasoning requires a shift: Predicates, i.e., maps from program states to truth values in \(\{\textsf{true},\textsf{false}\}\), are replaced by quantities1, which map program states to extended reals in \(\mathbb {R}\cup \{-\infty ,\infty \}\).
The classical quantifiers “there exists” \(\exists \) and “for all” \(\forall \) from predicate logic are replaced by quantitative supremum
and infimum
quantifiers [8]. These quantifiers naturally occur when reasoning with quantitative program logics: Very much like classical strongest post-conditions introduce an \(\exists \)-quantifier for assignments [21], quantitative strongest post introduces a
-quantifier (cf. [59, Table 2]). Similarly, whereas classical weakest pre-conditions introduce a \(\forall \)-quantifier for demonically resolving unbounded non-determinism of the form \(x \mathrel {\text {\texttt {:=}}}\mathbb {Q}\) (read: assign to \(x\) an arbitrary rational number) [20, 47], quantitative weakest pre-expectations introduce an
-quantifier [9, 51].
Example 1
In this paper, we focus on piecewise linear quantities such as
where \(x,y_1,\ldots \) are \(\mathbb {Q}\)-valued variables. We can think of \(g\) as a formula that evaluates to extended rationals from \(\mathbb {Q}\cup \{-\infty ,\infty \}\) instead of truth values. By prefixing \(g\) with, e.g., a supremum quantifier, we obtain a new piecewise linear quantity
, which, on variable valuation \(\sigma \), evaluates to the (variable valuation-dependent) supremum of \(g\) under all possible values for \(x\), i.e.,
Our Contribution: Quantitative Quantifier Elimination and Craig Interpolation. Piecewise linear quantities over \(\mathbb {Q}\)-valued variables are to quantitative probabilistic program verification what first-order linear rational arithmetic is to classical program verification: Their entailment problem, i.e.,
is decidable [6, 33], they are effectively closed under, e.g., weakest pre-expectations of loop-free linear probabilistic programs [6], and they have been shown to be sufficiently expressive for the verification of various probabilistic programs [5, 6, 14, 49, 58]. These facts render piecewise linear quantities one of the most prevalent quantitative assertion languages in automatic reasoning.
Anzeige
Reasoning with piecewise linear quantities containing the quantitative
or
quantifiers has, however, received scarce attention, let alone algorithmically. Similarly, the field of quantitative Craig interpolation is rather unexplored, as well. The goal of this paper is to lay the foundations for (i) developing quantitative quantifier elimination- and Craig interpolation-based approaches to automatic quantitative program verification and (ii) for simplifying the reasoning with quantitative assertions involving quantitative quantifiers. Towards this end:
1.
We contribute the — to the best of our knowledge — first quantitative quantifier elimination algorithm for arbitrary, possibly unbounded,\(\infty \)or\(-(\infty )\)-valued, or discontinuous piecewise linear quantities. Put more formally, given an arbitrary piecewise linear quantity \(f\) possibly containing quantitative quantifiers, our algorithm computes a quantifier-free equivalent of\(f\). For
from Example 1, our algorithm yields (after simplification)
We provide rigorous soundness proofs, illustrative examples, and upper space-complexity bounds on our algorithm.
3.
We contribute the — to the best of our knowledge — first Craig interpolation theorem for piecewise linear quantities: Using our quantifier elimination algorithm, we prove that for two arbitrary piecewise linear quantities \(f,f'\) with \(f\models f'\), both the strongest and the weakest \(g\) such that
$$ f\models g\models f'\qquad \text {and}\qquad \text {the free variables in }g\text { are free in } both f\text { and }f'$$
are quantifier-free and effectively constructible.
Example 2
Consider the following piecewise linear quantities:
We have \(f\models f'\). Using our quantifier elimination technique, we effectively construct both the strongest and the weakest2 Craig interpolants of \((f,f')\) given by
Remark 1
When applying classical Craig interpolation for a first-order theory \(\mathcal {T}\) to, e.g., loop invariant generation, “simple” Craig interpolants, i.e., interpolants that lie strictly “between” (w.r.t. \(\models _\mathcal {T}\)) the strongest and the weakest ones, are often very useful [1]. Our quantitative Craig interpolation technique presented in this paper does not aim for obtaining such “simple” interpolants. Rather, our goal is to prove that quantitative Craig interpolants at all exist and that they are effectively constructible. We discuss possible directions for obtaining simpler quantitative Craig interpolants in Section 5.
Related Work. Our quantifier elimination algorithm is based on ideas related to Fourier-Motzkin variable elimination [25, 45]. Most closely related is the work by Zamani, Sanner, and Fang on symbolic dynamic programming [50]. They introduce the symbolic \(\max _x\) operator on piecewise defined functions of type \(\mathbb {R}^n \rightarrow \mathbb {R}\), which also exploits the partitioning property (similar to Theorem 1) and disjunctive normal forms (similar to Theorem 2). We identify the following key differences: the functions considered in [50] must be (i) continuous, (ii) bounded (so that all suprema are actually maxima), and (iii) they must not contain \(\infty \) or \(-\infty \). We do not impose these restrictions since they do not apply to piecewise defined functions obtained from, e.g., applying the program logics mentioned in Section 1. [50], on the other hand, also considers piecewise quadratic functions, whereas we focus on piecewise linear functions. Extending our approach to piecewise quadratic functions is an interesting direction for future work. Finally, we provide a rigorous formalization and soundness proofs alongside upper space complexity bounds. Quantitative quantifier elimination is moreover related to parametric programming [54]. We are, however, not aware of an approach which tackles the computational problem we investigate as it is required from the perspective of a quantitative quantifier elimination problem.
Khatami, Pourmahdian, and Tavana [55] investigate a Craig interpolation property of first-order Gödel logic, where formulae evaluate to real numbers in the unit interval [0, 1]. Apart from the more restrictive semantic codomain, [55] operates in an uninterpreted setting whereas we operate within linear rational arithmetic extended by \(\infty \) and \(-\infty \). Baaz and Veith [4] investigate quantifier elimination of first-order logic over fuzzy algebras over the same semantic codomain. Teige and Fränzle [41] investigate Craig interpolation for stochastic Boolean satisfiability problems, where formulae also evaluate to numbers instead of truth values. Quantified variables are assumed to range over a finite domain.
Outline. In Section 2, we introduce piecewise linear quantities. We present our quantifier elimination algorithm alongside essential theorems and a complexity analysis in Section 3. Our quantitative Craig interpolation results are presented in Section 4. Finally, we discuss potential applications in Section 5.
2 Piecewise Linear Quantities
Throughout this paper, we fix a finite non-empty set \(\textsf{Vars}=\{x,y,z,\ldots \}\) of variables. We denote by \(\mathbb {N}_0\) the set of natural numbers including 0 and let \(\mathbb {N}= \mathbb {N}_0\setminus {0}\). The set of rationals (resp. reals) is denoted by \(\mathbb {Q}\) (resp. \(\mathbb {R}\)) and we denote by \(\mathbb {Q}^{\pm \infty }= \mathbb {Q}\cup \{-\infty ,\infty \}\) (resp. \(\mathbb {R}^{\pm \infty }= \mathbb {R}\cup \{-\infty ,\infty \}\)) the set of extended rationals (resp. reals). A (variable) valuation\(\sigma :\textsf{Vars}\rightarrow \mathbb {Q}\) assigns a rational number to each variable. The set of all valuations is denoted by \(\Sigma \).
Towards defining piecewise linear quantities and their semantics, we briefly recap linear arithmetic and Boolean expressions.
Definition 1
(Linear Arithmetic Expressions). The set \(\textsf{LinAX}\) of linear arithmetic expressions consists of all expressions \(a\) of the form
where \(q_0,\ldots ,q_{\vert \textsf{Vars}\vert } \in \mathbb {Q}\) and \(x_1,\ldots ,x_{\vert \textsf{Vars}\vert } \in \textsf{Vars}\). Moreover, we define the set \(\textsf{LinAX}^{\pm \infty }\) of extended linear arithmetic expressions as
Notice that every arithmetic expression is normalized in the sense that every variable occurs exactly once. We often omit summands \(q_i\cdot x_i\) (resp. \(q_0\)) with \(q_i= 0\) (resp. \(q_0=0\)) for the sake of readability. Given \(a\) as above, we denote by
the set of (necessarily free) variables occurring in \(a\). For \(\tilde{a}= \infty \) or \(\tilde{a}= -\infty \), we define \(\textsf{FV} \left( \tilde{a} \right) = \emptyset \). Given \(\tilde{a}\in \textsf{LinAX}^{\pm \infty }\) and \(x_j\in \textsf{Vars}\), we say that
Finally, given \(\sigma \in \Sigma \), the semantics\( ^{\sigma }\llbracket \tilde{a}\rrbracket \in \mathbb {Q}^{\pm \infty }\) of \(\tilde{a}\) under \(\sigma \) is defined as
(Boolean Expressions).Boolean expressions\(\varphi \) in the set \(\textsf{Bool}\) adhere to the following grammar, where \(\tilde{a}\in \textsf{LinAX}^{\pm \infty }\):
The Boolean constants \(\textsf{true},\textsf{false}\) and the Boolean connectives \(\vee \) and \(\longrightarrow \) are syntactic sugar. We assume that \(\lnot \) binds stronger than \(\wedge \) binds stronger than \(\vee \), and we use parentheses to resolve ambiguities. The set \(\textsf{FV} \left( \varphi \right) \) of (necessarily free) variables in \(\varphi \) is defined as usual. Given a valuation \(\sigma \), we write \(\sigma \models \varphi \) if \(\sigma \) satisfies \(\varphi \) and \(\sigma \not \models \varphi \) otherwise, which is defined in the standard way. Finally, if \(\sigma \not \models \varphi \) for all \(\sigma \in \Sigma \), then we say that \(\varphi \) is unsatisfiable3.
Definition 3
(Piecewise Linear Quantities (adapted from [8, 33])). The set \(\textsf{LinQuant}\) of (piecewise linear) quantities consists of all expressions
where \(k\in \mathbb {N}_0\), \(n\in \mathbb {N}\), and where
1.
and \(x_j\in \textsf{Vars}\) for all \(j\in \{1,\ldots ,k\}\),
2.
\(\varphi _i\in \textsf{Bool}\) and \(\tilde{a}_i\in \textsf{LinAX}^{\pm \infty }\) for all \(i\in \{1,\ldots ,n\}\),
3.
for all \(\sigma \in \Sigma \) and all \(i,j\in \{1,\ldots ,n\}\) with \(i\ne j\), we have4
Here \(\left[ \varphi \right] \) is the Iverson bracket [34] of the Boolean expression \(\varphi \), which evaluates to 1 under valuation \(\sigma \) if \(\sigma \models \varphi \), and to 0 otherwise.
is called the supremum quantifier and
is the infimum quantifier. The quantitative quantifiers take over the role of the classical \(\exists \)- and \(\forall \)-quantifiers from first-order predicate logic. Their semantics is detailed further below. If \(k= 0\), then we call \(f\)quantifier-free. Given \(f\) as above, the set of free variables in \(f\) is
For quantifier-free \(f\), we introduce the shorthand \(\left[ \varphi \right] \cdot f~ = ~\sum _{i=1}^n \left[ \varphi \wedge \varphi _i \right] \cdot \tilde{a}\).
Towards defining the semantics of quantities, we use the following notions: Given a valuation \(\sigma \in \Sigma \), a variable \(x\in \textsf{Vars}\), and \(q\in \mathbb {Q}\), we define the valuation obtained from updating the value of \(x\) under \(\sigma \) to \(q\) as
if \(r>0\), then \(r\cdot \infty = \infty \cdot r= \infty \)
7.
if \(r>0\), then \(r\cdot (-\infty ) = -\infty \cdot r= -\infty \)
8.
if \(r<0\), then \(r\cdot \infty = \infty \cdot r= -\infty \)
9.
if \(r<0\), then \(r\cdot (-\infty ) = -\infty \cdot r= \infty \)
The terms \(\infty +(-\infty )\) and \(-\infty +\infty \) are undefined. The condition from Definition 3.3 ensures that we never encounter such undefined terms, which yields the semantics of piecewise linear quantities to be well-defined:
Definition 4
(Semantics of Piecewise Linear Quantities). Let \(f\in \textsf{LinQuant}\) and \(\sigma \in \Sigma \). The semantics5\( ^{\sigma }\llbracket f\rrbracket \in \mathbb {R}^{\pm \infty }\) of \(f\) under \(\sigma \) is defined inductively:
In words: if \(f\) is quantifier-free, then \( ^{\sigma }\llbracket f\rrbracket \) evaluates to the sum of all extended arithmetic expressions \(\tilde{a}_j\) for which \(\sigma \models \varphi _j\). The semantics of
and
makes it evident that the quantitative quantifiers generalize the classical quantifiers: Whereas \(\exists \) maximizes — so to speak — a truth value, the
-quantifier maximizes a quantity by evaluating to the supremum obtained from evaluating \(f\) under all possible values for \(x\).
behaves analogously by evaluating to an infimum.
Finally, we say that two piecewise linear quantities \(f,f'\in \textsf{LinQuant}\) are (semantically) equivalent, denoted by \(f\equiv f'\), if \( ^{\sigma }\llbracket f\rrbracket = ^{\sigma }\llbracket f'\rrbracket \) for all \(\sigma \in \Sigma \).
3 Quantitative Quantifier Elimination
In this section, we detail our quantifier elimination procedure alongside illustrative examples. Given an arbitrary piecewise linear quantity
As with quantifier elimination for (theories of) classical first-order predicate logic, it suffices being able to eliminate piecewise linear quantities containing a single quantifier, which then enables to process quantities containing an arbitrary number of quantifiers in an inner- to outermost fashion, i.e.,
where
. We proceed by means of a 3-level divide-and-conquer approach. We describe each of the involved stages in Sections 3.1-3.3. In Section 3.4, we summarize our approach by providing an algorithm.
3.1 Stage 1: Exploiting the Guarded Normal Form
Our first step is to transform the input \(f\) into a normal form (an extension of [33, Section 5.1]), which enables us to subdivide the quantifier elimination problem into simpler sub-problems. Intuitively, this normal form enforces a more explicit representation of the \(\mathbb {R}^{\pm \infty }\)-valued function a piecewise linear quantity represents.
Definition 5
(Guarded Normal Form). Let \(g\in \textsf{LinQuant}\) be given by
and fix some variable \(x\in \textsf{Vars}\). We say that \(g\) is in guarded normal form w.r.t.\(x\), denoted by \(g\in \textsf{GNF}_x\), if all of the following conditions hold:
1.
the \(\varphi _i\) partition the set \(\Sigma \) of valuations, i.e., for all \(\sigma \in \Sigma \) there exists exactly one \(i\in \{1,\ldots ,n\}\) such that \(\sigma \models \varphi _i\),
2.
the \(\varphi _i\) are in disjunctive normal form (DNF), i.e.,
$$ \forall i \in \{1,\ldots ,n\}:\quad \varphi _i~\text {is of the from}~\bigvee \limits _{j}\bigwedge \limits _{j'}L_{j,j'}~, $$
where each \(L_{j,j'} \in \textsf{LinAX}^{\pm \infty }\) is a (strict or non-strict) linear inequality,
3.
for each linear inequality \(L\) in \(g\), it holds that if \(x\in \textsf{FV} \left( L \right) \), then
$$ L\quad = \quad x\sim \tilde{b}$$
for some \(\tilde{b}\in \textsf{LinAX}^{\pm \infty }\) with \(x\not \in \textsf{FV} \left( \tilde{b} \right) \) and \(\sim \in \{>,\ge ,<,\le \}\). \(\triangle \)
If Condition 5.1 holds, then we say that \(g\) is partitioning. Speaking of a normal form is justified by the fact that every piecewise linear quantity \(g\in \textsf{LinQuant}\) can effectively be transformed into a semantically equivalent \(g' \in \textsf{LinQuant}\) in guarded normal form with respect to variable \(x\in \textsf{Vars}\), i.e., such that \(g' \in \textsf{GNF}_x\) and \(g\equiv g'\). To see this, let \(g\) be given as above. Towards obtaining \(g'\), we first establish the partitioning property by enumerating the possible assignments of truth values to the \(\varphi _i\). Put more formally, we construct
where we let \(\epsilon + \tilde{e}= \tilde{e}= \tilde{e}+ \epsilon \) for all \(\tilde{e}\in \textsf{LinAX}^{\pm \infty }\) and obey the rules for treating \(\infty \) and \(-\infty \), respectively, as given in Section 2. We then obtain \(g'\) by transforming the so-obtained Boolean expressions into DNF and isolating \(x\) in every inequality where \(x\) occurs. Notice that if \(g\) satisfies the conditions from Definition 3, then so does \(g'\). In particular, when constructing sums of the form \(\sum _{i=1}^n \tilde{e}_i\), we never encounter expressions of the form \(\infty + (-\infty )\) or \(-\infty + \infty \).
Example 3
Recall the piecewise linear quantity from Example 1 given by
which is not in \(\textsf{GNF}_x\). Applying the construction from above yields
which is in \(\textsf{GNF}_x\) and will serve us as a running example. \(\triangle \)
Now assume w.l.o.g. that the input quantity \(f\) is in \(\textsf{GNF}_x\). Each of the Conditions 5.1-3 is essential to our approach. We will now exploit that \(f\) is partitioning. Given \(\varphi \in \textsf{Bool}\) and \(\tilde{a}\in \textsf{LinAX}^{\pm \infty }\), we define the shorthands
Notice that these quantities are always partitioning. Now consider the following:
Theorem 1
Let \(x\in \textsf{Vars}\) and let \(\sum \limits _{i=1}^{n}\left[ \varphi _i \right] \cdot \tilde{a}_i\in \textsf{GNF}_x\). We have for all \(\sigma \in \Sigma \):
1.
2.
Proof
This is a consequence of the fact that the quantity is partitioning and that \(-\infty \) (resp. \(\infty \)) are neutral wr.t. \(\max \) (resp. \(\min \)). See [10, App. A.1] for details. \(\square \)
We may thus consider each summand of the input quantity \(f\) separately. Assuming we can compute
and
, we obtain the sought-after quantifier-free equivalent of \(f\) by effectively constructing valuation-wise minima and maxima of finite sets of partitioning quantities as follows:
Lemma 1
Let \(M=\{h_1,\ldots ,h_n\} \subseteq \textsf{LinQuant}\) for some \(n\ge 1\), where each
\(\textsf{MAX}(M)\) iterates over all combinations of summands, which determine the value each of the \(h_i\) evaluate to (first summand). For each of these combinations, we check, for each \(i\in \{1,\ldots ,n\},\) whether \(h_i\) evaluates to the sought-after maximum (second summand). \(\textsf{MAX}(M)\) is partitioning since the \(h_i\) are and due to the fact that \(\textsf{MAX}(M)\) selects the maximizing quantity with the smallest index. The construction of \(\textsf{MIN}(M)\) is analogous and provided in [10, App. B.1]. \(\square \)
Continuing Example 3, we have for every \(\sigma \in \Sigma \),
3.2 Stage 2: Exploiting the Disjunctive Normal Form
In this stage, we aim to eliminate the quantifiers from the simpler quantities
Recall that we assume the input quantity \(f\) to be in guarded normal form w.r.t. \(x\), which yields the Boolean expression \(\varphi \) to be in DNF (cf. Definition 5.2). Exploiting the disjunctive shape of \(\varphi \) yields the following:
Theorem 2
Let \(\tilde{a}\in \textsf{LinAX}^{\pm \infty }\) be an extended arithmetic expression and let
be a Boolean expression in DNF for some \(n\ge 1\). We have for all \(\sigma \in \Sigma \):
1.
2.
Proof
We first observe that
and then make use of the fact that the supremum of a finite union of extended reals is the maximum of the individual suprema, i.e., the above is equal to
See [10, App. A.2] for a detailed proof. The reasoning for
is analogous. \(\square \)
Hence, combining Theorem 2 with Lemma 1 reduces our problem further to eliminating quantifiers from the above simpler quantities. Put formally:
The second argument of \(\textsf{MAX}\) from Example 4 is treated analogously. \(\triangle \)
3.3 Stage 3: Computing Valuation-Dependent Suprema and Infima
This is the most involved stage since we need to operate on the atomic level of the given expressions. We aim to eliminate the quantifiers from quantities of the form
where each \(L_i\) is a linear inequality. We start with an example.
Example 6
Continuing Example 5, we perform quantifier elimination on
Fix some valuation \(\sigma \). First observe that if there is no \(q\in \mathbb {Q}\) such that \(\sigma [x\mapsto q] \models D\) — or, phrased in predicate logic, if \(\sigma \not \models \exists x:D\) —, then \( ^{\sigma }\llbracket g\rrbracket \) evaluates to \(-\infty \). Otherwise, we need to inspect \(D\) and \(\tilde{a}\) closer in order to determine \( ^{\sigma }\llbracket g\rrbracket \). Hence, eliminating the
-quantifier involves characterizing whether \(\sigma \models \exists x:D\) holds without referring to\(x\). This boils down to performing classical quantifier elimination on the formula \(\exists x:D\). We leverage classical Fourier-Motzkin variable elimination: Compare the bounds \(D\) imposes on \(x\) and encode whether they are consistent. Towards this end, we construct
Now, how can we characterize \( ^{\sigma }\llbracket g\rrbracket \) in case \(\sigma \models \varphi _{\exists }(D,x)\)? We first observe that \(x\) occurs positively in \(\tilde{a}\). Therefore, intuitively, the
-quantifier aims to maximize the value of \(x\) under all possible assignments satisfying \(D\). Since we isolate \(x\) in every inequality where \(x\) occurs, we can readily read off from \(D\) that \(x\)’s maximal (or, in fact, supremal) value is given by the minimum of \(\sigma (y_1) + 2\) and \(-\sigma (y_3)\) — the least of all upper bounds imposed on \(x\). Overall, we get
The above quantifier-free equivalent of \(g\) indeed evaluates to \(-\infty \) if \(\sigma \not \models \varphi _{\exists }(D,x)\) and, otherwise, performs a case distinction on said least upper bounds on \(x\).
Finally, consider the quantity
and observe that \(D'\) does not impose any bound on \(x\) whatsoever. This highlights the need for a careful treatment of \(\infty \) (or, in dual situations, \(-\infty \)): Since \(x\) occurs positively in \(\tilde{a}\), we have \( ^{\sigma }\llbracket g'\rrbracket = \infty \) whenever \(\sigma \models y_1 < z\), and \( ^{\sigma }\llbracket g'\rrbracket = -\infty \) otherwise. We thus have
When considering
-quantifiers or when \(x\) occurs negatively in \(\tilde{a}\), the above described observations need to be dualized, which we detail further below. \(\triangle \)
We condense the following steps for eliminating the
- or
-quantifiers:
1.
Extract lower and upper bounds on \(x\) imposed by the Boolean expression \(D\).
2.
Construct the Boolean expression \(\varphi _{\exists }(D,x)\) via classical Fourier-Motzkin.
3.
Characterize least upper- and greatest lower bounds on \(x\) admitted by \(D\).
4.
Eliminate the
- or
-quantifiers by gluing the above concepts together.
We detail these steps in the subsequent paragraphs. Fix \(x\in \textsf{Vars}\), \(n\ge 1\), and
$$ D\quad = \quad \bigwedge _{i=1}^n L_i~. $$
Extracting Lower and Upper Bounds. Given \(\sim \in \{>,\ge ,<,\le \}\), we define
and let \(\textsf{UBnd}_{x}= \textsf{Bnd}_{x < \cdot }(D)\cup \textsf{Bnd}_{x \le \cdot }(D) \) and \(\textsf{LBnd}_{x} = \textsf{Bnd}_{x > \cdot }(D)\cup \textsf{Bnd}_{x \ge \cdot }(D)\). Including \(\infty \) and \(-\infty \), respectively, by default will be convenient when characterizing least upper- and greatest lower bounds on \(x\) admitted by \(D\): If there is no upper (resp. lower) bound on \(x\) whatsoever imposed by \(D\), our construction will automatically default to \(\infty \) (resp. \(-\infty \)). Classical Fourier-Motzkin Quantifier Elimination with Infinity. We define
as is standard in Fourier-Motzkin variable elimination. The soundness of this construction generalizes to Boolean expressions involving \(\infty \) or \(-\infty \):
Lemma 2
([25, 45]). For all \(\sigma \in \Sigma \), we have
Characterizing Suprema and Infima. Fix some ordering on the bounds on \(x\), i.e., let \(\textsf{UBnd}_{x} = \{\tilde{u}_1,\ldots ,\tilde{u}_{m_1}\}\) and \(\textsf{LBnd}_{x}= \{\tilde{\ell }_1,\ldots ,\tilde{\ell }_{m_2}\}\). We define:
Intuitively, \(\varphi _{\sup }(D,x,\tilde{u}_i)\) evaluates to \(\textsf{true}\) under valuation \(\sigma \) if \( ^{\sigma }\llbracket \tilde{u}_i\rrbracket \) evaluates to the least upper bound on \(x\) admitted by \(D\) under \(\sigma \) with minimali. The intuition for \(\varphi _{\inf }(D,x,\tilde{\ell }_i)\) is analogous. Put more formally:
An immediate consequence of Theorem 3 is that, for every \(\sigma \models \varphi _{\exists }(D,x)\),
It is in this sense that \(\varphi _{\sup }\) and \(\varphi _{\inf }\) characterize least upper- and greatest lower bounds on \(x\) admitted by \(D\). Eliminating the Quantitative Quantifiers Equipped with the preceding prerequisites, we formalize our construction and prove it sound. Given extended arithmetic expressions \(\tilde{a},\tilde{e}\in \textsf{LinAX}^{\pm \infty }\) and a variable \(x\in \textsf{Vars}\), we define
where in the last case we have \(\tilde{a}\in \textsf{LinAX}\) so \(\tilde{e}[x/\tilde{a}]\) is the standard syntactic replacement7 of \(x\) by \(\tilde{a}\) in \(\tilde{e}\). Our sought-after quantifier-free equivalents are8
(2)
and
(3)
These constructions comply with our intuition from Example 6. We apply classical Fourier-Motzkin variable elimination to check whether the respective supremum (infimum) evaluates to \(-\infty \) (reps. \(\infty \)). If \(\varphi _{\exists }(D,x)\) is satisfied, then we inspect \(\tilde{e}\) closer, select the right bound \(\tilde{u}\) (resp. \(\tilde{\ell }\)) on \(x\) in \(D\) via \(\varphi _{\sup }\) (resp. \(\varphi _{\inf }\)), and substitute \(x\) in \(\tilde{e}\) by \(\tilde{u}\) (\(\tilde{\ell }\)) while obeying the arithmetic laws for the extended reals given in Section 2. The resulting quantities are partitioning and:
Theorem 4
Let \(x\in \textsf{Vars}\) and \(\tilde{e}\in \textsf{LinAX}^{\pm \infty }\). We have:
1.
2.
Proof
Fixing some \(\sigma \in \Sigma \), we first distinguish the cases \(\sigma \models \varphi _{\exists }(D,x)\) and \(\sigma \not \models \varphi _{\exists }(D,x)\). For \(\sigma \models \varphi _{\exists }(D,x)\), we then distinguish the cases \(x\not \in \textsf{FV} \left( \tilde{e} \right) \) and \(x\in \textsf{FV} \left( \tilde{e} \right) \), the latter case being the most interesting. The key insight is that if \(\tilde{e}\) is of the form \(q_0 + \sum _{y\in \textsf{Vars}}q_{y} \cdot y\) and \(\sigma \models \varphi _{\exists }(D,x)\), then
by Theorem 3. See [10, App. A.4] for a detailed proof. \(\square \)
We summarize our quantifier elimination technique in Algorithm 1, which takes as input a partitioning \(f\in \textsf{LinQuant}\) and computes a quantifier-free equivalent \(\textsf{Elim}(f)\) of \(f\) by proceeding in a recursive inner- to outermost fashion. Since \(f\) is partitioning and since both \(\textsf{MAX}\) and \(\textsf{MIN}\) always return partitioning quantities, the transformation of \(g\) into \(\textsf{GNF}_x\) only involves transforming every Boolean expression into DNF and isolating \(x\) in every inequality where \(x\) occurs. The soundness of Algorithm 1 is an immediate consequence of our observations from the preceding sections. Moreover, the algorithm terminates because the number of recursive invocations equals the number of quantifiers occurring in \(f\).
In order to upper-bound the space complexity of Algorithm 1, we agree on the following: The size \(|\varphi |\) of a Boolean expression \(\varphi \) is the number of (not necessarily distinct) inequalities it contains. The width\(| f |_{\rightarrow }\) of \(f\in \textsf{LinQuant}\) is its number of summands, and its depth\(| f |_{\downarrow }\) is the maximum of the sizes of the Boolean expressions \(f\) contains.
Theorem 5
Algorithm 1 is sound and terminates. Moreover, for partitioning9\(f\in \textsf{LinQuant}\) with \(| f |_{\rightarrow } = n\) and \(| f |_{\downarrow }= m\) containing exactly one quantifier,
We exploit that (i) transforming a Boolean expression \(\varphi \) of size l into DNF produces at most \(2^l\) disjuncts, each consisting of at most l linear inequalities and (ii) if \(D\) is of size l, then \(|\varphi _{\exists }(D,x)| \le \left( \nicefrac {l+2}{2} \right) ^2\). See [10, App. A.6] for details. \(\square \)
Fixing m and l as above, the resulting upper bounds for quantities containing k quantifiers are thus non-elementary in k. Investigating lower space complexity bounds of Algorithm 1 or the computational complexity of the quantitative quantifier elimination problem is left for future work.
4 Quantitative Craig Interpolation
We now employ our quantifier elimination procedure \(\textsf{Elim}\) from Algorithm 1 to derive a quantitative Craig interpolation theorem. Let us first agree on a notion of quantitative Craig interpolants, which is a quantitative analogue of the notion from [32]. Given \(f,f'\in \textsf{LinQuant}\), we say that \(f\) (quantitatively) entails\(f'\), denoted by \(f\models f'\), if \(\forall \sigma \in \Sigma : ^{\sigma }\llbracket f\rrbracket \le ^{\sigma }\llbracket f'\rrbracket \).
Definition 6
(Quantitative Craig Interpolant). Given \(f,f',g\in \textsf{LinQuant}\) with \(f\models f'\), we say that \(g\) is a (quantitative) Craig interpolant of \((f,f')\), if
In words, \(g\) sits between \(f\) and \(f'\) and the free variables occurring in \(g\) also occur free in both\(f\) and \(f'\). We will now see that piecewise linear quantities enjoy the property of being quantifier-free interpolating [32]: For all \(f,f'\in \textsf{LinQuant}\) with \(f\models f'\), there exists a quantifier-free Craig interpolant of \((f,f')\). More precisely, we prove that both the strongest and the weakest Craig interpolants of \((f,f')\) are quantifier-free and effectively constructible. Our construction is inspired by existing techniques for constructing classical Craig interpolants via classical quantifier elimination [23, 24]: By “projecting-out” the free variables in \(f\) which are not free in \(f'\) via
, we obtain the strongest Craig interpolant of \((f,f')\). Dually, by “projecting-out” the free variables in \(f'\) which are not free in \(f\) via
, we obtain the weakest Craig interpolant of \((f,f')\). Put formally:
Theorem 6
Let \(f,f'\in \textsf{LinQuant}\) with \(f\models f'\). We have:
1.
For \(\{x_1,\ldots ,x_n\} = \textsf{FV} \left( f \right) \setminus \textsf{FV} \left( f' \right) \),
is the strongest quantitative Craig interpolant of \((f,f')\), i.e.,
Pre-processing \(f\) and \(f'\) to make them partitioning and simplifying yields
5 Conclusion
We have investigated both quantitative quantifier elimination and quantitative Craig interpolation for piecewise linear quantities — an assertion language in automatic quantitative software verification. We have provided a sound and complete quantifier elimination algorithm, proved it sound, and analyzed upper space-complexity bounds. Using our algorithm, we have derived a quantitative Craig interpolation theorem for arbitrary piecewise linear quantities.
We see ample space for future work. First, we could investigate alternative quantifier elimination procedures: Our algorithm can be understood as a quantitative generalization of Fourier-Motzkin variable elimination [25, 45]. It would be interesting to apply, e.g., virtual substitution [40] in the quantitative setting and to compare the so-obtained approaches — both empirically and theoretically. We might also benefit from improvements of Fourier-Motzkin variable elimination such as FMplex [48] to improve the practical feasability of our approach. Moreover, we have focussed on \(\mathbb {Q}\)-valued variables. We plan to investigate techniques which apply to integer-valued variables using, e.g., Cooper’s method [18] and in how far our results can be generalized to a non-linear setting.
Finally, we plan to investigate potential applications of our techniques:
1.
Dillig et al. [22] present a quantifier elimination-based algorithm for generating inductive loop invariants of classical programs abductively. Generalizing this algorithm to the probabilistic setting, where weakest preconditions are replaced by weakest preexpectations, might yield a promising application of our quantifier elimination algorithm.
2.
We are currently investigating the applicability of McMillan’s interpolation and SAT-based model checking algorithm [43] to probabilistic program verification. One of the major challenges is to obtain suitable quantitative interpolants and we hope that our results on the existence of interpolants spark the development of suitable techniques.
3.
In the light of the above application and Remark 1, we plan to adapt Albarghouthi’s and McMillan’s technique for computing [1] “simpler” interpolants.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
We adopt this term from Zhang and Kaminski [59]. In the realm of weakest pre-expectations, quantitative assertions are usually referred to as expectations [42]. In weighted programming, they are called weightings [7].
Unsatisfiability of Boolean expressions is decidable by SMT solving over linear rational arithmetic (LRA) as is implemented, e.g., by the solver \(\text {\textsc {Z3}} \) [46].
It follows from the soundness of our quantifier elimination algorithm (Theorem 5) that all \(f\in \textsf{LinQuant}\) evaluate to extended rationals in \(\mathbb {Q}^{\pm \infty }\).
If \(f\) needs to be pre-processed to make it partitioning via the construction from Section 3.1, then n is to be substituted by \(2^n\) and m is to be substituted by \(n\cdot m\).
and infimum
quantifiers [8]. These quantifiers naturally occur when reasoning with quantitative program logics: Very much like classical strongest post-conditions introduce an \(\exists \)-quantifier for assignments [21], quantitative strongest post introduces a
-quantifier (cf. [59, Table 2]). Similarly, whereas classical weakest pre-conditions introduce a \(\forall \)-quantifier for demonically resolving unbounded non-determinism of the form \(x \mathrel {\text {\texttt {:=}}}\mathbb {Q}\) (read: assign to \(x\) an arbitrary rational number) [20, 47], quantitative weakest pre-expectations introduce an
-quantifier [9, 51].
, which, on variable valuation \(\sigma \), evaluates to the (variable valuation-dependent) supremum of \(g\) under all possible values for \(x\), i.e., 
or
quantifiers has, however, received scarce attention, let alone algorithmically. Similarly, the field of quantitative Craig interpolation is rather unexplored, as well. The goal of this paper is to lay the foundations for (i) developing quantitative quantifier elimination- and Craig interpolation-based approaches to automatic quantitative program verification and (ii) for simplifying the reasoning with quantitative assertions involving quantitative quantifiers. Towards this end:
from Example 1, our algorithm yields (after simplification)
and \(x_j\in \textsf{Vars}\) for all \(j\in \{1,\ldots ,k\}\),
is called the supremum quantifier and
is the infimum quantifier. The quantitative quantifiers take over the role of the classical \(\exists \)- and \(\forall \)-quantifiers from first-order predicate logic. Their semantics is detailed further below. If \(k= 0\), then we call \(f\) quantifier-free. Given \(f\) as above, the set of free variables in \(f\) isFor quantifier-free \(f\), we introduce the shorthand \(\left[ \varphi \right] \cdot f~ = ~\sum _{i=1}^n \left[ \varphi \wedge \varphi _i \right] \cdot \tilde{a}\).
and
makes it evident that the quantitative quantifiers generalize the classical quantifiers: Whereas \(\exists \) maximizes — so to speak — a truth value, the
-quantifier maximizes a quantity by evaluating to the supremum obtained from evaluating \(f\) under all possible values for \(x\).
behaves analogously by evaluating to an infimum.
. We proceed by means of a 3-level divide-and-conquer approach. We describe each of the involved stages in Sections 3.1-3.3. In Section 3.4, we summarize our approach by providing an algorithm.
and
, we obtain the sought-after quantifier-free equivalent of \(f\) by effectively constructing valuation-wise minima and maxima of finite sets of partitioning quantities as follows:
is analogous. \(\square \)
-quantifier involves characterizing whether \(\sigma \models \exists x:D\) holds without referring to \(x\). This boils down to performing classical quantifier elimination on the formula \(\exists x:D\). We leverage classical Fourier-Motzkin variable elimination: Compare the bounds \(D\) imposes on \(x\) and encode whether they are consistent. Towards this end, we constructNow, how can we characterize \( ^{\sigma }\llbracket g\rrbracket \) in case \(\sigma \models \varphi _{\exists }(D,x)\)? We first observe that \(x\) occurs positively in \(\tilde{a}\). Therefore, intuitively, the
-quantifier aims to maximize the value of \(x\) under all possible assignments satisfying \(D\). Since we isolate \(x\) in every inequality where \(x\) occurs, we can readily read off from \(D\) that \(x\)’s maximal (or, in fact, supremal) value is given by the minimum of \(\sigma (y_1) + 2\) and \(-\sigma (y_3)\) — the least of all upper bounds imposed on \(x\). Overall, we getThe above quantifier-free equivalent of \(g\) indeed evaluates to \(-\infty \) if \(\sigma \not \models \varphi _{\exists }(D,x)\) and, otherwise, performs a case distinction on said least upper bounds on \(x\).
-quantifiers or when \(x\) occurs negatively in \(\tilde{a}\), the above described observations need to be dualized, which we detail further below. \(\triangle \)
- or
-quantifiers:
- or
-quantifiers by gluing the above concepts together.
and
These constructions comply with our intuition from Example 6. We apply classical Fourier-Motzkin variable elimination to check whether the respective supremum (infimum) evaluates to \(-\infty \) (reps. \(\infty \)). If \(\varphi _{\exists }(D,x)\) is satisfied, then we inspect \(\tilde{e}\) closer, select the right bound \(\tilde{u}\) (resp. \(\tilde{\ell }\)) on \(x\) in \(D\) via \(\varphi _{\sup }\) (resp. \(\varphi _{\inf }\)), and substitute \(x\) in \(\tilde{e}\) by \(\tilde{u}\) (\(\tilde{\ell }\)) while obeying the arithmetic laws for the extended reals given in Section 2. The resulting quantities are partitioning and:
, we obtain the strongest Craig interpolant of \((f,f')\). Dually, by “projecting-out” the free variables in \(f'\) which are not free in \(f\) via
, we obtain the weakest Craig interpolant of \((f,f')\). Put formally:
