Interval Methods in Hybrid Systems Analysis

critical, guarantees about their correct performance are
desirable. The hybrid systems model checker HyTech provides
such guarantees and has successfully verified some systems.
However, HyTech severely restricts the continuous dynamics of
the system being analyzed and, therefore, often forces the use
of prohibitively expensive discrete and polyhedral abstractions.
Tom Henzinger, Rupak Majumdar, and I have designed a new
algorithm, which is capable of directly verifying hybrid systems
with general continuous dynamics, such as linear differential
equations. The new algorithm conservatively overapproximates
the reachable states of a hybrid automaton by using interval
numerical methods. Interval numerical methods return sets of
points that enclose the true result of numerical computation
and, thus, avoid distortions due to the accumulation of round-
off errors. We are implementing the new algorithm in a
successor tool to HyTech called HyPerTech.