Reachability verification for hybrid automata

T.A. Henzinger, V. Rusu, in:, Springer, 1998, pp. 190–204.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published
Author
Series Title
LNCS
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 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.
Publishing Year
Date Published
1998-01-01
Acknowledgement
This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036. Supported by Lavoisier grant of the French Foreign Affairs Ministry and by SRI.
Volume
1386
Page
190 - 204
Conference
HSCC: Hybrid Systems - Computation and Control
IST-REx-ID

Cite this

Henzinger TA, Rusu V. Reachability verification for hybrid automata. In: Vol 1386. Springer; 1998:190-204. doi:10.1007/3-540-64358-3_40
Henzinger, T. A., & Rusu, V. (1998). Reachability verification for hybrid automata (Vol. 1386, pp. 190–204). Presented at the HSCC: Hybrid Systems - Computation and Control, Springer. https://doi.org/10.1007/3-540-64358-3_40
Henzinger, Thomas A, and Vlad Rusu. “Reachability Verification for Hybrid Automata,” 1386:190–204. Springer, 1998. https://doi.org/10.1007/3-540-64358-3_40.
T. A. Henzinger and V. Rusu, “Reachability verification for hybrid automata,” presented at the HSCC: Hybrid Systems - Computation and Control, 1998, vol. 1386, pp. 190–204.
Henzinger TA, Rusu V. 1998. Reachability verification for hybrid automata. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 1386. 190–204.
Henzinger, Thomas A., and Vlad Rusu. Reachability Verification for Hybrid Automata. Vol. 1386, Springer, 1998, pp. 190–204, doi:10.1007/3-540-64358-3_40.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar