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, (HSV)-V-3, has been developed, implementing the proposed algorithms and providing verification results from several benchmarks for performance demonstration.