Making predicate abstraction efficient: How to eliminate redundant predicates

In this paper we consider techniques to identify and remove redundant predicates during predicate abstraction. We give three criteria for identifying redundancy. A predicate is redundant if any of the following three holds (i) the predicate is equivalent to a propositional function of other predicates. (ii) removing the predicate preserves safety propetties satisfied by the abstract model (iii) removing it preserves bisimulation equivalence. We also show how to efficiently remove the redundant predicates once they are identified. Experimental results are included to demonstrate the effectiveness of our methods.