Progress on reachability analysis of hybrid systems using predicate abstraction

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. To compute the tran-sitions out of an abstract state, the tool needs to compute the set of discrete and continuous successors, and nd out all the abstract states that this set intersects with. The complexity of this computation grows exponentially with the number of abstraction predicates. In this paper we present various optimizations that are aimed at speeding up the search in the abstract state-space, and demonstrate their benets via case studies. We also discuss the completeness of the predicate abstraction technique for proving safety of hybrid systems.