Verifying Nonpolynomial Hybrid Systems by Qualitative Abstraction and Automated Theorem Proving

摘要

Few methods can automatically verify nonlinear hybrid systems that are modelled by nonpolynomial functions. Qualitative abstraction is a potential alternative to numerical reachability methods for formally verifying these systems. The QUANTUM abstracter is shown to be competitive at verifying several benchmark nonpolynomial hybrid systems.