Pre-Computation of post in Predicate Abstraction
There is an alternative definition, which can be used to convert the above problem into a finite-state exploration problem. (It will be particularly useful if we consider an extension from conjunctions to disjunction of conjunctions.)
is equivalent to the validity of the formula
Fix a predicate . Consider all for which the above condition holds, define them as
Clearly, if and , then also . So, we can represent using its minimal elements . These are minimal sufficient sets of predicates that ensure that holds.
Then, we can define equivalently
The advantage of this definition is that we compute for a given predicate and command given by , and then we can efficiently compute for all abstract values by checking inclusion of finite sets.
Approximation: The set can have up to elements. To avoid this, we can restrict it to only those subsets that have at most e.g. 3 predicates.
Note that using smaller means that some will be missing, the condition will be false in some cases, and in those cases will not be included in the postcondition, so the resulting abstract element will be larger in the lattice. So the approach is still correct, just not as precise.