A faster approximation technique for predicate abstraction of hybrid systems

Predicate abstraction is a powerful technique for extracting finite-state models from infinite-state systems, and is applied to verification of safety properties. In this paper, we propose a technique that can be used for accelerating the computation of abstract state spaces for hybrid systems. The technique is based on upper approximation of the state transition relation, and requires a polynomial number of reachability checks and Boolean operations to compute the abstract state space consisting of a (possibly) exponential number of abstract states.