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.