Counter-example guided predicate abstraction of hybrid systems

Abstract. Predicate abstraction has emerged to be a powerful tech-nique for extracting nite-state models from innite-state systems, and has been recently shown to enhance the eectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verier performs an on-the- y search of the nite discrete quotient whose states correspond to the truth assignments to the input predicates. The success of this approach depends on the choice of the predicates used for abstraction. In this paper, we focus on identifying these predicates automatically by analyzing spurious counter-examples generated by the search in the ab-stract state-space. We present the basic techniques for discovering new predicates that will rule out closely related spurious counter-examples, optimizations of these techniques, implementation of these in the veri-cation tool, and case studies demonstrating the promise of the approach.