Thomas A. Henzinger and Vlad Rusu. Reachability Verification for Hybrid Automata. In International Workshop
on Hybrid Systems: Computation and Control (HSCC' 98) , Berkeley (California, USA), pp 190-204, 1998, LNCS 1386.
Abstract 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
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.
Full postscript text.