Abstract:
Formal verification reveals the stability of large scale hybrid systems for all possible trajec tories in contrast with simulation that can check the stability only for limited number of
possible trajectories. This verification is a computationally expensive process as it requires
large state space and long execution time. To counter this problem, model reduction tech niques are employed to reduce the order of the system to some specific order, for which
reduced system is assumed to exhibit the same behavior as that of the higher order system.
This reduced system with less number of independent variables can be verified with smaller
state space and less time as compare to large scale system. The verification of large scale
system and then that of reduced system tantamount to the verification of model reduction
technique. In this study, we have verified the balance truncation model reduction technique
using SpaceEx model checker for number of hybrid systems of different order.
