Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods

T. Henzinger, B. Horowitz, R. Majumdar and H. Wong-Toi

Though the hybrid system model checker HYTECH has successfully verified some systems, it restricts the dynamics to linear hybrid automata. We have designed an algorithm capable of verifying systems with more general dynamics. This algorithm uses interval numerical methods to conservatively overapproximate the reachable states of a hybrid automaton. We have implemented our new algorithm in HYTECH+. Using three examples, we demonstrate that this algorithm enables both a more accurate and a more direct analysis of hybrid systems.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.