Abstract
A hybrid automaton consists of a discrete state component represented by a finite automaton, coupled with a (vector) continuous state component governed by a differential equation. For hybrid automata it is possible to reduce certain verification problems to those of checking language containment or language emptiness. Here we present a class of hybrid automata called suspension automata for which conditions can be given under which these problems are decidable.
Research supported by National Science Foundation under grants ECS111907 and IRI9120074.
Chapter PDF
References
R. Grossman, A. Nerode, A Ravn, and H. Rischel, editors. Hybrid Systems, volume LNCS 736. Springer, 1993.
R. Alur, C. Courcoubetis, T. Henzinger, and P. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, volume LNCS 736, pages 209–229. Springer, 1993.
D. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, volume LNCS 407. Springer, 1989.
R. Alur and D. Dill. Automata for modeling real-time systems. In Proceedings of the 17th Annual Colloquium on Automata, Languages, and Programming, 1990.
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In IEEE Proceedings of the Fifth Annual Symposium on Logic and Computer Science, 1990.
A. Olivero and S. Yovine. Kronos: A tool for verifying real-time systems, user's guide and reference manual. draft 0.0. Preprint. VERIMAG, B.P. 53X, 38401 Grenoble, France, May 1993.
P. Tzounakis. Verification of real time systems: The extension of COSPAN in dense time. Master's thesis, University of Crete, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McManis, J., Varaiya, P. (1994). Suspension automata: A decidable class of hybrid automata. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_47
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_47
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive