Counter-Example Based Predicate Discovery in Predicate Abstraction

The application of predicate abstraction to parameterized systems requires the use of quantified predicates. These predicates cannot be found automatically by existing techniques and are tedious for the user to provide. In this work we demonstrate a method of discovering most of these predicates automatically by analyzing spurious abstract counter-example traces. Since predicate discovery for unbounded state systems is an undecidable problem, it can fail on some problems. The method has been applied to a simplified version of the Ad hoc On-Demand Distance Vector Routing protocol where it successfully discovers all required predicates.