Quantifier Elimination (QE)

The Quantifier Elimination (QE) module uses quantifier elimination techniques to compute the strongest inductive invariant for a given transition system. This approach iteratively applies quantifier elimination to compute the least fixpoint of the strongest post-condition.

Overview

Quantifier Elimination is a technique that transforms quantified formulas into equivalent quantifier-free formulas. In the context of invariant generation, QE is used to compute the strongest inductive invariant by iteratively applying the strongest post-condition operator until a fixpoint is reached.

Algorithm

The QE prover implements the following algorithm:

1. Initialization: Start with the initial condition as the current invariant

2. Iteration: For each iteration: - Compute the strongest post-condition: ∃x. inv(x) ∧ trans(x,x’) - Apply quantifier elimination to get a quantifier-free formula - Rename variables to get the next state formula - Take the disjunction with the current invariant

3. Fixpoint Detection: Check if the new invariant is equivalent to the previous one

4. Safety Check: Verify that the computed invariant implies the safety property

Mathematical Formulation:

The algorithm computes the least fixpoint of the function:

\[F(I) = init ∨ ∃x. (I(x) ∧ trans(x,x'))[x' ↦ x]\]

where init is the initial condition, trans is the transition relation, and I is the current invariant.

Quantifier Elimination Tactics

The QE prover uses multiple quantifier elimination tactics:

• QE2: Z3’s advanced quantifier elimination tactic

• QE: Standard quantifier elimination tactic

References

[1]

1. Tarski, “A decision method for elementary algebra and geometry,” University of California Press, 1951.

[2]

7. 5. Collins, “Quantifier elimination for real closed fields by cylindrical algebraic decomposition,” in ISSAC, 1975.

[3]

12. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” in TACAS, 2008.