Lab 03: Quantifier Elimination

Exercise 1

If instead of good states we look at the complement set of error states, the $wp$ corresponds to doing $sp$ backwards.
In other words, for $P,Q\subseteq S$ , $r \subseteq S \times S$ , the following holds:

$\begin{equation*} S \setminus wp(r,Q) = sp(S \setminus Q,r^{-1}) \end{equation*}$

Prove this statement.

Quantifier Elimination

QE for Presburger Arithmetic
Here is also a PDF that does not have any folding/missing content issues.

More Efficient Handling of Conjunctions in DNF

More efficient handling of disjunctions and divisibility: see the Calculus of Computation textbook

Additional information:

Synthesis through Quantifier Elimination

Recall Hoare triple:

$\begin{equation*} \{ P \} r \{ Q \} \end{equation*}$

We have also seen how to do the following (at least for Presburger arithmetic):

given $P, r, Q$ , check if the condition holds
given $P$ and $r$ , compute the strongest $Q$
given $r$ and $Q$ , compute the weakest $P$

How can we compute:

given $P$ and $Q$ compute the largest relation $r$ such that the triple holds (hint: it is easy!)

But how to do functional synthesis:

given $r$ , find a (deterministic) function $f$ in our programming language such that $R(x,f(x))$ whenever $\exists y.. R(x,y)$ .

Here is one approach:

Slides about Complete Functional Synthesis

Exercise 2

Eliminate quantifiers in the following formula in Presburger arithmetic.

$\begin{equation*} \exists y. \exists x. x < -2 \wedge 1 - 5y < x \wedge 1 + y < 13x \end{equation*}$