## Reachability Verification for Hybrid Automata

*
Thomas A. Henzinger
and Vlad Rusu*

We study the reachability problem for hybrid automata. Automatic approaches,
which attempt to construct the reachable region by symbolic execution, often
do not terminate. In these cases, we require the user to guess the reachable
region, and we use a theorem prover (PVS) to verify the guess. We classify
hybrid automata according to the theory in which their reachable region can
be defined finitely. This is the theory in which the prover needs to operate
in order to verify the guess. The approach is interesting, because an
appropriate guess can often be deduced by extrapolating from the first few
steps of symbolic execution.

*Proceedings of the
First International Workshop on Hybrid Systems: Computation and Control*
(HSCC),
Lecture Notes in Computer Science 1386,
Springer, 1998, pp. 190-204.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1998 Springer.