Simulation‐based verification of bounded‐horizon safety for hybrid systems using dynamic number of simulations

The authors present a simulation‐based bounded‐horizon verification framework for hybrid systems with Lipschitz continuity on the continuous dynamics. In this framework, the bounded initial set is covered by a finite set of representative states, whose forward simulations are used to generate an over‐approximation of all the reachable states. A novel feature of the proposed approach is that the representative states are generated dynamically, on‐the‐fly, along with the forward simulations. This key innovation refines the current ‘reachability‐face’ by a new partition only when needed. This approach works for hybrid systems with state‐triggered discrete jumps and allows piecewise constant bounded inputs, extending the existing work applied to switched systems with neither state‐triggered discrete jumps nor inputs. Additionally, when the continuous dynamics is incremental (input‐to‐state) stable, the algorithm uses a simple Lipschitz‐based discrepancy function to provide a constant error bound of over‐approximation. This is of practical significance since a Lipschitz‐based discrepancy function is easily computable, while a more precise discrepancy function may not be available. Because of the constant error bound, the number of representative simulations also converges to a constant. A prototype verifier, HS 3 V , has been developed, implementing the proposed algorithms and providing verification results from several benchmarks for performance demonstration.