A faster approximation technique for predicate abstraction of hybrid systems
Kunihiko Hiraishi, Koichi Kobayashi · 2009 ICCAS-SICE · 2009
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.